%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ068+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 : n027.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 96.77s 50.55s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : PUZ068+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.12/0.31 % Computer : n027.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Tue Apr 8 17:21:21 EDT 2025 % 0.12/0.32 % CPUTime : % 96.77/50.54 % 96.77/50.55 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.77/50.55 % 96.77/50.55 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.77/50.56 %$ p > #nlpp > n9 > n8 > n7 > n6 > n5 > n4 > n3 > n2 > n1 % 96.77/50.56 % 96.77/50.56 %Foreground sorts: % 96.77/50.56 % 96.77/50.56 % 96.77/50.56 %Background operators: % 96.77/50.56 % 96.77/50.56 % 96.77/50.56 %Foreground operators: % 96.77/50.56 tff(n8, type, n8: $i). % 96.77/50.56 tff(n9, type, n9: $i). % 96.77/50.56 tff(n3, type, n3: $i). % 96.77/50.56 tff(n1, type, n1: $i). % 96.77/50.56 tff(n7, type, n7: $i). % 96.77/50.56 tff(n6, type, n6: $i). % 96.77/50.56 tff(n4, type, n4: $i). % 96.77/50.56 tff(p, type, p: ($i * $i * $i) > $o). % 96.77/50.56 tff(n2, type, n2: $i). % 96.77/50.56 tff(n5, type, n5: $i). % 96.77/50.56 % 96.77/50.56 %Saturated clause set: % 96.77/50.56 tff(c_21855, plain, (~p(n3, n9, n6))). % 96.77/50.56 tff(c_21837, plain, (~p(n4, n1, n2))). % 96.77/50.56 tff(c_21777, plain, (~p(n4, n5, n9))). % 96.77/50.56 tff(c_21832, plain, (~p(n4, n1, n3))). % 96.77/50.56 tff(c_21811, plain, (~p(n4, n1, n9))). % 96.77/50.56 tff(c_21497, plain, (~p(n9, n9, n7))). % 96.77/50.56 tff(c_21899, plain, (~p(n3, n2, n5))). % 96.77/50.56 tff(c_21502, plain, (~p(n9, n9, n6))). % 96.77/50.56 tff(c_21458, plain, (~p(n3, n1, n5))). % 96.77/50.56 tff(c_21907, plain, (~p(n3, n2, n2))). % 96.77/50.56 tff(c_21507, plain, (~p(n9, n9, n5))). % 96.77/50.56 tff(c_21880, plain, (~p(n3, n2, n9))). % 96.77/50.56 tff(c_21448, plain, (~p(n2, n3, n3))). % 96.77/50.57 tff(c_21889, plain, (~p(n3, n2, n7))). % 96.77/50.57 tff(c_22082, plain, (~p(n1, n4, n2))). % 96.77/50.57 tff(c_21976, plain, (~p(n2, n2, n3))). % 96.77/50.57 tff(c_21966, plain, (~p(n2, n2, n6))). % 96.77/50.57 tff(c_21941, plain, (~p(n2, n4, n3))). % 96.77/50.57 tff(c_21433, plain, (~p(n3, n5, n4))). % 96.77/50.57 tff(c_21934, plain, (~p(n2, n4, n5))). % 96.77/50.57 tff(c_21922, plain, (~p(n2, n4, n8))). % 96.77/50.57 tff(c_21917, plain, (~p(n2, n4, n9))). % 96.77/50.57 tff(c_21424, plain, (~p(n1, n5, n2))). % 96.77/50.57 tff(c_22067, plain, (~p(n1, n4, n6))). % 96.77/50.57 tff(c_22042, plain, (~p(n1, n5, n4))). % 96.77/50.57 tff(c_22008, plain, (~p(n1, n7, n4))). % 96.77/50.57 tff(c_21998, plain, (~p(n1, n7, n6))). % 96.77/50.57 tff(c_21988, plain, (~p(n1, n7, n9))). % 96.77/50.57 tff(c_21438, plain, (~p(n2, n6, n4))). % 96.77/50.57 tff(c_22022, plain, (~p(n1, n5, n9))). % 96.77/50.57 tff(c_21995, plain, (~p(n1, n7, n7))). % 96.77/50.57 tff(c_22097, plain, (~p(n6, n9, n4))). % 96.77/50.57 tff(c_21799, plain, (~p(n4, n5, n4))). % 96.77/50.57 tff(c_22093, plain, (~p(n7, n9, n4))). % 96.77/50.57 tff(c_22102, plain, (~p(n5, n9, n4))). % 96.77/50.57 tff(c_22106, plain, (~p(n4, n9, n4))). % 96.77/50.57 tff(c_22125, plain, (~p(n6, n9, n8))). % 96.77/50.57 tff(c_22120, plain, (~p(n7, n9, n8))). % 96.77/50.57 tff(c_21865, plain, (~p(n3, n9, n4))). % 96.77/50.57 tff(c_22153, plain, (~p(n1, n9, n8))). % 96.77/50.57 tff(c_22161, plain, (~p(n8, n8, n3))). % 96.77/50.57 tff(c_22165, plain, (~p(n9, n8, n5))). % 96.77/50.57 tff(c_21712, plain, (~p(n5, n3, n8))). % 96.77/50.57 tff(c_22183, plain, (~p(n5, n8, n5))). % 96.77/50.57 tff(c_22170, plain, (~p(n8, n8, n5))). % 96.77/50.57 tff(c_22275, plain, (~p(n5, n7, n1))). % 96.77/50.57 tff(c_22288, plain, (~p(n2, n7, n1))). % 96.77/50.57 tff(c_22242, plain, (~p(n5, n7, n7))). % 96.77/50.57 tff(c_21724, plain, (~p(n5, n3, n5))). % 96.77/50.57 tff(c_22234, plain, (~p(n7, n7, n7))). % 96.77/50.57 tff(c_22251, plain, (~p(n2, n7, n7))). % 96.77/50.57 tff(c_22302, plain, (~p(n7, n6, n3))). % 96.77/50.57 tff(c_21676, plain, (~p(n5, n6, n8))). % 96.77/50.57 tff(c_22310, plain, (~p(n4, n6, n3))). % 96.77/50.57 tff(c_22389, plain, (~p(n9, n4, n7))). % 96.77/50.57 tff(c_22402, plain, (~p(n5, n4, n7))). % 96.77/50.57 tff(c_22381, plain, (~p(n3, n5, n7))). % 96.87/50.57 tff(c_22393, plain, (~p(n8, n4, n7))). % 96.87/50.57 tff(c_21681, plain, (~p(n5, n6, n7))). % 96.87/50.57 tff(c_22346, plain, (~p(n5, n5, n1))). % 96.87/50.57 tff(c_22337, plain, (~p(n7, n5, n1))). % 96.87/50.57 tff(c_22364, plain, (~p(n7, n5, n7))). % 96.87/50.57 tff(c_21691, plain, (~p(n5, n6, n5))). % 96.87/50.57 tff(c_22355, plain, (~p(n2, n5, n1))). % 96.87/50.57 tff(c_22413, plain, (~p(n9, n4, n2))). % 96.87/50.57 tff(c_22508, plain, (~p(n2, n3, n4))). % 96.87/50.57 tff(c_22550, plain, (~p(n8, n2, n5))). % 96.87/50.57 tff(c_22513, plain, (~p(n1, n3, n4))). % 96.87/50.57 tff(c_21700, plain, (~p(n5, n6, n2))). % 96.87/50.57 tff(c_22555, plain, (~p(n7, n2, n5))). % 96.87/50.57 tff(c_22545, plain, (~p(n9, n2, n5))). % 96.87/50.57 tff(c_22540, plain, (~p(n4, n2, n3))). % 96.87/50.57 tff(c_21696, plain, (~p(n5, n6, n4))). % 96.87/50.57 tff(c_22536, plain, (~p(n5, n2, n3))). % 96.87/50.57 tff(c_22527, plain, (~p(n7, n2, n3))). % 96.87/50.57 tff(c_23913, plain, (~p(n6, n2, n9))). % 96.87/50.57 tff(c_23925, plain, (~p(n6, n4, n6))). % 96.87/50.57 tff(c_23873, plain, (~p(n6, n3, n8))). % 96.87/50.57 tff(c_21686, plain, (~p(n5, n6, n6))). % 96.87/50.57 tff(c_21626, plain, (~p(n7, n4, n2))). % 96.87/50.57 tff(c_21618, plain, (~p(n7, n4, n4))). % 96.87/50.57 tff(c_23454, plain, (~p(n8, n8, n1))). % 96.87/50.57 tff(c_21738, plain, (~p(n5, n3, n1))). % 96.87/50.57 tff(c_23461, plain, (~p(n8, n6, n1))). % 96.87/50.57 tff(c_23413, plain, (~p(n9, n2, n4))). % 96.87/50.57 tff(c_21652, plain, (~p(n6, n8, n4))). % 96.87/50.57 tff(c_21647, plain, (~p(n6, n8, n6))). % 96.87/50.57 tff(c_23136, plain, (p(n6, n5, n4))). % 96.87/50.57 tff(c_21733, plain, (~p(n5, n3, n2))). % 96.87/50.57 tff(c_21640, plain, (~p(n6, n8, n8))). % 96.87/50.57 tff(c_22860, plain, (p(n1, n6, n5))). % 96.87/50.57 tff(c_23403, plain, (~p(n9, n6, n4))). % 96.87/50.57 tff(c_21729, plain, (~p(n5, n3, n3))). % 96.87/50.57 tff(c_23112, plain, (~p(n6, n6, n6))). % 96.87/50.57 tff(c_23385, plain, (~p(n1, n1, n1))). % 96.87/50.57 tff(c_23380, plain, (~p(n2, n1, n4))). % 96.87/50.57 tff(c_23375, plain, (~p(n2, n1, n6))). % 96.87/50.58 tff(c_23330, plain, (~p(n7, n1, n6))). % 96.87/50.58 tff(c_21717, plain, (~p(n5, n3, n7))). % 96.87/50.58 tff(c_23049, plain, (~p(n6, n3, n7))). % 96.87/50.58 tff(c_23319, plain, (~p(n6, n1, n5))). % 96.87/50.58 tff(c_23301, plain, (~p(n6, n1, n1))). % 96.87/50.58 tff(c_21774, plain, (~p(n4, n7, n1))). % 96.87/50.58 tff(c_23295, plain, (~p(n7, n1, n1))). % 96.87/50.58 tff(c_23259, plain, (~p(n1, n2, n4))). % 96.87/50.58 tff(c_23255, plain, (~p(n3, n1, n1))). % 96.87/50.58 tff(c_23251, plain, (~p(n3, n1, n3))). % 96.87/50.58 tff(c_23249, plain, (~p(n3, n1, n6))). % 96.87/50.58 tff(c_21635, plain, (~p(n6, n8, n9))). % 96.87/50.58 tff(c_23247, plain, (~p(n3, n1, n7))). % 96.87/50.58 tff(c_23245, plain, (~p(n3, n1, n8))). % 96.87/50.58 tff(c_23243, plain, (~p(n3, n1, n9))). % 96.87/50.58 tff(c_21341, plain, (~p(n5, n3, n6))). % 96.87/50.58 tff(c_23239, plain, (~p(n9, n7, n4))). % 96.87/50.58 tff(c_23237, plain, (~p(n2, n7, n2))). % 96.87/50.58 tff(c_23226, plain, (p(n3, n1, n4))). % 96.87/50.58 tff(c_23196, plain, (~p(n5, n8, n4))). % 96.87/50.58 tff(c_23193, plain, (~p(n9, n8, n4))). % 96.87/50.58 tff(c_21657, plain, (~p(n6, n8, n3))). % 96.87/50.58 tff(c_23145, plain, (~p(n6, n5, n2))). % 96.87/50.58 tff(c_23158, plain, (p(n4, n8, n4))). % 96.87/50.58 tff(c_23150, plain, (~p(n8, n5, n4))). % 96.87/50.58 tff(c_21345, plain, (~p(n4, n1, n4))). % 96.87/50.58 tff(c_23152, plain, (~p(n7, n5, n4))). % 96.87/50.58 tff(c_21769, plain, (~p(n4, n7, n2))). % 96.87/50.58 tff(c_21764, plain, (~p(n4, n7, n3))). % 96.87/50.58 tff(c_21759, plain, (~p(n4, n7, n4))). % 96.87/50.58 tff(c_21753, plain, (~p(n4, n7, n6))). % 96.87/50.58 tff(c_21666, plain, (~p(n6, n8, n1))). % 96.87/50.58 tff(c_21748, plain, (~p(n4, n7, n8))). % 96.87/50.58 tff(c_21743, plain, (~p(n4, n7, n9))). % 96.87/50.58 tff(c_21794, plain, (~p(n4, n5, n5))). % 96.87/50.58 tff(c_21661, plain, (~p(n6, n8, n2))). % 96.87/50.58 tff(c_21790, plain, (~p(n4, n5, n6))). % 96.87/50.58 tff(c_21787, plain, (~p(n4, n5, n7))). % 96.87/50.58 tff(c_21782, plain, (~p(n4, n5, n8))). % 96.87/50.58 tff(c_21869, plain, (~p(n3, n9, n3))). % 96.87/50.58 tff(c_21873, plain, (~p(n3, n9, n2))). % 96.87/50.58 tff(c_21598, plain, (~p(n7, n4, n9))). % 96.87/50.58 tff(c_21850, plain, (~p(n3, n9, n7))). % 96.87/50.58 tff(c_21860, plain, (~p(n3, n9, n5))). % 96.87/50.58 tff(c_21845, plain, (~p(n3, n9, n9))). % 96.87/50.58 tff(c_21613, plain, (~p(n7, n4, n5))). % 96.87/50.58 tff(c_21842, plain, (~p(n4, n1, n1))). % 96.87/50.58 tff(c_21825, plain, (~p(n4, n1, n5))). % 96.87/50.58 tff(c_21821, plain, (~p(n4, n1, n7))). % 96.87/50.58 tff(c_21816, plain, (~p(n4, n1, n8))). % 96.87/50.58 tff(c_23057, plain, (~p(n5, n2, n4))). % 96.87/50.58 tff(c_21622, plain, (~p(n7, n4, n3))). % 96.87/50.58 tff(c_23055, plain, (~p(n5, n2, n8))). % 96.87/50.58 tff(c_23013, plain, (~p(n6, n3, n5))). % 96.87/50.58 tff(c_23027, plain, (~p(n5, n1, n1))). % 96.87/50.58 tff(c_21630, plain, (~p(n7, n4, n1))). % 96.87/50.58 tff(c_23023, plain, (~p(n5, n1, n4))). % 96.87/50.58 tff(c_22874, plain, (~p(n1, n6, n4))). % 96.87/50.58 tff(c_23011, plain, (p(n5, n1, n5))). % 96.87/50.58 tff(c_21902, plain, (~p(n3, n2, n4))). % 96.87/50.58 tff(c_21912, plain, (~p(n3, n2, n1))). % 96.87/50.58 tff(c_21529, plain, (~p(n8, n1, n8))). % 96.87/50.58 tff(c_21894, plain, (~p(n3, n2, n6))). % 96.87/50.58 tff(c_22891, plain, (~p(n2, n6, n5))). % 96.87/50.58 tff(c_21885, plain, (~p(n3, n2, n8))). % 96.87/50.58 tff(c_21534, plain, (~p(n8, n1, n7))). % 96.87/50.58 tff(c_22941, plain, (~p(n7, n7, n5))). % 96.87/50.58 tff(c_22957, plain, (~p(n5, n4, n5))). % 96.87/50.58 tff(c_22955, plain, (~p(n6, n4, n5))). % 96.87/50.58 tff(c_22065, plain, (~p(n1, n4, n7))). % 96.87/50.58 tff(c_22052, plain, (~p(n1, n5, n1))). % 96.87/50.58 tff(c_21543, plain, (~p(n8, n1, n5))). % 96.87/50.58 tff(c_22027, plain, (~p(n1, n5, n8))). % 96.87/50.58 tff(c_22037, plain, (~p(n1, n5, n5))). % 96.87/50.58 tff(c_22032, plain, (~p(n1, n5, n6))). % 96.87/50.58 tff(c_21553, plain, (~p(n8, n1, n3))). % 96.87/50.58 tff(c_22085, plain, (~p(n1, n4, n1))). % 96.87/50.58 tff(c_21971, plain, (~p(n2, n2, n4))). % 96.87/50.58 tff(c_21961, plain, (~p(n2, n2, n7))). % 96.87/50.58 tff(c_21979, plain, (~p(n2, n2, n2))). % 96.87/50.58 tff(c_21983, plain, (~p(n2, n2, n1))). % 96.87/50.58 tff(c_21548, plain, (~p(n8, n1, n4))). % 96.87/50.58 tff(c_21946, plain, (~p(n2, n4, n1))). % 96.87/50.58 tff(c_21938, plain, (~p(n2, n4, n4))). % 96.87/50.58 tff(c_21929, plain, (~p(n2, n4, n6))). % 96.87/50.58 tff(c_21539, plain, (~p(n8, n1, n6))). % 96.87/50.58 tff(c_21956, plain, (~p(n2, n2, n8))). % 96.87/50.58 tff(c_21951, plain, (~p(n2, n2, n9))). % 96.87/50.58 tff(c_22077, plain, (~p(n1, n4, n3))). % 96.87/50.58 tff(c_22060, plain, (~p(n1, n4, n8))). % 96.87/50.58 tff(c_22072, plain, (~p(n1, n4, n5))). % 96.87/50.58 tff(c_21563, plain, (~p(n7, n8, n9))). % 96.87/50.58 tff(c_22055, plain, (~p(n1, n4, n9))). % 96.87/50.58 tff(c_22045, plain, (~p(n1, n5, n3))). % 96.87/50.58 tff(c_22017, plain, (~p(n1, n7, n2))). % 96.87/50.58 tff(c_21568, plain, (~p(n7, n8, n8))). % 96.87/50.58 tff(c_22012, plain, (~p(n1, n7, n3))). % 96.87/50.59 tff(c_22003, plain, (~p(n1, n7, n5))). % 96.87/50.59 tff(c_22781, plain, (~p(n6, n7, n8))). % 96.87/50.59 tff(c_22768, plain, (~p(n6, n7, n5))). % 96.87/50.59 tff(c_22774, plain, (~p(n7, n7, n3))). % 96.87/50.59 tff(c_21573, plain, (~p(n7, n8, n7))). % 96.87/50.59 tff(c_22770, plain, (~p(n6, n7, n4))). % 96.87/50.59 tff(c_22758, plain, (~p(n9, n4, n3))). % 96.87/50.59 tff(c_22219, plain, (~p(n1, n8, n5))). % 96.87/50.59 tff(c_21582, plain, (~p(n7, n8, n5))). % 96.87/50.59 tff(c_22149, plain, (~p(n1, n9, n4))). % 96.87/50.59 tff(c_22135, plain, (~p(n4, n9, n8))). % 96.87/50.59 tff(c_22140, plain, (~p(n2, n9, n4))). % 96.87/50.59 tff(c_22130, plain, (~p(n5, n9, n8))). % 96.87/50.59 tff(c_22205, plain, (~p(n2, n8, n3))). % 96.87/50.59 tff(c_22517, plain, (~p(n9, n2, n3))). % 96.87/50.59 tff(c_22145, plain, (~p(n2, n9, n8))). % 96.87/50.59 tff(c_22210, plain, (~p(n2, n8, n5))). % 96.87/50.59 tff(c_22157, plain, (~p(n9, n8, n3))). % 96.87/50.59 tff(c_22522, plain, (~p(n8, n2, n3))). % 96.87/50.59 tff(c_22196, plain, (~p(n3, n8, n3))). % 96.87/50.59 tff(c_22200, plain, (~p(n3, n8, n5))). % 96.87/50.59 tff(c_22192, plain, (~p(n4, n8, n5))). % 96.87/50.59 tff(c_22179, plain, (~p(n5, n8, n3))). % 96.87/50.59 tff(c_22187, plain, (~p(n4, n8, n3))). % 96.87/50.59 tff(c_22531, plain, (~p(n6, n2, n3))). % 96.87/50.59 tff(c_22214, plain, (~p(n1, n8, n3))). % 96.87/50.59 tff(c_22766, plain, (~p(n6, n7, n9))). % 96.87/50.59 tff(c_22752, plain, (~p(n8, n4, n6))). % 96.87/50.59 tff(c_22328, plain, (~p(n9, n5, n1))). % 96.87/50.59 tff(c_22750, plain, (~p(n8, n4, n8))). % 96.87/50.59 tff(c_22306, plain, (~p(n6, n6, n3))). % 96.87/50.59 tff(c_22270, plain, (~p(n6, n7, n1))). % 96.87/50.59 tff(c_22284, plain, (~p(n3, n7, n1))). % 96.87/50.59 tff(c_22246, plain, (~p(n3, n7, n7))). % 96.87/50.59 tff(c_22333, plain, (~p(n8, n5, n1))). % 96.87/50.59 tff(c_22265, plain, (~p(n7, n7, n1))). % 96.87/50.59 tff(c_22261, plain, (~p(n8, n7, n1))). % 96.87/50.59 tff(c_22256, plain, (~p(n9, n7, n1))). % 96.87/50.59 tff(c_22342, plain, (~p(n6, n5, n1))). % 96.87/50.59 tff(c_22297, plain, (~p(n8, n6, n3))). % 96.87/50.59 tff(c_22292, plain, (~p(n9, n6, n3))). % 96.87/50.59 tff(c_22688, plain, (~p(n3, n3, n3))). % 96.87/50.59 tff(c_22685, plain, (~p(n6, n3, n3))). % 96.87/50.59 tff(c_22314, plain, (~p(n3, n6, n3))). % 96.87/50.59 tff(c_22323, plain, (~p(n1, n6, n3))). % 96.87/50.59 tff(c_22679, plain, (~p(n9, n3, n3))). % 96.87/50.59 tff(c_22674, plain, (~p(n4, n3, n6))). % 96.87/50.59 tff(c_22495, plain, (~p(n6, n3, n4))). % 96.87/50.59 tff(c_22318, plain, (~p(n2, n6, n3))). % 96.87/50.59 tff(c_22485, plain, (~p(n8, n3, n4))). % 96.87/50.59 tff(c_22481, plain, (~p(n9, n3, n4))). % 96.87/50.59 tff(c_22490, plain, (~p(n7, n3, n4))). % 96.87/50.59 tff(c_22450, plain, (~p(n8, n4, n4))). % 96.87/50.59 tff(c_22468, plain, (~p(n4, n4, n4))). % 96.87/50.59 tff(c_22229, plain, (~p(n8, n7, n7))). % 96.87/50.59 tff(c_22464, plain, (~p(n5, n4, n4))). % 96.87/50.59 tff(c_22473, plain, (~p(n3, n4, n4))). % 96.87/50.59 tff(c_22459, plain, (~p(n6, n4, n4))). % 96.87/50.59 tff(c_22238, plain, (~p(n6, n7, n7))). % 96.87/50.59 tff(c_22397, plain, (~p(n6, n4, n7))). % 96.87/50.59 tff(c_22385, plain, (~p(n2, n5, n7))). % 96.87/50.59 tff(c_22372, plain, (~p(n5, n5, n7))). % 96.87/50.59 tff(c_22350, plain, (~p(n3, n5, n1))). % 96.87/50.59 tff(c_22367, plain, (~p(n6, n5, n7))). % 96.87/50.59 tff(c_22115, plain, (~p(n8, n9, n8))). % 96.87/50.59 tff(c_22407, plain, (~p(n4, n4, n7))). % 96.87/50.59 tff(c_22446, plain, (~p(n9, n4, n4))). % 96.87/50.59 tff(c_22442, plain, (~p(n3, n4, n2))). % 96.87/50.59 tff(c_22089, plain, (~p(n8, n9, n4))). % 96.87/50.59 tff(c_22437, plain, (~p(n4, n4, n2))). % 96.87/50.59 tff(c_22432, plain, (~p(n5, n4, n2))). % 96.87/50.59 tff(c_22427, plain, (~p(n6, n4, n2))). % 96.87/50.59 tff(c_22418, plain, (~p(n8, n4, n2))). % 96.87/50.59 tff(c_22499, plain, (~p(n4, n3, n4))). % 96.87/50.59 tff(c_21519, plain, (~p(n9, n9, n1))). % 96.87/50.59 tff(c_22608, plain, (~p(n2, n9, n3))). % 96.87/50.59 tff(c_22503, plain, (~p(n3, n3, n4))). % 96.87/50.59 tff(c_22603, plain, (~p(n5, n9, n3))). % 96.87/50.59 tff(c_21514, plain, (~p(n9, n9, n2))). % 96.87/50.59 tff(c_22601, plain, (~p(n6, n9, n3))). % 96.87/50.59 tff(c_22599, plain, (~p(n7, n9, n3))). % 96.87/50.59 tff(c_22597, plain, (~p(n1, n9, n1))). % 96.87/50.59 tff(c_22595, plain, (~p(n1, n9, n2))). % 96.87/50.59 tff(c_24212, plain, (~p(n1, n8, n7))). % 96.87/50.59 tff(c_21483, plain, (~p(n1, n1, n5))). % 96.87/50.59 tff(c_22593, plain, (~p(n1, n9, n5))). % 96.87/50.59 tff(c_22591, plain, (~p(n1, n9, n6))). % 96.87/50.59 tff(c_22582, plain, (~p(n2, n7, n3))). % 96.87/50.59 tff(c_21478, plain, (~p(n1, n1, n3))). % 96.87/50.59 tff(c_22589, plain, (~p(n1, n9, n7))). % 96.87/50.59 tff(c_22587, plain, (~p(n1, n9, n9))). % 96.87/50.59 tff(c_22584, plain, (~p(n3, n7, n3))). % 96.87/50.59 tff(c_22569, plain, (~p(n4, n2, n5))). % 96.87/50.59 tff(c_22564, plain, (~p(n5, n2, n5))). % 96.87/50.59 tff(c_21245, plain, (~p(n5, n7, n5))). % 96.87/50.59 tff(c_22560, plain, (~p(n6, n2, n5))). % 96.87/50.59 tff(c_22580, plain, (p(n1, n9, n3))). % 96.87/50.59 tff(c_22578, plain, (~p(n1, n2, n3))). % 96.87/50.59 tff(c_21493, plain, (~p(n9, n9, n8))). % 96.87/50.59 tff(c_23841, plain, (~p(n6, n3, n1))). % 96.87/50.59 tff(c_23994, plain, (~p(n2, n8, n2))). % 96.87/50.59 tff(c_23992, plain, (~p(n2, n8, n7))). % 96.87/50.59 tff(c_23521, plain, (~p(n6, n9, n5))). % 96.87/50.59 tff(c_23990, plain, (~p(n3, n8, n6))). % 96.87/50.59 tff(c_21488, plain, (~p(n9, n9, n9))). % 96.87/50.59 tff(c_23988, plain, (~p(n8, n8, n6))). % 96.87/50.59 tff(c_23976, plain, (p(n2, n8, n6))). % 96.87/50.59 tff(c_23849, plain, (~p(n2, n3, n9))). % 96.87/50.59 tff(c_21473, plain, (~p(n1, n3, n5))). % 96.87/50.59 tff(c_23969, plain, (~p(n8, n9, n6))). % 96.87/50.59 tff(c_23844, plain, (~p(n3, n3, n1))). % 96.87/50.59 tff(c_23967, plain, (~p(n7, n9, n6))). % 96.87/50.59 tff(c_23851, plain, (~p(n2, n3, n8))). % 96.87/50.59 tff(c_23837, plain, (~p(n2, n3, n5))). % 96.87/50.59 tff(c_21463, plain, (~p(n2, n1, n3))). % 96.87/50.59 tff(c_23963, plain, (~p(n5, n9, n6))). % 96.87/50.59 tff(c_23857, plain, (~p(n8, n2, n8))). % 96.87/50.60 tff(c_23961, plain, (~p(n6, n9, n9))). % 96.87/50.60 tff(c_21240, plain, (~p(n5, n9, n5))). % 96.87/50.60 tff(c_23959, plain, (~p(n6, n9, n2))). % 96.87/50.60 tff(c_23865, plain, (~p(n4, n2, n9))). % 96.87/50.60 tff(c_23839, plain, (~p(n2, n3, n2))). % 96.87/50.60 tff(c_23957, plain, (~p(n2, n9, n6))). % 96.87/50.60 tff(c_23859, plain, (~p(n7, n2, n8))). % 96.87/50.60 tff(c_21453, plain, (~p(n3, n3, n5))). % 96.87/50.60 tff(c_23955, plain, (~p(n5, n8, n6))). % 96.87/50.60 tff(c_23921, plain, (p(n6, n4, n8))). % 96.87/50.60 tff(c_23855, plain, (~p(n9, n2, n8))). % 96.87/50.60 tff(c_21443, plain, (~p(n2, n5, n4))). % 96.87/50.60 tff(c_23953, plain, (~p(n5, n7, n6))). % 96.87/50.60 tff(c_23944, plain, (p(n6, n9, n6))). % 96.87/50.60 tff(c_23931, plain, (~p(n5, n4, n8))). % 96.87/50.60 tff(c_23929, plain, (~p(n9, n4, n8))). % 96.87/50.60 tff(c_23911, plain, (~p(n6, n2, n2))). % 96.87/50.60 tff(c_21421, plain, (~p(n2, n4, n7))). % 96.87/50.60 tff(c_23505, plain, (~p(n7, n3, n7))). % 96.87/50.60 tff(c_23927, plain, (~p(n5, n5, n8))). % 96.87/50.60 tff(c_23915, plain, (~p(n6, n9, n1))). % 96.87/50.60 tff(c_21416, plain, (~p(n2, n6, n7))). % 96.87/50.60 tff(c_23923, plain, (~p(n6, n4, n9))). % 96.87/50.60 tff(c_23867, plain, (~p(n4, n2, n2))). % 96.87/50.60 tff(c_23861, plain, (~p(n6, n2, n8))). % 96.87/50.60 tff(c_23879, plain, (p(n6, n2, n1))). % 96.87/50.60 tff(c_23863, plain, (~p(n1, n2, n8))). % 96.87/50.60 tff(c_21407, plain, (~p(n3, n6, n7))). % 96.87/50.60 tff(c_23488, plain, (~p(n7, n9, n7))). % 96.87/50.60 tff(c_23871, plain, (~p(n6, n1, n8))). % 96.87/50.60 tff(c_23472, plain, (~p(n8, n3, n1))). % 96.87/50.60 tff(c_21428, plain, (~p(n3, n6, n4))). % 96.87/50.60 tff(c_23449, plain, (~p(n8, n9, n1))). % 96.87/50.60 tff(c_23476, plain, (~p(n8, n2, n1))). % 96.87/50.60 tff(c_23181, plain, (~p(n5, n7, n4))). % 96.87/50.60 tff(c_22858, plain, (~p(n1, n2, n5))). % 96.87/50.60 tff(c_22834, plain, (~p(n9, n1, n4))). % 96.87/50.60 tff(c_21397, plain, (~p(n3, n5, n2))). % 96.87/50.60 tff(c_23139, plain, (~p(n4, n6, n4))). % 96.87/50.60 tff(c_23108, plain, (~p(n6, n6, n9))). % 96.87/50.60 tff(c_23106, plain, (~p(n7, n6, n7))). % 96.87/50.60 tff(c_21806, plain, (~p(n4, n5, n2))). % 96.87/50.60 tff(c_22862, plain, (~p(n3, n5, n5))). % 96.87/50.60 tff(c_23351, plain, (~p(n7, n1, n4))). % 96.87/50.60 tff(c_23051, plain, (~p(n6, n1, n7))). % 96.87/50.60 tff(c_23391, plain, (~p(n1, n1, n6))). % 96.87/50.60 tff(c_23396, plain, (~p(n1, n1, n4))). % 96.87/50.60 tff(c_21707, plain, (~p(n5, n3, n9))). % 96.87/50.60 tff(c_23372, plain, (~p(n2, n1, n5))). % 96.87/50.60 tff(c_23367, plain, (~p(n2, n1, n1))). % 96.87/50.60 tff(c_23335, plain, (~p(n6, n1, n6))). % 96.87/50.60 tff(c_21671, plain, (~p(n5, n6, n9))). % 96.87/50.60 tff(c_22864, plain, (~p(n3, n4, n5))). % 96.87/50.60 tff(c_23110, plain, (~p(n6, n6, n8))). % 96.87/50.60 tff(c_23191, plain, (~p(n4, n8, n2))). % 96.87/50.60 tff(c_23053, plain, (~p(n5, n2, n9))). % 96.87/50.60 tff(c_23314, plain, (~p(n7, n1, n5))). % 96.87/50.60 tff(c_21373, plain, (~p(n3, n9, n1))). % 96.87/50.60 tff(c_23253, plain, (~p(n3, n1, n2))). % 96.87/50.60 tff(c_23292, plain, (~p(n7, n1, n3))). % 96.87/50.60 tff(c_23039, plain, (p(n5, n2, n7))). % 96.87/50.60 tff(c_21382, plain, (~p(n2, n9, n1))). % 96.87/50.60 tff(c_23202, plain, (~p(n1, n8, n4))). % 96.87/50.60 tff(c_23185, plain, (~p(n4, n8, n8))). % 96.87/50.60 tff(c_23189, plain, (~p(n4, n8, n6))). % 96.87/50.60 tff(c_23066, plain, (~p(n8, n2, n7))). % 96.87/50.60 tff(c_23198, plain, (~p(n3, n8, n4))). % 96.87/50.60 tff(c_21225, plain, (~p(n9, n2, n1))). % 96.87/50.60 tff(c_23235, plain, (~p(n2, n7, n6))). % 96.87/50.60 tff(c_23233, plain, (~p(n2, n7, n9))). % 96.87/50.60 tff(c_23231, plain, (p(n2, n7, n4))). % 96.87/50.60 tff(c_21377, plain, (~p(n3, n8, n1))). % 96.87/50.60 tff(c_23205, plain, (~p(n4, n8, n1))). % 96.87/50.60 tff(c_23200, plain, (~p(n2, n8, n4))). % 96.87/50.60 tff(c_23183, plain, (~p(n4, n8, n9))). % 96.87/50.60 tff(c_23187, plain, (~p(n4, n8, n7))). % 96.87/50.60 tff(c_23157, plain, (~p(n6, n5, n8))). % 96.87/50.60 tff(c_21359, plain, (~p(n2, n7, n8))). % 96.87/50.60 tff(c_23154, plain, (~p(n5, n5, n4))). % 96.87/50.60 tff(c_23148, plain, (~p(n9, n5, n4))). % 96.87/50.60 tff(c_23143, plain, (~p(n6, n5, n6))). % 96.87/50.60 tff(c_21349, plain, (~p(n5, n2, n6))). % 96.87/50.60 tff(c_23141, plain, (~p(n6, n5, n9))). % 96.87/50.60 tff(c_23118, plain, (~p(n6, n6, n4))). % 96.87/50.60 tff(c_23116, plain, (~p(n4, n6, n7))). % 96.87/50.60 tff(c_23114, plain, (~p(n6, n6, n2))). % 96.87/50.60 tff(c_22866, plain, (~p(n1, n6, n9))). % 96.87/50.60 tff(c_21336, plain, (~p(n6, n2, n6))). % 96.87/50.60 tff(c_22822, plain, (~p(n9, n1, n7))). % 96.87/50.60 tff(c_23025, plain, (~p(n5, n1, n2))). % 96.87/50.60 tff(c_23021, plain, (~p(n5, n1, n6))). % 96.87/50.60 tff(c_21216, plain, (~p(n8, n5, n7))). % 96.87/50.60 tff(c_23019, plain, (~p(n5, n1, n7))). % 96.87/50.60 tff(c_23104, plain, (p(n6, n6, n7))). % 96.87/50.60 tff(c_23075, plain, (~p(n1, n2, n7))). % 96.87/50.60 tff(c_23070, plain, (~p(n6, n2, n7))). % 96.87/50.60 tff(c_23072, plain, (~p(n4, n2, n7))). % 96.87/50.60 tff(c_21211, plain, (~p(n8, n6, n7))). % 96.87/50.60 tff(c_23068, plain, (~p(n7, n2, n7))). % 96.87/50.60 tff(c_23061, plain, (~p(n5, n2, n1))). % 96.87/50.60 tff(c_23059, plain, (~p(n5, n2, n2))). % 96.87/50.60 tff(c_21326, plain, (~p(n4, n2, n4))). % 96.87/50.60 tff(c_23064, plain, (~p(n9, n2, n7))). % 96.87/50.60 tff(c_23017, plain, (~p(n5, n1, n8))). % 96.87/50.60 tff(c_22870, plain, (~p(n1, n6, n7))). % 96.87/50.60 tff(c_22868, plain, (~p(n1, n6, n8))). % 96.87/50.60 tff(c_23015, plain, (~p(n5, n1, n9))). % 96.87/50.60 tff(c_21608, plain, (~p(n7, n4, n6))). % 96.87/50.60 tff(c_22872, plain, (~p(n1, n6, n6))). % 96.87/50.60 tff(c_22889, plain, (~p(n3, n6, n5))). % 96.87/50.60 tff(c_22880, plain, (~p(n8, n6, n5))). % 96.87/50.60 tff(c_21524, plain, (~p(n8, n1, n9))). % 96.87/50.60 tff(c_22887, plain, (~p(n4, n6, n5))). % 96.87/50.60 tff(c_22878, plain, (~p(n9, n6, n5))). % 96.87/50.60 tff(c_22920, plain, (p(n4, n4, n5))). % 96.87/50.60 tff(c_22882, plain, (~p(n7, n6, n5))). % 96.87/50.60 tff(c_22923, plain, (p(n3, n7, n5))). % 96.87/50.60 tff(c_21321, plain, (~p(n6, n1, n4))). % 96.87/50.60 tff(c_22925, plain, (~p(n2, n9, n5))). % 96.87/50.60 tff(c_22927, plain, (~p(n3, n7, n9))). % 96.87/50.60 tff(c_22931, plain, (~p(n3, n7, n6))). % 96.87/50.60 tff(c_21558, plain, (~p(n8, n1, n2))). % 96.87/50.60 tff(c_22966, plain, (~p(n4, n4, n8))). % 96.87/50.60 tff(c_22964, plain, (~p(n4, n4, n9))). % 96.87/50.60 tff(c_22962, plain, (~p(n4, n4, n1))). % 96.87/50.60 tff(c_22960, plain, (~p(n4, n4, n6))). % 96.87/50.60 tff(c_22953, plain, (~p(n9, n4, n5))). % 96.87/50.60 tff(c_21311, plain, (~p(n4, n4, n3))). % 96.87/50.60 tff(c_22951, plain, (~p(n5, n5, n5))). % 96.87/50.60 tff(c_22949, plain, (~p(n6, n5, n5))). % 96.87/50.60 tff(c_22943, plain, (~p(n2, n7, n5))). % 96.87/50.60 tff(c_21302, plain, (~p(n5, n6, n1))). % 96.87/50.60 tff(c_22939, plain, (~p(n8, n7, n5))). % 96.87/50.60 tff(c_22937, plain, (~p(n9, n7, n5))). % 96.87/50.60 tff(c_22935, plain, (~p(n3, n7, n2))). % 96.87/50.60 tff(c_22933, plain, (~p(n3, n7, n4))). % 96.87/50.60 tff(c_22929, plain, (~p(n3, n7, n8))). % 96.87/50.60 tff(c_21293, plain, (~p(n6, n4, n1))). % 96.87/50.60 tff(c_22884, plain, (~p(n6, n6, n5))). % 96.87/50.60 tff(c_22756, plain, (~p(n8, n4, n1))). % 96.87/50.60 tff(c_22772, plain, (~p(n6, n7, n2))). % 96.87/50.60 tff(c_21577, plain, (~p(n7, n8, n6))). % 96.87/50.60 tff(c_22776, plain, (~p(n5, n7, n3))). % 96.87/50.60 tff(c_22876, plain, (~p(n1, n6, n1))). % 96.87/50.60 tff(c_22779, plain, (~p(n6, n7, n6))). % 96.87/50.60 tff(c_22754, plain, (~p(n8, n4, n5))). % 96.87/50.60 tff(c_22764, plain, (p(n6, n7, n3))). % 96.87/50.60 tff(c_21588, plain, (~p(n7, n8, n2))). % 96.87/50.60 tff(c_22760, plain, (~p(n5, n4, n3))). % 96.87/50.61 tff(c_22695, plain, (~p(n4, n3, n2))). % 96.87/50.61 tff(c_22693, plain, (~p(n4, n3, n5))). % 96.87/50.61 tff(c_21593, plain, (~p(n7, n8, n1))). % 96.87/50.61 tff(c_22691, plain, (~p(n4, n3, n8))). % 96.87/50.61 tff(c_22746, plain, (p(n8, n4, n3))). % 96.87/50.61 tff(c_22799, plain, (p(n9, n1, n3))). % 96.87/50.61 tff(c_22748, plain, (~p(n8, n4, n9))). % 96.87/50.61 tff(c_22820, plain, (~p(n9, n1, n9))). % 96.87/50.61 tff(c_21283, plain, (~p(n6, n4, n3))). % 96.87/50.61 tff(c_22683, plain, (~p(n7, n3, n3))). % 96.87/50.61 tff(c_22824, plain, (~p(n9, n1, n5))). % 96.87/50.61 tff(c_22681, plain, (~p(n8, n3, n3))). % 96.87/50.61 tff(c_21273, plain, (~p(n5, n8, n7))). % 96.87/50.61 tff(c_22826, plain, (~p(n9, n1, n2))). % 96.87/50.61 tff(c_22676, plain, (~p(n4, n3, n1))). % 96.87/50.61 tff(c_22828, plain, (~p(n9, n1, n8))). % 96.87/50.61 tff(c_22830, plain, (~p(n9, n1, n1))). % 96.87/50.61 tff(c_22672, plain, (~p(n4, n3, n7))). % 96.87/50.61 tff(c_21260, plain, (~p(n6, n8, n7))). % 96.87/50.61 tff(c_22832, plain, (~p(n9, n1, n6))). % 96.87/50.61 tff(c_22670, plain, (~p(n4, n3, n9))). % 96.87/50.61 tff(c_22666, plain, (~p(n6, n1, n3))). % 96.87/50.61 tff(c_21264, plain, (~p(n4, n7, n5))). % 96.87/50.61 tff(c_22668, plain, (~p(n5, n1, n3))). % 96.87/50.61 tff(c_22646, plain, (~p(n2, n5, n6))). % 96.87/50.61 tff(c_22660, plain, (~p(n5, n5, n3))). % 96.87/50.61 tff(c_22662, plain, (~p(n3, n5, n3))). % 96.87/50.61 tff(c_22658, plain, (~p(n7, n5, n3))). % 96.87/50.61 tff(c_22224, plain, (~p(n9, n7, n7))). % 96.87/50.61 tff(c_22644, plain, (~p(n2, n5, n8))). % 96.87/50.61 tff(c_22656, plain, (~p(n8, n5, n3))). % 96.87/50.61 tff(c_22648, plain, (~p(n2, n5, n5))). % 96.87/50.61 tff(c_21250, plain, (~p(n4, n9, n5))). % 96.87/50.61 tff(c_22654, plain, (~p(n9, n5, n3))). % 96.87/50.61 tff(c_22650, plain, (~p(n2, n5, n2))). % 96.87/50.61 tff(c_22638, plain, (p(n2, n5, n3))). % 96.87/50.61 tff(c_22642, plain, (~p(n2, n5, n9))). % 96.87/50.61 tff(c_22640, plain, (~p(n3, n4, n3))). % 96.87/50.61 tff(c_21192, plain, (~p(n8, n7, n3))). % 96.87/50.61 tff(c_22605, plain, (~p(n4, n9, n3))). % 96.87/50.61 tff(c_22635, plain, (p(n4, n3, n3))). % 96.87/50.61 tff(c_24419, plain, (~p(n8, n6, n9))). % 96.87/50.61 tff(c_21468, plain, (~p(n1, n3, n3))). % 96.87/50.61 tff(c_24417, plain, (~p(n9, n6, n9))). % 96.87/50.61 tff(c_24415, plain, (~p(n5, n4, n9))). % 96.87/50.61 tff(c_24411, plain, (~p(n4, n6, n2))). % 96.87/50.61 tff(c_24409, plain, (~p(n5, n9, n2))). % 96.87/50.61 tff(c_24407, plain, (~p(n7, n9, n2))). % 96.87/50.61 tff(c_21182, plain, (~p(n9, n7, n3))). % 96.87/50.61 tff(c_24405, plain, (~p(n5, n7, n2))). % 96.87/50.61 tff(c_24391, plain, (~p(n5, n8, n2))). % 96.87/50.61 tff(c_24389, plain, (~p(n8, n8, n2))). % 96.87/50.61 tff(c_21178, plain, (~p(n9, n9, n3))). % 96.87/50.61 tff(c_24387, plain, (~p(n9, n8, n2))). % 96.87/50.61 tff(c_24385, plain, (~p(n1, n1, n2))). % 96.87/50.61 tff(c_24381, plain, (~p(n3, n3, n9))). % 96.87/50.61 tff(c_24378, plain, (~p(n6, n3, n2))). % 96.87/50.61 tff(c_24376, plain, (~p(n7, n3, n2))). % 96.87/50.61 tff(c_21412, plain, (~p(n3, n4, n7))). % 96.87/50.61 tff(c_24374, plain, (~p(n8, n3, n2))). % 96.87/50.61 tff(c_24370, plain, (~p(n1, n2, n2))). % 96.87/50.61 tff(c_24368, plain, (~p(n3, n3, n6))). % 96.87/50.61 tff(c_21402, plain, (~p(n1, n6, n2))). % 96.87/50.61 tff(c_24366, plain, (~p(n1, n3, n2))). % 96.87/50.61 tff(c_24363, plain, (~p(n9, n3, n2))). % 96.87/50.61 tff(c_24361, plain, (~p(n9, n3, n5))). % 96.87/50.61 tff(c_24359, plain, (~p(n9, n3, n6))). % 96.87/50.61 tff(c_24347, plain, (p(n7, n9, n5))). % 96.87/50.61 tff(c_21392, plain, (~p(n3, n6, n2))). % 96.87/50.61 tff(c_24357, plain, (~p(n9, n3, n8))). % 96.87/50.61 tff(c_24355, plain, (~p(n9, n3, n9))). % 96.87/50.61 tff(c_24343, plain, (p(n4, n9, n2))). % 96.87/50.61 tff(c_21387, plain, (~p(n2, n8, n1))). % 96.87/50.61 tff(c_24344, plain, (p(n4, n6, n9))). % 96.87/50.61 tff(c_24334, plain, (p(n1, n8, n2))). % 96.87/50.61 tff(c_24333, plain, (p(n3, n3, n2))). % 96.87/50.61 tff(c_24318, plain, (~p(n8, n9, n2))). % 96.87/50.61 tff(c_24330, plain, (p(n9, n3, n7))). % 96.87/50.61 tff(c_21369, plain, (~p(n1, n7, n8))). % 96.87/50.61 tff(c_24325, plain, (~p(n8, n3, n7))). % 96.87/50.61 tff(c_24316, plain, (~p(n8, n9, n5))). % 96.87/50.61 tff(c_24310, plain, (~p(n1, n8, n9))). % 96.87/50.61 tff(c_21220, plain, (~p(n9, n3, n1))). % 96.87/50.61 tff(c_24308, plain, (~p(n4, n9, n9))). % 96.87/50.61 tff(c_24306, plain, (~p(n5, n9, n9))). % 96.87/50.61 tff(c_24304, plain, (~p(n7, n9, n9))). % 96.87/50.61 tff(c_24298, plain, (~p(n3, n8, n9))). % 96.87/50.61 tff(c_24302, plain, (~p(n8, n9, n9))). % 96.87/50.61 tff(c_21364, plain, (~p(n1, n8, n8))). % 96.87/50.61 tff(c_24294, plain, (~p(n3, n8, n2))). % 96.87/50.61 tff(c_24292, plain, (~p(n8, n8, n7))). % 96.87/50.61 tff(c_24290, plain, (~p(n9, n8, n7))). % 96.87/50.61 tff(c_21354, plain, (~p(n2, n8, n8))). % 96.87/50.61 tff(c_24281, plain, (p(n3, n8, n7))). % 96.87/50.61 tff(c_24286, plain, (p(n8, n9, n7))). % 96.87/50.61 tff(c_24285, plain, (p(n2, n9, n9))). % 96.87/50.61 tff(c_24276, plain, (~p(n2, n1, n9))). % 96.87/50.61 tff(c_24279, plain, (~p(n2, n9, n7))). % 96.87/50.61 tff(c_21331, plain, (~p(n6, n3, n6))). % 96.87/50.61 tff(c_24274, plain, (~p(n3, n3, n7))). % 96.87/50.61 tff(c_24173, plain, (~p(n2, n1, n8))). % 96.87/50.61 tff(c_24272, plain, (p(n2, n1, n7))). % 96.87/50.61 tff(c_21207, plain, (~p(n9, n5, n7))). % 96.87/50.61 tff(c_24194, plain, (~p(n1, n8, n1))). % 96.87/50.61 tff(c_24001, plain, (~p(n2, n8, n9))). % 96.87/50.61 tff(c_24270, plain, (~p(n1, n1, n7))). % 96.87/50.61 tff(c_24249, plain, (~p(n1, n3, n7))). % 96.87/50.61 tff(c_23998, plain, (~p(n1, n8, n6))). % 96.87/50.61 tff(c_21202, plain, (~p(n9, n6, n7))). % 96.87/50.61 tff(c_23996, plain, (~p(n9, n8, n6))). % 96.87/50.61 tff(c_24179, plain, (~p(n2, n1, n2))). % 96.87/50.61 tff(c_24022, plain, (~p(n3, n3, n8))). % 96.87/50.61 tff(c_21603, plain, (~p(n7, n4, n8))). % 96.87/50.61 tff(c_24100, plain, (~p(n2, n9, n2))). % 96.87/50.61 tff(c_23516, plain, (~p(n7, n1, n7))). % 96.87/50.61 tff(c_23846, plain, (~p(n1, n3, n1))). % 96.87/50.61 tff(c_23833, plain, (~p(n1, n2, n1))). % 96.87/50.61 tff(c_23835, plain, (~p(n2, n3, n7))). % 96.87/50.61 tff(c_21316, plain, (~p(n6, n2, n4))). % 96.87/50.61 tff(c_23806, plain, (~p(n4, n6, n8))). % 96.87/50.61 tff(c_23831, plain, (~p(n2, n3, n6))). % 96.87/50.61 tff(c_23804, plain, (~p(n7, n6, n8))). % 96.87/50.61 tff(c_21298, plain, (~p(n4, n5, n3))). % 96.87/50.61 tff(c_23802, plain, (~p(n8, n6, n8))). % 96.87/50.61 tff(c_23828, plain, (p(n4, n2, n8))). % 96.87/50.61 tff(c_23818, plain, (p(n2, n3, n1))). % 96.87/50.61 tff(c_23796, plain, (~p(n2, n6, n2))). % 96.87/50.61 tff(c_23800, plain, (~p(n9, n6, n8))). % 96.87/50.61 tff(c_21288, plain, (~p(n6, n6, n1))). % 96.87/50.61 tff(c_23794, plain, (~p(n2, n6, n6))). % 96.87/50.61 tff(c_23798, plain, (~p(n2, n6, n1))). % 96.87/50.61 tff(c_23792, plain, (~p(n2, n6, n9))). % 96.87/50.61 tff(c_21306, plain, (~p(n5, n4, n1))). % 96.87/50.61 tff(c_23790, plain, (p(n2, n6, n8))). % 96.87/50.61 tff(c_23773, plain, (~p(n3, n6, n8))). % 96.87/50.61 tff(c_23742, plain, (~p(n4, n6, n6))). % 96.87/50.61 tff(c_23780, plain, (~p(n3, n5, n8))). % 96.87/50.61 tff(c_23759, plain, (~p(n4, n2, n6))). % 96.87/50.61 tff(c_21278, plain, (~p(n6, n5, n3))). % 96.87/50.61 tff(c_23763, plain, (~p(n3, n8, n8))). % 96.87/50.61 tff(c_23787, plain, (~p(n3, n4, n8))). % 96.87/50.61 tff(c_23729, plain, (~p(n4, n9, n6))). % 96.87/50.61 tff(c_21255, plain, (~p(n6, n9, n7))). % 96.87/50.61 tff(c_23720, plain, (~p(n4, n2, n1))). % 96.87/50.61 tff(c_23676, plain, (~p(n4, n6, n1))). % 96.87/50.61 tff(c_23652, plain, (~p(n4, n9, n7))). % 96.87/50.61 tff(c_23664, plain, (~p(n4, n9, n1))). % 96.87/50.61 tff(c_24421, plain, (~p(n7, n6, n9))). % 96.87/50.61 tff(c_21268, plain, (~p(n5, n9, n7))). % 96.87/50.61 tff(c_24423, plain, (~p(n3, n6, n9))). % 96.87/50.61 tff(c_24430, plain, (~p(n5, n5, n9))). % 96.87/50.61 tff(c_24435, plain, (~p(n7, n9, n1))). % 96.87/50.61 tff(c_21197, plain, (~p(n7, n7, n4))). % 96.87/50.61 tff(c_24438, plain, (~p(n7, n5, n5))). % 96.87/50.61 tff(c_24465, plain, (p(n6, n1, n2))). % 96.87/50.61 tff(c_24453, plain, (p(n9, n5, n5))). % 96.87/50.61 tff(c_24509, plain, (p(n8, n3, n5))). % 96.87/50.61 tff(c_24464, plain, (p(n6, n3, n9))). % 96.87/50.61 tff(c_21187, plain, (~p(n8, n9, n3))). % 96.87/50.61 tff(c_24440, plain, (~p(n7, n3, n5))). % 96.87/50.61 tff(c_24542, plain, (p(n5, n5, n2))). % 96.87/50.61 tff(c_24475, plain, (p(n5, n9, n1))). % 96.87/50.61 tff(c_21174, plain, (~p(n7, n8, n4))). % 96.87/50.61 tff(c_24479, plain, (p(n5, n4, n6))). % 96.87/50.61 tff(c_24490, plain, (p(n7, n6, n1))). % 96.87/50.61 tff(c_24491, plain, (p(n9, n8, n1))). % 96.87/50.61 tff(c_24499, plain, (~p(n9, n5, n9))). % 96.87/50.61 tff(c_24501, plain, (~p(n9, n5, n8))). % 96.87/50.61 tff(c_21235, plain, (~p(n7, n2, n1))). % 96.87/50.61 tff(c_24503, plain, (~p(n8, n5, n5))). % 96.87/50.61 tff(c_24506, plain, (~p(n9, n5, n2))). % 96.87/50.61 tff(c_24508, plain, (~p(n9, n5, n6))). % 96.87/50.61 tff(c_21230, plain, (~p(n7, n3, n1))). % 96.87/50.61 tff(c_24511, plain, (~p(n8, n3, n8))). % 96.87/50.61 tff(c_24513, plain, (~p(n8, n3, n9))). % 96.87/50.61 tff(c_24518, plain, (~p(n8, n3, n6))). % 96.87/50.62 tff(c_24528, plain, (~p(n7, n3, n9))). % 96.87/50.62 tff(c_24530, plain, (~p(n1, n3, n9))). % 96.87/50.62 tff(c_21169, plain, (~p(n8, n7, n4))). % 96.87/50.62 tff(c_24532, plain, (~p(n6, n1, n9))). % 96.87/50.62 tff(c_24536, plain, (~p(n7, n1, n2))). % 96.87/50.62 tff(c_24544, plain, (~p(n5, n5, n6))). % 96.87/50.62 tff(c_21164, plain, (~p(n8, n8, n4))). % 96.87/50.62 tff(c_24548, plain, (~p(n8, n5, n2))). % 96.87/50.62 tff(c_24550, plain, (~p(n7, n5, n2))). % 96.87/50.62 tff(c_24554, plain, (~p(n5, n8, n1))). % 96.87/50.62 tff(c_24557, plain, (~p(n9, n4, n6))). % 96.87/50.62 tff(c_24559, plain, (~p(n3, n4, n6))). % 96.87/50.62 tff(c_24794, plain, (~p(n8, n7, n2))). % 96.87/50.62 tff(c_24567, plain, (~p(n7, n6, n6))). % 96.87/50.62 tff(c_24569, plain, (~p(n7, n6, n4))). % 96.87/50.62 tff(c_24571, plain, (~p(n9, n4, n1))). % 96.87/50.62 tff(c_24774, plain, (~p(n1, n2, n6))). % 96.87/50.62 tff(c_24573, plain, (~p(n7, n6, n2))). % 96.87/50.62 tff(c_24575, plain, (~p(n9, n6, n1))). % 96.87/50.62 tff(c_24577, plain, (~p(n3, n6, n1))). % 96.87/50.62 tff(c_24582, plain, (~p(n9, n8, n8))). % 96.87/50.62 tff(c_24641, plain, (p(n9, n7, n8))). % 96.87/50.62 tff(c_24705, plain, (~p(n3, n5, n6))). % 96.87/50.62 tff(c_24587, plain, (~p(n9, n8, n9))). % 96.87/50.62 tff(c_24664, plain, (p(n9, n4, n9))). % 96.87/50.62 tff(c_24629, plain, (p(n7, n2, n4))). % 96.87/50.62 tff(c_24703, plain, (~p(n9, n6, n6))). % 96.87/50.62 tff(c_24630, plain, (p(n8, n6, n4))). % 96.87/50.62 tff(c_24631, plain, (p(n3, n4, n1))). % 96.87/50.62 tff(c_24635, plain, (p(n3, n6, n6))). % 96.87/50.62 tff(c_24643, plain, (~p(n8, n8, n8))). % 96.87/50.62 tff(c_24645, plain, (~p(n8, n7, n8))). % 96.87/50.62 tff(c_24674, plain, (~p(n7, n5, n9))). % 96.87/50.62 tff(c_24647, plain, (~p(n7, n7, n8))). % 96.87/50.62 tff(c_24649, plain, (~p(n5, n7, n8))). % 96.87/50.62 tff(c_24651, plain, (~p(n9, n7, n6))). % 96.87/50.62 tff(c_21072, plain, (p(n3, n2, n3))). % 96.87/50.62 tff(c_24654, plain, (~p(n9, n7, n9))). % 96.87/50.62 tff(c_24656, plain, (~p(n9, n7, n2))). % 96.87/50.62 tff(c_24666, plain, (~p(n8, n5, n9))). % 96.87/50.62 tff(c_24668, plain, (~p(n3, n4, n9))). % 96.87/50.62 tff(c_24672, plain, (~p(n9, n2, n9))). % 96.87/50.62 tff(c_21074, plain, (p(n3, n9, n8))). % 96.87/50.62 tff(c_21070, plain, (p(n2, n4, n2))). % 96.87/50.62 tff(c_24679, plain, (~p(n7, n2, n9))). % 96.87/50.62 tff(c_24681, plain, (~p(n7, n2, n2))). % 96.87/50.62 tff(c_21076, plain, (p(n4, n1, n6))). % 96.87/50.62 tff(c_24683, plain, (~p(n8, n2, n4))). % 96.87/50.62 tff(c_24687, plain, (~p(n7, n2, n6))). % 96.87/50.62 tff(c_24689, plain, (~p(n8, n6, n6))). % 96.87/50.62 tff(c_24691, plain, (~p(n8, n6, n2))). % 96.87/50.62 tff(c_24740, plain, (p(n9, n6, n2))). % 96.87/50.62 tff(c_21078, plain, (p(n4, n5, n1))). % 96.87/50.62 tff(c_21068, plain, (p(n2, n2, n5))). % 96.87/50.62 tff(c_24709, plain, (p(n8, n8, n9))). % 96.87/50.62 tff(c_24753, plain, (p(n8, n5, n8))). % 96.87/50.62 tff(c_21080, plain, (p(n4, n7, n7))). % 96.87/50.62 tff(c_24711, plain, (p(n5, n8, n8))). % 96.87/50.62 tff(c_24715, plain, (p(n5, n7, n9))). % 96.87/50.62 tff(c_24770, plain, (p(n9, n2, n6))). % 96.87/50.62 tff(c_24781, plain, (p(n3, n5, n9))). % 96.87/50.62 tff(c_24732, plain, (p(n7, n7, n2))). % 96.87/50.62 tff(c_21082, plain, (p(n5, n3, n4))). % 96.87/50.62 tff(c_21066, plain, (p(n1, n7, n1))). % 96.87/50.62 tff(c_24745, plain, (~p(n5, n8, n9))). % 96.87/50.62 tff(c_24747, plain, (~p(n7, n7, n9))). % 96.87/50.62 tff(c_21084, plain, (p(n5, n6, n3))). % 96.87/50.62 tff(c_24749, plain, (~p(n8, n7, n9))). % 96.87/50.62 tff(c_24751, plain, (~p(n8, n2, n9))). % 96.87/50.62 tff(c_24755, plain, (~p(n8, n5, n6))). % 96.87/50.62 tff(c_24757, plain, (~p(n7, n5, n8))). % 96.87/50.62 tff(c_24772, plain, (~p(n8, n2, n6))). % 96.87/50.62 tff(c_21086, plain, (p(n6, n8, n5))). % 96.87/50.62 tff(c_21064, plain, (p(n1, n5, n7))). % 96.87/50.62 tff(c_24776, plain, (~p(n7, n3, n6))). % 96.87/50.62 tff(c_24778, plain, (~p(n9, n2, n2))). % 96.87/50.62 tff(c_21088, plain, (p(n7, n4, n7))). % 96.87/50.62 tff(c_24792, plain, (~p(n7, n7, n6))). % 96.87/50.62 tff(c_24830, plain, (p(n8, n2, n2))). % 96.87/50.62 tff(c_24805, plain, (p(n7, n1, n9))). % 96.87/50.62 tff(c_24827, plain, (p(n8, n7, n6))). % 96.87/50.62 tff(c_24807, plain, (p(n1, n2, n9))). % 96.87/50.62 tff(c_21090, plain, (p(n7, n8, n3))). % 96.87/50.62 tff(c_21062, plain, (p(n1, n4, n4))). % 96.87/50.62 tff(c_24810, plain, (p(n7, n5, n6))). % 96.87/50.62 tff(c_24813, plain, (p(n1, n3, n6))). % 96.87/50.62 tff(c_21092, plain, (p(n8, n1, n1))). % 96.87/50.62 tff(c_24816, plain, (p(n7, n3, n8))). % 96.87/50.62 tff(c_24822, plain, (~p(n7, n1, n8))). % 96.87/50.62 tff(c_24824, plain, (~p(n1, n1, n9))). % 96.87/50.62 tff(c_24835, plain, (~p(n1, n3, n8))). % 96.87/50.62 tff(c_24850, plain, (p(n1, n1, n8))). % 96.87/50.62 tff(c_21094, plain, (p(n9, n9, n4))). % 96.87/50.62 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 96.87/50.62 %------------------------------------------------------------------------------