%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP581-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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 : Mon Jun 24 06:39:58 EDT 2024 % Result : Unsatisfiable 86.14s 86.18s % Output : CNFRefutation 86.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : GRP581-1 : TPTP v8.2.0. Released v2.6.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Jun 20 06:54:08 EDT 2024 % 0.13/0.33 % CPUTime : % 0.54/0.56 start to proof:theBenchmark % 86.11/86.15 %------------------------------------------- % 86.11/86.15 % File :CSE---1.7 % 86.11/86.15 % Problem :theBenchmark % 86.11/86.15 % Transform :cnf % 86.11/86.15 % Format :tptp:raw % 86.11/86.15 % Command :java -jar mcs_scs.jar %d %s % 86.11/86.15 % 86.11/86.15 % Result :Theorem 85.550000s % 86.11/86.15 % Output :CNFRefutation 85.550000s % 86.11/86.15 %------------------------------------------- % 86.14/86.17 %-------------------------------------------------------------------------- % 86.14/86.17 % File : GRP581-1 : TPTP v8.2.0. Released v2.6.0. % 86.14/86.17 % Domain : Group Theory (Abelian) % 86.14/86.17 % Problem : Axiom for Abelian group theory, in double div and id, part 1 % 86.14/86.17 % Version : [McC93] (equality) axioms. % 86.14/86.17 % English : % 86.14/86.17 % 86.14/86.17 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 86.14/86.17 % Source : [TPTP] % 86.14/86.17 % Names : % 86.14/86.17 % 86.14/86.17 % Status : Unsatisfiable % 86.14/86.17 % Rating : 0.00 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.06 v6.2.0, 0.07 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.00 v2.6.0 % 86.14/86.17 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 86.14/86.17 % Number of literals : 5 ( 5 equ; 1 neg) % 86.14/86.17 % Maximal clause size : 1 ( 1 avg) % 86.14/86.17 % Maximal term depth : 6 ( 2 avg) % 86.14/86.17 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 86.14/86.17 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 86.14/86.17 % Number of variables : 7 ( 0 sgn) % 86.14/86.17 % SPC : CNF_UNS_RFO_PEQ_UEQ % 86.14/86.17 % 86.14/86.17 % Comments : A UEQ part of GRP103-1 % 86.14/86.17 %-------------------------------------------------------------------------- % 86.14/86.17 cnf(single_axiom,axiom, % 86.14/86.17 double_divide(double_divide(A,double_divide(double_divide(identity,B),double_divide(C,double_divide(B,A)))),double_divide(identity,identity)) = C ). % 86.14/86.17 % 86.14/86.17 cnf(multiply,axiom, % 86.14/86.17 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 86.14/86.17 % 86.14/86.17 cnf(inverse,axiom, % 86.14/86.18 inverse(A) = double_divide(A,identity) ). % 86.14/86.18 % 86.14/86.18 cnf(identity,axiom, % 86.14/86.18 identity = double_divide(A,inverse(A)) ). % 86.14/86.18 % 86.14/86.18 cnf(prove_these_axioms_1,negated_conjecture, % 86.14/86.18 multiply(inverse(a1),a1) != identity ). % 86.14/86.18 % 86.14/86.18 %-------------------------------------------------------------------------- % 86.14/86.18 %------------------------------------------- % 86.14/86.18 % Proof found % 86.14/86.18 % SZS status Theorem for theBenchmark % 86.14/86.18 % SZS output start Proof % 86.14/86.20 %ClaNum:8(EqnAxiom:5) % 86.14/86.20 %VarNum:8(SingletonVarNum:4) % 86.14/86.20 %MaxLitNum:1 % 86.14/86.20 %MaxfuncDepth:3 % 86.14/86.20 %SharedTerms:7 % 86.14/86.20 %goalClause: 8 % 86.14/86.20 %singleGoalClaCount:1 % 86.14/86.20 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 86.14/86.20 [6]E(f2(x61,f2(x61,a1)),a1) % 86.14/86.20 [7]E(f2(f2(x71,f2(f2(a1,x72),f2(x73,f2(x72,x71)))),f2(a1,a1)),x73) % 86.14/86.20 %EqnAxiom % 86.14/86.20 [1]E(x11,x11) % 86.14/86.20 [2]E(x22,x21)+~E(x21,x22) % 86.14/86.20 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 86.14/86.20 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 86.14/86.20 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 86.14/86.20 % 86.14/86.20 %------------------------------------------- % 86.14/86.22 cnf(9,plain, % 86.14/86.22 (E(x91,f2(f2(x92,f2(f2(a1,x93),f2(x91,f2(x93,x92)))),f2(a1,a1)))), % 86.14/86.22 inference(scs_inference,[],[7,2])). % 86.14/86.22 cnf(10,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 86.14/86.22 inference(scs_inference,[],[8,7,6,2,3])). % 86.14/86.22 cnf(11,plain, % 86.14/86.22 (~E(a1,f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.22 inference(scs_inference,[],[8,7,6,2,3,5])). % 86.14/86.22 cnf(12,plain, % 86.14/86.22 (E(a1,f2(x121,f2(x121,a1)))), % 86.14/86.22 inference(scs_inference,[],[6,2])). % 86.14/86.22 cnf(13,plain, % 86.14/86.22 (E(a1,f2(f2(x131,f2(f2(a1,x132),f2(f2(x133,f2(x133,a1)),f2(x132,x131)))),f2(a1,a1)))), % 86.14/86.22 inference(scs_inference,[],[9,12,3])). % 86.14/86.22 cnf(15,plain, % 86.14/86.22 (E(f2(f2(x151,f2(f2(a1,x152),f2(f2(x153,f2(x153,a1)),f2(x152,x151)))),f2(a1,a1)),a1)), % 86.14/86.22 inference(scs_inference,[],[13,2])). % 86.14/86.22 cnf(18,plain, % 86.14/86.22 (E(f2(f2(x181,f2(f2(a1,x182),f2(a1,f2(x182,x181)))),f2(a1,a1)),f2(x183,f2(x183,a1)))), % 86.14/86.22 inference(scs_inference,[],[6,9,3,2])). % 86.14/86.22 cnf(19,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x191,f2(f2(a1,x192),f2(a1,f2(x192,x191)))),f2(a1,a1)))), % 86.14/86.22 inference(scs_inference,[],[18,10,3])). % 86.14/86.22 cnf(22,plain, % 86.14/86.22 (E(f2(f2(x221,f2(f2(a1,x222),f2(f2(x223,f2(x223,a1)),f2(x222,x221)))),f2(a1,a1)),f2(x224,f2(x224,a1)))), % 86.14/86.22 inference(scs_inference,[],[6,13,3,2])). % 86.14/86.22 cnf(23,plain, % 86.14/86.22 (~E(a1,f2(f2(x231,f2(f2(a1,x232),f2(f2(f2(a3,f2(a3,a1)),a1),f2(x232,x231)))),f2(a1,a1)))), % 86.14/86.22 inference(scs_inference,[],[11,7,3])). % 86.14/86.22 cnf(25,plain, % 86.14/86.22 (E(f2(f2(x251,f2(x251,a1)),x252),f2(a1,x252))), % 86.14/86.22 inference(scs_inference,[],[6,4])). % 86.14/86.22 cnf(26,plain, % 86.14/86.22 (E(f2(x261,f2(x262,f2(x262,a1))),f2(x261,a1))), % 86.14/86.22 inference(scs_inference,[],[6,4,5])). % 86.14/86.22 cnf(28,plain, % 86.14/86.22 (~E(f2(x281,f2(x281,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.22 inference(scs_inference,[],[6,19,12,11,4,5,2,3])). % 86.14/86.22 cnf(29,plain, % 86.14/86.22 (E(f2(f2(f2(x291,f2(x291,a1)),x292),x293),f2(f2(a1,x292),x293))), % 86.14/86.22 inference(scs_inference,[],[25,4])). % 86.14/86.22 cnf(30,plain, % 86.14/86.22 (E(f2(x301,f2(f2(x302,f2(x302,a1)),x303)),f2(x301,f2(a1,x303)))), % 86.14/86.22 inference(scs_inference,[],[25,4,5])). % 86.14/86.22 cnf(31,plain, % 86.14/86.22 (~E(f2(a1,f2(f2(x311,f2(x311,a1)),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.22 inference(scs_inference,[],[25,28,4,5,3])). % 86.14/86.22 cnf(34,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(a1,f2(f2(x341,f2(x341,a1)),a1)))), % 86.14/86.22 inference(scs_inference,[],[25,28,4,5,3,2])). % 86.14/86.22 cnf(35,plain, % 86.14/86.22 (E(f2(f2(x351,f2(x352,f2(x352,a1))),x353),f2(f2(x351,a1),x353))), % 86.14/86.22 inference(scs_inference,[],[26,4])). % 86.14/86.22 cnf(36,plain, % 86.14/86.22 (E(f2(x361,f2(x362,f2(x363,f2(x363,a1)))),f2(x361,f2(x362,a1)))), % 86.14/86.22 inference(scs_inference,[],[26,4,5])). % 86.14/86.22 cnf(40,plain, % 86.14/86.22 (E(f2(a1,x401),f2(f2(x402,f2(x402,a1)),x401))), % 86.14/86.22 inference(scs_inference,[],[12,4])). % 86.14/86.22 cnf(41,plain, % 86.14/86.22 (E(f2(x411,a1),f2(x411,f2(x412,f2(x412,a1))))), % 86.14/86.22 inference(scs_inference,[],[12,4,5])). % 86.14/86.22 cnf(42,plain, % 86.14/86.22 (E(f2(f2(a1,x421),x422),f2(f2(f2(x423,f2(x423,a1)),x421),x422))), % 86.14/86.22 inference(scs_inference,[],[40,4])). % 86.14/86.22 cnf(43,plain, % 86.14/86.22 (E(f2(x431,f2(a1,x432)),f2(x431,f2(f2(x433,f2(x433,a1)),x432)))), % 86.14/86.22 inference(scs_inference,[],[40,4,5])). % 86.14/86.22 cnf(44,plain, % 86.14/86.22 (~E(f2(f2(x441,f2(x441,a1)),f2(f2(x442,f2(x442,a1)),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.22 inference(scs_inference,[],[40,31,4,5,3])). % 86.14/86.22 cnf(46,plain, % 86.14/86.22 (E(f2(f2(x461,a1),x462),f2(f2(x461,f2(x463,f2(x463,a1))),x462))), % 86.14/86.22 inference(scs_inference,[],[41,4])). % 86.14/86.22 cnf(47,plain, % 86.14/86.22 (E(f2(x471,f2(x472,a1)),f2(x471,f2(x472,f2(x473,f2(x473,a1)))))), % 86.14/86.22 inference(scs_inference,[],[41,4,5])). % 86.14/86.22 cnf(48,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x481,f2(x481,a1)),f2(f2(x482,f2(x482,a1)),a1)))), % 86.14/86.22 inference(scs_inference,[],[41,44,4,5,2])). % 86.14/86.22 cnf(49,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),f2(x491,f2(x491,a1))),f2(a1,f2(f2(x492,f2(x492,a1)),a1)))), % 86.14/86.22 inference(scs_inference,[],[41,34,44,4,5,2,3])). % 86.14/86.22 cnf(51,plain, % 86.14/86.22 (E(f2(f2(f2(x511,f2(f2(a1,x512),f2(x513,f2(x512,x511)))),f2(a1,a1)),x514),f2(x513,x514))), % 86.14/86.22 inference(scs_inference,[],[7,4])). % 86.14/86.22 cnf(54,plain, % 86.14/86.22 (~E(f2(a1,f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(x541,f2(x541,a1))))), % 86.14/86.22 inference(scs_inference,[],[30,49,7,4,5,2,3])). % 86.14/86.22 cnf(56,plain, % 86.14/86.22 (~E(f2(f2(a3,f2(a3,a1)),f2(x561,f2(x561,a1))),f2(a1,f2(a1,a1)))), % 86.14/86.22 inference(scs_inference,[],[54,2])). % 86.14/86.23 cnf(57,plain, % 86.14/86.23 (~E(a1,f2(f2(a3,f2(a3,a1)),f2(x571,f2(x571,a1))))), % 86.14/86.23 inference(scs_inference,[],[6,54,2,3])). % 86.14/86.23 cnf(59,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),f2(x591,f2(x591,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[57,2])). % 86.14/86.23 cnf(60,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x601,f2(x601,a1)),f2(a1,a1))),f2(a1,f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[57,56,43,2,3])). % 86.14/86.23 cnf(63,plain, % 86.14/86.23 (~E(f2(a1,f2(a1,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x631,f2(x631,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[60,2])). % 86.14/86.23 cnf(64,plain, % 86.14/86.23 (E(f2(x641,f2(x641,f2(x642,f2(x642,a1)))),a1)), % 86.14/86.23 inference(scs_inference,[],[6,60,36,2,3])). % 86.14/86.23 cnf(68,plain, % 86.14/86.23 (~E(a1,f2(f2(a3,f2(a3,a1)),f2(f2(x681,f2(x681,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[6,63,3])). % 86.14/86.23 cnf(74,plain, % 86.14/86.23 (~E(f2(f2(f2(x741,f2(x741,a1)),x742),f2(f2(a1,x742),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[42,28,3])). % 86.14/86.23 cnf(77,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x771,f2(x771,a1)),x772),f2(f2(a1,x772),a1)))), % 86.14/86.23 inference(scs_inference,[],[42,28,3,2])). % 86.14/86.23 cnf(78,plain, % 86.14/86.23 (~E(f2(f2(f2(x781,f2(x781,a1)),f2(x782,f2(x782,a1))),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[46,74,3])). % 86.14/86.23 cnf(81,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(f2(x811,f2(x811,a1)),f2(x812,f2(x812,a1))),f2(f2(a1,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[78,2])). % 86.14/86.23 cnf(91,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(a1,f2(x911,f2(x911,a1))),f2(f2(a1,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[29,78,3,2])). % 86.14/86.23 cnf(92,plain, % 86.14/86.23 (~E(f2(a1,f2(x921,f2(x921,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[59,25,3])). % 86.14/86.23 cnf(94,plain, % 86.14/86.23 (~E(a1,f2(a1,f2(x941,f2(x941,a1))))), % 86.14/86.23 inference(scs_inference,[],[59,25,3,2])). % 86.14/86.23 cnf(99,plain, % 86.14/86.23 (~E(f2(f2(x991,f2(f2(a1,x992),f2(a1,f2(x992,x991)))),f2(a1,a1)),f2(a1,f2(x993,f2(x993,a1))))), % 86.14/86.23 inference(scs_inference,[],[94,9,3])). % 86.14/86.23 cnf(101,plain, % 86.14/86.23 (~E(f2(a1,f2(x1011,f2(x1011,a1))),f2(f2(x1012,f2(f2(a1,x1013),f2(a1,f2(x1013,x1012)))),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[94,9,3,2])). % 86.14/86.23 cnf(104,plain, % 86.14/86.23 (~E(f2(f2(a1,f2(x1041,f2(x1041,a1))),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),f2(x1042,f2(x1042,a1))))), % 86.14/86.23 inference(scs_inference,[],[91,41,3,2])). % 86.14/86.23 cnf(105,plain, % 86.14/86.23 (~E(f2(a1,a1),f2(f2(x1051,f2(f2(a1,x1052),f2(a1,f2(x1052,x1051)))),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[101,26,3])). % 86.14/86.23 cnf(107,plain, % 86.14/86.23 (~E(f2(f2(x1071,f2(f2(a1,x1072),f2(a1,f2(x1072,x1071)))),f2(a1,a1)),f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[101,26,3,2])). % 86.14/86.23 cnf(108,plain, % 86.14/86.23 (E(f2(f2(f2(x1081,f2(f2(a1,x1082),f2(f2(x1083,f2(x1083,a1)),f2(x1082,x1081)))),f2(a1,a1)),x1084),f2(a1,x1084))), % 86.14/86.23 inference(scs_inference,[],[15,4])). % 86.14/86.23 cnf(111,plain, % 86.14/86.23 (~E(f2(f2(f2(x1111,f2(x1111,a1)),f2(f2(a1,x1112),f2(a1,f2(x1112,a1)))),f2(a1,a1)),f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[107,15,23,42,4,5,2,3])). % 86.14/86.23 cnf(114,plain, % 86.14/86.23 (E(f2(x1141,x1142),f2(f2(f2(x1143,f2(f2(a1,x1144),f2(x1141,f2(x1144,x1143)))),f2(a1,a1)),x1142))), % 86.14/86.23 inference(scs_inference,[],[9,4])). % 86.14/86.23 cnf(115,plain, % 86.14/86.23 (E(f2(x1151,x1152),f2(x1151,f2(f2(x1153,f2(f2(a1,x1154),f2(x1152,f2(x1154,x1153)))),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[9,4,5])). % 86.14/86.23 cnf(117,plain, % 86.14/86.23 (~E(f2(f2(x1171,f2(x1171,a1)),a1),f2(f2(x1172,f2(f2(a1,x1173),f2(a1,f2(x1173,x1172)))),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[105,111,40,9,4,5,2,3])). % 86.14/86.23 cnf(119,plain, % 86.14/86.23 (~E(f2(f2(x1191,f2(f2(a1,x1192),f2(a1,f2(x1192,x1191)))),f2(a1,a1)),f2(f2(x1193,f2(x1193,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[117,2])). % 86.14/86.23 cnf(120,plain, % 86.14/86.23 (~E(f2(f2(f2(x1201,f2(f2(a1,x1202),f2(f2(a3,f2(a3,a1)),f2(x1202,x1201)))),f2(a1,a1)),a1),a1)), % 86.14/86.23 inference(scs_inference,[],[114,117,8,2,3])). % 86.14/86.23 cnf(123,plain, % 86.14/86.23 (~E(f2(a1,a1),a1)), % 86.14/86.23 inference(scs_inference,[],[108,120,2,3])). % 86.14/86.23 cnf(125,plain, % 86.14/86.23 (~E(a1,f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[123,2])). % 86.14/86.23 cnf(126,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x1261,f2(f2(a1,x1262),f2(a1,f2(x1262,x1261)))),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[123,115,2,3])). % 86.14/86.23 cnf(129,plain, % 86.14/86.23 (~E(f2(x1291,f2(x1291,a1)),f2(a1,f2(x1292,f2(x1292,a1))))), % 86.14/86.23 inference(scs_inference,[],[126,99,18,2,3])). % 86.14/86.23 cnf(131,plain, % 86.14/86.23 (~E(f2(a1,f2(x1311,f2(x1311,a1))),f2(x1312,f2(x1312,a1)))), % 86.14/86.23 inference(scs_inference,[],[129,2])). % 86.14/86.23 cnf(132,plain, % 86.14/86.23 (~E(f2(f2(x1321,f2(f2(a1,x1322),f2(f2(x1323,f2(x1323,a1)),f2(x1322,x1321)))),f2(a1,a1)),f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[125,129,13,2,3])). % 86.14/86.23 cnf(134,plain, % 86.14/86.23 (~E(f2(x1341,f2(x1341,a1)),f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[132,22,2,3])). % 86.14/86.23 cnf(136,plain, % 86.14/86.23 (~E(f2(a1,a1),f2(x1361,f2(x1361,a1)))), % 86.14/86.23 inference(scs_inference,[],[134,2])). % 86.14/86.23 cnf(137,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x1371,f2(x1371,a1)),f2(a1,a1))),f2(x1372,f2(x1372,a1)))), % 86.14/86.23 inference(scs_inference,[],[134,131,43,2,3])). % 86.14/86.23 cnf(140,plain, % 86.14/86.23 (~E(f2(x1401,f2(x1401,a1)),f2(a1,f2(f2(x1402,f2(x1402,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[137,2])). % 86.14/86.23 cnf(141,plain, % 86.14/86.23 (~E(f2(f2(x1411,f2(x1412,f2(x1412,a1))),f2(f2(x1411,a1),a1)),f2(a1,a1))), % 86.14/86.23 inference(scs_inference,[],[137,134,46,2,3])). % 86.14/86.23 cnf(144,plain, % 86.14/86.23 (~E(f2(a1,a1),f2(f2(x1441,f2(x1442,f2(x1442,a1))),f2(f2(x1441,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[141,2])). % 86.14/86.23 cnf(145,plain, % 86.14/86.23 (~E(f2(f2(f2(x1451,f2(f2(a1,x1452),f2(a1,f2(x1452,x1451)))),f2(a1,a1)),a1),f2(x1453,f2(x1453,a1)))), % 86.14/86.23 inference(scs_inference,[],[136,141,114,2,3])). % 86.14/86.23 cnf(148,plain, % 86.14/86.23 (~E(f2(x1481,f2(x1481,f2(x1482,f2(x1482,a1)))),f2(a1,f2(f2(x1483,f2(x1483,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[140,145,47,2,3])). % 86.14/86.23 cnf(150,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x1501,f2(x1501,a1)),f2(a1,a1))),f2(x1502,f2(x1502,f2(x1503,f2(x1503,a1)))))), % 86.14/86.23 inference(scs_inference,[],[148,2])). % 86.14/86.23 cnf(151,plain, % 86.14/86.23 (~E(f2(f2(a1,a1),f2(f2(a1,a1),a1)),f2(f2(a3,f2(a3,a1)),f2(x1511,f2(x1511,a1))))), % 86.14/86.23 inference(scs_inference,[],[104,148,35,2,3])). % 86.14/86.23 cnf(154,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),f2(x1541,f2(x1541,a1))),f2(f2(a1,a1),f2(f2(a1,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[151,2])). % 86.14/86.23 cnf(155,plain, % 86.14/86.23 (~E(a1,f2(a1,f2(f2(x1551,f2(x1551,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[64,151,148,2,3])). % 86.14/86.23 cnf(157,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x1571,f2(x1571,a1)),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[155,2])). % 86.14/86.23 cnf(158,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x1581,f2(f2(a1,x1582),f2(a1,f2(x1582,x1581)))),f2(a1,a1))),f2(x1583,f2(x1583,a1)))), % 86.14/86.23 inference(scs_inference,[],[155,136,115,2,3])). % 86.14/86.23 cnf(161,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x1611,f2(x1611,a1)),f2(a1,a1))),f2(f2(a1,a1),f2(f2(a1,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[154,158,43,2,3])). % 86.14/86.23 cnf(165,plain, % 86.14/86.23 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(x1651,f2(x1651,f2(x1652,f2(x1652,a1)))))), % 86.14/86.23 inference(scs_inference,[],[161,150,30,2,3])). % 86.14/86.23 cnf(168,plain, % 86.14/86.23 (~E(f2(x1681,f2(x1681,f2(x1682,f2(x1682,a1)))),f2(a1,f2(a1,f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[165,2])). % 86.14/86.23 cnf(169,plain, % 86.14/86.23 (~E(f2(x1691,f2(x1691,a1)),f2(f2(x1692,f2(x1692,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[165,119,18,2,3])). % 86.14/86.23 cnf(171,plain, % 86.14/86.23 (~E(f2(f2(x1711,f2(x1711,a1)),a1),f2(x1712,f2(x1712,a1)))), % 86.14/86.23 inference(scs_inference,[],[169,2])). % 86.14/86.23 cnf(172,plain, % 86.14/86.23 (~E(f2(f2(f2(x1721,f2(f2(a1,x1722),f2(a1,f2(x1722,x1721)))),f2(a1,a1)),f2(x1723,f2(x1723,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[169,92,114,2,3])). % 86.14/86.23 cnf(175,plain, % 86.14/86.23 (~E(f2(x1751,f2(x1751,a1)),f2(f2(a3,f2(a3,a1)),f2(f2(x1752,f2(x1752,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[12,68,172,2,3])). % 86.14/86.23 cnf(177,plain, % 86.14/86.23 (~E(f2(x1771,f2(x1771,a1)),f2(f2(a3,f2(a3,a1)),f2(x1772,f2(x1772,a1))))), % 86.14/86.23 inference(scs_inference,[],[12,175,57,2,3])). % 86.14/86.23 cnf(179,plain, % 86.14/86.23 (~E(f2(f2(f2(x1791,f2(x1791,a1)),f2(a1,a1)),a1),f2(x1792,f2(x1792,a1)))), % 86.14/86.23 inference(scs_inference,[],[171,177,42,2,3])). % 86.14/86.23 cnf(182,plain, % 86.14/86.23 (~E(f2(x1821,f2(x1821,a1)),f2(f2(f2(x1822,f2(x1822,a1)),f2(a1,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[179,2])). % 86.14/86.23 cnf(183,plain, % 86.14/86.23 (~E(f2(f2(a3,f2(a3,a1)),f2(f2(x1831,f2(f2(a1,x1832),f2(a1,f2(x1832,x1831)))),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[179,8,115,2,3])). % 86.14/86.23 cnf(186,plain, % 86.14/86.23 (~E(f2(f2(x1861,f2(x1862,f2(x1862,a1))),f2(f2(x1861,a1),a1)),f2(f2(f2(x1863,f2(x1863,a1)),f2(a1,a1)),a1))), % 86.14/86.23 inference(scs_inference,[],[182,183,46,2,3])). % 86.14/86.23 cnf(189,plain, % 86.14/86.23 (~E(f2(f2(f2(x1891,f2(x1891,a1)),f2(a1,a1)),a1),f2(f2(x1892,f2(x1893,f2(x1893,a1))),f2(f2(x1892,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[186,2])). % 86.14/86.23 cnf(190,plain, % 86.14/86.23 (~E(f2(f2(f2(x1901,f2(f2(a1,x1902),f2(a1,f2(x1902,x1901)))),f2(a1,a1)),a1),a1)), % 86.14/86.23 inference(scs_inference,[],[186,123,114,2,3])). % 86.14/86.23 cnf(193,plain, % 86.14/86.23 (~E(f2(f2(x1931,f2(x1931,a1)),f2(f2(x1932,f2(x1932,a1)),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[157,190,40,2,3])). % 86.14/86.23 cnf(195,plain, % 86.14/86.23 (~E(a1,f2(f2(x1951,f2(x1951,a1)),f2(f2(x1952,f2(x1952,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[193,2])). % 86.14/86.23 cnf(196,plain, % 86.14/86.23 (~E(f2(f2(a1,f2(f2(x1961,f2(x1961,a1)),a1)),f2(f2(x1962,f2(x1962,a1)),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[193,29,2,3])). % 86.14/86.23 cnf(200,plain, % 86.14/86.23 (~E(f2(a1,f2(x2001,f2(x2001,a1))),f2(f2(x2002,f2(x2003,f2(x2003,a1))),f2(f2(x2002,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[144,196,41,2,3])). % 86.14/86.23 cnf(203,plain, % 86.14/86.23 (~E(f2(f2(a1,f2(a1,a1)),a1),f2(f2(x2031,f2(x2032,f2(x2032,a1))),f2(f2(x2031,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[200,189,29,2,3])). % 86.14/86.23 cnf(207,plain, % 86.14/86.23 (~E(f2(x2071,f2(x2071,a1)),f2(f2(x2072,f2(x2072,a1)),f2(f2(x2073,f2(x2073,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[195,203,12,2,3])). % 86.14/86.23 cnf(208,plain, % 86.14/86.23 (~E(f2(f2(x2081,f2(x2081,a1)),f2(f2(x2082,f2(x2082,a1)),f2(a1,a1))),f2(x2083,f2(x2083,a1)))), % 86.14/86.23 inference(scs_inference,[],[207,2])). % 86.14/86.23 cnf(209,plain, % 86.14/86.23 (~E(f2(f2(a1,f2(f2(x2091,f2(x2091,a1)),a1)),f2(a1,f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[207,196,30,2,3])). % 86.14/86.23 cnf(213,plain, % 86.14/86.23 (~E(f2(f2(f2(x2131,f2(x2131,a1)),f2(a1,a1)),f2(f2(x2132,f2(x2132,a1)),f2(a1,a1))),f2(x2133,f2(x2133,a1)))), % 86.14/86.23 inference(scs_inference,[],[208,209,42,2,3])). % 86.14/86.23 cnf(216,plain, % 86.14/86.23 (~E(f2(x2161,f2(x2161,a1)),f2(f2(f2(x2162,f2(x2162,a1)),f2(a1,a1)),f2(f2(x2163,f2(x2163,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[213,2])). % 86.14/86.23 cnf(217,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x2171,f2(x2171,a1)),f2(a1,a1))),f2(f2(x2172,f2(x2173,f2(x2173,a1))),f2(f2(x2172,a1),a1)))), % 86.14/86.23 inference(scs_inference,[],[213,200,43,2,3])). % 86.14/86.23 cnf(221,plain, % 86.14/86.23 (~E(f2(f2(x2211,f2(x2211,a1)),f2(a1,a1)),f2(f2(f2(x2212,f2(x2212,a1)),f2(a1,a1)),f2(f2(x2213,f2(x2213,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[216,217,40,2,3])). % 86.14/86.23 cnf(224,plain, % 86.14/86.23 (~E(f2(f2(f2(x2241,f2(x2241,a1)),f2(a1,a1)),f2(f2(x2242,f2(x2242,a1)),f2(a1,a1))),f2(f2(x2243,f2(x2243,a1)),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[221,2])). % 86.14/86.23 cnf(225,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x2251,f2(f2(a1,x2252),f2(f2(x2253,f2(x2253,a1)),f2(x2252,x2251)))),f2(a1,a1))),a1)), % 86.14/86.23 inference(scs_inference,[],[221,92,115,2,3])). % 86.14/86.23 cnf(228,plain, % 86.14/86.23 (~E(f2(f2(a1,f2(a1,a1)),f2(f2(x2281,f2(x2281,a1)),f2(a1,a1))),f2(f2(x2282,f2(x2282,a1)),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[224,225,29,2,3])). % 86.14/86.23 cnf(230,plain, % 86.14/86.23 (~E(f2(f2(x2301,f2(x2301,a1)),f2(a1,a1)),f2(f2(a1,f2(a1,a1)),f2(f2(x2302,f2(x2302,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[228,2])). % 86.14/86.23 cnf(231,plain, % 86.14/86.23 (~E(f2(a1,f2(f2(x2311,f2(x2311,a1)),f2(a1,a1))),f2(f2(x2312,f2(x2312,a1)),f2(a1,a1)))), % 86.14/86.23 inference(scs_inference,[],[228,25,2,3])). % 86.14/86.23 cnf(234,plain, % 86.14/86.23 (~E(f2(f2(f2(x2341,f2(x2341,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(a1,f2(a1,a1)),f2(f2(x2342,f2(x2342,a1)),f2(a1,a1))))), % 86.14/86.23 inference(scs_inference,[],[231,230,42,2,3])). % 86.14/86.23 cnf(238,plain, % 86.14/86.24 (~E(f2(f2(x2381,f2(x2381,a1)),f2(a1,f2(a1,a1))),f2(x2382,f2(x2382,a1)))), % 86.14/86.24 inference(scs_inference,[],[234,208,30,2,3])). % 86.14/86.24 cnf(241,plain, % 86.14/86.24 (~E(f2(x2411,f2(x2411,a1)),f2(f2(x2412,f2(x2412,a1)),f2(a1,f2(a1,a1))))), % 86.14/86.24 inference(scs_inference,[],[238,2])). % 86.14/86.24 cnf(242,plain, % 86.14/86.24 (~E(f2(f2(a1,f2(f2(x2421,f2(x2421,a1)),a1)),f2(a1,f2(a1,a1))),f2(x2422,f2(x2422,a1)))), % 86.14/86.24 inference(scs_inference,[],[238,29,2,3])). % 86.14/86.24 cnf(246,plain, % 86.14/86.24 (~E(f2(f2(a1,f2(f2(x2461,f2(x2461,a1)),a1)),a1),a1)), % 86.14/86.24 inference(scs_inference,[],[242,209,26,2,3])). % 86.14/86.24 cnf(249,plain, % 86.14/86.24 (~E(f2(x2491,f2(x2491,f2(x2492,f2(x2492,a1)))),f2(f2(x2493,f2(x2493,a1)),f2(a1,f2(a1,a1))))), % 86.14/86.24 inference(scs_inference,[],[241,246,47,2,3])). % 86.14/86.24 cnf(251,plain, % 86.14/86.24 (~E(f2(f2(x2511,f2(x2511,a1)),f2(a1,f2(a1,a1))),f2(x2512,f2(x2512,f2(x2513,f2(x2513,a1)))))), % 86.14/86.24 inference(scs_inference,[],[249,2])). % 86.14/86.24 cnf(256,plain, % 86.14/86.24 (E(f2(a1,x2561),f2(f2(f2(x2562,f2(f2(a1,x2563),f2(f2(x2564,f2(x2564,a1)),f2(x2563,x2562)))),f2(a1,a1)),x2561))), % 86.14/86.24 inference(scs_inference,[],[13,4])). % 86.14/86.24 cnf(258,plain, % 86.14/86.24 (~E(f2(f2(f2(x2581,f2(f2(a1,x2582),f2(f2(x2583,f2(x2583,a1)),f2(x2582,x2581)))),f2(a1,a1)),a1),a1)), % 86.14/86.24 inference(scs_inference,[],[256,123,3])). % 86.14/86.24 cnf(264,plain, % 86.14/86.24 (~E(f2(f2(x2641,f2(x2641,a1)),a1),a1)), % 86.14/86.24 inference(scs_inference,[],[51,258,3])). % 86.14/86.24 cnf(268,plain, % 86.14/86.24 (~E(f2(f2(x2681,f2(x2681,a1)),f2(f2(x2682,f2(f2(a1,x2683),f2(a1,f2(x2683,x2682)))),f2(a1,a1))),a1)), % 86.14/86.24 inference(scs_inference,[],[264,115,2,3])). % 86.14/86.24 cnf(271,plain, % 86.14/86.24 (~E(a1,f2(f2(x2711,f2(x2711,a1)),f2(a1,f2(a1,a1))))), % 86.14/86.24 inference(scs_inference,[],[268,64,249,2,3])). % 86.14/86.24 cnf(273,plain, % 86.14/86.24 (~E(f2(f2(x2731,f2(x2731,a1)),f2(a1,f2(a1,a1))),a1)), % 86.14/86.24 inference(scs_inference,[],[271,2])). % 86.14/86.24 cnf(278,plain, % 86.14/86.24 (~E(f2(f2(f2(x2781,f2(x2781,a1)),f2(a1,a1)),f2(a1,f2(a1,a1))),a1)), % 86.14/86.24 inference(scs_inference,[],[273,42,3])). % 86.14/86.24 cnf(282,plain, % 86.14/86.24 (~E(f2(a1,f2(f2(x2821,f2(x2821,a1)),f2(x2822,f2(x2822,a1)))),f2(a1,f2(a1,f2(a1,a1))))), % 86.14/86.24 inference(scs_inference,[],[25,168,3])). % 86.14/86.24 cnf(286,plain, % 86.14/86.24 (~E(f2(a1,f2(f2(x2861,f2(x2861,a1)),a1)),f2(a1,f2(a1,f2(a1,a1))))), % 86.14/86.24 inference(scs_inference,[],[282,36,2,3])). % 86.14/86.24 cnf(289,plain, % 86.14/86.24 (~E(f2(a1,a1),f2(f2(f2(x2891,f2(x2891,a1)),x2892),f2(f2(a1,x2892),a1)))), % 86.14/86.24 inference(scs_inference,[],[25,77,286,2,3])). % 86.14/86.24 cnf(291,plain, % 86.14/86.24 (~E(f2(f2(f2(x2911,f2(x2911,a1)),x2912),f2(f2(a1,x2912),a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[289,2])). % 86.14/86.24 cnf(292,plain, % 86.14/86.24 (~E(f2(a1,f2(x2921,f2(x2921,a1))),f2(f2(f2(x2922,f2(x2922,a1)),x2923),f2(f2(a1,x2923),a1)))), % 86.14/86.24 inference(scs_inference,[],[289,41,2,3])). % 86.14/86.24 cnf(294,plain, % 86.14/86.24 (~E(f2(f2(f2(x2941,f2(x2941,a1)),x2942),f2(f2(a1,x2942),a1)),f2(a1,f2(x2943,f2(x2943,a1))))), % 86.14/86.24 inference(scs_inference,[],[292,2])). % 86.14/86.24 cnf(295,plain, % 86.14/86.24 (~E(f2(a1,a1),f2(f2(f2(x2951,f2(x2951,a1)),f2(x2952,f2(x2952,a1))),f2(f2(a1,a1),a1)))), % 86.14/86.24 inference(scs_inference,[],[25,292,81,2,3])). % 86.14/86.24 cnf(297,plain, % 86.14/86.24 (~E(f2(f2(f2(x2971,f2(x2971,a1)),f2(x2972,f2(x2972,a1))),f2(f2(a1,a1),a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[295,2])). % 86.14/86.24 cnf(298,plain, % 86.14/86.24 (~E(f2(f2(f2(x2981,f2(x2981,a1)),x2982),f2(f2(a1,x2982),f2(x2983,f2(x2983,a1)))),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[291,295,47,2,3])). % 86.14/86.24 cnf(301,plain, % 86.14/86.24 (~E(f2(a1,a1),f2(f2(x3011,f2(x3011,a1)),f2(f2(x3012,f2(x3012,a1)),a1)))), % 86.14/86.24 inference(scs_inference,[],[25,298,48,2,3])). % 86.14/86.24 cnf(303,plain, % 86.14/86.24 (~E(f2(f2(x3031,f2(x3031,a1)),f2(f2(x3032,f2(x3032,a1)),a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[301,2])). % 86.14/86.24 cnf(304,plain, % 86.14/86.24 (~E(f2(f2(f2(x3041,f2(x3041,a1)),f2(x3042,f2(x3042,a1))),f2(f2(a1,a1),a1)),f2(a1,f2(x3043,f2(x3043,a1))))), % 86.14/86.24 inference(scs_inference,[],[301,294,46,2,3])). % 86.14/86.24 cnf(308,plain, % 86.14/86.24 (~E(f2(a1,f2(f2(x3081,f2(x3081,a1)),a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[25,303,304,2,3])). % 86.14/86.24 cnf(312,plain, % 86.14/86.24 (~E(f2(a1,f2(f2(x3121,f2(x3121,a1)),f2(x3122,f2(x3122,a1)))),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[308,47,2,3])). % 86.14/86.24 cnf(315,plain, % 86.14/86.24 (~E(f2(a1,f2(f2(x3151,f2(x3151,a1)),a1)),f2(a1,f2(x3152,f2(x3152,a1))))), % 86.14/86.24 inference(scs_inference,[],[25,312,129,2,3])). % 86.14/86.24 cnf(319,plain, % 86.14/86.24 (~E(f2(f2(f2(x3191,f2(x3191,a1)),f2(x3192,f2(x3192,a1))),f2(f2(a1,a1),f2(x3193,f2(x3193,a1)))),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[297,315,47,2,3])). % 86.14/86.24 cnf(322,plain, % 86.14/86.24 (~E(f2(f2(f2(x3221,f2(x3221,a1)),f2(a1,a1)),a1),a1)), % 86.14/86.24 inference(scs_inference,[],[26,278,319,2,3])). % 86.14/86.24 cnf(325,plain, % 86.14/86.24 (~E(f2(f2(f2(x3251,f2(x3251,a1)),f2(a1,a1)),f2(x3252,f2(x3252,a1))),a1)), % 86.14/86.24 inference(scs_inference,[],[322,41,2,3])). % 86.14/86.24 cnf(328,plain, % 86.14/86.24 (~E(f2(f2(x3281,f2(x3281,a1)),a1),f2(x3282,f2(x3282,f2(x3283,f2(x3283,a1)))))), % 86.14/86.24 inference(scs_inference,[],[26,325,251,2,3])). % 86.14/86.24 cnf(330,plain, % 86.14/86.24 (~E(f2(x3301,f2(x3301,f2(x3302,f2(x3302,a1)))),f2(f2(x3303,f2(x3303,a1)),a1))), % 86.14/86.24 inference(scs_inference,[],[328,2])). % 86.14/86.24 cnf(359,plain, % 86.14/86.24 (~E(f2(f2(x3591,f2(x3591,a1)),f2(a1,f2(x3592,f2(x3592,a1)))),f2(f2(x3593,f2(x3593,a1)),a1))), % 86.14/86.24 inference(scs_inference,[],[40,330,3])). % 86.14/86.24 cnf(436,plain, % 86.14/86.24 (~E(f2(f2(x4361,f2(x4361,a1)),a1),f2(f2(x4362,f2(x4362,a1)),f2(a1,a1)))), % 86.14/86.24 inference(scs_inference,[],[359,36,3,2])). % 86.14/86.24 cnf(444,plain, % 86.14/86.24 (~E(f2(a1,a1),f2(f2(x4441,f2(x4441,a1)),f2(a1,a1)))), % 86.14/86.24 inference(scs_inference,[],[436,25,3])). % 86.14/86.24 cnf(446,plain, % 86.14/86.24 (~E(f2(f2(x4461,f2(x4461,a1)),f2(a1,a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[436,25,3,2])). % 86.14/86.24 cnf(447,plain, % 86.14/86.24 (~E(f2(f2(f2(x4471,f2(f2(a1,x4472),f2(f2(x4473,f2(x4473,a1)),f2(x4472,x4471)))),f2(a1,a1)),f2(a1,a1)),f2(a1,a1))), % 86.14/86.24 inference(scs_inference,[],[446,114,3])). % 86.14/86.24 cnf(450,plain, % 86.14/86.24 (~E(f2(f2(x4501,f2(f2(a1,x4502),f2(f2(a1,a1),f2(x4502,x4501)))),f2(a1,a1)),f2(f2(x4503,f2(x4503,a1)),f2(a1,a1)))), % 86.14/86.24 inference(scs_inference,[],[444,447,9,2,3])). % 86.14/86.24 cnf(588,plain, % 86.14/86.24 ($false), % 86.14/86.24 inference(scs_inference,[],[450,36,42,3,4]), % 86.14/86.24 ['proof']). % 86.14/86.24 % SZS output end Proof % 86.14/86.24 % Total time :85.550000s %------------------------------------------------------------------------------