%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ069+2 : TPTP v9.0.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 08:25:13 PM UTC 2025 % Result : Satisfiable 92.20s 49.89s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : PUZ069+2 : TPTP v9.0.0. Bugfixed v5.4.0. % 0.00/0.09 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.28 % CPULimit : 300 % 0.12/0.28 % WCLimit : 300 % 0.12/0.28 % DateTime : Tue Apr 8 17:21:46 EDT 2025 % 0.12/0.28 % CPUTime : % 92.20/49.89 % 92.20/49.89 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 92.20/49.89 % 92.20/49.89 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 92.20/49.90 %$ p > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n3 > n2 > n1 % 92.20/49.90 % 92.20/49.90 %Foreground sorts: % 92.20/49.90 % 92.20/49.90 % 92.20/49.90 %Background operators: % 92.20/49.90 % 92.20/49.90 % 92.20/49.90 %Foreground operators: % 92.20/49.90 tff(n8, type, n8: $i). % 92.20/49.90 tff(n9, type, n9: $i). % 92.20/49.90 tff(n3, type, n3: $i). % 92.20/49.90 tff(n1, type, n1: $i). % 92.20/49.90 tff(n7, type, n7: $i). % 92.20/49.90 tff(n6, type, n6: $i). % 92.20/49.90 tff(n4, type, n4: $i). % 92.20/49.90 tff(p, type, p: ($i * $i * $i) > $o). % 92.20/49.90 tff(n2, type, n2: $i). % 92.20/49.90 tff(n5, type, n5: $i). % 92.20/49.90 % 92.20/49.90 %Saturated clause set: % 92.27/49.91 tff(c_21746, plain, (~p(n5, n1, n6))). % 92.27/49.91 tff(c_21760, plain, (~p(n5, n1, n3))). % 92.27/49.91 tff(c_21794, plain, (~p(n4, n5, n5))). % 92.27/49.91 tff(c_21765, plain, (~p(n5, n1, n2))). % 92.27/49.91 tff(c_21770, plain, (~p(n5, n1, n1))). % 92.27/49.91 tff(c_21755, plain, (~p(n5, n1, n4))). % 92.27/49.91 tff(c_21736, plain, (~p(n5, n1, n8))). % 92.27/49.91 tff(c_21741, plain, (~p(n5, n1, n7))). % 92.27/49.91 tff(c_21702, plain, (~p(n5, n8, n8))). % 92.27/49.91 tff(c_21799, plain, (~p(n4, n5, n2))). % 92.27/49.91 tff(c_21802, plain, (~p(n4, n5, n1))). % 92.27/49.91 tff(c_21821, plain, (~p(n4, n4, n6))). % 92.27/49.91 tff(c_21707, plain, (~p(n5, n8, n7))). % 92.27/49.91 tff(c_21784, plain, (~p(n4, n5, n7))). % 92.27/49.91 tff(c_21485, plain, (~p(n2, n2, n1))). % 92.27/49.91 tff(c_21774, plain, (~p(n4, n5, n9))). % 92.27/49.91 tff(c_21852, plain, (~p(n3, n7, n6))). % 92.27/49.91 tff(c_21857, plain, (~p(n3, n7, n5))). % 92.27/49.91 tff(c_21722, plain, (~p(n5, n8, n3))). % 92.27/49.91 tff(c_21865, plain, (~p(n3, n7, n2))). % 92.27/49.91 tff(c_21868, plain, (~p(n3, n7, n1))). % 92.27/49.91 tff(c_21860, plain, (~p(n3, n7, n4))). % 92.27/49.91 tff(c_21727, plain, (~p(n5, n8, n2))). % 92.27/49.91 tff(c_21847, plain, (~p(n3, n7, n7))). % 92.27/49.91 tff(c_21837, plain, (~p(n3, n7, n9))). % 92.27/49.91 tff(c_21953, plain, (~p(n2, n6, n5))). % 92.27/49.91 tff(c_21966, plain, (~p(n2, n6, n2))). % 92.27/49.91 tff(c_21900, plain, (~p(n3, n2, n3))). % 92.27/49.91 tff(c_21732, plain, (~p(n5, n8, n1))). % 92.27/49.91 tff(c_21885, plain, (~p(n3, n2, n6))). % 92.27/49.91 tff(c_21873, plain, (~p(n3, n2, n9))). % 92.27/49.91 tff(c_21946, plain, (~p(n2, n6, n7))). % 92.27/49.91 tff(c_21717, plain, (~p(n5, n8, n4))). % 92.27/49.91 tff(c_21924, plain, (~p(n2, n7, n4))). % 92.27/49.91 tff(c_21914, plain, (~p(n2, n7, n7))). % 92.27/49.91 tff(c_21905, plain, (~p(n2, n7, n9))). % 92.27/49.91 tff(c_22055, plain, (~p(n1, n1, n6))). % 92.27/49.91 tff(c_21991, plain, (~p(n1, n4, n4))). % 92.27/49.91 tff(c_21639, plain, (~p(n6, n6, n8))). % 92.27/49.91 tff(c_22005, plain, (~p(n1, n4, n1))). % 92.27/49.91 tff(c_22009, plain, (~p(n1, n3, n9))). % 92.27/49.91 tff(c_22023, plain, (~p(n1, n3, n5))). % 92.27/49.91 tff(c_21653, plain, (~p(n6, n6, n5))). % 92.27/49.91 tff(c_22028, plain, (~p(n1, n3, n4))). % 92.27/49.91 tff(c_22059, plain, (~p(n1, n1, n5))). % 92.27/49.91 tff(c_22064, plain, (~p(n1, n1, n4))). % 92.27/49.91 tff(c_22069, plain, (~p(n1, n1, n3))). % 92.27/49.91 tff(c_22014, plain, (~p(n1, n3, n8))). % 92.27/49.91 tff(c_21675, plain, (~p(n6, n5, n7))). % 92.27/49.91 tff(c_22033, plain, (~p(n1, n3, n3))). % 92.27/49.91 tff(c_22040, plain, (~p(n1, n3, n1))). % 92.27/49.91 tff(c_22001, plain, (~p(n1, n4, n2))). % 92.27/49.91 tff(c_21688, plain, (~p(n6, n5, n3))). % 92.27/49.91 tff(c_21986, plain, (~p(n1, n4, n5))). % 92.27/49.91 tff(c_22047, plain, (~p(n1, n1, n8))). % 92.27/49.91 tff(c_22152, plain, (~p(n6, n7, n2))). % 92.27/49.91 tff(c_22148, plain, (~p(n7, n7, n2))). % 92.27/49.91 tff(c_22235, plain, (~p(n1, n7, n5))). % 92.27/49.91 tff(c_21693, plain, (~p(n6, n5, n1))). % 92.27/49.91 tff(c_22212, plain, (~p(n5, n7, n5))). % 92.27/49.92 tff(c_22217, plain, (~p(n4, n7, n5))). % 92.27/49.92 tff(c_22208, plain, (~p(n6, n7, n5))). % 92.27/49.92 tff(c_21680, plain, (~p(n6, n5, n6))). % 92.27/49.92 tff(c_22226, plain, (~p(n1, n7, n2))). % 92.27/49.92 tff(c_22203, plain, (~p(n7, n7, n5))). % 92.27/49.92 tff(c_22157, plain, (~p(n5, n7, n2))). % 92.27/49.92 tff(c_22126, plain, (~p(n2, n8, n1))). % 92.27/49.92 tff(c_22107, plain, (~p(n4, n8, n1))). % 92.27/49.92 tff(c_21665, plain, (~p(n6, n5, n9))). % 92.27/49.92 tff(c_22103, plain, (~p(n6, n8, n6))). % 92.27/49.92 tff(c_22089, plain, (~p(n9, n8, n6))). % 92.27/49.92 tff(c_22084, plain, (~p(n6, n8, n1))). % 92.27/49.92 tff(c_21351, plain, (~p(n4, n2, n9))). % 92.27/49.92 tff(c_22144, plain, (~p(n9, n7, n2))). % 92.27/49.92 tff(c_22175, plain, (~p(n7, n7, n3))). % 92.27/49.92 tff(c_22485, plain, (~p(n6, n3, n7))). % 92.27/49.92 tff(c_22481, plain, (~p(n7, n3, n7))). % 92.27/49.92 tff(c_22476, plain, (~p(n8, n3, n7))). % 92.27/49.92 tff(c_21670, plain, (~p(n6, n5, n8))). % 92.27/49.92 tff(c_22471, plain, (~p(n9, n3, n7))). % 92.27/49.92 tff(c_23444, plain, (~p(n7, n7, n1))). % 92.27/49.92 tff(c_21557, plain, (~p(n8, n2, n1))). % 92.27/49.92 tff(c_21660, plain, (~p(n6, n6, n1))). % 92.27/49.92 tff(c_21549, plain, (~p(n8, n2, n4))). % 92.27/49.92 tff(c_21534, plain, (~p(n8, n2, n7))). % 92.27/49.92 tff(c_23427, plain, (~p(n8, n1, n2))). % 92.27/49.92 tff(c_23359, plain, (~p(n9, n8, n9))). % 92.27/49.92 tff(c_21580, plain, (~p(n7, n8, n5))). % 92.27/49.92 tff(c_21602, plain, (~p(n7, n4, n8))). % 92.27/49.92 tff(c_21585, plain, (~p(n7, n8, n4))). % 92.27/49.92 tff(c_21590, plain, (~p(n7, n8, n3))). % 92.27/49.92 tff(c_23361, plain, (~p(n9, n8, n8))). % 92.27/49.92 tff(c_21607, plain, (~p(n7, n4, n6))). % 92.27/49.92 tff(c_23347, plain, (~p(n8, n6, n2))). % 92.27/49.92 tff(c_23363, plain, (~p(n9, n8, n7))). % 92.27/49.92 tff(c_23373, plain, (~p(n9, n1, n5))). % 92.27/49.92 tff(c_23301, plain, (~p(n7, n1, n1))). % 92.27/49.92 tff(c_23275, plain, (~p(n8, n1, n3))). % 92.27/49.92 tff(c_21611, plain, (~p(n7, n4, n5))). % 92.27/49.92 tff(c_23288, plain, (~p(n3, n1, n3))). % 92.27/49.92 tff(c_23319, plain, (~p(n3, n1, n1))). % 92.27/49.92 tff(c_21626, plain, (~p(n7, n4, n2))). % 92.27/49.92 tff(c_21621, plain, (~p(n7, n4, n3))). % 92.27/49.92 tff(c_23268, plain, (~p(n3, n1, n9))). % 92.27/49.92 tff(c_23264, plain, (~p(n4, n1, n9))). % 92.27/49.92 tff(c_23250, plain, (~p(n8, n1, n9))). % 92.27/49.92 tff(c_23221, plain, (~p(n3, n5, n2))). % 92.27/49.92 tff(c_23260, plain, (~p(n6, n1, n9))). % 92.27/49.92 tff(c_21616, plain, (~p(n7, n4, n4))). % 92.27/49.92 tff(c_23219, plain, (~p(n7, n5, n2))). % 92.27/49.92 tff(c_23217, plain, (~p(n8, n5, n2))). % 92.27/49.92 tff(c_23215, plain, (~p(n9, n5, n2))). % 92.27/49.92 tff(c_21567, plain, (~p(n7, n8, n8))). % 92.27/49.92 tff(c_23213, plain, (~p(n2, n5, n1))). % 92.27/49.92 tff(c_23211, plain, (~p(n2, n5, n7))). % 92.27/49.92 tff(c_23209, plain, (~p(n2, n5, n8))). % 92.27/49.92 tff(c_23207, plain, (~p(n2, n5, n9))). % 92.27/49.92 tff(c_23205, plain, (~p(n3, n6, n2))). % 92.27/49.92 tff(c_21572, plain, (~p(n7, n8, n7))). % 92.27/49.92 tff(c_23187, plain, (~p(n2, n8, n2))). % 92.27/49.92 tff(c_21643, plain, (~p(n6, n6, n7))). % 92.27/49.92 tff(c_23182, plain, (~p(n8, n8, n2))). % 92.27/49.92 tff(c_21576, plain, (~p(n7, n8, n6))). % 92.27/49.92 tff(c_23180, plain, (~p(n1, n8, n4))). % 92.27/49.92 tff(c_23178, plain, (~p(n1, n8, n7))). % 92.27/49.92 tff(c_23176, plain, (~p(n1, n8, n8))). % 92.27/49.92 tff(c_23150, plain, (~p(n8, n4, n1))). % 92.27/49.92 tff(c_23152, plain, (~p(n6, n4, n5))). % 92.27/49.92 tff(c_21529, plain, (~p(n8, n2, n8))). % 92.27/49.92 tff(c_23111, plain, (~p(n3, n6, n5))). % 92.27/49.92 tff(c_21712, plain, (~p(n5, n8, n5))). % 92.27/49.92 tff(c_23107, plain, (~p(n8, n6, n5))). % 92.27/49.92 tff(c_21544, plain, (~p(n8, n2, n5))). % 92.27/49.92 tff(c_23105, plain, (~p(n9, n6, n5))). % 92.27/49.92 tff(c_23103, plain, (~p(n1, n6, n1))). % 92.27/49.92 tff(c_21817, plain, (~p(n4, n4, n7))). % 92.27/49.92 tff(c_21832, plain, (~p(n4, n4, n1))). % 92.27/49.92 tff(c_21807, plain, (~p(n4, n4, n9))). % 92.27/49.92 tff(c_21554, plain, (~p(n8, n2, n2))). % 92.27/49.92 tff(c_21812, plain, (~p(n4, n4, n8))). % 92.27/49.92 tff(c_21789, plain, (~p(n4, n5, n6))). % 92.27/49.92 tff(c_21779, plain, (~p(n4, n5, n8))). % 92.27/49.92 tff(c_21326, plain, (~p(n5, n6, n2))). % 92.27/49.92 tff(c_23028, plain, (~p(n5, n7, n9))). % 92.27/49.92 tff(c_21842, plain, (~p(n3, n7, n8))). % 92.27/49.92 tff(c_23019, plain, (~p(n7, n7, n4))). % 92.27/49.92 tff(c_21971, plain, (~p(n2, n6, n1))). % 92.27/49.92 tff(c_21895, plain, (~p(n3, n2, n4))). % 92.27/49.92 tff(c_21314, plain, (~p(n6, n6, n2))). % 92.27/49.92 tff(c_21890, plain, (~p(n3, n2, n5))). % 92.27/49.92 tff(c_21878, plain, (~p(n3, n2, n8))). % 92.27/49.92 tff(c_21962, plain, (~p(n2, n6, n3))). % 92.27/49.93 tff(c_21318, plain, (~p(n4, n4, n5))). % 92.27/49.93 tff(c_21932, plain, (~p(n2, n7, n2))). % 92.27/49.93 tff(c_21957, plain, (~p(n2, n6, n4))). % 92.27/49.93 tff(c_21941, plain, (~p(n2, n6, n9))). % 92.27/49.93 tff(c_21936, plain, (~p(n2, n7, n1))). % 92.27/49.93 tff(c_21929, plain, (~p(n2, n7, n3))). % 92.27/49.93 tff(c_21322, plain, (~p(n6, n5, n2))). % 92.27/49.93 tff(c_21919, plain, (~p(n2, n7, n6))). % 92.37/49.93 tff(c_21910, plain, (~p(n2, n7, n8))). % 92.37/49.93 tff(c_22973, plain, (p(n5, n7, n4))). % 92.37/49.93 tff(c_21295, plain, (~p(n6, n4, n4))). % 92.37/49.93 tff(c_22789, plain, (~p(n4, n8, n7))). % 92.37/49.93 tff(c_22913, plain, (~p(n6, n1, n5))). % 92.37/49.93 tff(c_22976, plain, (p(n4, n9, n5))). % 92.37/49.93 tff(c_22939, plain, (~p(n2, n2, n5))). % 92.37/49.93 tff(c_22930, plain, (~p(n9, n2, n5))). % 92.37/49.93 tff(c_21495, plain, (~p(n8, n7, n8))). % 92.37/49.93 tff(c_22915, plain, (~p(n4, n3, n5))). % 92.37/49.93 tff(c_22923, plain, (~p(n5, n2, n7))). % 92.37/49.93 tff(c_22917, plain, (~p(n4, n1, n5))). % 92.37/49.93 tff(c_21500, plain, (~p(n8, n7, n7))). % 92.37/49.93 tff(c_22827, plain, (~p(n3, n9, n2))). % 92.37/49.93 tff(c_22450, plain, (~p(n6, n4, n6))). % 92.37/49.93 tff(c_22829, plain, (~p(n2, n9, n2))). % 92.37/49.93 tff(c_22052, plain, (~p(n1, n1, n7))). % 92.37/49.93 tff(c_22840, plain, (~p(n2, n1, n6))). % 92.37/49.93 tff(c_21505, plain, (~p(n8, n7, n6))). % 92.37/49.93 tff(c_22836, plain, (~p(n2, n1, n9))). % 92.37/49.93 tff(c_22872, plain, (p(n5, n2, n5))). % 92.37/49.93 tff(c_22846, plain, (~p(n2, n1, n1))). % 92.37/49.93 tff(c_21282, plain, (~p(n4, n6, n5))). % 92.37/49.93 tff(c_22844, plain, (~p(n2, n1, n4))). % 92.37/49.93 tff(c_22838, plain, (~p(n2, n1, n8))). % 92.37/49.93 tff(c_22842, plain, (~p(n2, n1, n5))). % 92.37/49.93 tff(c_22422, plain, (~p(n3, n4, n2))). % 92.37/49.93 tff(c_22417, plain, (~p(n3, n4, n7))). % 92.37/49.93 tff(c_21331, plain, (~p(n5, n5, n2))). % 92.37/49.93 tff(c_22409, plain, (~p(n6, n4, n2))). % 92.37/49.93 tff(c_22373, plain, (~p(n1, n5, n4))). % 92.37/49.93 tff(c_22363, plain, (~p(n2, n5, n4))). % 92.37/49.93 tff(c_21514, plain, (~p(n8, n7, n4))). % 92.37/49.93 tff(c_22359, plain, (~p(n2, n5, n5))). % 92.37/49.93 tff(c_22354, plain, (~p(n3, n5, n4))). % 92.37/49.93 tff(c_22298, plain, (~p(n1, n6, n3))). % 92.37/49.93 tff(c_22349, plain, (~p(n3, n5, n5))). % 92.37/49.93 tff(c_22275, plain, (~p(n7, n6, n8))). % 92.37/49.93 tff(c_21519, plain, (~p(n8, n7, n3))). % 92.37/49.93 tff(c_22284, plain, (~p(n5, n6, n8))). % 92.37/49.93 tff(c_22194, plain, (~p(n9, n7, n5))). % 92.37/49.93 tff(c_22184, plain, (~p(n5, n7, n3))). % 92.37/49.93 tff(c_22166, plain, (~p(n9, n7, n3))). % 92.37/49.93 tff(c_22180, plain, (~p(n6, n7, n3))). % 92.37/49.93 tff(c_22231, plain, (~p(n1, n7, n3))). % 92.37/49.93 tff(c_22248, plain, (~p(n7, n6, n3))). % 92.37/49.93 tff(c_22239, plain, (~p(n9, n6, n3))). % 92.37/49.93 tff(c_22244, plain, (~p(n8, n6, n3))). % 92.37/49.93 tff(c_22080, plain, (~p(n8, n8, n1))). % 92.37/49.93 tff(c_22253, plain, (~p(n5, n6, n3))). % 92.37/49.93 tff(c_22289, plain, (~p(n4, n6, n8))). % 92.37/49.93 tff(c_22294, plain, (~p(n3, n6, n8))). % 92.37/49.93 tff(c_22094, plain, (~p(n8, n8, n6))). % 92.37/49.93 tff(c_22257, plain, (~p(n4, n6, n3))). % 92.37/49.93 tff(c_22270, plain, (~p(n8, n6, n8))). % 92.37/49.93 tff(c_22261, plain, (~p(n3, n6, n3))). % 92.37/49.93 tff(c_22265, plain, (~p(n9, n6, n8))). % 92.37/49.93 tff(c_22303, plain, (~p(n1, n6, n8))). % 92.37/49.93 tff(c_22112, plain, (~p(n4, n8, n6))). % 92.37/49.93 tff(c_22312, plain, (~p(n8, n5, n5))). % 92.37/49.93 tff(c_22307, plain, (~p(n9, n5, n5))). % 92.37/49.93 tff(c_22317, plain, (~p(n7, n5, n5))). % 92.37/49.93 tff(c_22131, plain, (~p(n2, n8, n6))). % 92.37/49.93 tff(c_22322, plain, (~p(n5, n5, n5))). % 92.37/49.93 tff(c_22326, plain, (~p(n9, n5, n4))). % 92.37/49.93 tff(c_22345, plain, (~p(n5, n5, n4))). % 92.37/49.93 tff(c_22331, plain, (~p(n8, n5, n4))). % 92.37/49.93 tff(c_22336, plain, (~p(n7, n5, n4))). % 92.37/49.93 tff(c_22140, plain, (~p(n1, n8, n6))). % 92.37/49.93 tff(c_22368, plain, (~p(n1, n5, n5))). % 92.37/49.93 tff(c_22413, plain, (~p(n5, n4, n2))). % 92.37/49.93 tff(c_22382, plain, (~p(n8, n4, n7))). % 92.37/49.93 tff(c_22189, plain, (~p(n4, n7, n3))). % 92.37/49.93 tff(c_22378, plain, (~p(n9, n4, n7))). % 92.37/49.93 tff(c_22386, plain, (~p(n6, n4, n7))). % 92.37/49.93 tff(c_22391, plain, (~p(n5, n4, n7))). % 92.37/49.93 tff(c_22396, plain, (~p(n9, n4, n2))). % 92.37/49.93 tff(c_22401, plain, (~p(n8, n4, n2))). % 92.37/49.93 tff(c_22043, plain, (~p(n1, n1, n9))). % 92.37/49.93 tff(c_22651, plain, (~p(n4, n9, n3))). % 92.37/49.93 tff(c_22649, plain, (~p(n5, n9, n3))). % 92.37/49.93 tff(c_22645, plain, (~p(n8, n9, n3))). % 92.37/49.93 tff(c_21983, plain, (~p(n1, n4, n7))). % 92.37/49.93 tff(c_22639, plain, (~p(n9, n9, n3))). % 92.37/49.93 tff(c_22637, plain, (~p(n7, n9, n1))). % 92.37/49.93 tff(c_22590, plain, (~p(n8, n5, n3))). % 92.37/49.93 tff(c_22588, plain, (~p(n9, n5, n3))). % 92.37/49.93 tff(c_22584, plain, (~p(n1, n5, n1))). % 92.37/49.93 tff(c_21996, plain, (~p(n1, n4, n3))). % 92.37/49.93 tff(c_22520, plain, (~p(n5, n2, n3))). % 92.37/49.94 tff(c_22516, plain, (~p(n6, n2, n3))). % 92.37/49.94 tff(c_22504, plain, (~p(n2, n3, n7))). % 92.37/49.94 tff(c_22019, plain, (~p(n1, n3, n6))). % 92.37/49.94 tff(c_22512, plain, (~p(n7, n2, n3))). % 92.37/49.94 tff(c_22508, plain, (~p(n9, n2, n3))). % 92.37/49.94 tff(c_22500, plain, (~p(n3, n3, n7))). % 92.37/49.94 tff(c_22495, plain, (~p(n4, n3, n7))). % 92.37/49.94 tff(c_22490, plain, (~p(n5, n3, n7))). % 92.37/49.94 tff(c_21480, plain, (~p(n2, n3, n1))). % 92.37/49.94 tff(c_22554, plain, (~p(n4, n2, n2))). % 92.37/49.94 tff(c_22525, plain, (~p(n4, n2, n3))). % 92.37/49.94 tff(c_22530, plain, (~p(n9, n2, n2))). % 92.37/49.94 tff(c_21472, plain, (~p(n1, n1, n2))). % 92.37/49.94 tff(c_22539, plain, (~p(n7, n2, n2))). % 92.37/49.94 tff(c_24164, plain, (~p(n7, n5, n6))). % 92.37/49.94 tff(c_23936, plain, (p(n5, n4, n8))). % 92.37/49.94 tff(c_24160, plain, (~p(n8, n9, n6))). % 92.37/49.94 tff(c_23912, plain, (~p(n2, n8, n8))). % 92.37/49.94 tff(c_21476, plain, (~p(n3, n2, n1))). % 92.37/49.94 tff(c_24152, plain, (~p(n9, n1, n7))). % 92.37/49.94 tff(c_23855, plain, (~p(n4, n1, n6))). % 92.37/49.94 tff(c_24150, plain, (~p(n9, n2, n7))). % 92.37/49.94 tff(c_21198, plain, (~p(n8, n7, n1))). % 92.37/49.94 tff(c_24046, plain, (~p(n1, n7, n7))). % 92.37/49.94 tff(c_24148, plain, (~p(n9, n9, n7))). % 92.37/49.94 tff(c_24016, plain, (~p(n1, n9, n6))). % 92.37/49.94 tff(c_24146, plain, (~p(n8, n9, n7))). % 92.37/49.94 tff(c_24136, plain, (p(n7, n7, n6))). % 92.37/49.94 tff(c_21247, plain, (~p(n6, n7, n6))). % 92.37/49.94 tff(c_24144, plain, (~p(n8, n8, n7))). % 92.37/49.94 tff(c_24091, plain, (~p(n6, n7, n7))). % 92.37/49.94 tff(c_24120, plain, (p(n9, n7, n7))). % 92.37/49.94 tff(c_21439, plain, (~p(n2, n1, n2))). % 92.37/49.94 tff(c_24142, plain, (~p(n9, n7, n6))). % 92.37/49.94 tff(c_24118, plain, (~p(n1, n2, n8))). % 92.37/49.94 tff(c_23943, plain, (~p(n5, n5, n8))). % 92.37/49.94 tff(c_24116, plain, (~p(n1, n9, n8))). % 92.37/49.94 tff(c_24109, plain, (~p(n7, n7, n8))). % 92.37/49.94 tff(c_21444, plain, (~p(n3, n2, n7))). % 92.37/49.94 tff(c_23954, plain, (~p(n2, n3, n8))). % 92.37/49.94 tff(c_24107, plain, (~p(n9, n7, n8))). % 92.37/49.94 tff(c_24105, plain, (~p(n3, n8, n8))). % 92.37/49.94 tff(c_21457, plain, (~p(n2, n2, n7))). % 92.37/49.94 tff(c_24103, plain, (~p(n3, n9, n8))). % 92.37/49.94 tff(c_24099, plain, (~p(n6, n2, n1))). % 92.37/49.94 tff(c_24097, plain, (~p(n6, n3, n1))). % 92.37/49.94 tff(c_24095, plain, (~p(n6, n9, n1))). % 92.37/49.94 tff(c_24093, plain, (~p(n6, n7, n8))). % 92.37/49.94 tff(c_21237, plain, (~p(n7, n1, n3))). % 92.37/49.94 tff(c_24068, plain, (~p(n1, n2, n6))). % 92.37/49.94 tff(c_24088, plain, (p(n1, n7, n8))). % 92.37/49.94 tff(c_24087, plain, (p(n6, n7, n1))). % 92.37/49.94 tff(c_21416, plain, (~p(n3, n5, n6))). % 92.37/49.94 tff(c_24077, plain, (~p(n1, n9, n1))). % 92.37/49.94 tff(c_24086, plain, (~p(n1, n7, n1))). % 92.37/49.94 tff(c_24073, plain, (~p(n1, n2, n7))). % 92.37/49.94 tff(c_24038, plain, (~p(n1, n9, n7))). % 92.37/49.94 tff(c_24025, plain, (~p(n1, n7, n6))). % 92.37/49.94 tff(c_21425, plain, (~p(n2, n6, n6))). % 92.37/49.94 tff(c_23963, plain, (~p(n2, n2, n8))). % 92.37/49.94 tff(c_23950, plain, (~p(n2, n3, n5))). % 92.37/49.94 tff(c_23940, plain, (~p(n5, n4, n1))). % 92.37/49.94 tff(c_21421, plain, (~p(n1, n4, n8))). % 92.37/49.94 tff(c_23935, plain, (~p(n2, n4, n8))). % 92.37/49.94 tff(c_23863, plain, (~p(n4, n1, n2))). % 92.37/49.94 tff(c_23907, plain, (~p(n2, n9, n8))). % 92.37/49.94 tff(c_23843, plain, (~p(n4, n2, n4))). % 92.37/49.94 tff(c_23839, plain, (~p(n4, n2, n6))). % 92.37/49.94 tff(c_21448, plain, (~p(n1, n3, n2))). % 92.37/49.94 tff(c_23658, plain, (~p(n5, n5, n9))). % 92.37/49.94 tff(c_23457, plain, (~p(n7, n5, n1))). % 92.37/49.94 tff(c_23432, plain, (~p(n8, n1, n5))). % 92.37/49.94 tff(c_21462, plain, (~p(n2, n1, n7))). % 92.37/49.94 tff(c_23450, plain, (~p(n7, n6, n1))). % 92.37/49.94 tff(c_23405, plain, (~p(n8, n3, n5))). % 92.37/49.94 tff(c_23355, plain, (~p(n8, n8, n5))). % 92.37/49.94 tff(c_23356, plain, (p(n9, n8, n5))). % 92.37/49.94 tff(c_23400, plain, (~p(n8, n3, n2))). % 92.37/49.94 tff(c_21452, plain, (~p(n3, n1, n7))). % 92.37/49.94 tff(c_23367, plain, (~p(n2, n8, n5))). % 92.37/49.94 tff(c_23296, plain, (~p(n8, n1, n1))). % 92.37/49.94 tff(c_23314, plain, (~p(n4, n1, n1))). % 92.37/49.94 tff(c_21827, plain, (~p(n4, n4, n4))). % 92.37/49.94 tff(c_23305, plain, (~p(n6, n1, n1))). % 92.37/49.94 tff(c_23291, plain, (~p(n9, n1, n1))). % 92.37/49.94 tff(c_23245, plain, (~p(n9, n1, n9))). % 92.37/49.94 tff(c_23203, plain, (p(n2, n5, n2))). % 92.37/49.94 tff(c_23185, plain, (~p(n3, n8, n2))). % 92.37/49.94 tff(c_21401, plain, (~p(n3, n4, n8))). % 92.37/49.94 tff(c_23255, plain, (~p(n7, n1, n9))). % 92.37/49.94 tff(c_23170, plain, (~p(n1, n2, n2))). % 92.37/49.94 tff(c_23172, plain, (p(n1, n8, n2))). % 92.37/49.94 tff(c_21750, plain, (~p(n5, n1, n5))). % 92.37/49.94 tff(c_23174, plain, (~p(n1, n8, n9))). % 92.37/49.94 tff(c_23148, plain, (~p(n8, n4, n4))). % 92.37/49.94 tff(c_23146, plain, (~p(n8, n4, n8))). % 92.37/49.94 tff(c_23109, plain, (~p(n7, n6, n5))). % 92.37/49.94 tff(c_23142, plain, (p(n8, n4, n5))). % 92.37/49.94 tff(c_21391, plain, (~p(n1, n8, n5))). % 92.37/49.94 tff(c_23144, plain, (~p(n8, n4, n9))). % 92.37/49.94 tff(c_23365, plain, (~p(n9, n8, n4))). % 92.37/49.94 tff(c_22774, plain, (p(n5, n9, n2))). % 92.37/49.94 tff(c_21386, plain, (~p(n1, n8, n3))). % 92.37/49.94 tff(c_23371, plain, (~p(n9, n3, n5))). % 92.37/49.94 tff(c_22781, plain, (p(n2, n1, n3))). % 92.37/49.94 tff(c_23101, plain, (~p(n1, n6, n2))). % 92.37/49.94 tff(c_22787, plain, (~p(n4, n8, n8))). % 92.37/49.94 tff(c_22703, plain, (~p(n6, n4, n3))). % 92.37/49.94 tff(c_21698, plain, (~p(n5, n8, n9))). % 92.37/49.94 tff(c_23099, plain, (~p(n1, n6, n4))). % 92.37/49.94 tff(c_23083, plain, (~p(n1, n2, n5))). % 92.37/49.94 tff(c_23097, plain, (~p(n1, n6, n6))). % 92.37/49.94 tff(c_21376, plain, (~p(n1, n9, n3))). % 92.37/49.94 tff(c_23095, plain, (~p(n1, n6, n7))). % 92.37/49.94 tff(c_23093, plain, (~p(n1, n6, n9))). % 92.37/49.94 tff(c_23088, plain, (~p(n2, n4, n5))). % 92.37/49.94 tff(c_23090, plain, (~p(n3, n4, n5))). % 92.37/49.94 tff(c_23026, plain, (~p(n1, n7, n4))). % 92.37/49.94 tff(c_21371, plain, (~p(n3, n8, n5))). % 92.37/49.94 tff(c_23023, plain, (~p(n4, n7, n4))). % 92.37/49.94 tff(c_23021, plain, (~p(n6, n7, n4))). % 92.37/49.94 tff(c_23017, plain, (~p(n9, n7, n4))). % 92.37/49.94 tff(c_21361, plain, (~p(n2, n8, n3))). % 92.37/49.95 tff(c_23084, plain, (p(n1, n6, n5))). % 92.37/49.95 tff(c_23014, plain, (~p(n6, n9, n4))). % 92.37/49.95 tff(c_23012, plain, (~p(n5, n7, n1))). % 92.37/49.95 tff(c_23010, plain, (~p(n5, n7, n6))). % 92.37/49.95 tff(c_23008, plain, (~p(n5, n7, n7))). % 92.37/49.95 tff(c_21634, plain, (~p(n6, n6, n9))). % 92.37/49.95 tff(c_22984, plain, (~p(n4, n9, n7))). % 92.37/49.95 tff(c_22980, plain, (~p(n4, n9, n9))). % 92.37/49.95 tff(c_23006, plain, (~p(n5, n7, n8))). % 92.37/49.95 tff(c_21648, plain, (~p(n6, n6, n6))). % 92.37/49.95 tff(c_22785, plain, (~p(n4, n8, n9))). % 92.37/49.95 tff(c_23002, plain, (~p(n6, n8, n4))). % 92.37/49.95 tff(c_22996, plain, (~p(n2, n9, n5))). % 92.37/49.95 tff(c_22994, plain, (~p(n6, n9, n5))). % 92.37/49.95 tff(c_22988, plain, (~p(n4, n9, n1))). % 92.37/49.95 tff(c_21685, plain, (~p(n6, n5, n4))). % 92.37/49.95 tff(c_22992, plain, (~p(n8, n9, n5))). % 92.37/49.95 tff(c_22982, plain, (~p(n4, n9, n8))). % 92.37/49.95 tff(c_22990, plain, (~p(n9, n9, n5))). % 92.37/49.95 tff(c_21217, plain, (~p(n8, n5, n7))). % 92.37/49.95 tff(c_22986, plain, (~p(n4, n9, n4))). % 92.37/49.95 tff(c_22712, plain, (~p(n5, n3, n4))). % 92.37/49.95 tff(c_22978, plain, (~p(n6, n8, n5))). % 92.37/49.95 tff(c_22701, plain, (~p(n8, n4, n3))). % 92.37/49.95 tff(c_22783, plain, (p(n4, n8, n3))). % 92.37/49.95 tff(c_21212, plain, (~p(n8, n6, n7))). % 92.37/49.95 tff(c_22936, plain, (~p(n4, n2, n5))). % 92.37/49.95 tff(c_22942, plain, (~p(n5, n2, n4))). % 92.37/49.95 tff(c_22927, plain, (~p(n5, n2, n1))). % 92.37/49.95 tff(c_21597, plain, (~p(n7, n4, n9))). % 92.37/49.95 tff(c_22932, plain, (~p(n7, n2, n5))). % 92.37/49.95 tff(c_22934, plain, (~p(n6, n2, n5))). % 92.37/49.95 tff(c_22925, plain, (~p(n5, n2, n6))). % 92.37/49.95 tff(c_22911, plain, (~p(n6, n3, n5))). % 92.37/49.95 tff(c_22921, plain, (~p(n5, n2, n8))). % 92.37/49.95 tff(c_21346, plain, (~p(n4, n3, n9))). % 92.37/49.95 tff(c_22831, plain, (~p(n1, n9, n2))). % 92.37/49.95 tff(c_22919, plain, (~p(n5, n2, n9))). % 92.37/49.95 tff(c_22463, plain, (~p(n3, n4, n6))). % 92.37/49.95 tff(c_21630, plain, (~p(n7, n4, n1))). % 92.37/49.95 tff(c_22426, plain, (~p(n2, n4, n7))). % 92.37/49.95 tff(c_22467, plain, (~p(n2, n4, n6))). % 92.37/49.95 tff(c_22455, plain, (~p(n5, n4, n6))). % 92.37/49.95 tff(c_22431, plain, (~p(n2, n4, n2))). % 92.37/49.95 tff(c_22441, plain, (~p(n8, n4, n6))). % 92.37/49.95 tff(c_21562, plain, (~p(n7, n8, n9))). % 92.37/49.95 tff(c_22436, plain, (~p(n9, n4, n6))). % 92.37/49.95 tff(c_22825, plain, (~p(n4, n9, n2))). % 92.37/49.95 tff(c_22807, plain, (~p(n5, n9, n9))). % 92.37/49.95 tff(c_21524, plain, (~p(n8, n2, n9))). % 92.37/49.95 tff(c_22823, plain, (~p(n6, n9, n2))). % 92.37/49.95 tff(c_22821, plain, (~p(n8, n9, n2))). % 92.37/49.95 tff(c_22819, plain, (~p(n5, n9, n7))). % 92.37/49.95 tff(c_22815, plain, (~p(n5, n9, n4))). % 92.37/49.95 tff(c_22811, plain, (~p(n5, n9, n6))). % 92.37/49.95 tff(c_21539, plain, (~p(n8, n2, n6))). % 92.37/49.95 tff(c_22817, plain, (~p(n5, n9, n1))). % 92.37/49.95 tff(c_22813, plain, (~p(n5, n9, n5))). % 92.37/49.95 tff(c_22809, plain, (~p(n5, n9, n8))). % 92.37/49.95 tff(c_21310, plain, (~p(n4, n4, n3))). % 92.37/49.95 tff(c_22803, plain, (~p(n6, n8, n2))). % 92.37/49.95 tff(c_22800, plain, (~p(n4, n8, n4))). % 92.37/49.95 tff(c_22795, plain, (~p(n6, n8, n3))). % 92.37/49.95 tff(c_22798, plain, (~p(n3, n8, n3))). % 92.37/49.95 tff(c_22714, plain, (~p(n5, n3, n1))). % 92.37/49.95 tff(c_21305, plain, (~p(n5, n4, n4))). % 92.37/49.95 tff(c_22793, plain, (~p(n4, n8, n2))). % 92.37/49.95 tff(c_22791, plain, (~p(n4, n8, n5))). % 92.37/49.95 tff(c_22718, plain, (~p(n5, n3, n8))). % 92.37/49.95 tff(c_21291, plain, (~p(n4, n5, n3))). % 92.37/49.95 tff(c_22731, plain, (~p(n6, n3, n3))). % 92.37/49.95 tff(c_22735, plain, (~p(n2, n3, n3))). % 92.37/49.95 tff(c_22733, plain, (~p(n4, n3, n3))). % 92.37/49.95 tff(c_22720, plain, (~p(n5, n3, n6))). % 92.37/49.95 tff(c_22724, plain, (~p(n5, n3, n2))). % 92.37/49.95 tff(c_21490, plain, (~p(n8, n7, n9))). % 92.37/49.95 tff(c_22729, plain, (~p(n8, n3, n3))). % 92.37/49.95 tff(c_22722, plain, (~p(n5, n3, n5))). % 92.37/49.95 tff(c_22726, plain, (~p(n3, n3, n3))). % 92.37/49.95 tff(c_21277, plain, (~p(n5, n4, n5))). % 92.37/49.95 tff(c_22716, plain, (~p(n5, n3, n9))). % 92.37/49.95 tff(c_22710, plain, (~p(n4, n1, n3))). % 92.37/49.95 tff(c_22708, plain, (~p(n6, n1, n3))). % 92.37/49.95 tff(c_22697, plain, (~p(n9, n4, n4))). % 92.37/49.95 tff(c_22689, plain, (p(n9, n4, n3))). % 92.37/49.95 tff(c_21510, plain, (~p(n8, n7, n5))). % 92.37/49.95 tff(c_22695, plain, (~p(n9, n4, n5))). % 92.37/49.95 tff(c_22653, plain, (~p(n3, n9, n3))). % 92.37/49.95 tff(c_22699, plain, (~p(n9, n4, n1))). % 92.37/49.95 tff(c_21267, plain, (~p(n5, n5, n3))). % 92.37/49.95 tff(c_22693, plain, (~p(n9, n4, n8))). % 92.37/49.95 tff(c_22684, plain, (p(n5, n3, n3))). % 92.37/49.95 tff(c_22576, plain, (~p(n1, n5, n9))). % 92.37/49.95 tff(c_22647, plain, (~p(n6, n9, n3))). % 92.37/49.95 tff(c_22691, plain, (~p(n9, n4, n9))). % 92.37/49.95 tff(c_22162, plain, (~p(n4, n7, n2))). % 92.37/49.95 tff(c_22643, plain, (~p(n7, n9, n6))). % 92.37/49.95 tff(c_22641, plain, (~p(n7, n9, n5))). % 92.37/49.95 tff(c_22629, plain, (~p(n7, n9, n8))). % 92.37/49.95 tff(c_22076, plain, (~p(n9, n8, n1))). % 92.37/49.95 tff(c_22635, plain, (~p(n7, n9, n7))). % 92.37/49.95 tff(c_22633, plain, (~p(n7, n9, n9))). % 92.37/49.95 tff(c_22631, plain, (~p(n7, n9, n4))). % 92.37/49.95 tff(c_22627, plain, (~p(n9, n8, n3))). % 92.37/49.95 tff(c_22597, plain, (~p(n2, n5, n3))). % 92.37/49.95 tff(c_22121, plain, (~p(n3, n8, n6))). % 92.37/49.95 tff(c_22595, plain, (~p(n3, n5, n3))). % 92.37/49.95 tff(c_22592, plain, (~p(n7, n5, n3))). % 92.37/49.95 tff(c_22625, plain, (~p(n8, n8, n3))). % 92.37/49.95 tff(c_22136, plain, (~p(n1, n8, n1))). % 92.37/49.95 tff(c_22618, plain, (p(n7, n9, n3))). % 92.37/49.95 tff(c_22582, plain, (~p(n1, n5, n2))). % 92.37/49.95 tff(c_22574, plain, (~p(n3, n4, n3))). % 92.37/49.95 tff(c_22580, plain, (~p(n1, n5, n6))). % 92.37/49.95 tff(c_22578, plain, (~p(n1, n5, n7))). % 92.37/49.95 tff(c_21976, plain, (~p(n1, n4, n9))). % 92.37/49.95 tff(c_22544, plain, (~p(n6, n2, n2))). % 92.37/49.95 tff(c_22549, plain, (~p(n5, n2, n2))). % 92.37/49.95 tff(c_22558, plain, (~p(n2, n2, n3))). % 92.37/49.95 tff(c_21467, plain, (~p(n3, n3, n1))). % 92.37/49.95 tff(c_22572, plain, (~p(n2, n4, n3))). % 92.37/49.95 tff(c_22569, plain, (p(n1, n5, n3))). % 92.37/49.95 tff(c_22563, plain, (~p(n2, n2, n2))). % 92.37/49.95 tff(c_22567, plain, (~p(n1, n2, n3))). % 92.37/49.95 tff(c_24338, plain, (~p(n7, n1, n5))). % 92.37/49.95 tff(c_21194, plain, (~p(n7, n8, n2))). % 92.37/49.95 tff(c_24336, plain, (~p(n3, n1, n6))). % 92.37/49.95 tff(c_24330, plain, (~p(n9, n5, n1))). % 92.37/49.95 tff(c_24328, plain, (~p(n9, n6, n1))). % 92.37/49.95 tff(c_21242, plain, (~p(n6, n9, n6))). % 92.37/49.95 tff(c_24326, plain, (~p(n1, n2, n1))). % 92.37/49.95 tff(c_24324, plain, (~p(n9, n2, n4))). % 92.37/49.95 tff(c_24322, plain, (~p(n9, n2, n6))). % 92.37/49.95 tff(c_24320, plain, (~p(n9, n2, n8))). % 92.37/49.95 tff(c_24316, plain, (p(n9, n2, n1))). % 92.37/49.95 tff(c_21179, plain, (~p(n9, n9, n1))). % 92.37/49.95 tff(c_24318, plain, (~p(n9, n2, n9))). % 92.37/49.95 tff(c_24292, plain, (~p(n3, n3, n5))). % 92.37/49.95 tff(c_24290, plain, (~p(n3, n3, n4))). % 92.37/49.95 tff(c_21184, plain, (~p(n9, n7, n1))). % 92.37/49.95 tff(c_24314, plain, (p(n7, n3, n5))). % 92.37/49.95 tff(c_24313, plain, (p(n3, n1, n5))). % 92.37/49.95 tff(c_24287, plain, (~p(n7, n3, n8))). % 92.37/49.95 tff(c_24285, plain, (~p(n8, n3, n8))). % 92.37/49.95 tff(c_24283, plain, (~p(n9, n3, n8))). % 92.37/49.95 tff(c_21411, plain, (~p(n3, n6, n6))). % 92.37/49.95 tff(c_24273, plain, (~p(n8, n3, n1))). % 92.37/49.95 tff(c_24281, plain, (~p(n3, n3, n6))). % 92.37/49.95 tff(c_24271, plain, (~p(n9, n3, n1))). % 92.37/49.96 tff(c_21429, plain, (~p(n2, n5, n6))). % 92.37/49.96 tff(c_24279, plain, (~p(n3, n3, n9))). % 92.37/49.96 tff(c_24266, plain, (p(n3, n3, n8))). % 92.37/49.96 tff(c_24255, plain, (p(n4, n3, n1))). % 92.37/49.96 tff(c_24253, plain, (~p(n6, n2, n8))). % 92.37/49.96 tff(c_24251, plain, (~p(n6, n3, n8))). % 92.37/49.96 tff(c_21434, plain, (~p(n2, n3, n2))). % 92.37/49.96 tff(c_24247, plain, (~p(n4, n3, n8))). % 92.37/49.96 tff(c_24244, plain, (~p(n3, n1, n8))). % 92.37/49.96 tff(c_24240, plain, (~p(n7, n1, n8))). % 92.37/49.96 tff(c_21396, plain, (~p(n3, n5, n8))). % 92.37/49.96 tff(c_24242, plain, (~p(n6, n1, n8))). % 92.37/49.96 tff(c_24238, plain, (~p(n9, n1, n8))). % 92.37/49.96 tff(c_24234, plain, (~p(n6, n2, n7))). % 92.37/49.96 tff(c_24232, plain, (~p(n4, n2, n8))). % 92.37/49.96 tff(c_24228, plain, (p(n4, n1, n8))). % 92.37/49.96 tff(c_21232, plain, (~p(n7, n3, n3))). % 92.37/49.96 tff(c_24230, plain, (~p(n4, n2, n1))). % 92.37/49.96 tff(c_24227, plain, (p(n4, n2, n7))). % 92.37/49.96 tff(c_24208, plain, (~p(n4, n1, n7))). % 92.37/49.96 tff(c_21381, plain, (~p(n1, n9, n5))). % 92.37/49.96 tff(c_24206, plain, (~p(n6, n1, n7))). % 92.37/49.96 tff(c_24202, plain, (~p(n8, n1, n6))). % 92.37/49.96 tff(c_24204, plain, (~p(n8, n1, n4))). % 92.37/49.96 tff(c_24174, plain, (~p(n9, n9, n6))). % 92.37/49.96 tff(c_24198, plain, (p(n8, n1, n7))). % 92.37/49.96 tff(c_21227, plain, (~p(n9, n1, n3))). % 92.37/49.96 tff(c_24170, plain, (~p(n7, n1, n6))). % 92.37/49.96 tff(c_24200, plain, (~p(n8, n1, n8))). % 92.37/49.96 tff(c_24168, plain, (~p(n7, n2, n6))). % 92.37/49.96 tff(c_21356, plain, (~p(n2, n9, n3))). % 92.37/49.96 tff(c_24166, plain, (~p(n7, n3, n6))). % 92.37/49.96 tff(c_23470, plain, (~p(n7, n7, n7))). % 92.37/49.96 tff(c_23825, plain, (~p(n4, n3, n4))). % 92.37/49.96 tff(c_23485, plain, (~p(n7, n3, n1))). % 92.37/49.96 tff(c_23475, plain, (~p(n7, n6, n7))). % 92.37/49.96 tff(c_21366, plain, (~p(n3, n9, n5))). % 92.37/49.96 tff(c_23479, plain, (~p(n7, n5, n7))). % 92.37/49.96 tff(c_23829, plain, (~p(n4, n3, n2))). % 92.37/49.96 tff(c_23494, plain, (~p(n7, n2, n1))). % 92.37/49.96 tff(c_21207, plain, (~p(n9, n5, n7))). % 92.37/49.96 tff(c_23662, plain, (~p(n2, n4, n9))). % 92.37/49.96 tff(c_23859, plain, (~p(n4, n1, n4))). % 92.37/49.96 tff(c_23821, plain, (~p(n4, n3, n6))). % 92.37/49.96 tff(c_23499, plain, (~p(n7, n2, n7))). % 92.37/49.96 tff(c_23660, plain, (~p(n3, n4, n9))). % 92.37/49.96 tff(c_21202, plain, (~p(n9, n6, n7))). % 92.37/49.96 tff(c_23652, plain, (~p(n6, n4, n8))). % 92.37/49.96 tff(c_23650, plain, (~p(n5, n6, n9))). % 92.37/49.96 tff(c_23656, plain, (~p(n5, n4, n9))). % 92.37/49.96 tff(c_21336, plain, (~p(n6, n3, n9))). % 92.37/49.96 tff(c_23624, plain, (~p(n4, n7, n7))). % 92.37/49.96 tff(c_23508, plain, (~p(n7, n1, n7))). % 92.37/49.96 tff(c_23648, plain, (p(n6, n4, n9))). % 92.37/49.96 tff(c_23622, plain, (~p(n4, n7, n1))). % 92.37/49.96 tff(c_23654, plain, (~p(n6, n4, n1))). % 92.37/49.96 tff(c_21341, plain, (~p(n6, n2, n9))). % 92.37/49.96 tff(c_23617, plain, (~p(n1, n7, n9))). % 92.37/49.96 tff(c_23613, plain, (~p(n7, n7, n9))). % 92.37/49.96 tff(c_23615, plain, (~p(n6, n7, n9))). % 92.37/49.96 tff(c_21300, plain, (~p(n5, n6, n4))). % 92.37/49.96 tff(c_23899, plain, (~p(n3, n1, n2))). % 92.37/49.96 tff(c_23611, plain, (~p(n9, n7, n9))). % 92.37/49.96 tff(c_23893, plain, (~p(n3, n3, n2))). % 92.37/49.96 tff(c_23605, plain, (~p(n6, n9, n9))). % 92.37/49.96 tff(c_23609, plain, (~p(n4, n7, n8))). % 92.37/49.96 tff(c_21287, plain, (~p(n6, n6, n4))). % 92.37/49.96 tff(c_23589, plain, (~p(n4, n6, n7))). % 92.37/49.96 tff(c_23597, plain, (p(n4, n7, n9))). % 92.37/49.96 tff(c_23607, plain, (~p(n6, n8, n9))). % 92.37/49.96 tff(c_21272, plain, (~p(n5, n4, n3))). % 92.37/49.96 tff(c_23585, plain, (~p(n4, n6, n2))). % 92.37/49.96 tff(c_23587, plain, (~p(n4, n6, n4))). % 92.37/49.96 tff(c_23582, plain, (~p(n7, n6, n6))). % 92.37/49.96 tff(c_23580, plain, (~p(n9, n6, n6))). % 92.37/49.96 tff(c_23577, plain, (~p(n4, n6, n9))). % 92.37/49.96 tff(c_21262, plain, (~p(n5, n6, n5))). % 92.37/49.96 tff(c_23575, plain, (~p(n8, n6, n6))). % 92.37/49.96 tff(c_23573, plain, (~p(n4, n6, n1))). % 92.37/49.96 tff(c_23571, plain, (p(n4, n6, n6))). % 92.37/49.96 tff(c_21257, plain, (~p(n4, n7, n6))). % 92.37/49.96 tff(c_23559, plain, (~p(n5, n6, n6))). % 92.37/49.96 tff(c_23568, plain, (~p(n5, n5, n6))). % 92.37/49.96 tff(c_24340, plain, (~p(n3, n1, n4))). % 92.37/49.96 tff(c_24344, plain, (~p(n7, n3, n4))). % 92.37/49.96 tff(c_24346, plain, (~p(n7, n3, n2))). % 92.37/49.96 tff(c_22116, plain, (~p(n3, n8, n1))). % 92.37/49.96 tff(c_24351, plain, (~p(n7, n3, n9))). % 92.37/49.96 tff(c_24356, plain, (p(n7, n2, n8))). % 92.37/49.96 tff(c_24370, plain, (p(n3, n9, n6))). % 92.37/49.96 tff(c_21252, plain, (~p(n4, n9, n6))). % 92.37/49.96 tff(c_24385, plain, (~p(n7, n2, n4))). % 92.37/49.96 tff(c_24387, plain, (~p(n7, n5, n8))). % 92.37/49.96 tff(c_24390, plain, (~p(n7, n2, n9))). % 92.37/49.96 tff(c_24394, plain, (~p(n2, n9, n6))). % 92.37/49.96 tff(c_24398, plain, (~p(n3, n9, n4))). % 92.37/49.96 tff(c_21189, plain, (~p(n8, n9, n1))). % 92.37/49.96 tff(c_24400, plain, (~p(n3, n9, n7))). % 92.37/49.96 tff(c_24402, plain, (~p(n3, n9, n9))). % 92.37/49.96 tff(c_24404, plain, (~p(n3, n9, n1))). % 92.37/49.96 tff(c_21174, plain, (~p(n7, n9, n2))). % 92.37/49.96 tff(c_24409, plain, (p(n7, n5, n9))). % 92.37/49.96 tff(c_24421, plain, (p(n2, n9, n1))). % 92.37/49.96 tff(c_24423, plain, (~p(n9, n5, n9))). % 92.37/49.96 tff(c_24425, plain, (~p(n8, n5, n9))). % 92.37/49.96 tff(c_24427, plain, (~p(n3, n5, n9))). % 92.37/49.96 tff(c_21406, plain, (~p(n1, n5, n8))). % 92.37/49.96 tff(c_24430, plain, (~p(n7, n6, n9))). % 92.37/49.96 tff(c_24433, plain, (~p(n8, n6, n9))). % 92.37/49.96 tff(c_24435, plain, (~p(n9, n6, n9))). % 92.37/49.96 tff(c_21169, plain, (~p(n9, n8, n2))). % 92.37/49.96 tff(c_24439, plain, (~p(n2, n9, n4))). % 92.37/49.96 tff(c_24441, plain, (~p(n2, n9, n7))). % 92.37/49.96 tff(c_24443, plain, (~p(n2, n4, n1))). % 92.37/49.96 tff(c_24460, plain, (p(n2, n8, n7))). % 92.37/49.96 tff(c_24452, plain, (p(n3, n6, n9))). % 92.37/49.96 tff(c_21164, plain, (~p(n9, n9, n2))). % 92.37/49.96 tff(c_24445, plain, (~p(n2, n9, n9))). % 92.37/49.96 tff(c_24461, plain, (p(n6, n9, n7))). % 92.37/49.96 tff(c_24462, plain, (p(n2, n4, n4))). % 92.37/49.96 tff(c_21222, plain, (~p(n9, n3, n3))). % 92.37/49.96 tff(c_24463, plain, (p(n3, n4, n1))). % 92.37/49.96 tff(c_24470, plain, (~p(n3, n6, n7))). % 92.37/49.96 tff(c_24472, plain, (~p(n3, n6, n1))). % 92.37/49.96 tff(c_24475, plain, (~p(n3, n8, n9))). % 92.37/49.96 tff(c_24477, plain, (~p(n3, n6, n4))). % 92.37/49.96 tff(c_24698, plain, (~p(n8, n9, n4))). % 92.37/49.96 tff(c_24481, plain, (~p(n6, n8, n7))). % 92.37/49.96 tff(c_24483, plain, (~p(n3, n8, n7))). % 92.37/49.96 tff(c_24485, plain, (~p(n2, n8, n9))). % 92.37/49.96 tff(c_24677, plain, (~p(n9, n1, n2))). % 92.37/49.96 tff(c_24487, plain, (~p(n2, n8, n4))). % 92.37/49.96 tff(c_24495, plain, (~p(n6, n9, n8))). % 92.37/49.96 tff(c_24499, plain, (~p(n3, n4, n4))). % 92.37/49.96 tff(c_24504, plain, (~p(n2, n3, n4))). % 92.37/49.96 tff(c_24506, plain, (~p(n2, n2, n4))). % 92.37/49.96 tff(c_24642, plain, (~p(n6, n1, n6))). % 92.37/49.96 tff(c_24514, plain, (~p(n3, n5, n1))). % 92.37/49.96 tff(c_24516, plain, (p(n3, n5, n7))). % 92.37/49.96 tff(c_24517, plain, (p(n5, n6, n7))). % 92.37/49.96 tff(c_24615, plain, (~p(n8, n6, n4))). % 92.37/49.96 tff(c_24545, plain, (p(n8, n8, n9))). % 92.37/49.96 tff(c_24559, plain, (p(n3, n8, n4))). % 92.37/49.96 tff(c_24564, plain, (p(n1, n9, n9))). % 92.37/49.96 tff(c_24523, plain, (p(n6, n8, n8))). % 92.37/49.96 tff(c_24584, plain, (p(n1, n2, n4))). % 92.37/49.96 tff(c_24573, plain, (~p(n1, n2, n9))). % 92.37/49.96 tff(c_24537, plain, (~p(n5, n5, n7))). % 92.37/49.96 tff(c_24540, plain, (~p(n5, n6, n1))). % 92.37/49.96 tff(c_24547, plain, (~p(n8, n8, n8))). % 92.37/49.96 tff(c_21072, plain, (p(n3, n2, n2))). % 92.37/49.96 tff(c_24549, plain, (~p(n8, n8, n4))). % 92.37/49.96 tff(c_24551, plain, (~p(n9, n9, n9))). % 92.37/49.96 tff(c_24553, plain, (~p(n8, n9, n9))). % 92.37/49.96 tff(c_24555, plain, (~p(n8, n3, n9))). % 92.37/49.96 tff(c_24563, plain, (~p(n1, n9, n4))). % 92.37/49.96 tff(c_21074, plain, (p(n3, n7, n3))). % 92.37/49.96 tff(c_21070, plain, (p(n2, n7, n5))). % 92.37/49.96 tff(c_24588, plain, (~p(n6, n2, n4))). % 92.37/49.96 tff(c_24595, plain, (p(n5, n5, n1))). % 92.37/49.96 tff(c_21076, plain, (p(n4, n4, n2))). % 92.37/49.96 tff(c_24597, plain, (p(n8, n6, n1))). % 92.37/49.96 tff(c_24602, plain, (p(n9, n3, n9))). % 92.37/49.96 tff(c_24607, plain, (p(n2, n2, n9))). % 92.37/49.96 tff(c_24609, plain, (p(n6, n2, n6))). % 92.37/49.96 tff(c_24611, plain, (~p(n8, n5, n1))). % 92.37/49.96 tff(c_21078, plain, (p(n4, n5, n4))). % 92.37/49.96 tff(c_21068, plain, (p(n2, n6, n8))). % 92.37/49.96 tff(c_24621, plain, (~p(n9, n3, n4))). % 92.37/49.96 tff(c_24623, plain, (~p(n9, n3, n2))). % 92.37/49.96 tff(c_21080, plain, (p(n5, n1, n9))). % 92.37/49.96 tff(c_24625, plain, (~p(n2, n3, n9))). % 92.37/49.96 tff(c_24627, plain, (~p(n9, n3, n6))). % 92.37/49.96 tff(c_24631, plain, (~p(n2, n2, n6))). % 92.37/49.96 tff(c_24640, plain, (~p(n6, n3, n6))). % 92.37/49.96 tff(c_24652, plain, (p(n6, n3, n2))). % 92.37/49.96 tff(c_21082, plain, (p(n5, n8, n6))). % 92.37/49.96 tff(c_21066, plain, (p(n1, n4, n6))). % 92.37/49.96 tff(c_24653, plain, (p(n2, n3, n6))). % 92.37/49.96 tff(c_24660, plain, (p(n9, n1, n6))). % 92.37/49.96 tff(c_21084, plain, (p(n6, n5, n5))). % 92.37/49.96 tff(c_24663, plain, (~p(n6, n3, n4))). % 92.37/49.96 tff(c_24665, plain, (~p(n6, n1, n2))). % 92.37/49.96 tff(c_24667, plain, (~p(n8, n3, n6))). % 92.37/49.96 tff(c_24673, plain, (~p(n9, n1, n4))). % 92.37/49.96 tff(c_24675, plain, (~p(n9, n5, n6))). % 92.37/49.96 tff(c_21086, plain, (p(n6, n6, n3))). % 92.37/49.96 tff(c_21064, plain, (p(n1, n3, n7))). % 92.37/49.96 tff(c_24683, plain, (p(n6, n1, n4))). % 92.37/49.96 tff(c_24684, plain, (p(n8, n3, n4))). % 92.37/49.96 tff(c_21088, plain, (p(n7, n4, n7))). % 92.37/49.96 tff(c_24686, plain, (p(n8, n5, n6))). % 92.37/49.96 tff(c_24692, plain, (p(n9, n5, n8))). % 92.37/49.96 tff(c_24693, plain, (p(n9, n6, n2))). % 92.37/49.96 tff(c_24694, plain, (p(n7, n1, n2))). % 92.37/49.96 tff(c_24696, plain, (~p(n7, n1, n4))). % 92.37/49.96 tff(c_21090, plain, (p(n7, n8, n1))). % 92.37/49.97 tff(c_21062, plain, (p(n1, n1, n1))). % 92.37/49.97 tff(c_24704, plain, (~p(n8, n5, n8))). % 92.37/49.97 tff(c_24713, plain, (~p(n9, n9, n8))). % 92.37/49.97 tff(c_21092, plain, (p(n8, n2, n3))). % 92.37/49.97 tff(c_24717, plain, (~p(n9, n6, n4))). % 92.37/49.97 tff(c_24719, plain, (~p(n7, n6, n2))). % 92.37/49.97 tff(c_24728, plain, (p(n7, n6, n4))). % 92.37/49.97 tff(c_24729, plain, (p(n9, n9, n4))). % 92.37/49.97 tff(c_24730, plain, (p(n8, n9, n8))). % 92.37/49.97 tff(c_21094, plain, (p(n8, n7, n2))). % 92.37/49.97 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 92.37/49.97 %------------------------------------------------------------------------------