%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ080+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 : n023.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:15 PM UTC 2025 % Result : Satisfiable 79.69s 37.05s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PUZ080+2 : TPTP v9.0.0. Bugfixed v5.4.0. % 0.07/0.12 % 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.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 17:24:09 EDT 2025 % 0.12/0.34 % CPUTime : % 79.69/37.05 % 79.69/37.05 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 79.69/37.05 % 79.69/37.05 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 79.77/37.07 %$ p > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n3 > n2 > n1 % 79.77/37.07 % 79.77/37.07 %Foreground sorts: % 79.77/37.07 % 79.77/37.07 % 79.77/37.07 %Background operators: % 79.77/37.07 % 79.77/37.07 % 79.77/37.07 %Foreground operators: % 79.77/37.07 tff(n8, type, n8: $i). % 79.77/37.07 tff(n9, type, n9: $i). % 79.77/37.07 tff(n3, type, n3: $i). % 79.77/37.07 tff(n1, type, n1: $i). % 79.77/37.07 tff(n7, type, n7: $i). % 79.77/37.07 tff(n6, type, n6: $i). % 79.77/37.07 tff(n4, type, n4: $i). % 79.77/37.07 tff(p, type, p: ($i * $i * $i) > $o). % 79.77/37.07 tff(n2, type, n2: $i). % 79.77/37.07 tff(n5, type, n5: $i). % 79.77/37.07 % 79.77/37.07 %Saturated clause set: % 79.77/37.07 tff(c_22219, plain, (~p(n2, n8, n9))). % 79.77/37.07 tff(c_22279, plain, (~p(n2, n5, n2))). % 79.77/37.07 tff(c_22185, plain, (~p(n3, n1, n8))). % 79.77/37.07 tff(c_22263, plain, (~p(n2, n5, n6))). % 79.77/37.07 tff(c_22254, plain, (~p(n2, n5, n8))). % 79.77/37.07 tff(c_22307, plain, (~p(n2, n2, n3))). % 79.77/37.07 tff(c_21649, plain, (~p(n9, n7, n4))). % 79.77/37.07 tff(c_21654, plain, (~p(n9, n7, n2))). % 79.77/37.07 tff(c_22197, plain, (~p(n3, n1, n5))). % 79.77/37.07 tff(c_22378, plain, (~p(n1, n4, n2))). % 79.77/37.07 tff(c_21659, plain, (~p(n9, n7, n1))). % 79.77/37.07 tff(c_22347, plain, (~p(n1, n6, n3))). % 79.77/37.07 tff(c_22214, plain, (~p(n3, n1, n1))). % 79.77/37.07 tff(c_22350, plain, (~p(n1, n6, n2))). % 79.77/37.07 tff(c_22333, plain, (~p(n1, n6, n6))). % 79.77/37.07 tff(c_22324, plain, (~p(n1, n6, n8))). % 79.77/37.07 tff(c_22356, plain, (~p(n1, n4, n8))). % 79.77/37.07 tff(c_21672, plain, (~p(n9, n3, n6))). % 79.77/37.07 tff(c_22244, plain, (~p(n2, n8, n2))). % 79.77/37.07 tff(c_21692, plain, (~p(n9, n3, n1))). % 79.77/37.07 tff(c_22390, plain, (~p(n7, n9, n7))). % 79.77/37.07 tff(c_21805, plain, (~p(n8, n1, n4))). % 79.77/37.07 tff(c_22228, plain, (~p(n2, n8, n7))). % 79.77/37.07 tff(c_21814, plain, (~p(n8, n1, n1))). % 79.77/37.07 tff(c_21698, plain, (~p(n8, n9, n8))). % 79.77/37.07 tff(c_21703, plain, (~p(n8, n9, n6))). % 79.77/37.07 tff(c_21730, plain, (~p(n8, n7, n7))). % 79.77/37.07 tff(c_21713, plain, (~p(n8, n9, n4))). % 79.77/37.07 tff(c_22239, plain, (~p(n2, n8, n3))). % 79.77/37.07 tff(c_21719, plain, (~p(n8, n9, n2))). % 79.77/37.07 tff(c_21725, plain, (~p(n8, n7, n8))). % 79.77/37.07 tff(c_21478, plain, (~p(n4, n4, n7))). % 79.77/37.07 tff(c_22249, plain, (~p(n2, n8, n1))). % 79.77/37.07 tff(c_21481, plain, (~p(n5, n5, n8))). % 79.77/37.07 tff(c_21789, plain, (~p(n8, n1, n9))). % 79.77/37.07 tff(c_21733, plain, (~p(n8, n7, n6))). % 79.77/37.08 tff(c_21738, plain, (~p(n8, n7, n5))). % 79.77/37.08 tff(c_21748, plain, (~p(n8, n7, n3))). % 79.77/37.08 tff(c_22202, plain, (~p(n3, n1, n4))). % 79.77/37.08 tff(c_21743, plain, (~p(n8, n7, n4))). % 79.77/37.08 tff(c_21750, plain, (~p(n8, n7, n2))). % 79.77/37.08 tff(c_21755, plain, (~p(n8, n7, n1))). % 79.77/37.08 tff(c_21620, plain, (~p(n1, n2, n9))). % 79.77/37.08 tff(c_21809, plain, (~p(n8, n1, n2))). % 79.77/37.08 tff(c_21794, plain, (~p(n8, n1, n7))). % 79.77/37.08 tff(c_21800, plain, (~p(n8, n1, n5))). % 79.77/37.08 tff(c_21784, plain, (~p(n8, n3, n2))). % 79.77/37.08 tff(c_21776, plain, (~p(n8, n3, n4))). % 79.77/37.08 tff(c_21610, plain, (~p(n1, n3, n9))). % 79.77/37.08 tff(c_21781, plain, (~p(n8, n3, n3))). % 79.77/37.08 tff(c_21768, plain, (~p(n8, n3, n6))). % 79.77/37.08 tff(c_21771, plain, (~p(n8, n3, n5))). % 79.77/37.08 tff(c_22129, plain, (~p(n4, n1, n6))). % 79.77/37.08 tff(c_21764, plain, (~p(n8, n3, n7))). % 79.77/37.08 tff(c_21761, plain, (~p(n8, n3, n8))). % 79.77/37.08 tff(c_21757, plain, (~p(n8, n3, n9))). % 79.77/37.08 tff(c_21844, plain, (~p(n7, n7, n2))). % 79.77/37.08 tff(c_21831, plain, (~p(n7, n7, n5))). % 79.77/37.08 tff(c_21603, plain, (~p(n2, n2, n9))). % 79.77/37.08 tff(c_21817, plain, (~p(n7, n7, n9))). % 79.77/37.08 tff(c_21827, plain, (~p(n7, n7, n6))). % 79.77/37.08 tff(c_21820, plain, (~p(n7, n7, n8))). % 79.77/37.08 tff(c_21606, plain, (~p(n3, n1, n7))). % 79.77/37.08 tff(c_21836, plain, (~p(n7, n7, n4))). % 79.77/37.08 tff(c_21841, plain, (~p(n7, n7, n3))). % 79.77/37.08 tff(c_21863, plain, (~p(n7, n6, n5))). % 79.77/37.08 tff(c_21858, plain, (~p(n7, n6, n7))). % 79.77/37.08 tff(c_21853, plain, (~p(n7, n6, n8))). % 79.77/37.08 tff(c_21590, plain, (~p(n2, n5, n3))). % 79.77/37.08 tff(c_21848, plain, (~p(n7, n6, n9))). % 79.77/37.08 tff(c_21878, plain, (~p(n7, n6, n1))). % 79.77/37.08 tff(c_21893, plain, (~p(n7, n4, n5))). % 79.77/37.08 tff(c_21586, plain, (~p(n1, n4, n9))). % 79.77/37.08 tff(c_21898, plain, (~p(n7, n4, n4))). % 79.77/37.08 tff(c_21889, plain, (~p(n7, n4, n6))). % 79.77/37.08 tff(c_21885, plain, (~p(n7, n4, n8))). % 79.77/37.08 tff(c_21880, plain, (~p(n7, n4, n9))). % 79.77/37.08 tff(c_22963, plain, (~p(n4, n3, n8))). % 79.77/37.08 tff(c_21566, plain, (~p(n2, n4, n1))). % 79.77/37.08 tff(c_22996, plain, (~p(n2, n3, n1))). % 79.77/37.08 tff(c_22976, plain, (~p(n3, n3, n8))). % 79.77/37.08 tff(c_22991, plain, (~p(n2, n3, n8))). % 79.77/37.08 tff(c_22026, plain, (~p(n4, n9, n9))). % 79.77/37.08 tff(c_23001, plain, (~p(n2, n3, n6))). % 79.77/37.08 tff(c_23014, plain, (~p(n1, n3, n6))). % 79.77/37.08 tff(c_23010, plain, (~p(n1, n3, n1))). % 79.77/37.08 tff(c_23005, plain, (~p(n1, n3, n8))). % 79.77/37.08 tff(c_22019, plain, (~p(n5, n4, n2))). % 79.77/37.08 tff(c_21554, plain, (~p(n3, n4, n1))). % 79.77/37.08 tff(c_22015, plain, (~p(n5, n4, n3))). % 79.77/37.08 tff(c_22003, plain, (~p(n5, n4, n8))). % 79.77/37.08 tff(c_22010, plain, (~p(n5, n4, n5))). % 79.77/37.08 tff(c_21559, plain, (~p(n1, n6, n9))). % 79.77/37.08 tff(c_21984, plain, (~p(n5, n6, n4))). % 79.77/37.08 tff(c_21987, plain, (~p(n5, n6, n3))). % 79.77/37.08 tff(c_21992, plain, (~p(n5, n6, n2))). % 79.77/37.08 tff(c_21976, plain, (~p(n5, n6, n6))). % 79.87/37.08 tff(c_21969, plain, (~p(n5, n6, n9))). % 79.87/37.08 tff(c_21546, plain, (~p(n3, n4, n9))). % 79.87/37.08 tff(c_22006, plain, (~p(n5, n4, n7))). % 79.87/37.08 tff(c_21998, plain, (~p(n5, n4, n9))). % 79.87/37.08 tff(c_22953, plain, (~p(n5, n3, n1))). % 79.87/37.08 tff(c_22043, plain, (~p(n4, n9, n5))). % 79.87/37.08 tff(c_22948, plain, (~p(n5, n3, n8))). % 79.87/37.08 tff(c_22124, plain, (~p(n4, n1, n7))). % 79.87/37.08 tff(c_22146, plain, (~p(n4, n1, n1))). % 79.87/37.08 tff(c_22160, plain, (~p(n3, n9, n7))). % 79.87/37.08 tff(c_22176, plain, (~p(n3, n9, n2))). % 79.87/37.08 tff(c_22051, plain, (~p(n4, n9, n3))). % 79.87/37.08 tff(c_22180, plain, (~p(n3, n9, n1))). % 79.87/37.08 tff(c_22096, plain, (~p(n4, n4, n6))). % 79.87/37.08 tff(c_22056, plain, (~p(n4, n9, n1))). % 79.87/37.08 tff(c_21532, plain, (~p(n1, n7, n4))). % 79.87/37.08 tff(c_22048, plain, (~p(n4, n9, n4))). % 79.87/37.08 tff(c_22039, plain, (~p(n4, n9, n6))). % 79.87/37.08 tff(c_22035, plain, (~p(n4, n9, n7))). % 79.87/37.08 tff(c_22031, plain, (~p(n4, n9, n8))). % 79.87/37.08 tff(c_22099, plain, (~p(n4, n4, n5))). % 79.87/37.09 tff(c_21357, plain, (~p(n7, n3, n3))). % 79.87/37.09 tff(c_22110, plain, (~p(n4, n4, n2))). % 79.87/37.09 tff(c_22106, plain, (~p(n4, n4, n3))). % 79.87/37.09 tff(c_22084, plain, (~p(n4, n6, n2))). % 79.87/37.09 tff(c_21979, plain, (~p(n5, n6, n5))). % 79.87/37.09 tff(c_22079, plain, (~p(n4, n6, n3))). % 79.87/37.09 tff(c_22072, plain, (~p(n4, n6, n5))). % 79.87/37.09 tff(c_22069, plain, (~p(n4, n6, n7))). % 79.87/37.09 tff(c_22066, plain, (~p(n4, n6, n8))). % 79.87/37.09 tff(c_22061, plain, (~p(n4, n6, n9))). % 79.87/37.09 tff(c_21348, plain, (~p(n8, n2, n6))). % 79.87/37.09 tff(c_22104, plain, (~p(n4, n4, n4))). % 79.87/37.09 tff(c_22089, plain, (~p(n4, n4, n9))). % 79.87/37.09 tff(c_22171, plain, (~p(n3, n9, n3))). % 79.87/37.09 tff(c_21527, plain, (~p(n1, n8, n4))). % 79.87/37.09 tff(c_22166, plain, (~p(n3, n9, n5))). % 79.87/37.09 tff(c_22155, plain, (~p(n3, n9, n8))). % 79.87/37.09 tff(c_22151, plain, (~p(n3, n9, n9))). % 79.87/37.09 tff(c_22142, plain, (~p(n4, n1, n2))). % 79.87/37.09 tff(c_22138, plain, (~p(n4, n1, n3))). % 79.87/37.09 tff(c_21338, plain, (~p(n9, n2, n6))). % 79.87/37.09 tff(c_22133, plain, (~p(n4, n1, n5))). % 79.87/37.09 tff(c_22120, plain, (~p(n4, n1, n8))). % 79.87/37.09 tff(c_22116, plain, (~p(n4, n1, n9))). % 79.87/37.09 tff(c_21522, plain, (~p(n1, n9, n6))). % 79.87/37.09 tff(c_22723, plain, (~p(n9, n4, n9))). % 79.87/37.09 tff(c_22719, plain, (~p(n8, n5, n1))). % 79.87/37.09 tff(c_22209, plain, (~p(n3, n1, n2))). % 79.87/37.09 tff(c_22205, plain, (~p(n3, n1, n3))). % 79.87/37.09 tff(c_22192, plain, (~p(n3, n1, n6))). % 79.87/37.09 tff(c_21512, plain, (~p(n3, n7, n6))). % 79.87/37.09 tff(c_22232, plain, (~p(n2, n8, n5))). % 79.87/37.09 tff(c_22223, plain, (~p(n2, n8, n8))). % 79.87/37.09 tff(c_22473, plain, (~p(n1, n9, n4))). % 79.87/37.09 tff(c_21508, plain, (~p(n2, n8, n4))). % 79.87/37.09 tff(c_22297, plain, (~p(n2, n2, n5))). % 79.87/37.09 tff(c_22272, plain, (~p(n2, n5, n4))). % 79.87/37.09 tff(c_22267, plain, (~p(n2, n5, n5))). % 79.87/37.09 tff(c_22259, plain, (~p(n2, n5, n7))). % 79.87/37.09 tff(c_22302, plain, (~p(n2, n2, n4))). % 79.87/37.09 tff(c_21322, plain, (~p(n8, n2, n8))). % 79.87/37.09 tff(c_22317, plain, (~p(n2, n2, n1))). % 79.87/37.09 tff(c_22312, plain, (~p(n2, n2, n2))). % 79.87/37.09 tff(c_22293, plain, (~p(n2, n2, n6))). % 79.87/37.09 tff(c_21500, plain, (~p(n5, n2, n4))). % 79.87/37.09 tff(c_22288, plain, (~p(n2, n2, n8))). % 79.87/37.09 tff(c_22468, plain, (~p(n1, n9, n2))). % 79.87/37.09 tff(c_22459, plain, (~p(n2, n9, n4))). % 79.87/37.09 tff(c_22463, plain, (~p(n1, n9, n7))). % 79.87/37.09 tff(c_22454, plain, (~p(n2, n9, n2))). % 79.87/37.09 tff(c_21496, plain, (~p(n5, n3, n4))). % 79.87/37.09 tff(c_22450, plain, (~p(n2, n9, n7))). % 79.87/37.09 tff(c_22411, plain, (~p(n7, n9, n2))). % 79.87/37.09 tff(c_22442, plain, (~p(n5, n9, n4))). % 79.87/37.09 tff(c_21942, plain, (~p(n6, n5, n9))). % 79.87/37.09 tff(c_22369, plain, (~p(n1, n4, n5))). % 79.87/37.09 tff(c_22383, plain, (~p(n1, n4, n1))). % 79.87/37.09 tff(c_22374, plain, (~p(n1, n4, n4))). % 79.87/37.09 tff(c_22342, plain, (~p(n1, n6, n4))). % 79.87/37.09 tff(c_22337, plain, (~p(n1, n6, n5))). % 79.87/37.09 tff(c_21959, plain, (~p(n6, n5, n3))). % 79.87/37.09 tff(c_22329, plain, (~p(n1, n6, n7))). % 79.87/37.09 tff(c_22364, plain, (~p(n1, n4, n6))). % 79.87/37.09 tff(c_22360, plain, (~p(n1, n4, n7))). % 79.87/37.09 tff(c_21964, plain, (~p(n6, n5, n2))). % 79.87/37.09 tff(c_22415, plain, (~p(n6, n9, n2))). % 79.87/37.09 tff(c_22437, plain, (~p(n6, n9, n4))). % 79.87/37.09 tff(c_22432, plain, (~p(n7, n9, n4))). % 79.87/37.09 tff(c_22423, plain, (~p(n9, n9, n4))). % 79.87/37.09 tff(c_22419, plain, (~p(n5, n9, n2))). % 79.87/37.09 tff(c_21952, plain, (~p(n6, n5, n5))). % 79.87/37.09 tff(c_22402, plain, (~p(n9, n9, n2))). % 79.87/37.09 tff(c_22398, plain, (~p(n5, n9, n7))). % 79.87/37.09 tff(c_22393, plain, (~p(n6, n9, n7))). % 79.87/37.09 tff(c_21466, plain, (~p(n6, n5, n8))). % 79.87/37.09 tff(c_22386, plain, (~p(n9, n9, n7))). % 79.87/37.09 tff(c_22530, plain, (~p(n6, n7, n9))). % 79.87/37.10 tff(c_22482, plain, (~p(n8, n8, n6))). % 79.87/37.10 tff(c_22505, plain, (~p(n3, n8, n6))). % 79.87/37.10 tff(c_22501, plain, (~p(n4, n8, n6))). % 79.87/37.10 tff(c_21457, plain, (~p(n4, n5, n4))). % 79.87/37.10 tff(c_22496, plain, (~p(n5, n8, n6))). % 79.87/37.10 tff(c_22491, plain, (~p(n6, n8, n6))). % 79.87/37.10 tff(c_22487, plain, (~p(n7, n8, n6))). % 79.87/37.10 tff(c_21461, plain, (~p(n6, n6, n8))). % 79.87/37.10 tff(c_22477, plain, (~p(n9, n8, n6))). % 79.87/37.10 tff(c_21860, plain, (~p(n7, n6, n6))). % 79.87/37.10 tff(c_21868, plain, (~p(n7, n6, n4))). % 79.87/37.10 tff(c_21873, plain, (~p(n7, n6, n3))). % 79.87/37.10 tff(c_23872, plain, (~p(n4, n8, n5))). % 79.87/37.10 tff(c_21474, plain, (~p(n5, n6, n8))). % 79.87/37.10 tff(c_23876, plain, (~p(n5, n9, n5))). % 79.87/37.10 tff(c_21902, plain, (~p(n7, n4, n3))). % 79.87/37.10 tff(c_21906, plain, (~p(n7, n4, n2))). % 79.87/37.10 tff(c_21445, plain, (~p(n5, n4, n6))). % 79.87/37.10 tff(c_23852, plain, (~p(n6, n8, n1))). % 79.87/37.10 tff(c_21909, plain, (~p(n7, n4, n1))). % 79.87/37.10 tff(c_21912, plain, (~p(n7, n3, n9))). % 79.87/37.10 tff(c_21917, plain, (~p(n7, n3, n8))). % 79.87/37.10 tff(c_21920, plain, (~p(n7, n3, n7))). % 79.87/37.10 tff(c_21449, plain, (~p(n4, n6, n4))). % 79.87/37.10 tff(c_21924, plain, (~p(n7, n3, n5))). % 79.87/37.10 tff(c_21929, plain, (~p(n7, n3, n4))). % 79.87/37.10 tff(c_21936, plain, (~p(n7, n3, n2))). % 79.87/37.10 tff(c_21432, plain, (~p(n4, n6, n1))). % 79.87/37.10 tff(c_21940, plain, (~p(n7, n3, n1))). % 79.87/37.10 tff(c_23621, plain, (~p(n8, n8, n9))). % 79.87/37.10 tff(c_23583, plain, (~p(n9, n2, n8))). % 79.87/37.10 tff(c_23613, plain, (~p(n8, n8, n7))). % 79.87/37.10 tff(c_23324, plain, (~p(n8, n8, n8))). % 79.87/37.10 tff(c_21424, plain, (~p(n5, n4, n1))). % 79.87/37.10 tff(c_23529, plain, (~p(n9, n5, n6))). % 79.87/37.10 tff(c_23515, plain, (~p(n9, n8, n3))). % 79.87/37.10 tff(c_23326, plain, (~p(n7, n9, n6))). % 79.87/37.10 tff(c_21435, plain, (~p(n6, n4, n6))). % 79.87/37.10 tff(c_23295, plain, (~p(n2, n6, n9))). % 79.87/37.10 tff(c_23505, plain, (~p(n1, n1, n9))). % 79.87/37.10 tff(c_23500, plain, (~p(n1, n1, n4))). % 79.87/37.10 tff(c_23495, plain, (~p(n1, n1, n5))). % 79.87/37.10 tff(c_23491, plain, (~p(n1, n1, n3))). % 79.87/37.10 tff(c_21428, plain, (~p(n6, n5, n6))). % 79.87/37.10 tff(c_23332, plain, (~p(n9, n9, n8))). % 79.87/37.10 tff(c_23338, plain, (~p(n5, n9, n8))). % 79.87/37.10 tff(c_23328, plain, (~p(n7, n9, n5))). % 79.87/37.10 tff(c_21470, plain, (~p(n4, n4, n1))). % 79.87/37.10 tff(c_23334, plain, (~p(n9, n8, n8))). % 79.87/37.10 tff(c_23476, plain, (~p(n2, n1, n5))). % 79.87/37.10 tff(c_23471, plain, (~p(n2, n1, n3))). % 79.87/37.10 tff(c_23341, plain, (~p(n2, n9, n8))). % 79.87/37.10 tff(c_23414, plain, (~p(n7, n1, n2))). % 79.87/37.10 tff(c_21708, plain, (~p(n8, n9, n5))). % 79.87/37.10 tff(c_23419, plain, (~p(n5, n1, n5))). % 79.87/37.10 tff(c_23417, plain, (~p(n6, n1, n5))). % 79.87/37.10 tff(c_23412, plain, (~p(n7, n1, n6))). % 79.87/37.10 tff(c_21408, plain, (~p(n5, n6, n1))). % 79.87/37.10 tff(c_23410, plain, (~p(n8, n2, n5))). % 79.87/37.10 tff(c_23408, plain, (~p(n9, n2, n5))). % 79.87/37.10 tff(c_23405, plain, (~p(n2, n9, n6))). % 79.87/37.10 tff(c_23401, plain, (~p(n6, n9, n6))). % 79.87/37.10 tff(c_23399, plain, (~p(n9, n9, n3))). % 79.87/37.10 tff(c_21695, plain, (~p(n8, n9, n9))). % 79.87/37.10 tff(c_23403, plain, (~p(n5, n9, n6))). % 79.87/37.10 tff(c_23351, plain, (~p(n6, n7, n6))). % 79.87/37.10 tff(c_23357, plain, (~p(n5, n7, n4))). % 79.87/37.10 tff(c_21667, plain, (~p(n9, n3, n7))). % 79.87/37.10 tff(c_23368, plain, (p(n7, n1, n5))). % 79.87/37.10 tff(c_23361, plain, (~p(n3, n7, n4))). % 79.87/37.10 tff(c_23359, plain, (~p(n4, n7, n4))). % 79.87/37.10 tff(c_23365, plain, (p(n9, n9, n6))). % 79.87/37.10 tff(c_23353, plain, (~p(n6, n7, n5))). % 79.87/37.10 tff(c_21675, plain, (~p(n9, n3, n5))). % 79.87/37.10 tff(c_23349, plain, (~p(n6, n7, n7))). % 79.87/37.10 tff(c_23347, plain, (~p(n6, n7, n8))). % 79.87/37.10 tff(c_23343, plain, (~p(n1, n9, n8))). % 79.87/37.10 tff(c_21687, plain, (~p(n9, n3, n2))). % 79.87/37.10 tff(c_23336, plain, (~p(n6, n9, n8))). % 79.87/37.10 tff(c_23330, plain, (~p(n7, n9, n1))). % 79.87/37.10 tff(c_23299, plain, (p(n7, n9, n8))). % 79.87/37.10 tff(c_22967, plain, (~p(n4, n3, n1))). % 79.87/37.10 tff(c_22981, plain, (~p(n3, n3, n1))). % 79.87/37.10 tff(c_21680, plain, (~p(n9, n3, n4))). % 79.87/37.10 tff(c_22986, plain, (~p(n3, n3, n6))). % 79.87/37.10 tff(c_22958, plain, (~p(n5, n3, n6))). % 79.87/37.10 tff(c_22972, plain, (~p(n4, n3, n6))). % 79.87/37.11 tff(c_21633, plain, (~p(n9, n7, n8))). % 79.87/37.11 tff(c_22939, plain, (~p(n6, n3, n1))). % 79.87/37.11 tff(c_22943, plain, (~p(n6, n3, n6))). % 79.87/37.11 tff(c_22934, plain, (~p(n6, n3, n8))). % 79.87/37.11 tff(c_22918, plain, (~p(n2, n4, n3))). % 79.87/37.11 tff(c_22893, plain, (~p(n8, n4, n3))). % 79.87/37.11 tff(c_21639, plain, (~p(n9, n7, n6))). % 79.87/37.11 tff(c_22914, plain, (~p(n3, n4, n3))). % 79.87/37.11 tff(c_22901, plain, (~p(n6, n4, n3))). % 79.87/37.11 tff(c_22875, plain, (~p(n2, n4, n7))). % 79.87/37.11 tff(c_21625, plain, (~p(n1, n1, n7))). % 79.87/37.11 tff(c_22864, plain, (~p(n3, n4, n4))). % 79.87/37.11 tff(c_22884, plain, (~p(n2, n4, n8))). % 79.87/37.11 tff(c_22859, plain, (~p(n3, n4, n7))). % 79.87/37.11 tff(c_22840, plain, (~p(n8, n4, n8))). % 79.87/37.11 tff(c_22868, plain, (~p(n3, n4, n8))). % 79.87/37.11 tff(c_21644, plain, (~p(n9, n7, n5))). % 79.87/37.11 tff(c_22849, plain, (~p(n6, n4, n8))). % 79.87/37.11 tff(c_22823, plain, (~p(n8, n4, n4))). % 79.87/37.11 tff(c_22832, plain, (~p(n6, n4, n4))). % 79.87/37.11 tff(c_21399, plain, (~p(n5, n7, n2))). % 79.87/37.11 tff(c_22879, plain, (~p(n2, n4, n4))). % 79.87/37.11 tff(c_22814, plain, (~p(n6, n4, n1))). % 79.87/37.11 tff(c_22733, plain, (~p(n9, n4, n4))). % 79.87/37.11 tff(c_22731, plain, (~p(n9, n4, n5))). % 79.87/37.11 tff(c_22729, plain, (~p(n9, n4, n6))). % 79.87/37.11 tff(c_21394, plain, (~p(n5, n8, n2))). % 79.87/37.11 tff(c_22725, plain, (~p(n9, n4, n8))). % 79.87/37.11 tff(c_22727, plain, (~p(n9, n4, n7))). % 79.87/37.11 tff(c_22717, plain, (~p(n7, n5, n1))). % 79.87/37.11 tff(c_21389, plain, (~p(n6, n7, n2))). % 79.87/37.11 tff(c_22721, plain, (~p(n9, n4, n3))). % 79.87/37.11 tff(c_22713, plain, (~p(n9, n5, n1))). % 79.87/37.11 tff(c_22694, plain, (~p(n6, n6, n1))). % 79.87/37.11 tff(c_22709, plain, (~p(n2, n6, n1))). % 79.87/37.11 tff(c_22705, plain, (~p(n3, n6, n1))). % 79.87/37.11 tff(c_21384, plain, (~p(n6, n8, n2))). % 79.87/37.11 tff(c_22670, plain, (~p(n2, n6, n2))). % 79.87/37.11 tff(c_22647, plain, (~p(n6, n6, n6))). % 79.87/37.11 tff(c_22679, plain, (~p(n2, n6, n6))). % 79.87/37.11 tff(c_21615, plain, (~p(n1, n3, n7))). % 79.87/37.11 tff(c_22675, plain, (~p(n2, n6, n7))). % 79.87/37.11 tff(c_22592, plain, (~p(n2, n7, n1))). % 79.87/37.11 tff(c_22509, plain, (~p(n1, n8, n6))). % 79.87/37.11 tff(c_22525, plain, (~p(n6, n7, n3))). % 79.87/37.11 tff(c_22578, plain, (~p(n3, n7, n1))). % 79.87/37.11 tff(c_21598, plain, (~p(n3, n3, n7))). % 79.87/37.11 tff(c_22639, plain, (~p(n8, n6, n6))). % 79.87/37.11 tff(c_22539, plain, (~p(n5, n7, n3))). % 79.87/37.11 tff(c_22535, plain, (~p(n6, n7, n1))). % 79.87/37.11 tff(c_21594, plain, (~p(n2, n3, n9))). % 79.87/37.11 tff(c_22549, plain, (~p(n5, n7, n1))). % 79.87/37.11 tff(c_22544, plain, (~p(n5, n7, n9))). % 79.87/37.11 tff(c_22554, plain, (~p(n4, n7, n3))). % 79.87/37.11 tff(c_22559, plain, (~p(n4, n7, n9))). % 79.87/37.11 tff(c_22574, plain, (~p(n3, n7, n9))). % 79.87/37.11 tff(c_21576, plain, (~p(n3, n5, n3))). % 79.87/37.11 tff(c_22564, plain, (~p(n4, n7, n1))). % 79.87/37.11 tff(c_22569, plain, (~p(n3, n7, n3))). % 79.87/37.11 tff(c_22583, plain, (~p(n2, n7, n3))). % 79.87/37.11 tff(c_21571, plain, (~p(n3, n6, n3))). % 79.87/37.11 tff(c_22588, plain, (~p(n2, n7, n9))). % 79.87/37.11 tff(c_22601, plain, (~p(n1, n7, n9))). % 79.87/37.11 tff(c_22660, plain, (~p(n3, n6, n7))). % 79.87/37.11 tff(c_22597, plain, (~p(n1, n7, n3))). % 79.87/37.11 tff(c_22606, plain, (~p(n1, n7, n1))). % 79.87/37.11 tff(c_21581, plain, (~p(n2, n6, n3))). % 79.87/37.11 tff(c_22665, plain, (~p(n3, n6, n6))). % 79.87/37.11 tff(c_22614, plain, (~p(n8, n6, n2))). % 79.87/37.11 tff(c_22635, plain, (~p(n9, n6, n6))). % 79.87/37.11 tff(c_21563, plain, (~p(n2, n5, n1))). % 79.87/37.11 tff(c_22631, plain, (~p(n6, n6, n7))). % 79.87/37.11 tff(c_22610, plain, (~p(n9, n6, n2))). % 79.87/37.11 tff(c_22618, plain, (~p(n6, n6, n2))). % 79.87/37.11 tff(c_22655, plain, (~p(n3, n6, n2))). % 79.87/37.11 tff(c_22683, plain, (~p(n9, n6, n1))). % 79.87/37.11 tff(c_21380, plain, (~p(n7, n1, n1))). % 79.87/37.11 tff(c_22687, plain, (~p(n8, n6, n1))). % 79.87/37.11 tff(c_22715, plain, (p(n9, n4, n1))). % 79.87/37.11 tff(c_22811, plain, (~p(n8, n4, n7))). % 79.87/37.11 tff(c_21550, plain, (~p(n3, n5, n1))). % 79.87/37.11 tff(c_22804, plain, (~p(n8, n4, n1))). % 79.87/37.11 tff(c_22756, plain, (~p(n5, n5, n1))). % 79.87/37.11 tff(c_22800, plain, (~p(n1, n5, n9))). % 79.87/37.11 tff(c_22760, plain, (~p(n4, n5, n1))). % 79.87/37.11 tff(c_22794, plain, (~p(n3, n5, n9))). % 79.87/37.11 tff(c_21375, plain, (~p(n7, n1, n8))). % 79.87/37.11 tff(c_22789, plain, (~p(n4, n5, n9))). % 79.87/37.11 tff(c_22784, plain, (~p(n5, n5, n9))). % 79.87/37.11 tff(c_22797, plain, (~p(n1, n5, n1))). % 79.87/37.11 tff(c_21542, plain, (~p(n3, n6, n9))). % 79.87/37.11 tff(c_22771, plain, (~p(n8, n5, n9))). % 79.87/37.11 tff(c_22775, plain, (~p(n7, n5, n9))). % 79.87/37.11 tff(c_23149, plain, (p(n6, n4, n9))). % 79.87/37.11 tff(c_22766, plain, (~p(n9, n5, n9))). % 79.87/37.11 tff(c_23140, plain, (p(n6, n6, n3))). % 79.87/37.11 tff(c_21537, plain, (~p(n1, n7, n6))). % 79.87/37.11 tff(c_23116, plain, (~p(n1, n5, n3))). % 79.87/37.11 tff(c_23113, plain, (~p(n4, n5, n3))). % 79.87/37.11 tff(c_23111, plain, (~p(n5, n5, n3))). % 79.87/37.11 tff(c_21361, plain, (~p(n7, n2, n8))). % 79.87/37.11 tff(c_23107, plain, (~p(n9, n5, n3))). % 79.87/37.11 tff(c_23102, plain, (~p(n7, n5, n4))). % 79.87/37.11 tff(c_23098, plain, (~p(n7, n5, n6))). % 79.87/37.11 tff(c_23104, plain, (~p(n7, n5, n2))). % 79.87/37.11 tff(c_23066, plain, (~p(n4, n2, n7))). % 79.87/37.11 tff(c_21353, plain, (~p(n8, n1, n6))). % 79.87/37.11 tff(c_23062, plain, (~p(n5, n2, n7))). % 79.87/37.11 tff(c_23071, plain, (~p(n3, n2, n7))). % 79.87/37.11 tff(c_23096, plain, (~p(n7, n5, n8))). % 79.87/37.11 tff(c_21343, plain, (~p(n9, n1, n6))). % 79.87/37.11 tff(c_23035, plain, (~p(n9, n1, n2))). % 79.87/37.11 tff(c_23057, plain, (~p(n6, n2, n7))). % 79.87/37.11 tff(c_23037, plain, (~p(n8, n2, n7))). % 79.87/37.11 tff(c_23031, plain, (~p(n9, n1, n5))). % 79.87/37.11 tff(c_23033, plain, (~p(n9, n1, n4))). % 79.87/37.11 tff(c_21334, plain, (~p(n9, n2, n3))). % 79.87/37.11 tff(c_23029, plain, (~p(n9, n1, n8))). % 79.87/37.11 tff(c_23027, plain, (~p(n9, n1, n9))). % 79.87/37.11 tff(c_23025, plain, (~p(n9, n1, n3))). % 79.87/37.11 tff(c_21331, plain, (~p(n9, n3, n3))). % 79.87/37.11 tff(c_23023, plain, (~p(n7, n2, n7))). % 79.87/37.11 tff(c_23087, plain, (p(n7, n5, n3))). % 79.87/37.11 tff(c_23021, plain, (p(n9, n1, n7))). % 79.87/37.11 tff(c_23019, plain, (~p(n9, n2, n7))). % 79.87/37.11 tff(c_23086, plain, (~p(n7, n1, n3))). % 79.87/37.11 tff(c_21517, plain, (~p(n2, n7, n4))). % 79.87/37.11 tff(c_23083, plain, (~p(n7, n1, n7))). % 79.87/37.11 tff(c_23075, plain, (~p(n1, n2, n7))). % 79.87/37.11 tff(c_24319, plain, (p(n6, n2, n6))). % 79.87/37.11 tff(c_21504, plain, (~p(n3, n9, n6))). % 79.87/37.11 tff(c_24295, plain, (~p(n3, n8, n8))). % 79.87/37.11 tff(c_24302, plain, (~p(n6, n2, n8))). % 79.87/37.11 tff(c_24307, plain, (p(n6, n1, n2))). % 79.87/37.11 tff(c_24281, plain, (p(n6, n3, n7))). % 79.87/37.11 tff(c_24299, plain, (~p(n1, n8, n8))). % 79.87/37.12 tff(c_21317, plain, (~p(n9, n1, n1))). % 79.87/37.12 tff(c_24304, plain, (~p(n6, n1, n8))). % 79.87/37.12 tff(c_24291, plain, (~p(n2, n3, n7))). % 79.87/37.12 tff(c_24270, plain, (~p(n6, n8, n7))). % 79.87/37.12 tff(c_21312, plain, (~p(n9, n2, n1))). % 79.87/37.12 tff(c_24282, plain, (p(n6, n8, n8))). % 79.87/37.12 tff(c_24289, plain, (~p(n4, n3, n7))). % 79.87/37.12 tff(c_24267, plain, (~p(n1, n7, n7))). % 79.87/37.12 tff(c_24274, plain, (~p(n4, n8, n7))). % 79.87/37.12 tff(c_24287, plain, (~p(n6, n3, n2))). % 79.87/37.12 tff(c_21486, plain, (~p(n6, n3, n4))). % 79.87/37.12 tff(c_24265, plain, (~p(n2, n7, n7))). % 79.87/37.12 tff(c_24259, plain, (p(n4, n7, n7))). % 79.87/37.12 tff(c_24258, plain, (~p(n4, n7, n8))). % 79.87/37.12 tff(c_21308, plain, (~p(n8, n5, n7))). % 79.87/37.12 tff(c_24230, plain, (~p(n3, n6, n4))). % 79.87/37.12 tff(c_24253, plain, (~p(n4, n8, n8))). % 79.87/37.12 tff(c_24226, plain, (~p(n2, n6, n8))). % 79.87/37.12 tff(c_24228, plain, (~p(n2, n6, n5))). % 79.87/37.12 tff(c_24208, plain, (~p(n4, n3, n4))). % 79.87/37.12 tff(c_21305, plain, (~p(n8, n6, n7))). % 79.87/37.12 tff(c_24212, plain, (~p(n2, n3, n4))). % 79.87/37.12 tff(c_24263, plain, (~p(n3, n7, n7))). % 79.87/37.12 tff(c_24224, plain, (p(n2, n6, n4))). % 79.87/37.12 tff(c_21300, plain, (~p(n9, n5, n7))). % 79.87/37.12 tff(c_24204, plain, (~p(n1, n3, n2))). % 79.87/37.12 tff(c_24210, plain, (~p(n3, n3, n4))). % 79.87/37.12 tff(c_24192, plain, (p(n1, n3, n4))). % 79.87/37.12 tff(c_24200, plain, (~p(n1, n3, n5))). % 79.87/37.12 tff(c_24177, plain, (~p(n1, n2, n4))). % 79.87/37.12 tff(c_21491, plain, (~p(n6, n2, n4))). % 79.87/37.12 tff(c_24202, plain, (~p(n1, n3, n3))). % 79.87/37.12 tff(c_24175, plain, (~p(n3, n2, n4))). % 79.87/37.12 tff(c_24173, plain, (~p(n4, n2, n4))). % 79.87/37.12 tff(c_21291, plain, (~p(n8, n4, n2))). % 79.87/37.12 tff(c_24164, plain, (~p(n3, n2, n2))). % 79.87/37.12 tff(c_24166, plain, (~p(n1, n2, n2))). % 79.87/37.12 tff(c_24160, plain, (~p(n6, n2, n2))). % 79.87/37.12 tff(c_24153, plain, (~p(n1, n8, n2))). % 79.87/37.12 tff(c_24156, plain, (~p(n8, n2, n2))). % 79.87/37.12 tff(c_21286, plain, (~p(n8, n5, n2))). % 79.87/37.12 tff(c_24162, plain, (~p(n4, n2, n2))). % 79.87/37.12 tff(c_24151, plain, (~p(n3, n8, n2))). % 79.87/37.12 tff(c_24133, plain, (p(n8, n8, n2))). % 79.87/37.12 tff(c_21452, plain, (~p(n4, n5, n7))). % 79.87/37.12 tff(c_24169, plain, (p(n8, n2, n4))). % 79.87/37.12 tff(c_24122, plain, (~p(n8, n5, n4))). % 79.87/37.12 tff(c_24126, plain, (~p(n1, n5, n4))). % 79.87/37.12 tff(c_24114, plain, (~p(n3, n8, n5))). % 79.87/37.12 tff(c_24120, plain, (~p(n8, n6, n4))). % 79.87/37.12 tff(c_21440, plain, (~p(n5, n5, n6))). % 79.87/37.12 tff(c_24124, plain, (~p(n3, n5, n4))). % 79.87/37.12 tff(c_24130, plain, (~p(n9, n2, n4))). % 79.87/37.12 tff(c_24134, plain, (p(n9, n2, n2))). % 79.87/37.12 tff(c_21420, plain, (~p(n6, n5, n4))). % 79.87/37.12 tff(c_24100, plain, (p(n9, n5, n4))). % 79.87/37.12 tff(c_24112, plain, (~p(n8, n8, n5))). % 79.87/37.12 tff(c_24099, plain, (p(n9, n8, n5))). % 79.87/37.12 tff(c_24110, plain, (~p(n9, n8, n2))). % 79.87/37.12 tff(c_24087, plain, (~p(n9, n5, n5))). % 79.87/37.12 tff(c_21415, plain, (~p(n6, n6, n4))). % 79.87/37.12 tff(c_24116, plain, (~p(n1, n8, n5))). % 79.87/37.12 tff(c_24093, plain, (~p(n1, n5, n5))). % 79.87/37.12 tff(c_24085, plain, (~p(n4, n5, n6))). % 79.87/37.12 tff(c_21411, plain, (~p(n6, n4, n7))). % 79.87/37.12 tff(c_24091, plain, (~p(n3, n5, n5))). % 79.87/37.12 tff(c_24083, plain, (~p(n4, n5, n8))). % 79.87/37.12 tff(c_24071, plain, (p(n4, n5, n5))). % 79.87/37.12 tff(c_24089, plain, (~p(n8, n5, n5))). % 79.87/37.12 tff(c_24068, plain, (~p(n5, n2, n2))). % 79.87/37.12 tff(c_21404, plain, (~p(n6, n5, n7))). % 79.87/37.12 tff(c_24066, plain, (~p(n5, n3, n2))). % 79.87/37.12 tff(c_24070, plain, (~p(n5, n1, n2))). % 79.87/37.12 tff(c_24058, plain, (~p(n5, n5, n5))). % 79.87/37.12 tff(c_21662, plain, (~p(n9, n3, n9))). % 79.87/37.12 tff(c_24060, plain, (~p(n3, n5, n2))). % 79.87/37.12 tff(c_24001, plain, (~p(n5, n5, n4))). % 79.87/37.12 tff(c_24063, plain, (~p(n1, n5, n2))). % 79.87/37.12 tff(c_23983, plain, (~p(n5, n7, n7))). % 79.87/37.12 tff(c_24005, plain, (~p(n5, n3, n7))). % 79.87/37.12 tff(c_21630, plain, (~p(n9, n7, n9))). % 79.87/37.12 tff(c_23978, plain, (~p(n5, n8, n7))). % 79.87/37.12 tff(c_23956, plain, (~p(n6, n2, n1))). % 79.87/37.12 tff(c_23951, plain, (~p(n6, n2, n3))). % 79.87/37.12 tff(c_21272, plain, (~p(n8, n8, n1))). % 79.87/37.12 tff(c_23944, plain, (~p(n6, n2, n5))). % 79.87/37.12 tff(c_23969, plain, (~p(n6, n1, n1))). % 79.87/37.12 tff(c_23940, plain, (~p(n6, n3, n9))). % 79.87/37.12 tff(c_23909, plain, (~p(n6, n8, n9))). % 79.87/37.12 tff(c_23887, plain, (~p(n6, n8, n5))). % 79.87/37.12 tff(c_21269, plain, (~p(n8, n9, n1))). % 79.87/37.12 tff(c_23926, plain, (~p(n6, n3, n5))). % 79.87/37.12 tff(c_23882, plain, (~p(n4, n7, n5))). % 79.87/37.12 tff(c_23933, plain, (~p(n6, n3, n3))). % 79.87/37.12 tff(c_21266, plain, (~p(n7, n7, n7))). % 79.87/37.12 tff(c_23874, plain, (~p(n5, n8, n5))). % 79.87/37.12 tff(c_23878, plain, (~p(n2, n9, n5))). % 79.87/37.12 tff(c_23880, plain, (~p(n1, n9, n5))). % 79.87/37.12 tff(c_23865, plain, (~p(n6, n9, n9))). % 79.87/37.12 tff(c_23868, plain, (p(n6, n9, n5))). % 79.87/37.12 tff(c_21261, plain, (~p(n9, n8, n1))). % 79.87/37.12 tff(c_23870, plain, (~p(n5, n7, n5))). % 79.87/37.12 tff(c_23847, plain, (~p(n6, n9, n1))). % 79.87/37.12 tff(c_23833, plain, (~p(n6, n9, n3))). % 79.87/37.12 tff(c_21256, plain, (~p(n9, n9, n1))). % 79.87/37.12 tff(c_23838, plain, (~p(n6, n8, n3))). % 79.87/37.12 tff(c_23681, plain, (~p(n8, n2, n3))). % 79.87/37.12 tff(c_23567, plain, (~p(n9, n5, n8))). % 79.87/37.12 tff(c_23311, plain, (p(n6, n7, n4))). % 79.87/37.12 tff(c_23291, plain, (~p(n9, n6, n4))). % 79.87/37.12 tff(c_21251, plain, (~p(n7, n8, n9))). % 79.87/37.12 tff(c_23293, plain, (~p(n8, n6, n9))). % 79.87/37.12 tff(c_23289, plain, (~p(n9, n6, n5))). % 79.87/37.12 tff(c_23283, plain, (~p(n4, n8, n4))). % 79.87/37.12 tff(c_21247, plain, (~p(n7, n8, n7))). % 79.87/37.12 tff(c_23287, plain, (~p(n9, n6, n8))). % 79.87/37.12 tff(c_23279, plain, (~p(n6, n8, n4))). % 79.87/37.12 tff(c_23275, plain, (~p(n9, n8, n4))). % 79.87/37.12 tff(c_23277, plain, (~p(n8, n8, n4))). % 79.87/37.12 tff(c_23281, plain, (~p(n5, n8, n4))). % 79.87/37.12 tff(c_21242, plain, (~p(n7, n8, n3))). % 79.87/37.12 tff(c_23272, plain, (~p(n3, n8, n4))). % 79.87/37.12 tff(c_23268, plain, (~p(n7, n8, n5))). % 79.87/37.12 tff(c_23266, plain, (~p(n7, n8, n2))). % 79.87/37.12 tff(c_21370, plain, (~p(n7, n2, n3))). % 79.87/37.12 tff(c_23270, plain, (~p(n7, n8, n1))). % 79.87/37.12 tff(c_23250, plain, (p(n7, n8, n4))). % 79.87/37.12 tff(c_23155, plain, (~p(n6, n4, n5))). % 79.87/37.12 tff(c_23243, plain, (~p(n3, n2, n9))). % 79.87/37.12 tff(c_23144, plain, (~p(n6, n6, n5))). % 79.87/37.12 tff(c_21366, plain, (~p(n7, n2, n1))). % 79.87/37.12 tff(c_23109, plain, (~p(n8, n5, n3))). % 79.87/37.12 tff(c_23090, plain, (~p(n7, n5, n7))). % 79.87/37.12 tff(c_23100, plain, (~p(n7, n5, n5))). % 79.87/37.12 tff(c_21237, plain, (~p(n7, n9, n9))). % 79.87/37.12 tff(c_23092, plain, (~p(n8, n6, n3))). % 79.87/37.12 tff(c_23160, plain, (~p(n8, n4, n9))). % 79.87/37.12 tff(c_23094, plain, (~p(n9, n6, n3))). % 79.87/37.12 tff(c_23174, plain, (~p(n6, n1, n7))). % 79.87/37.12 tff(c_23142, plain, (~p(n6, n6, n9))). % 79.87/37.12 tff(c_21232, plain, (~p(n7, n9, n3))). % 79.87/37.12 tff(c_23157, plain, (~p(n6, n4, n2))). % 79.87/37.12 tff(c_23162, plain, (~p(n2, n4, n9))). % 79.87/37.12 tff(c_23241, plain, (~p(n4, n2, n9))). % 79.87/37.12 tff(c_21327, plain, (~p(n8, n1, n8))). % 79.87/37.12 tff(c_23179, plain, (~p(n6, n1, n3))). % 79.87/37.12 tff(c_23257, plain, (p(n9, n6, n9))). % 79.87/37.12 tff(c_23183, plain, (~p(n5, n1, n7))). % 79.87/37.12 tff(c_23235, plain, (~p(n9, n2, n9))). % 79.87/37.12 tff(c_23264, plain, (~p(n7, n8, n8))). % 79.87/37.12 tff(c_21227, plain, (~p(n9, n8, n9))). % 79.87/37.12 tff(c_23187, plain, (~p(n5, n1, n3))). % 79.87/37.12 tff(c_23232, plain, (~p(n5, n2, n9))). % 79.87/37.12 tff(c_23237, plain, (~p(n8, n2, n9))). % 79.87/37.12 tff(c_21222, plain, (~p(n9, n9, n9))). % 79.87/37.12 tff(c_23230, plain, (~p(n7, n2, n2))). % 79.87/37.12 tff(c_23239, plain, (~p(n6, n2, n9))). % 79.87/37.12 tff(c_23224, plain, (~p(n7, n2, n6))). % 79.87/37.12 tff(c_23228, plain, (~p(n7, n2, n4))). % 79.87/37.12 tff(c_23221, plain, (p(n7, n2, n9))). % 79.87/37.12 tff(c_21218, plain, (~p(n8, n8, n3))). % 79.87/37.12 tff(c_23200, plain, (~p(n7, n1, n4))). % 79.87/37.12 tff(c_23226, plain, (~p(n7, n2, n5))). % 79.87/37.13 tff(c_23220, plain, (~p(n7, n1, n9))). % 79.87/37.13 tff(c_21296, plain, (~p(n9, n6, n7))). % 79.87/37.13 tff(c_23205, plain, (~p(n6, n1, n4))). % 79.87/37.13 tff(c_23209, plain, (~p(n5, n1, n4))). % 79.87/37.13 tff(c_23397, plain, (~p(n9, n9, n5))). % 79.87/37.13 tff(c_23486, plain, (~p(n2, n1, n9))). % 80.08/37.13 tff(c_23481, plain, (~p(n2, n1, n4))). % 80.08/37.13 tff(c_21215, plain, (~p(n8, n9, n3))). % 80.08/37.13 tff(c_23468, plain, (~p(n2, n1, n7))). % 80.08/37.13 tff(c_23657, plain, (~p(n8, n2, n1))). % 80.08/37.13 tff(c_23459, plain, (~p(n5, n1, n9))). % 80.08/37.13 tff(c_21211, plain, (~p(n9, n7, n7))). % 80.08/37.13 tff(c_23455, plain, (~p(n6, n1, n9))). % 80.08/37.13 tff(c_23988, plain, (~p(n5, n5, n7))). % 80.08/37.13 tff(c_24056, plain, (p(n5, n5, n2))). % 80.08/37.13 tff(c_24044, plain, (~p(n5, n1, n6))). % 80.08/37.13 tff(c_24042, plain, (~p(n5, n2, n6))). % 80.08/37.13 tff(c_21206, plain, (~p(n9, n8, n7))). % 80.08/37.13 tff(c_24054, plain, (~p(n4, n5, n2))). % 80.08/37.13 tff(c_24038, plain, (~p(n2, n7, n6))). % 80.08/37.13 tff(c_24033, plain, (p(n5, n7, n6))). % 80.08/37.13 tff(c_21281, plain, (~p(n9, n4, n2))). % 80.08/37.13 tff(c_24036, plain, (~p(n5, n7, n8))). % 80.08/37.13 tff(c_24022, plain, (~p(n4, n7, n2))). % 80.08/37.13 tff(c_24019, plain, (~p(n4, n8, n2))). % 80.08/37.13 tff(c_24032, plain, (~p(n4, n7, n6))). % 80.08/37.13 tff(c_24297, plain, (~p(n5, n8, n8))). % 80.08/37.13 tff(c_21276, plain, (~p(n9, n5, n2))). % 80.08/37.13 tff(c_24323, plain, (~p(n6, n1, n6))). % 80.08/37.13 tff(c_24325, plain, (~p(n4, n3, n2))). % 80.08/37.13 tff(c_24327, plain, (~p(n2, n1, n2))). % 80.08/37.13 tff(c_24780, plain, (~p(n5, n2, n3))). % 80.08/37.13 tff(c_24329, plain, (~p(n1, n1, n2))). % 80.08/37.13 tff(c_24333, plain, (~p(n4, n2, n6))). % 80.08/37.13 tff(c_24335, plain, (~p(n3, n2, n6))). % 80.08/37.13 tff(c_24337, plain, (~p(n1, n2, n6))). % 80.08/37.13 tff(c_24350, plain, (p(n1, n7, n2))). % 80.08/37.13 tff(c_24763, plain, (~p(n5, n1, n8))). % 80.08/37.13 tff(c_24359, plain, (~p(n1, n7, n8))). % 80.08/37.13 tff(c_24361, plain, (~p(n1, n7, n5))). % 80.08/37.13 tff(c_24363, plain, (~p(n3, n7, n2))). % 80.08/37.13 tff(c_24730, plain, (~p(n2, n3, n2))). % 80.08/37.13 tff(c_24365, plain, (~p(n2, n7, n2))). % 80.08/37.13 tff(c_24372, plain, (p(n1, n2, n5))). % 80.08/37.13 tff(c_24378, plain, (~p(n1, n2, n3))). % 80.08/37.13 tff(c_24380, plain, (~p(n1, n2, n1))). % 80.08/37.13 tff(c_24382, plain, (~p(n5, n2, n5))). % 80.08/37.13 tff(c_24682, plain, (~p(n3, n4, n5))). % 80.08/37.13 tff(c_24384, plain, (~p(n4, n2, n5))). % 80.08/37.13 tff(c_24386, plain, (~p(n3, n2, n5))). % 80.08/37.13 tff(c_24390, plain, (~p(n1, n2, n8))). % 80.08/37.13 tff(c_24680, plain, (~p(n3, n7, n5))). % 80.08/37.13 tff(c_24392, plain, (~p(n3, n3, n5))). % 80.08/37.13 tff(c_24394, plain, (~p(n2, n3, n5))). % 80.08/37.13 tff(c_24400, plain, (p(n5, n3, n5))). % 80.08/37.13 tff(c_24413, plain, (~p(n4, n3, n5))). % 80.08/37.13 tff(c_24416, plain, (~p(n5, n3, n3))). % 80.08/37.13 tff(c_24646, plain, (~p(n3, n5, n6))). % 80.08/37.13 tff(c_24418, plain, (~p(n5, n3, n9))). % 80.08/37.13 tff(c_24427, plain, (p(n4, n3, n9))). % 80.08/37.13 tff(c_24429, plain, (~p(n3, n3, n9))). % 80.08/37.13 tff(c_24628, plain, (~p(n8, n5, n8))). % 80.08/37.13 tff(c_24432, plain, (~p(n4, n3, n3))). % 80.08/37.13 tff(c_24453, plain, (~p(n4, n8, n9))). % 80.08/37.13 tff(c_24481, plain, (~p(n4, n2, n8))). % 80.08/37.13 tff(c_24533, plain, (~p(n3, n8, n9))). % 80.08/37.13 tff(c_24561, plain, (~p(n2, n9, n9))). % 80.08/37.13 tff(c_24575, plain, (~p(n2, n4, n6))). % 80.08/37.13 tff(c_21076, plain, (p(n4, n1, n4))). % 80.08/37.13 tff(c_24609, plain, (~p(n2, n1, n6))). % 80.08/37.13 tff(c_24610, plain, (p(n1, n1, n6))). % 80.08/37.13 tff(c_21078, plain, (p(n4, n4, n8))). % 80.08/37.13 tff(c_24613, plain, (~p(n1, n1, n8))). % 80.08/37.13 tff(c_24615, plain, (~p(n1, n1, n1))). % 80.08/37.13 tff(c_24620, plain, (p(n1, n5, n8))). % 80.08/37.13 tff(c_24624, plain, (~p(n1, n5, n7))). % 80.08/37.13 tff(c_24626, plain, (~p(n1, n5, n6))). % 80.08/37.13 tff(c_21080, plain, (p(n4, n6, n6))). % 80.08/37.13 tff(c_21074, plain, (p(n3, n9, n4))). % 80.08/37.13 tff(c_24630, plain, (~p(n3, n5, n8))). % 80.08/37.13 tff(c_24632, plain, (~p(n3, n6, n8))). % 80.08/37.13 tff(c_21082, plain, (p(n4, n9, n2))). % 80.08/37.13 tff(c_24636, plain, (p(n3, n5, n7))). % 80.08/37.13 tff(c_24637, plain, (p(n1, n8, n7))). % 80.08/37.13 tff(c_24639, plain, (p(n8, n6, n8))). % 80.08/37.13 tff(c_24640, plain, (p(n8, n5, n6))). % 80.08/37.13 tff(c_24644, plain, (p(n3, n6, n5))). % 80.08/37.13 tff(c_21084, plain, (p(n5, n4, n4))). % 80.08/37.13 tff(c_21072, plain, (p(n3, n1, n9))). % 80.08/37.13 tff(c_24649, plain, (~p(n3, n8, n7))). % 80.08/37.13 tff(c_24651, plain, (~p(n1, n8, n3))). % 80.08/37.13 tff(c_21086, plain, (p(n5, n6, n7))). % 80.08/37.13 tff(c_24655, plain, (~p(n1, n8, n1))). % 80.08/37.13 tff(c_24657, plain, (~p(n1, n8, n9))). % 80.08/37.13 tff(c_24662, plain, (~p(n8, n6, n5))). % 80.08/37.13 tff(c_24667, plain, (~p(n8, n4, n6))). % 80.08/37.13 tff(c_24675, plain, (~p(n2, n4, n5))). % 80.08/37.13 tff(c_21088, plain, (p(n6, n5, n1))). % 80.08/37.13 tff(c_21070, plain, (p(n2, n8, n6))). % 80.08/37.13 tff(c_24698, plain, (p(n3, n7, n8))). % 80.08/37.13 tff(c_24683, plain, (p(n3, n4, n6))). % 80.08/37.13 tff(c_21090, plain, (p(n7, n3, n6))). % 80.08/37.13 tff(c_24689, plain, (p(n1, n9, n9))). % 80.08/37.13 tff(c_24690, plain, (p(n5, n8, n9))). % 80.08/37.13 tff(c_24691, plain, (p(n8, n4, n5))). % 80.08/37.13 tff(c_24695, plain, (p(n2, n7, n5))). % 80.08/37.13 tff(c_24696, plain, (p(n2, n4, n2))). % 80.08/37.13 tff(c_21092, plain, (p(n7, n4, n7))). % 80.08/37.13 tff(c_21068, plain, (p(n2, n5, n9))). % 80.08/37.13 tff(c_24701, plain, (~p(n3, n4, n2))). % 80.08/37.13 tff(c_24703, plain, (~p(n1, n9, n3))). % 80.08/37.13 tff(c_21094, plain, (p(n7, n6, n2))). % 80.08/37.13 tff(c_24705, plain, (~p(n1, n9, n1))). % 80.08/37.13 tff(c_24707, plain, (~p(n5, n9, n9))). % 80.08/37.13 tff(c_24713, plain, (~p(n5, n8, n1))). % 80.08/37.13 tff(c_24715, plain, (~p(n5, n8, n3))). % 80.08/37.13 tff(c_24723, plain, (~p(n2, n7, n8))). % 80.08/37.13 tff(c_21096, plain, (p(n7, n7, n1))). % 80.08/37.13 tff(c_21066, plain, (p(n2, n2, n7))). % 80.08/37.13 tff(c_24736, plain, (~p(n3, n2, n8))). % 80.08/37.13 tff(c_24739, plain, (p(n3, n3, n2))). % 80.08/37.13 tff(c_21098, plain, (p(n8, n1, n3))). % 80.08/37.13 tff(c_24751, plain, (p(n2, n1, n8))). % 80.08/37.13 tff(c_24753, plain, (p(n2, n3, n3))). % 80.08/37.13 tff(c_24755, plain, (p(n5, n2, n8))). % 80.08/37.13 tff(c_24758, plain, (~p(n3, n3, n3))). % 80.08/37.13 tff(c_24761, plain, (~p(n2, n1, n1))). % 80.08/37.13 tff(c_21100, plain, (p(n8, n3, n1))). % 80.08/37.13 tff(c_21064, plain, (p(n1, n6, n1))). % 80.08/37.13 tff(c_24770, plain, (~p(n3, n2, n3))). % 80.08/37.13 tff(c_24774, plain, (~p(n2, n9, n3))). % 80.08/37.13 tff(c_21102, plain, (p(n8, n7, n9))). % 80.08/37.13 tff(c_24776, plain, (~p(n5, n2, n1))). % 80.08/37.13 tff(c_24787, plain, (p(n3, n2, n1))). % 80.08/37.13 tff(c_24798, plain, (p(n3, n8, n3))). % 80.08/37.13 tff(c_24785, plain, (p(n2, n9, n1))). % 80.08/37.13 tff(c_24786, plain, (p(n5, n1, n1))). % 80.08/37.13 tff(c_21104, plain, (p(n8, n9, n7))). % 80.08/37.13 tff(c_21062, plain, (p(n1, n4, n3))). % 80.08/37.13 tff(c_24791, plain, (p(n5, n9, n3))). % 80.08/37.13 tff(c_24796, plain, (p(n4, n2, n3))). % 80.08/37.13 tff(c_21106, plain, (p(n9, n3, n8))). % 80.08/37.13 tff(c_24800, plain, (~p(n4, n8, n3))). % 80.08/37.13 tff(c_24802, plain, (~p(n3, n8, n1))). % 80.08/37.13 tff(c_24806, plain, (~p(n5, n9, n1))). % 80.08/37.13 tff(c_24812, plain, (~p(n4, n2, n1))). % 80.08/37.13 tff(c_24840, plain, (p(n4, n8, n1))). % 80.08/37.13 tff(c_21108, plain, (p(n9, n7, n3))). % 80.08/37.13 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 80.08/37.13 %------------------------------------------------------------------------------