%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ079+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n024.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 68.25s 39.56s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PUZ079+2 : TPTP v9.0.0. Bugfixed v5.4.0. % 0.10/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.10/0.32 % Computer : n024.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Tue Apr 8 17:23:21 EDT 2025 % 0.10/0.32 % CPUTime : % 68.25/39.56 % 68.25/39.56 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.25/39.56 % 68.25/39.56 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.25/39.58 %$ p > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n3 > n2 > n1 % 68.25/39.58 % 68.25/39.58 %Foreground sorts: % 68.25/39.58 % 68.25/39.58 % 68.25/39.58 %Background operators: % 68.25/39.58 % 68.25/39.58 % 68.25/39.58 %Foreground operators: % 68.25/39.58 tff(n8, type, n8: $i). % 68.25/39.58 tff(n9, type, n9: $i). % 68.25/39.58 tff(n3, type, n3: $i). % 68.25/39.58 tff(n1, type, n1: $i). % 68.25/39.58 tff(n7, type, n7: $i). % 68.25/39.58 tff(n6, type, n6: $i). % 68.25/39.58 tff(n4, type, n4: $i). % 68.25/39.58 tff(p, type, p: ($i * $i * $i) > $o). % 68.25/39.58 tff(n2, type, n2: $i). % 68.25/39.58 tff(n5, type, n5: $i). % 68.25/39.58 % 68.25/39.58 %Saturated clause set: % 68.25/39.58 tff(c_21686, plain, (~p(n9, n9, n8))). % 68.25/39.58 tff(c_21673, plain, (~p(n2, n3, n1))). % 68.25/39.58 tff(c_21710, plain, (~p(n9, n9, n1))). % 68.25/39.58 tff(c_21678, plain, (~p(n2, n2, n1))). % 68.25/39.58 tff(c_21663, plain, (~p(n1, n1, n4))). % 68.25/39.58 tff(c_21410, plain, (~p(n6, n8, n3))). % 68.25/39.58 tff(c_21406, plain, (~p(n4, n9, n6))). % 68.25/39.58 tff(c_21669, plain, (~p(n3, n2, n1))). % 68.25/39.58 tff(c_22369, plain, (~p(n2, n4, n2))). % 68.25/39.58 tff(c_21665, plain, (~p(n3, n3, n1))). % 68.25/39.58 tff(c_21434, plain, (~p(n6, n9, n5))). % 68.25/39.58 tff(c_21430, plain, (~p(n4, n8, n8))). % 68.25/39.58 tff(c_22359, plain, (~p(n2, n4, n6))). % 68.25/39.58 tff(c_21426, plain, (~p(n4, n9, n1))). % 68.25/39.58 tff(c_21438, plain, (~p(n6, n7, n5))). % 68.25/39.58 tff(c_21682, plain, (~p(n9, n9, n9))). % 68.25/39.58 tff(c_21454, plain, (~p(n4, n7, n8))). % 68.25/39.58 tff(c_21450, plain, (~p(n4, n8, n1))). % 68.25/39.58 tff(c_22374, plain, (~p(n2, n4, n1))). % 68.25/39.58 tff(c_21690, plain, (~p(n9, n9, n7))). % 68.25/39.58 tff(c_21695, plain, (~p(n9, n9, n6))). % 68.25/39.58 tff(c_21699, plain, (~p(n9, n9, n5))). % 68.25/39.58 tff(c_21638, plain, (~p(n1, n4, n7))). % 68.25/39.58 tff(c_21704, plain, (~p(n9, n9, n3))). % 68.25/39.58 tff(c_21737, plain, (~p(n9, n6, n1))). % 68.25/39.58 tff(c_21733, plain, (~p(n9, n6, n2))). % 68.25/39.58 tff(c_21727, plain, (~p(n9, n6, n4))). % 68.25/39.58 tff(c_21716, plain, (~p(n9, n6, n8))). % 68.25/39.58 tff(c_21628, plain, (~p(n3, n6, n6))). % 68.25/39.58 tff(c_21721, plain, (~p(n9, n6, n7))). % 68.25/39.59 tff(c_21730, plain, (~p(n9, n6, n3))). % 68.25/39.59 tff(c_21757, plain, (~p(n9, n4, n4))). % 68.25/39.59 tff(c_21634, plain, (~p(n3, n5, n6))). % 68.25/39.59 tff(c_21748, plain, (~p(n9, n4, n7))). % 68.25/39.59 tff(c_21743, plain, (~p(n9, n4, n8))). % 68.25/39.59 tff(c_21753, plain, (~p(n9, n4, n6))). % 68.25/39.59 tff(c_21763, plain, (~p(n9, n4, n2))). % 68.25/39.59 tff(c_21795, plain, (~p(n9, n1, n1))). % 68.25/39.59 tff(c_21642, plain, (~p(n2, n6, n6))). % 68.25/39.59 tff(c_21790, plain, (~p(n9, n1, n3))). % 68.25/39.59 tff(c_21787, plain, (~p(n9, n1, n4))). % 68.25/39.59 tff(c_21778, plain, (~p(n9, n1, n6))). % 68.25/39.59 tff(c_21611, plain, (~p(n1, n6, n5))). % 68.25/39.59 tff(c_21845, plain, (~p(n8, n4, n3))). % 68.25/39.59 tff(c_21819, plain, (~p(n8, n6, n2))). % 68.25/39.59 tff(c_21810, plain, (~p(n8, n6, n6))). % 68.25/39.59 tff(c_21815, plain, (~p(n8, n6, n4))). % 68.25/39.59 tff(c_21806, plain, (~p(n8, n6, n7))). % 68.25/39.59 tff(c_21615, plain, (~p(n2, n4, n4))). % 68.25/39.59 tff(c_21801, plain, (~p(n8, n6, n8))). % 68.25/39.59 tff(c_21798, plain, (~p(n8, n6, n9))). % 68.25/39.59 tff(c_21840, plain, (~p(n8, n4, n4))). % 68.25/39.59 tff(c_21594, plain, (~p(n3, n5, n5))). % 68.25/39.59 tff(c_21826, plain, (~p(n8, n4, n8))). % 68.25/39.59 tff(c_21831, plain, (~p(n8, n4, n7))). % 68.25/39.59 tff(c_21848, plain, (~p(n8, n4, n2))). % 68.25/39.59 tff(c_21853, plain, (~p(n8, n4, n1))). % 68.25/39.59 tff(c_21988, plain, (~p(n6, n8, n5))). % 68.25/39.59 tff(c_22208, plain, (~p(n4, n1, n6))). % 68.25/39.59 tff(c_21976, plain, (~p(n6, n8, n9))). % 68.25/39.59 tff(c_21983, plain, (~p(n6, n8, n7))). % 68.25/39.59 tff(c_21980, plain, (~p(n6, n8, n8))). % 68.25/39.59 tff(c_21645, plain, (~p(n2, n5, n6))). % 68.25/39.59 tff(c_21938, plain, (~p(n7, n3, n3))). % 68.25/39.59 tff(c_21930, plain, (~p(n7, n3, n5))). % 68.25/39.59 tff(c_21925, plain, (~p(n7, n3, n6))). % 68.25/39.59 tff(c_21896, plain, (~p(n7, n5, n7))). % 68.25/39.59 tff(c_21885, plain, (~p(n7, n7, n1))). % 68.25/39.59 tff(c_22184, plain, (~p(n4, n2, n4))). % 68.25/39.59 tff(c_21534, plain, (~p(n4, n1, n3))). % 68.25/39.59 tff(c_21537, plain, (~p(n5, n2, n4))). % 68.25/39.59 tff(c_21902, plain, (~p(n7, n5, n4))). % 68.25/39.59 tff(c_22197, plain, (~p(n4, n1, n9))). % 68.25/39.59 tff(c_21875, plain, (~p(n7, n7, n5))). % 68.25/39.59 tff(c_21880, plain, (~p(n7, n7, n3))). % 68.25/39.59 tff(c_21870, plain, (~p(n7, n7, n6))). % 68.25/39.59 tff(c_21866, plain, (~p(n7, n7, n7))). % 68.25/39.59 tff(c_21861, plain, (~p(n7, n7, n8))). % 68.25/39.59 tff(c_22313, plain, (~p(n3, n3, n2))). % 68.25/39.59 tff(c_21856, plain, (~p(n7, n7, n9))). % 68.25/39.59 tff(c_21891, plain, (~p(n7, n5, n8))). % 68.25/39.59 tff(c_21909, plain, (~p(n7, n5, n2))). % 68.25/39.59 tff(c_22242, plain, (~p(n3, n7, n4))). % 68.25/39.59 tff(c_21920, plain, (~p(n7, n3, n8))). % 68.25/39.59 tff(c_21915, plain, (~p(n7, n3, n9))). % 68.25/39.59 tff(c_21966, plain, (~p(n6, n9, n3))). % 68.25/39.59 tff(c_21962, plain, (~p(n6, n9, n4))). % 68.25/39.59 tff(c_21969, plain, (~p(n6, n9, n2))). % 68.25/39.59 tff(c_22114, plain, (~p(n4, n9, n9))). % 68.25/39.59 tff(c_21957, plain, (~p(n6, n9, n6))). % 68.25/39.59 tff(c_21952, plain, (~p(n6, n9, n7))). % 68.25/39.59 tff(c_21949, plain, (~p(n6, n9, n9))). % 68.25/39.59 tff(c_22121, plain, (~p(n4, n9, n7))). % 68.25/39.59 tff(c_22880, plain, (~p(n5, n5, n5))). % 68.25/39.59 tff(c_22075, plain, (~p(n5, n7, n4))). % 68.25/39.59 tff(c_22082, plain, (~p(n5, n7, n2))). % 68.25/39.59 tff(c_22033, plain, (~p(n6, n1, n8))). % 68.25/39.59 tff(c_22039, plain, (~p(n6, n1, n6))). % 68.25/39.59 tff(c_22133, plain, (~p(n4, n9, n2))). % 68.25/39.59 tff(c_22053, plain, (~p(n6, n1, n2))). % 68.25/39.59 tff(c_22057, plain, (~p(n6, n1, n1))). % 68.25/39.59 tff(c_22048, plain, (~p(n6, n1, n4))). % 68.25/39.59 tff(c_21366, plain, (~p(n7, n3, n2))). % 68.25/39.59 tff(c_22043, plain, (~p(n6, n1, n5))). % 68.25/39.59 tff(c_22028, plain, (~p(n6, n2, n2))). % 68.25/39.59 tff(c_22019, plain, (~p(n6, n2, n5))). % 68.25/39.59 tff(c_22012, plain, (~p(n6, n2, n7))). % 68.25/39.59 tff(c_22008, plain, (~p(n6, n2, n8))). % 68.25/39.59 tff(c_21570, plain, (~p(n1, n8, n5))). % 68.25/39.59 tff(c_22066, plain, (~p(n5, n7, n7))). % 68.25/39.59 tff(c_22778, plain, (~p(n5, n6, n6))). % 68.25/39.59 tff(c_22744, plain, (~p(n1, n7, n2))). % 68.25/39.59 tff(c_21369, plain, (~p(n8, n2, n7))). % 68.25/39.59 tff(c_22749, plain, (~p(n1, n7, n1))). % 68.25/39.59 tff(c_22296, plain, (~p(n3, n3, n7))). % 68.25/39.59 tff(c_22161, plain, (~p(n4, n8, n2))). % 68.25/39.59 tff(c_22158, plain, (~p(n4, n8, n3))). % 68.25/39.59 tff(c_22154, plain, (~p(n4, n8, n4))). % 68.25/39.59 tff(c_21556, plain, (~p(n1, n9, n5))). % 68.25/39.59 tff(c_22107, plain, (~p(n5, n3, n2))). % 68.25/39.59 tff(c_22095, plain, (~p(n5, n3, n6))). % 68.25/39.60 tff(c_22100, plain, (~p(n5, n3, n5))). % 68.25/39.60 tff(c_21560, plain, (~p(n2, n8, n9))). % 68.25/39.60 tff(c_22088, plain, (~p(n5, n3, n8))). % 68.25/39.60 tff(c_22151, plain, (~p(n4, n8, n6))). % 68.25/39.60 tff(c_22147, plain, (~p(n4, n8, n7))). % 68.25/39.60 tff(c_22140, plain, (~p(n4, n8, n9))). % 68.25/39.60 tff(c_22130, plain, (~p(n4, n9, n4))). % 68.25/39.60 tff(c_22059, plain, (~p(n5, n7, n9))). % 68.25/39.60 tff(c_22127, plain, (~p(n4, n9, n5))). % 68.25/39.60 tff(c_22118, plain, (~p(n4, n9, n8))). % 68.25/39.60 tff(c_22305, plain, (~p(n3, n3, n5))). % 68.25/39.60 tff(c_22005, plain, (~p(n6, n2, n9))). % 68.25/39.60 tff(c_22259, plain, (~p(n3, n5, n8))). % 68.25/39.60 tff(c_22277, plain, (~p(n3, n5, n2))). % 68.25/39.60 tff(c_22272, plain, (~p(n3, n5, n3))). % 68.25/39.60 tff(c_22282, plain, (~p(n3, n5, n1))). % 68.25/39.60 tff(c_22309, plain, (~p(n3, n3, n3))). % 68.25/39.60 tff(c_22015, plain, (~p(n6, n2, n6))). % 68.25/39.60 tff(c_22180, plain, (~p(n4, n2, n5))). % 68.25/39.60 tff(c_22205, plain, (~p(n4, n1, n7))). % 68.25/39.60 tff(c_22200, plain, (~p(n4, n1, n8))). % 68.25/39.60 tff(c_21531, plain, (~p(n5, n3, n4))). % 68.25/39.60 tff(c_22219, plain, (~p(n4, n1, n2))). % 68.25/39.60 tff(c_22213, plain, (~p(n4, n1, n5))). % 68.25/39.60 tff(c_22194, plain, (~p(n4, n2, n1))). % 68.25/39.60 tff(c_22189, plain, (~p(n4, n2, n2))). % 68.25/39.60 tff(c_22175, plain, (~p(n4, n2, n6))). % 68.25/39.60 tff(c_21524, plain, (~p(n6, n2, n4))). % 68.25/39.60 tff(c_22170, plain, (~p(n4, n2, n8))). % 68.25/39.60 tff(c_22300, plain, (~p(n3, n3, n6))). % 68.25/39.60 tff(c_22251, plain, (~p(n3, n7, n2))). % 68.25/39.60 tff(c_21512, plain, (~p(n4, n2, n3))). % 68.25/39.60 tff(c_22255, plain, (~p(n3, n7, n1))). % 68.25/39.60 tff(c_22246, plain, (~p(n3, n7, n3))). % 68.25/39.60 tff(c_22237, plain, (~p(n3, n7, n6))). % 68.25/39.60 tff(c_22232, plain, (~p(n3, n7, n7))). % 68.25/39.60 tff(c_22227, plain, (~p(n3, n7, n8))). % 68.25/39.60 tff(c_21515, plain, (~p(n5, n1, n7))). % 68.25/39.60 tff(c_22291, plain, (~p(n3, n3, n8))). % 68.25/39.60 tff(c_22287, plain, (~p(n3, n3, n9))). % 68.25/39.60 tff(c_22603, plain, (~p(n3, n9, n9))). % 68.25/39.60 tff(c_21501, plain, (~p(n4, n2, n9))). % 68.25/39.60 tff(c_22585, plain, (~p(n7, n9, n9))). % 68.25/39.60 tff(c_22606, plain, (~p(n2, n9, n9))). % 68.46/39.60 tff(c_22619, plain, (~p(n7, n8, n6))). % 68.46/39.60 tff(c_22445, plain, (~p(n1, n4, n5))). % 68.46/39.60 tff(c_22448, plain, (~p(n1, n4, n4))). % 68.46/39.60 tff(c_21505, plain, (~p(n6, n1, n7))). % 68.46/39.60 tff(c_22356, plain, (~p(n2, n4, n7))). % 68.46/39.60 tff(c_22364, plain, (~p(n2, n4, n3))). % 68.46/39.60 tff(c_22329, plain, (~p(n2, n6, n5))). % 68.46/39.60 tff(c_21520, plain, (~p(n6, n3, n4))). % 68.46/39.60 tff(c_22335, plain, (~p(n2, n6, n3))). % 68.46/39.60 tff(c_22344, plain, (~p(n2, n6, n1))). % 68.46/39.60 tff(c_22339, plain, (~p(n2, n6, n2))). % 68.46/39.60 tff(c_22332, plain, (~p(n2, n6, n4))). % 68.46/39.60 tff(c_22322, plain, (~p(n2, n6, n8))). % 68.46/39.60 tff(c_21492, plain, (~p(n4, n3, n9))). % 68.46/39.60 tff(c_22351, plain, (~p(n2, n4, n8))). % 68.46/39.60 tff(c_22456, plain, (~p(n1, n4, n2))). % 68.46/39.60 tff(c_22461, plain, (~p(n1, n4, n1))). % 68.46/39.60 tff(c_21528, plain, (~p(n4, n1, n1))). % 68.46/39.60 tff(c_22387, plain, (~p(n1, n9, n6))). % 68.46/39.60 tff(c_22400, plain, (~p(n1, n9, n2))). % 68.46/39.60 tff(c_22405, plain, (~p(n1, n9, n1))). % 68.46/39.60 tff(c_22396, plain, (~p(n1, n9, n3))). % 68.46/39.60 tff(c_22393, plain, (~p(n1, n9, n4))). % 68.46/39.60 tff(c_21339, plain, (~p(n7, n4, n6))). % 68.46/39.60 tff(c_22382, plain, (~p(n1, n9, n7))). % 68.46/39.60 tff(c_22378, plain, (~p(n1, n9, n8))). % 68.46/39.60 tff(c_22419, plain, (~p(n1, n6, n6))). % 68.46/39.60 tff(c_21336, plain, (~p(n8, n4, n5))). % 68.46/39.60 tff(c_22416, plain, (~p(n1, n6, n7))). % 68.46/39.60 tff(c_22427, plain, (~p(n1, n6, n2))). % 68.46/39.60 tff(c_22432, plain, (~p(n1, n6, n1))). % 68.46/39.60 tff(c_22423, plain, (~p(n1, n6, n3))). % 68.46/39.60 tff(c_22411, plain, (~p(n1, n6, n8))). % 68.46/39.60 tff(c_21333, plain, (~p(n7, n5, n9))). % 68.46/39.60 tff(c_22451, plain, (~p(n1, n4, n3))). % 68.46/39.60 tff(c_22438, plain, (~p(n1, n4, n8))). % 68.46/39.60 tff(c_22497, plain, (~p(n8, n9, n4))). % 68.46/39.60 tff(c_21321, plain, (~p(n7, n5, n1))). % 68.46/39.60 tff(c_22472, plain, (~p(n1, n1, n7))). % 68.46/39.60 tff(c_22501, plain, (~p(n7, n9, n4))). % 68.46/39.60 tff(c_22493, plain, (~p(n1, n1, n2))). % 68.46/39.60 tff(c_22488, plain, (~p(n1, n1, n3))). % 68.46/39.60 tff(c_22481, plain, (~p(n1, n1, n5))). % 68.46/39.60 tff(c_21471, plain, (~p(n5, n3, n9))). % 68.46/39.60 tff(c_22477, plain, (~p(n1, n1, n6))). % 68.46/39.60 tff(c_22467, plain, (~p(n1, n1, n8))). % 68.46/39.60 tff(c_22464, plain, (~p(n1, n1, n9))). % 68.46/39.60 tff(c_21464, plain, (~p(n6, n2, n3))). % 68.46/39.60 tff(c_23228, plain, (~p(n8, n1, n9))). % 68.46/39.60 tff(c_23300, plain, (~p(n5, n4, n4))). % 68.46/39.60 tff(c_23323, plain, (~p(n9, n5, n1))). % 68.46/39.60 tff(c_23319, plain, (~p(n9, n5, n8))). % 68.46/39.60 tff(c_23325, plain, (~p(n6, n5, n7))). % 68.46/39.60 tff(c_21475, plain, (~p(n6, n1, n3))). % 68.46/39.60 tff(c_23507, plain, (~p(n6, n3, n1))). % 68.46/39.60 tff(c_23505, plain, (~p(n8, n3, n5))). % 68.46/39.60 tff(c_23510, plain, (~p(n1, n3, n1))). % 68.46/39.61 tff(c_21314, plain, (~p(n9, n6, n5))). % 68.46/39.61 tff(c_23503, plain, (~p(n8, n3, n9))). % 68.46/39.61 tff(c_21991, plain, (~p(n6, n8, n4))). % 68.46/39.61 tff(c_21998, plain, (~p(n6, n8, n2))). % 68.46/39.61 tff(c_23501, plain, (~p(n8, n3, n6))). % 68.46/39.61 tff(c_23321, plain, (~p(n9, n5, n6))). % 68.46/39.61 tff(c_21468, plain, (~p(n5, n3, n1))). % 68.46/39.61 tff(c_23327, plain, (~p(n5, n5, n7))). % 68.46/39.61 tff(c_23221, plain, (~p(n7, n1, n2))). % 68.46/39.61 tff(c_23331, plain, (~p(n2, n5, n7))). % 68.46/39.61 tff(c_21934, plain, (~p(n7, n3, n4))). % 68.46/39.61 tff(c_23329, plain, (~p(n4, n5, n7))). % 68.46/39.61 tff(c_23350, plain, (~p(n6, n6, n8))). % 68.46/39.61 tff(c_23338, plain, (p(n7, n6, n8))). % 68.46/39.61 tff(c_23347, plain, (~p(n7, n6, n5))). % 68.46/39.61 tff(c_23191, plain, (~p(n1, n5, n2))). % 68.46/39.61 tff(c_21944, plain, (~p(n7, n3, n1))). % 68.46/39.61 tff(c_23390, plain, (~p(n2, n1, n2))). % 68.46/39.61 tff(c_23184, plain, (~p(n5, n5, n2))). % 68.46/39.61 tff(c_23352, plain, (~p(n5, n6, n8))). % 68.46/39.61 tff(c_21296, plain, (~p(n9, n5, n9))). % 68.46/39.61 tff(c_23174, plain, (~p(n7, n6, n2))). % 68.46/39.61 tff(c_23170, plain, (~p(n8, n5, n4))). % 68.46/39.61 tff(c_23380, plain, (~p(n3, n1, n2))). % 68.46/39.61 tff(c_23186, plain, (~p(n4, n5, n2))). % 68.46/39.61 tff(c_23356, plain, (~p(n3, n6, n8))). % 68.46/39.61 tff(c_21289, plain, (~p(n9, n6, n9))). % 68.46/39.61 tff(c_23182, plain, (~p(n6, n5, n2))). % 68.46/39.61 tff(c_23180, plain, (~p(n9, n5, n2))). % 68.46/39.61 tff(c_23137, plain, (~p(n5, n2, n7))). % 68.46/39.61 tff(c_21275, plain, (~p(n8, n6, n1))). % 68.46/39.61 tff(c_23354, plain, (~p(n4, n6, n8))). % 68.46/39.61 tff(c_23189, plain, (~p(n2, n5, n2))). % 68.46/39.61 tff(c_23118, plain, (~p(n7, n2, n1))). % 68.46/39.61 tff(c_23106, plain, (~p(n1, n3, n4))). % 68.46/39.61 tff(c_23092, plain, (~p(n2, n3, n4))). % 68.46/39.61 tff(c_21767, plain, (~p(n9, n1, n9))). % 68.46/39.61 tff(c_23096, plain, (~p(n1, n3, n7))). % 68.46/39.61 tff(c_23087, plain, (~p(n2, n3, n3))). % 68.46/39.61 tff(c_23080, plain, (~p(n4, n3, n4))). % 68.46/39.61 tff(c_21771, plain, (~p(n9, n1, n8))). % 68.46/39.61 tff(c_23083, plain, (~p(n2, n3, n7))). % 68.46/39.61 tff(c_23061, plain, (~p(n9, n3, n4))). % 68.46/39.61 tff(c_23058, plain, (~p(n4, n3, n3))). % 68.46/39.61 tff(c_23055, plain, (~p(n4, n3, n7))). % 68.46/39.61 tff(c_23051, plain, (~p(n6, n3, n3))). % 68.46/39.61 tff(c_21782, plain, (~p(n9, n1, n5))). % 68.46/39.61 tff(c_23043, plain, (~p(n8, n3, n3))). % 68.46/39.61 tff(c_23028, plain, (~p(n9, n3, n7))). % 68.46/39.61 tff(c_23038, plain, (~p(n9, n3, n3))). % 68.46/39.61 tff(c_21740, plain, (~p(n9, n4, n9))). % 68.46/39.61 tff(c_22984, plain, (~p(n5, n4, n5))). % 68.46/39.61 tff(c_22979, plain, (~p(n6, n4, n5))). % 68.46/39.61 tff(c_23032, plain, (~p(n8, n3, n7))). % 68.46/39.61 tff(c_22989, plain, (~p(n4, n4, n5))). % 68.46/39.61 tff(c_23020, plain, (~p(n3, n4, n6))). % 68.46/39.61 tff(c_21459, plain, (~p(n4, n7, n6))). % 68.46/39.61 tff(c_22993, plain, (~p(n3, n4, n5))). % 68.46/39.61 tff(c_23006, plain, (~p(n6, n4, n6))). % 68.46/39.61 tff(c_23010, plain, (~p(n5, n4, n6))). % 68.46/39.61 tff(c_21447, plain, (~p(n5, n7, n5))). % 68.46/39.61 tff(c_22955, plain, (~p(n4, n4, n9))). % 68.46/39.61 tff(c_23015, plain, (~p(n4, n4, n6))). % 68.46/39.61 tff(c_22943, plain, (~p(n5, n4, n1))). % 68.46/39.61 tff(c_22915, plain, (~p(n2, n5, n9))). % 68.46/39.61 tff(c_22946, plain, (~p(n5, n4, n9))). % 68.46/39.61 tff(c_21442, plain, (~p(n5, n9, n5))). % 68.46/39.61 tff(c_22907, plain, (~p(n4, n5, n9))). % 68.46/39.61 tff(c_22902, plain, (~p(n5, n5, n9))). % 68.46/39.61 tff(c_22885, plain, (~p(n4, n5, n5))). % 68.46/39.61 tff(c_21423, plain, (~p(n5, n7, n3))). % 68.46/39.61 tff(c_22875, plain, (~p(n6, n5, n5))). % 68.46/39.61 tff(c_22871, plain, (~p(n8, n5, n5))). % 68.46/39.61 tff(c_22851, plain, (~p(n5, n6, n4))). % 68.46/39.61 tff(c_22860, plain, (~p(n3, n6, n4))). % 68.46/39.61 tff(c_22787, plain, (~p(n4, n6, n6))). % 68.46/39.61 tff(c_21419, plain, (~p(n5, n8, n3))). % 68.46/39.61 tff(c_22765, plain, (~p(n7, n6, n3))). % 68.46/39.61 tff(c_22783, plain, (~p(n5, n6, n3))). % 68.46/39.61 tff(c_22769, plain, (~p(n6, n6, n6))). % 68.46/39.61 tff(c_21414, plain, (~p(n6, n7, n3))). % 68.46/39.61 tff(c_22773, plain, (~p(n6, n6, n3))). % 68.46/39.61 tff(c_22753, plain, (~p(n1, n7, n5))). % 68.46/39.61 tff(c_22736, plain, (~p(n2, n7, n1))). % 68.46/39.61 tff(c_22646, plain, (~p(n5, n8, n5))). % 68.46/39.61 tff(c_22638, plain, (~p(n7, n8, n5))). % 68.46/39.61 tff(c_21403, plain, (~p(n6, n8, n1))). % 68.46/39.61 tff(c_22581, plain, (~p(n8, n9, n9))). % 68.46/39.61 tff(c_22567, plain, (~p(n2, n9, n8))). % 68.46/39.61 tff(c_22572, plain, (~p(n2, n9, n3))). % 68.46/39.61 tff(c_21399, plain, (~p(n5, n7, n6))). % 68.46/39.61 tff(c_22594, plain, (~p(n5, n9, n9))). % 68.46/39.61 tff(c_22557, plain, (~p(n3, n9, n3))). % 68.46/39.61 tff(c_22562, plain, (~p(n2, n9, n4))). % 68.46/39.61 tff(c_22552, plain, (~p(n3, n9, n8))). % 68.46/39.61 tff(c_22548, plain, (~p(n3, n9, n4))). % 68.46/39.61 tff(c_21659, plain, (~p(n1, n2, n4))). % 68.46/39.61 tff(c_22519, plain, (~p(n5, n9, n4))). % 68.46/39.61 tff(c_22509, plain, (~p(n8, n9, n8))). % 68.46/39.61 tff(c_22532, plain, (~p(n8, n9, n3))). % 68.46/39.61 tff(c_21655, plain, (~p(n2, n1, n4))). % 68.46/39.61 tff(c_22514, plain, (~p(n7, n9, n8))). % 68.46/39.61 tff(c_22524, plain, (~p(n5, n9, n8))). % 68.46/39.61 tff(c_22545, plain, (~p(n5, n9, n3))). % 68.46/39.61 tff(c_22536, plain, (~p(n7, n9, n3))). % 68.46/39.61 tff(c_22633, plain, (~p(n8, n8, n5))). % 68.46/39.61 tff(c_21387, plain, (~p(n5, n8, n8))). % 68.46/39.61 tff(c_22610, plain, (~p(n9, n8, n6))). % 68.46/39.61 tff(c_22614, plain, (~p(n8, n8, n6))). % 68.46/39.61 tff(c_22628, plain, (~p(n9, n8, n5))). % 68.46/39.61 tff(c_21650, plain, (~p(n2, n2, n4))). % 68.46/39.61 tff(c_22624, plain, (~p(n5, n8, n6))). % 68.46/39.61 tff(c_22655, plain, (~p(n3, n8, n5))). % 68.46/39.61 tff(c_22650, plain, (~p(n3, n8, n6))). % 68.46/39.61 tff(c_22658, plain, (~p(n2, n8, n6))). % 68.46/39.62 tff(c_22761, plain, (~p(n7, n6, n6))). % 68.46/39.62 tff(c_21632, plain, (~p(n1, n4, n9))). % 68.46/39.62 tff(c_22731, plain, (~p(n2, n7, n2))). % 68.46/39.62 tff(c_22665, plain, (~p(n1, n8, n6))). % 68.46/39.62 tff(c_22713, plain, (~p(n8, n7, n5))). % 68.46/39.62 tff(c_21624, plain, (~p(n1, n5, n5))). % 68.46/39.62 tff(c_22728, plain, (~p(n4, n7, n5))). % 68.46/39.62 tff(c_22708, plain, (~p(n9, n7, n5))). % 68.46/39.62 tff(c_22696, plain, (~p(n6, n7, n1))). % 68.46/39.62 tff(c_22674, plain, (~p(n8, n7, n2))). % 68.46/39.62 tff(c_22671, plain, (~p(n9, n7, n2))). % 68.46/39.62 tff(c_21619, plain, (~p(n1, n5, n7))). % 68.46/39.62 tff(c_22678, plain, (~p(n6, n7, n2))). % 68.46/39.62 tff(c_22699, plain, (~p(n4, n7, n2))). % 68.46/39.62 tff(c_22683, plain, (~p(n9, n7, n1))). % 68.46/39.62 tff(c_21606, plain, (~p(n2, n5, n4))). % 68.46/39.62 tff(c_22687, plain, (~p(n8, n7, n1))). % 68.46/39.62 tff(c_22704, plain, (~p(n4, n7, n1))). % 68.46/39.62 tff(c_22741, plain, (~p(n2, n7, n5))). % 68.46/39.62 tff(c_22792, plain, (~p(n4, n6, n3))). % 68.46/39.62 tff(c_22867, plain, (~p(n9, n5, n5))). % 68.46/39.62 tff(c_21591, plain, (~p(n2, n4, n9))). % 68.46/39.62 tff(c_22856, plain, (~p(n4, n6, n4))). % 68.46/39.62 tff(c_22798, plain, (~p(n3, n6, n3))). % 68.46/39.62 tff(c_22841, plain, (~p(n7, n6, n4))). % 68.46/39.62 tff(c_21599, plain, (~p(n3, n5, n4))). % 68.46/39.62 tff(c_22846, plain, (~p(n6, n6, n4))). % 68.46/39.62 tff(c_22829, plain, (~p(n3, n6, n7))). % 68.46/39.62 tff(c_22820, plain, (~p(n5, n6, n7))). % 68.46/39.62 tff(c_22825, plain, (~p(n4, n6, n7))). % 68.46/39.62 tff(c_22811, plain, (~p(n7, n6, n7))). % 68.46/39.62 tff(c_21582, plain, (~p(n3, n4, n7))). % 68.46/39.62 tff(c_22815, plain, (~p(n6, n6, n7))). % 68.46/39.62 tff(c_22912, plain, (~p(n2, n5, n5))). % 68.46/39.62 tff(c_22898, plain, (~p(n6, n5, n9))). % 68.46/39.62 tff(c_21574, plain, (~p(n2, n6, n9))). % 68.46/39.62 tff(c_22891, plain, (~p(n8, n5, n9))). % 68.46/39.62 tff(c_22939, plain, (~p(n6, n4, n9))). % 68.46/39.62 tff(c_22936, plain, (~p(n6, n4, n1))). % 68.46/39.62 tff(c_22928, plain, (~p(n7, n4, n1))). % 68.46/39.62 tff(c_22932, plain, (~p(n7, n4, n9))). % 68.46/39.62 tff(c_21578, plain, (~p(n3, n5, n7))). % 68.46/39.62 tff(c_22921, plain, (~p(n1, n5, n9))). % 68.46/39.62 tff(c_22951, plain, (~p(n4, n4, n1))). % 68.46/39.62 tff(c_22965, plain, (~p(n3, n4, n9))). % 68.46/39.62 tff(c_21596, plain, (~p(n1, n6, n9))). % 68.46/39.62 tff(c_22960, plain, (~p(n3, n4, n1))). % 68.46/39.62 tff(c_23065, plain, (~p(n8, n3, n4))). % 68.46/39.62 tff(c_22976, plain, (~p(n7, n4, n5))). % 68.46/39.62 tff(c_23101, plain, (~p(n1, n3, n3))). % 68.46/39.62 tff(c_23176, plain, (~p(n7, n4, n2))). % 68.46/39.62 tff(c_21362, plain, (~p(n9, n1, n7))). % 68.46/39.62 tff(c_23113, plain, (~p(n8, n2, n1))). % 68.46/39.62 tff(c_23130, plain, (~p(n7, n2, n7))). % 68.46/39.62 tff(c_23109, plain, (~p(n9, n2, n1))). % 68.46/39.62 tff(c_21565, plain, (~p(n2, n7, n9))). % 68.46/39.62 tff(c_23172, plain, (~p(n8, n5, n3))). % 68.46/39.62 tff(c_23123, plain, (~p(n5, n2, n1))). % 68.46/39.62 tff(c_23143, plain, (~p(n3, n2, n7))). % 68.46/39.62 tff(c_24295, plain, (~p(n1, n5, n4))). % 68.46/39.62 tff(c_23166, plain, (~p(n8, n5, n8))). % 68.46/39.62 tff(c_21553, plain, (~p(n3, n7, n9))). % 68.46/39.62 tff(c_23168, plain, (~p(n8, n5, n7))). % 68.46/39.62 tff(c_23150, plain, (~p(n2, n2, n7))). % 68.46/39.62 tff(c_23157, plain, (~p(n1, n2, n7))). % 68.46/39.62 tff(c_21549, plain, (~p(n3, n8, n9))). % 68.46/39.62 tff(c_23164, plain, (p(n8, n5, n2))). % 68.46/39.62 tff(c_23154, plain, (~p(n1, n2, n1))). % 68.46/39.62 tff(c_23162, plain, (~p(n8, n1, n2))). % 68.46/39.62 tff(c_24291, plain, (~p(n2, n8, n1))). % 68.46/39.62 tff(c_24287, plain, (~p(n2, n8, n8))). % 68.46/39.62 tff(c_21546, plain, (~p(n2, n8, n5))). % 68.46/39.62 tff(c_24284, plain, (~p(n3, n2, n3))). % 68.46/39.62 tff(c_24280, plain, (~p(n3, n4, n2))). % 68.46/39.62 tff(c_24282, plain, (~p(n3, n8, n3))). % 68.46/39.62 tff(c_21542, plain, (~p(n2, n9, n5))). % 68.46/39.62 tff(c_24269, plain, (~p(n1, n5, n3))). % 68.46/39.62 tff(c_24255, plain, (p(n5, n5, n4))). % 68.46/39.62 tff(c_24263, plain, (p(n1, n2, n2))). % 68.46/39.62 tff(c_24265, plain, (p(n5, n4, n8))). % 68.46/39.62 tff(c_24252, plain, (p(n2, n8, n4))). % 68.46/39.62 tff(c_21348, plain, (~p(n8, n3, n2))). % 68.46/39.62 tff(c_24278, plain, (~p(n3, n4, n8))). % 68.46/39.62 tff(c_24251, plain, (p(n3, n4, n3))). % 68.46/39.62 tff(c_24267, plain, (~p(n2, n5, n3))). % 68.46/39.62 tff(c_21509, plain, (~p(n5, n3, n7))). % 68.46/39.62 tff(c_24250, plain, (p(n6, n5, n3))). % 68.46/39.62 tff(c_24234, plain, (~p(n6, n5, n4))). % 68.46/39.62 tff(c_24247, plain, (~p(n5, n4, n2))). % 68.46/39.62 tff(c_24229, plain, (~p(n1, n7, n4))). % 68.46/39.62 tff(c_24232, plain, (~p(n5, n8, n4))). % 68.46/39.62 tff(c_21497, plain, (~p(n6, n3, n7))). % 68.46/39.62 tff(c_24242, plain, (~p(n2, n8, n2))). % 68.46/39.62 tff(c_24244, plain, (~p(n1, n8, n2))). % 68.46/39.62 tff(c_24227, plain, (~p(n2, n7, n4))). % 68.46/39.62 tff(c_21487, plain, (~p(n4, n3, n1))). % 68.46/39.62 tff(c_24214, plain, (p(n6, n4, n7))). % 68.46/39.62 tff(c_24240, plain, (~p(n3, n8, n2))). % 68.46/39.62 tff(c_24217, plain, (p(n5, n8, n2))). % 68.46/39.62 tff(c_24224, plain, (~p(n6, n4, n3))). % 68.46/39.62 tff(c_24209, plain, (~p(n5, n8, n7))). % 68.46/39.62 tff(c_21484, plain, (~p(n5, n1, n1))). % 68.46/39.62 tff(c_24204, plain, (~p(n6, n7, n7))). % 68.46/39.62 tff(c_24206, plain, (~p(n5, n9, n2))). % 68.46/39.62 tff(c_24212, plain, (~p(n5, n4, n7))). % 68.46/39.62 tff(c_21329, plain, (~p(n7, n5, n3))). % 68.46/39.62 tff(c_24215, plain, (p(n6, n7, n4))). % 68.46/39.62 tff(c_24175, plain, (~p(n2, n1, n7))). % 68.46/39.62 tff(c_24200, plain, (p(n5, n9, n7))). % 68.46/39.62 tff(c_24182, plain, (~p(n3, n1, n8))). % 68.46/39.62 tff(c_24186, plain, (~p(n3, n9, n7))). % 68.46/39.62 tff(c_21318, plain, (~p(n9, n4, n5))). % 68.46/39.62 tff(c_24165, plain, (~p(n2, n3, n5))). % 68.46/39.62 tff(c_24176, plain, (p(n3, n1, n7))). % 68.46/39.62 tff(c_24180, plain, (~p(n3, n1, n6))). % 68.46/39.62 tff(c_21310, plain, (~p(n7, n5, n6))). % 68.46/39.62 tff(c_24184, plain, (~p(n3, n1, n3))). % 68.46/39.62 tff(c_24188, plain, (~p(n3, n8, n7))). % 68.46/39.62 tff(c_24145, plain, (~p(n2, n7, n7))). % 68.46/39.62 tff(c_24171, plain, (~p(n2, n2, n5))). % 68.46/39.62 tff(c_24141, plain, (~p(n2, n8, n7))). % 68.46/39.62 tff(c_21305, plain, (~p(n7, n6, n9))). % 68.46/39.62 tff(c_24123, plain, (~p(n3, n2, n9))). % 68.46/39.62 tff(c_24137, plain, (~p(n2, n9, n7))). % 68.46/39.62 tff(c_24129, plain, (~p(n3, n1, n5))). % 68.46/39.62 tff(c_21300, plain, (~p(n7, n6, n1))). % 68.46/39.62 tff(c_24119, plain, (~p(n3, n2, n5))). % 68.46/39.62 tff(c_24069, plain, (~p(n4, n5, n4))). % 68.46/39.62 tff(c_24103, plain, (~p(n3, n8, n4))). % 68.46/39.62 tff(c_24051, plain, (~p(n6, n4, n2))). % 68.46/39.62 tff(c_24045, plain, (~p(n2, n3, n2))). % 68.46/39.62 tff(c_21479, plain, (~p(n5, n2, n9))). % 68.46/39.62 tff(c_24047, plain, (~p(n1, n3, n2))). % 68.46/39.62 tff(c_24043, plain, (~p(n4, n3, n2))). % 68.46/39.62 tff(c_24041, plain, (~p(n5, n2, n2))). % 68.46/39.62 tff(c_21293, plain, (~p(n8, n4, n6))). % 68.46/39.62 tff(c_24033, plain, (~p(n6, n3, n5))). % 68.46/39.63 tff(c_24038, plain, (p(n6, n3, n2))). % 68.46/39.63 tff(c_24030, plain, (~p(n6, n6, n2))). % 68.46/39.63 tff(c_24019, plain, (~p(n5, n6, n5))). % 68.46/39.63 tff(c_24027, plain, (p(n6, n6, n5))). % 68.46/39.63 tff(c_21284, plain, (~p(n8, n5, n1))). % 68.46/39.63 tff(c_24017, plain, (~p(n5, n6, n2))). % 68.46/39.63 tff(c_24021, plain, (~p(n3, n6, n9))). % 68.46/39.63 tff(c_24007, plain, (p(n5, n6, n9))). % 68.46/39.63 tff(c_21279, plain, (~p(n8, n5, n6))). % 68.46/39.63 tff(c_24006, plain, (~p(n4, n6, n9))). % 68.46/39.63 tff(c_24001, plain, (~p(n1, n7, n9))). % 68.46/39.63 tff(c_23992, plain, (~p(n4, n7, n4))). % 68.46/39.63 tff(c_23999, plain, (~p(n9, n7, n9))). % 68.46/39.63 tff(c_23997, plain, (~p(n5, n8, n9))). % 68.46/39.63 tff(c_21271, plain, (~p(n9, n4, n3))). % 68.46/39.63 tff(c_23890, plain, (~p(n5, n5, n1))). % 68.46/39.63 tff(c_23995, plain, (p(n4, n7, n9))). % 68.46/39.63 tff(c_23969, plain, (~p(n4, n7, n7))). % 68.46/39.63 tff(c_21266, plain, (~p(n9, n5, n3))). % 68.46/39.63 tff(c_23882, plain, (~p(n5, n8, n1))). % 68.46/39.63 tff(c_23948, plain, (~p(n4, n4, n3))). % 68.46/39.63 tff(c_23857, plain, (~p(n6, n7, n9))). % 68.46/39.63 tff(c_23870, plain, (~p(n6, n3, n9))). % 68.46/39.63 tff(c_23841, plain, (~p(n6, n5, n1))). % 68.46/39.63 tff(c_21261, plain, (~p(n8, n8, n2))). % 68.46/39.63 tff(c_23806, plain, (~p(n6, n5, n6))). % 68.46/39.63 tff(c_23886, plain, (~p(n5, n6, n1))). % 68.46/39.63 tff(c_23789, plain, (~p(n6, n7, n8))). % 68.46/39.63 tff(c_21256, plain, (~p(n8, n9, n2))). % 68.46/39.63 tff(c_23793, plain, (~p(n6, n7, n6))). % 68.46/39.63 tff(c_23801, plain, (~p(n6, n5, n8))). % 68.46/39.63 tff(c_23782, plain, (~p(n7, n1, n7))). % 68.46/39.63 tff(c_23734, plain, (~p(n7, n8, n7))). % 68.46/39.63 tff(c_23309, plain, (p(n9, n5, n7))). % 68.46/39.63 tff(c_21252, plain, (~p(n9, n8, n2))). % 68.46/39.63 tff(c_23776, plain, (~p(n7, n1, n5))). % 68.46/39.63 tff(c_23232, plain, (~p(n7, n1, n9))). % 68.46/39.63 tff(c_23298, plain, (~p(n6, n4, n4))). % 68.46/39.63 tff(c_21245, plain, (~p(n7, n7, n4))). % 68.46/39.63 tff(c_23302, plain, (~p(n4, n4, n4))). % 68.46/39.63 tff(c_23293, plain, (~p(n7, n4, n7))). % 68.46/39.63 tff(c_23295, plain, (~p(n9, n5, n4))). % 68.46/39.63 tff(c_23237, plain, (~p(n5, n1, n2))). % 68.46/39.63 tff(c_23289, plain, (p(n7, n4, n4))). % 68.46/39.63 tff(c_21249, plain, (~p(n9, n9, n2))). % 68.46/39.63 tff(c_23291, plain, (~p(n7, n4, n8))). % 68.46/39.63 tff(c_23265, plain, (~p(n9, n2, n4))). % 68.46/39.63 tff(c_23270, plain, (~p(n3, n2, n4))). % 68.46/39.63 tff(c_21396, plain, (~p(n6, n9, n1))). % 68.46/39.63 tff(c_23261, plain, (~p(n8, n2, n9))). % 68.46/39.63 tff(c_23263, plain, (~p(n8, n2, n6))). % 68.46/39.63 tff(c_23267, plain, (~p(n7, n2, n4))). % 68.46/39.63 tff(c_23241, plain, (~p(n5, n1, n9))). % 68.46/39.63 tff(c_23257, plain, (~p(n8, n2, n5))). % 68.46/39.63 tff(c_21392, plain, (~p(n5, n7, n8))). % 68.46/39.63 tff(c_23259, plain, (~p(n8, n2, n3))). % 68.46/39.63 tff(c_23249, plain, (~p(n8, n1, n4))). % 68.46/39.63 tff(c_23250, plain, (p(n8, n2, n4))). % 68.46/39.63 tff(c_21240, plain, (~p(n7, n8, n4))). % 68.46/39.63 tff(c_23255, plain, (~p(n8, n2, n8))). % 68.46/39.63 tff(c_23376, plain, (~p(n5, n1, n4))). % 68.46/39.63 tff(c_23387, plain, (~p(n3, n1, n4))). % 68.46/39.63 tff(c_23253, plain, (~p(n7, n1, n4))). % 68.46/39.63 tff(c_23472, plain, (~p(n9, n8, n1))). % 68.46/39.63 tff(c_21382, plain, (~p(n5, n9, n6))). % 68.46/39.63 tff(c_23499, plain, (~p(n8, n3, n8))). % 68.46/39.63 tff(c_23384, plain, (~p(n3, n1, n9))). % 68.46/39.63 tff(c_23437, plain, (~p(n9, n7, n4))). % 68.46/39.63 tff(c_21602, plain, (~p(n3, n4, n4))). % 68.46/39.63 tff(c_23395, plain, (~p(n2, n1, n9))). % 68.46/39.63 tff(c_23433, plain, (~p(n9, n8, n4))). % 68.46/39.63 tff(c_23429, plain, (~p(n2, n1, n1))). % 68.46/39.63 tff(c_23405, plain, (~p(n8, n1, n1))). % 68.46/39.63 tff(c_23425, plain, (~p(n3, n1, n1))). % 68.46/39.63 tff(c_21587, plain, (~p(n3, n6, n5))). % 68.46/39.63 tff(c_23447, plain, (~p(n9, n7, n6))). % 68.46/39.63 tff(c_23410, plain, (~p(n7, n1, n1))). % 68.46/39.63 tff(c_23456, plain, (~p(n9, n8, n7))). % 68.46/39.63 tff(c_21378, plain, (~p(n7, n2, n2))). % 68.46/39.63 tff(c_23496, plain, (p(n8, n3, n1))). % 68.46/39.63 tff(c_23460, plain, (~p(n9, n7, n7))). % 68.46/39.63 tff(c_23488, plain, (~p(n9, n3, n6))). % 68.46/39.63 tff(c_23560, plain, (~p(n9, n2, n2))). % 68.46/39.63 tff(c_23495, plain, (~p(n9, n3, n1))). % 68.46/39.63 tff(c_21373, plain, (~p(n8, n1, n7))). % 68.46/39.63 tff(c_23527, plain, (~p(n9, n2, n6))). % 68.46/39.63 tff(c_23556, plain, (~p(n9, n3, n2))). % 68.46/39.63 tff(c_23771, plain, (~p(n7, n1, n8))). % 68.46/39.63 tff(c_21358, plain, (~p(n9, n2, n7))). % 68.46/39.63 tff(c_23571, plain, (~p(n8, n7, n3))). % 68.46/39.63 tff(c_23588, plain, (~p(n8, n8, n9))). % 68.46/39.63 tff(c_23566, plain, (~p(n8, n8, n3))). % 68.46/39.63 tff(c_23593, plain, (~p(n8, n7, n9))). % 68.46/39.63 tff(c_23610, plain, (~p(n8, n8, n1))). % 68.46/39.63 tff(c_21235, plain, (~p(n8, n7, n4))). % 68.46/39.63 tff(c_23606, plain, (~p(n8, n9, n1))). % 68.46/39.63 tff(c_23761, plain, (~p(n7, n2, n5))). % 68.46/39.63 tff(c_23694, plain, (~p(n8, n1, n5))). % 68.46/39.63 tff(c_21353, plain, (~p(n8, n2, n2))). % 68.46/39.63 tff(c_23650, plain, (~p(n8, n1, n3))). % 68.46/39.63 tff(c_23688, plain, (~p(n8, n9, n7))). % 68.46/39.63 tff(c_23690, plain, (~p(n3, n9, n5))). % 68.46/39.63 tff(c_23756, plain, (~p(n7, n2, n8))). % 68.46/39.63 tff(c_23663, plain, (~p(n7, n9, n2))). % 68.46/39.63 tff(c_21230, plain, (~p(n8, n8, n4))). % 68.46/39.63 tff(c_23730, plain, (~p(n7, n9, n7))). % 68.46/39.63 tff(c_23667, plain, (~p(n7, n8, n2))). % 68.46/39.63 tff(c_23686, plain, (~p(n8, n9, n6))). % 68.46/39.63 tff(c_21343, plain, (~p(n7, n4, n3))). % 68.46/39.63 tff(c_23673, plain, (~p(n7, n8, n8))). % 68.46/39.63 tff(c_23683, plain, (p(n8, n9, n5))). % 68.46/39.63 tff(c_23682, plain, (~p(n7, n9, n5))). % 68.46/39.63 tff(c_23810, plain, (~p(n6, n4, n8))). % 68.46/39.63 tff(c_23822, plain, (~p(n6, n3, n6))). % 68.46/39.63 tff(c_21325, plain, (~p(n8, n6, n5))). % 68.46/39.63 tff(c_23862, plain, (~p(n6, n6, n9))). % 68.46/39.63 tff(c_23817, plain, (~p(n6, n3, n8))). % 68.46/39.63 tff(c_23878, plain, (~p(n5, n9, n1))). % 68.46/39.63 tff(c_24647, plain, (~p(n1, n8, n1))). % 68.46/39.63 tff(c_23837, plain, (~p(n6, n6, n1))). % 68.46/39.63 tff(c_23906, plain, (~p(n5, n5, n3))). % 68.46/39.63 tff(c_23978, plain, (~p(n4, n4, n7))). % 68.46/39.63 tff(c_23910, plain, (~p(n5, n4, n3))). % 68.46/39.63 tff(c_23956, plain, (~p(n4, n3, n5))). % 68.46/39.63 tff(c_24587, plain, (~p(n7, n8, n1))). % 68.46/39.63 tff(c_23916, plain, (~p(n5, n2, n3))). % 68.46/39.63 tff(c_23922, plain, (~p(n5, n1, n3))). % 68.46/39.63 tff(c_23942, plain, (~p(n4, n5, n3))). % 68.46/39.63 tff(c_24585, plain, (~p(n7, n8, n3))). % 68.46/39.63 tff(c_23930, plain, (~p(n4, n7, n3))). % 68.46/39.63 tff(c_23938, plain, (~p(n4, n6, n5))). % 68.46/39.63 tff(c_24289, plain, (~p(n2, n8, n3))). % 68.46/39.63 tff(c_24293, plain, (~p(n1, n8, n4))). % 68.46/39.63 tff(c_24298, plain, (~p(n5, n5, n6))). % 68.46/39.63 tff(c_24556, plain, (~p(n2, n1, n8))). % 68.46/39.63 tff(c_24300, plain, (~p(n5, n5, n8))). % 68.46/39.63 tff(c_24306, plain, (~p(n1, n2, n9))). % 68.46/39.63 tff(c_24308, plain, (~p(n1, n2, n8))). % 68.46/39.63 tff(c_24511, plain, (~p(n2, n5, n8))). % 68.46/39.63 tff(c_24310, plain, (~p(n1, n2, n6))). % 68.46/39.63 tff(c_24312, plain, (~p(n1, n2, n5))). % 68.46/39.63 tff(c_24314, plain, (~p(n1, n2, n3))). % 68.46/39.63 tff(c_24317, plain, (~p(n3, n2, n2))). % 68.46/39.63 tff(c_24319, plain, (~p(n2, n2, n2))). % 68.46/39.63 tff(c_24500, plain, (~p(n7, n2, n9))). % 68.46/39.63 tff(c_24322, plain, (~p(n4, n4, n8))). % 68.46/39.63 tff(c_24331, plain, (~p(n5, n2, n8))). % 68.46/39.63 tff(c_24333, plain, (~p(n5, n1, n8))). % 68.46/39.63 tff(c_24473, plain, (~p(n3, n2, n6))). % 68.46/39.63 tff(c_24369, plain, (p(n2, n9, n2))). % 68.46/39.63 tff(c_24342, plain, (p(n3, n6, n2))). % 68.46/39.63 tff(c_24343, plain, (p(n4, n4, n2))). % 68.46/39.63 tff(c_24358, plain, (p(n4, n5, n6))). % 68.46/39.63 tff(c_24366, plain, (p(n1, n3, n5))). % 68.46/39.64 tff(c_24429, plain, (~p(n2, n3, n8))). % 68.46/39.64 tff(c_24335, plain, (~p(n4, n5, n8))). % 68.46/39.64 tff(c_24425, plain, (p(n4, n3, n8))). % 68.46/39.64 tff(c_24381, plain, (~p(n4, n6, n2))). % 68.46/39.64 tff(c_24406, plain, (~p(n1, n3, n9))). % 68.46/39.64 tff(c_24383, plain, (~p(n3, n6, n1))). % 68.46/39.64 tff(c_24387, plain, (~p(n3, n9, n2))). % 68.46/39.64 tff(c_24397, plain, (~p(n1, n5, n6))). % 68.46/39.64 tff(c_24400, plain, (~p(n4, n5, n1))). % 68.46/39.64 tff(c_24402, plain, (~p(n4, n3, n6))). % 68.46/39.64 tff(c_21080, plain, (p(n4, n1, n4))). % 68.46/39.64 tff(c_21078, plain, (p(n3, n7, n5))). % 68.46/39.64 tff(c_24408, plain, (~p(n1, n3, n8))). % 68.46/39.64 tff(c_24410, plain, (~p(n1, n3, n6))). % 68.46/39.64 tff(c_21082, plain, (p(n4, n2, n7))). % 68.46/39.64 tff(c_24412, plain, (~p(n9, n3, n5))). % 68.46/39.64 tff(c_24416, plain, (~p(n2, n1, n5))). % 68.46/39.64 tff(c_24418, plain, (~p(n2, n9, n1))). % 68.46/39.64 tff(c_24422, plain, (~p(n2, n9, n6))). % 68.46/39.64 tff(c_24427, plain, (~p(n9, n3, n8))). % 68.46/39.64 tff(c_21084, plain, (p(n4, n8, n5))). % 68.46/39.64 tff(c_21076, plain, (p(n3, n5, n9))). % 68.46/39.64 tff(c_24440, plain, (p(n4, n6, n1))). % 68.46/39.64 tff(c_24469, plain, (p(n2, n3, n6))). % 68.46/39.64 tff(c_21086, plain, (p(n4, n9, n3))). % 68.46/39.64 tff(c_24453, plain, (p(n9, n2, n5))). % 68.46/39.64 tff(c_24490, plain, (p(n9, n3, n9))). % 68.46/39.64 tff(c_24455, plain, (p(n5, n1, n5))). % 68.46/39.64 tff(c_24459, plain, (p(n2, n5, n1))). % 68.46/39.64 tff(c_24471, plain, (~p(n2, n3, n9))). % 68.46/39.64 tff(c_21088, plain, (p(n5, n3, n3))). % 68.46/39.64 tff(c_21074, plain, (p(n3, n3, n4))). % 68.46/39.64 tff(c_24475, plain, (~p(n2, n7, n6))). % 68.46/39.64 tff(c_24477, plain, (~p(n2, n2, n6))). % 68.46/39.64 tff(c_21090, plain, (p(n5, n7, n1))). % 68.46/39.64 tff(c_24481, plain, (~p(n5, n2, n5))). % 68.46/39.64 tff(c_24484, plain, (~p(n9, n2, n3))). % 68.46/39.64 tff(c_24486, plain, (~p(n9, n2, n9))). % 68.46/39.64 tff(c_24488, plain, (~p(n9, n2, n8))). % 68.46/39.64 tff(c_24494, plain, (~p(n9, n8, n9))). % 68.46/39.64 tff(c_21092, plain, (p(n6, n1, n9))). % 68.46/39.64 tff(c_21072, plain, (p(n2, n6, n7))). % 68.46/39.64 tff(c_24506, plain, (~p(n5, n1, n6))). % 68.46/39.64 tff(c_24509, plain, (~p(n1, n5, n1))). % 68.46/39.64 tff(c_21094, plain, (p(n6, n2, n1))). % 68.46/39.64 tff(c_24531, plain, (p(n8, n1, n8))). % 68.46/39.64 tff(c_24516, plain, (p(n2, n2, n9))). % 68.46/39.64 tff(c_24517, plain, (p(n3, n9, n6))). % 68.46/39.64 tff(c_24518, plain, (p(n3, n2, n8))). % 68.46/39.64 tff(c_24524, plain, (p(n5, n2, n6))). % 68.46/39.64 tff(c_21096, plain, (p(n6, n8, n6))). % 68.46/39.64 tff(c_21070, plain, (p(n2, n4, n5))). % 68.46/39.64 tff(c_24533, plain, (p(n7, n8, n9))). % 68.46/39.64 tff(c_24538, plain, (p(n1, n5, n8))). % 68.46/39.64 tff(c_21098, plain, (p(n6, n9, n8))). % 68.46/39.64 tff(c_24542, plain, (~p(n2, n2, n8))). % 68.46/39.64 tff(c_24544, plain, (~p(n2, n2, n3))). % 68.46/39.64 tff(c_24546, plain, (~p(n7, n9, n6))). % 68.46/39.64 tff(c_24548, plain, (~p(n1, n7, n6))). % 68.46/39.64 tff(c_24550, plain, (~p(n3, n9, n1))). % 68.46/39.64 tff(c_21100, plain, (p(n7, n3, n7))). % 68.46/39.64 tff(c_21068, plain, (p(n1, n9, n9))). % 68.46/39.64 tff(c_24558, plain, (~p(n3, n8, n8))). % 68.46/39.64 tff(c_24565, plain, (~p(n7, n2, n6))). % 68.46/39.64 tff(c_21102, plain, (p(n7, n5, n5))). % 68.46/39.64 tff(c_24574, plain, (~p(n8, n8, n8))). % 68.46/39.64 tff(c_24576, plain, (~p(n8, n7, n8))). % 68.46/39.64 tff(c_24579, plain, (~p(n8, n1, n6))). % 68.46/39.64 tff(c_24582, plain, (~p(n1, n8, n9))). % 68.46/39.64 tff(c_24608, plain, (p(n8, n8, n7))). % 68.46/39.64 tff(c_21104, plain, (p(n7, n7, n2))). % 68.46/39.64 tff(c_21066, plain, (p(n1, n6, n4))). % 68.46/39.64 tff(c_24617, plain, (p(n2, n7, n8))). % 68.46/39.64 tff(c_24593, plain, (p(n2, n1, n3))). % 68.46/39.64 tff(c_21106, plain, (p(n8, n4, n9))). % 68.46/39.64 tff(c_24594, plain, (p(n7, n2, n3))). % 68.46/39.64 tff(c_24637, plain, (p(n7, n1, n6))). % 68.46/39.64 tff(c_24596, plain, (p(n8, n7, n6))). % 68.46/39.64 tff(c_24597, plain, (p(n7, n9, n1))). % 68.46/39.64 tff(c_24600, plain, (p(n3, n8, n1))). % 68.46/39.64 tff(c_21108, plain, (p(n8, n6, n3))). % 68.46/39.64 tff(c_21064, plain, (p(n1, n4, n6))). % 68.46/39.64 tff(c_24619, plain, (~p(n2, n7, n3))). % 68.46/39.64 tff(c_24621, plain, (~p(n9, n7, n8))). % 68.46/39.64 tff(c_21110, plain, (p(n9, n1, n2))). % 68.46/39.64 tff(c_24623, plain, (~p(n1, n7, n8))). % 68.46/39.64 tff(c_24625, plain, (~p(n1, n8, n8))). % 68.46/39.64 tff(c_24628, plain, (~p(n2, n1, n6))). % 68.46/39.64 tff(c_24630, plain, (~p(n7, n1, n3))). % 68.46/39.64 tff(c_24644, plain, (~p(n8, n7, n7))). % 68.46/39.64 tff(c_21112, plain, (p(n9, n4, n1))). % 68.46/39.64 tff(c_21062, plain, (p(n1, n1, n1))). % 68.46/39.64 tff(c_24657, plain, (~p(n1, n8, n7))). % 68.46/39.64 tff(c_24669, plain, (p(n9, n7, n3))). % 68.46/39.64 tff(c_21114, plain, (p(n9, n6, n6))). % 68.46/39.64 tff(c_24670, plain, (p(n9, n8, n8))). % 68.46/39.64 tff(c_24686, plain, (p(n1, n8, n3))). % 68.46/39.64 tff(c_24674, plain, (p(n1, n7, n7))). % 68.46/39.64 tff(c_24677, plain, (~p(n1, n7, n3))). % 68.46/39.64 tff(c_24679, plain, (~p(n9, n8, n3))). % 68.46/39.64 tff(c_21116, plain, (p(n9, n9, n4))). % 68.46/39.64 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.46/39.64 %------------------------------------------------------------------------------