%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP001+6 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n018.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:38:24 EDT 2024 % Result : Theorem 0.60s 0.93s % Output : CNFRefutation 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : GRP001+6 : TPTP v8.2.0. Released v3.1.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n018.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.36 % DateTime : Thu Jun 20 08:50:09 EDT 2024 % 0.13/0.36 % CPUTime : % 0.58/0.61 start to proof:theBenchmark % 0.60/0.92 %------------------------------------------- % 0.60/0.92 % File :CSE---1.7 % 0.60/0.92 % Problem :theBenchmark % 0.60/0.92 % Transform :cnf % 0.60/0.92 % Format :tptp:raw % 0.60/0.92 % Command :java -jar mcs_scs.jar %d %s % 0.60/0.92 % 0.60/0.92 % Result :Theorem 0.270000s % 0.60/0.92 % Output :CNFRefutation 0.270000s % 0.60/0.92 %------------------------------------------- % 0.60/0.92 %------------------------------------------------------------------------------ % 0.60/0.92 % File : GRP001+6 : TPTP v8.2.0. Released v3.1.0. % 0.60/0.92 % Domain : Group Theory % 0.60/0.92 % Problem : X^2 = identity => commutativity % 0.60/0.92 % Version : Especial. % 0.60/0.92 % English : If the square of every element is the identity, the system % 0.60/0.92 % is commutative. % 0.60/0.92 % 0.60/0.92 % Refs : [Shu04] Shults (2004), Email to G. Sutcliffe % 0.60/0.92 % Source : [Shu04] % 0.60/0.92 % Names : % 0.60/0.92 % 0.60/0.92 % Status : Theorem % 0.60/0.92 % Rating : 0.00 v7.5.0, 0.14 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.18 v6.1.0, 0.24 v6.0.0, 0.50 v5.5.0, 0.21 v5.4.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.00 v5.0.0, 0.10 v4.1.0, 0.17 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.14 v3.5.0, 0.00 v3.2.0, 0.33 v3.1.0 % 0.60/0.92 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 0.60/0.92 % Number of atoms : 16 ( 0 equ) % 0.60/0.92 % Maximal formula atoms : 16 ( 16 avg) % 0.60/0.92 % Number of connectives : 15 ( 0 ~; 0 |; 10 &) % 0.60/0.92 % ( 0 <=>; 5 =>; 0 <=; 0 <~>) % 0.60/0.92 % Maximal formula depth : 15 ( 15 avg) % 0.60/0.92 % Maximal term depth : 2 ( 1 avg) % 0.60/0.92 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 0.60/0.92 % Number of functors : 1 ( 1 usr; 0 con; 1-1 aty) % 0.60/0.93 % Number of variables : 24 ( 23 !; 1 ?) % 0.60/0.93 % SPC : FOF_THM_RFO_NEQ % 0.60/0.93 % 0.60/0.93 % Comments : % 0.60/0.93 %------------------------------------------------------------------------------ % 0.60/0.93 fof(commutativity,conjecture, % 0.60/0.93 ! [E] : % 0.60/0.93 ( ( ! [X,Y] : % 0.60/0.93 ? [Z] : product(X,Y,Z) % 0.60/0.93 & ! [X,Y,Z,U,V,W] : % 0.60/0.93 ( ( product(X,Y,U) % 0.60/0.93 & product(Y,Z,V) % 0.60/0.93 & product(U,Z,W) ) % 0.60/0.93 => product(X,V,W) ) % 0.60/0.93 & ! [X,Y,Z,U,V,W] : % 0.60/0.93 ( ( product(X,Y,U) % 0.60/0.93 & product(Y,Z,V) % 0.60/0.93 & product(X,V,W) ) % 0.60/0.93 => product(U,Z,W) ) % 0.60/0.93 & ! [X] : product(X,E,X) % 0.60/0.93 & ! [X] : product(E,X,X) % 0.60/0.93 & ! [X] : product(X,inverse(X),E) % 0.60/0.93 & ! [X] : product(inverse(X),X,E) ) % 0.60/0.93 => ( ! [X] : product(X,X,E) % 0.60/0.93 => ! [U,V,W] : % 0.60/0.93 ( product(U,V,W) % 0.60/0.93 => product(V,U,W) ) ) ) ). % 0.60/0.93 % 0.60/0.93 %------------------------------------------------------------------------------ % 0.60/0.93 %------------------------------------------- % 0.60/0.93 % Proof found % 0.60/0.93 % SZS status Theorem for theBenchmark % 0.60/0.93 % SZS output start Proof % 0.60/0.93 %ClaNum:10(EqnAxiom:0) % 0.60/0.93 %VarNum:38(SingletonVarNum:19) % 0.60/0.93 %MaxLitNum:4 % 0.60/0.93 %MaxfuncDepth:1 % 0.60/0.93 %SharedTerms:6 % 0.60/0.93 %goalClause: 1 2 3 4 5 6 7 8 9 10 % 0.60/0.93 %singleGoalClaCount:8 % 0.60/0.93 [1]P1(a1,a4,a5) % 0.60/0.93 [8]~P1(a4,a1,a5) % 0.60/0.93 [2]P1(x21,x21,a2) % 0.60/0.93 [3]P1(x31,a2,x31) % 0.60/0.93 [4]P1(a2,x41,x41) % 0.60/0.93 [5]P1(x51,f6(x51),a2) % 0.60/0.93 [6]P1(f6(x61),x61,a2) % 0.60/0.93 [7]P1(x71,x72,f3(x71,x72)) % 0.60/0.93 [9]~P1(x96,x94,x91)+P1(x91,x92,x93)+~P1(x94,x92,x95)+~P1(x96,x95,x93) % 0.60/0.93 [10]~P1(x101,x106,x104)+P1(x101,x102,x103)+~P1(x104,x105,x103)+~P1(x106,x105,x102) % 0.60/0.93 %EqnAxiom % 0.60/0.93 % 0.60/0.93 %------------------------------------------- % 0.62/0.93 cnf(11,plain, % 0.62/0.93 (P1(a5,a4,a1)), % 0.62/0.93 inference(scs_inference,[],[1,2,3,9])). % 0.62/0.93 cnf(13,plain, % 0.62/0.93 (P1(x131,x131,a2)), % 0.62/0.94 inference(rename_variables,[],[2])). % 0.62/0.94 cnf(15,plain, % 0.62/0.94 (P1(a1,a5,a4)), % 0.62/0.94 inference(scs_inference,[],[1,2,13,3,4,9,10])). % 0.62/0.94 cnf(19,plain, % 0.62/0.94 (P1(a5,f6(a4),f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[1,7,5,9])). % 0.62/0.94 cnf(20,plain, % 0.62/0.94 (P1(x201,x202,f3(x201,x202))), % 0.62/0.94 inference(rename_variables,[],[7])). % 0.62/0.94 cnf(23,plain, % 0.62/0.94 (P1(a1,a1,f3(a4,a4))), % 0.62/0.94 inference(scs_inference,[],[1,11,15,7,20,5,9,10])). % 0.62/0.94 cnf(26,plain, % 0.62/0.94 (P1(a5,a4,f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[1,2,7,9])). % 0.62/0.94 cnf(27,plain, % 0.62/0.94 (P1(x271,x272,f3(x271,x272))), % 0.62/0.94 inference(rename_variables,[],[7])). % 0.62/0.94 cnf(30,plain, % 0.62/0.94 (P1(a1,a5,f3(f3(a4,a4),a4))), % 0.62/0.94 inference(scs_inference,[],[1,23,2,7,27,9,10])). % 0.62/0.94 cnf(33,plain, % 0.62/0.94 (P1(a5,f6(a4),a1)), % 0.62/0.94 inference(scs_inference,[],[1,3,5,9])). % 0.62/0.94 cnf(49,plain, % 0.62/0.94 (P1(x491,x492,f3(x491,x492))), % 0.62/0.94 inference(rename_variables,[],[7])). % 0.62/0.94 cnf(52,plain, % 0.62/0.94 (P1(a1,f3(a4,a4),f3(f3(a4,a4),a1))), % 0.62/0.94 inference(scs_inference,[],[1,23,3,7,49,9,10])). % 0.62/0.94 cnf(61,plain, % 0.62/0.94 (P1(a1,f3(f3(a4,a4),a1),a2)), % 0.62/0.94 inference(scs_inference,[],[52,23,2,10])). % 0.62/0.94 cnf(67,plain, % 0.62/0.94 (P1(a1,a4,f3(f3(a4,a4),a5))), % 0.62/0.94 inference(scs_inference,[],[15,23,7,10])). % 0.62/0.94 cnf(70,plain, % 0.62/0.94 (P1(f6(a5),a1,f6(a4))), % 0.62/0.94 inference(scs_inference,[],[33,6,4,10])). % 0.62/0.94 cnf(74,plain, % 0.62/0.94 (P1(a5,f3(a1,a2),f6(a4))), % 0.62/0.94 inference(scs_inference,[],[19,2,4,10])). % 0.62/0.94 cnf(78,plain, % 0.62/0.94 (P1(a5,f3(a1,a2),f3(a2,a4))), % 0.62/0.94 inference(scs_inference,[],[26,2,7,10])). % 0.62/0.94 cnf(82,plain, % 0.62/0.94 (P1(a5,f3(a2,a4),f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[78,2,4,10])). % 0.62/0.94 cnf(86,plain, % 0.62/0.94 (P1(a5,f3(a1,a2),f3(a2,f3(a2,a4)))), % 0.62/0.94 inference(scs_inference,[],[82,2,7,10])). % 0.62/0.94 cnf(90,plain, % 0.62/0.94 (P1(a5,f3(a2,f3(a2,a4)),f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[86,2,4,10])). % 0.62/0.94 cnf(94,plain, % 0.62/0.94 (P1(a5,f6(a4),f3(a2,f3(a1,a2)))), % 0.62/0.94 inference(scs_inference,[],[74,2,7,10])). % 0.62/0.94 cnf(99,plain, % 0.62/0.94 (P1(a5,f6(a4),f3(a2,a1))), % 0.62/0.94 inference(scs_inference,[],[70,5,7,10])). % 0.62/0.94 cnf(103,plain, % 0.62/0.94 (P1(a5,f3(a2,f3(a1,a2)),f6(a4))), % 0.62/0.94 inference(scs_inference,[],[94,2,4,10])). % 0.62/0.94 cnf(107,plain, % 0.62/0.94 (P1(a5,f3(a2,a1),f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[99,2,7,10])). % 0.62/0.94 cnf(111,plain, % 0.62/0.94 (P1(a5,f3(a2,f6(a4)),f3(a2,a1))), % 0.62/0.94 inference(scs_inference,[],[107,2,4,10])). % 0.62/0.94 cnf(115,plain, % 0.62/0.94 (P1(f6(a5),f3(f3(a4,a4),a5),a2)), % 0.62/0.94 inference(scs_inference,[],[67,70,6,10])). % 0.62/0.94 cnf(118,plain, % 0.62/0.94 (P1(a5,a1,f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[33,2,7,10])). % 0.62/0.94 cnf(125,plain, % 0.62/0.94 (P1(a5,f3(a2,f6(a4)),a1)), % 0.62/0.94 inference(scs_inference,[],[118,2,4,10])). % 0.62/0.94 cnf(129,plain, % 0.62/0.94 (P1(a5,f3(a1,a2),f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[19,2,7,10])). % 0.62/0.94 cnf(133,plain, % 0.62/0.94 (P1(a5,f3(a2,f6(a4)),f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[129,2,4,10])). % 0.62/0.94 cnf(137,plain, % 0.62/0.94 (P1(f6(a5),a1,f3(a2,a4))), % 0.62/0.94 inference(scs_inference,[],[11,6,7,10])). % 0.62/0.94 cnf(141,plain, % 0.62/0.94 (P1(f3(a2,a4),a4,a2)), % 0.62/0.94 inference(scs_inference,[],[1,137,6,9])). % 0.62/0.94 cnf(147,plain, % 0.62/0.94 (P1(a5,a2,f3(f3(a1,a2),a4))), % 0.62/0.94 inference(scs_inference,[],[141,82,7,10])). % 0.62/0.94 cnf(154,plain, % 0.62/0.94 (P1(f6(a5),f3(a1,a2),f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[133,6,4,10])). % 0.62/0.94 cnf(158,plain, % 0.62/0.94 (P1(a5,f3(a1,a2),a4)), % 0.62/0.94 inference(scs_inference,[],[26,2,4,10])). % 0.62/0.94 cnf(166,plain, % 0.62/0.94 (P1(f3(f3(a4,a4),a4),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[1,158,30,9])). % 0.62/0.94 cnf(172,plain, % 0.62/0.94 (P1(a4,f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[1,158,15,9])). % 0.62/0.94 cnf(178,plain, % 0.62/0.94 (P1(a2,f3(a2,a1),a1)), % 0.62/0.94 inference(scs_inference,[],[125,107,2,9])). % 0.62/0.94 cnf(179,plain, % 0.62/0.94 (P1(x1791,x1791,a2)), % 0.62/0.94 inference(rename_variables,[],[2])). % 0.62/0.94 cnf(181,plain, % 0.62/0.94 (P1(f3(f3(a4,a4),a4),a5,f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[125,166,107,2,179,4,9,10])). % 0.62/0.94 cnf(188,plain, % 0.62/0.94 (P1(a1,a5,f3(a2,f3(a2,a4)))), % 0.62/0.94 inference(scs_inference,[],[1,90,172,86,7,9,10])). % 0.62/0.94 cnf(190,plain, % 0.62/0.94 (P1(f3(a2,f3(a2,a4)),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[1,158,188,9])). % 0.62/0.94 cnf(196,plain, % 0.62/0.94 (P1(f3(a2,a5),f3(a2,f6(a4)),a1)), % 0.62/0.94 inference(scs_inference,[],[111,178,7,9])). % 0.62/0.94 cnf(210,plain, % 0.62/0.94 (P1(a2,f3(a4,a4),a2)), % 0.62/0.94 inference(scs_inference,[],[61,2,52,9])). % 0.62/0.94 cnf(215,plain, % 0.62/0.94 (P1(f3(a1,a2),f3(a2,f6(a4)),a5)), % 0.62/0.94 inference(scs_inference,[],[166,133,181,9])). % 0.62/0.94 cnf(221,plain, % 0.62/0.94 (P1(f3(f3(a1,a2),a5),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[215,129,7,9])). % 0.62/0.94 cnf(224,plain, % 0.62/0.94 (P1(f3(a2,f3(a2,a4)),a5,f3(a2,a1))), % 0.62/0.94 inference(scs_inference,[],[190,215,129,111,7,9,10])). % 0.62/0.94 cnf(226,plain, % 0.62/0.94 (P1(f3(a2,a1),f3(a2,f3(a2,a4)),a5)), % 0.62/0.94 inference(scs_inference,[],[190,90,224,9])). % 0.62/0.94 cnf(232,plain, % 0.62/0.94 (P1(f3(f3(a2,a1),a5),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[226,86,7,9])). % 0.62/0.94 cnf(237,plain, % 0.62/0.94 (P1(a2,f3(a1,a2),a1)), % 0.62/0.94 inference(scs_inference,[],[125,154,5,9])). % 0.62/0.94 cnf(240,plain, % 0.62/0.94 (P1(f3(f3(a2,a1),a5),a5,f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[232,125,154,5,2,4,9,10])). % 0.62/0.94 cnf(244,plain, % 0.62/0.94 (P1(f3(a2,a5),f6(a4),a1)), % 0.62/0.94 inference(scs_inference,[],[237,19,7,9])). % 0.62/0.94 cnf(247,plain, % 0.62/0.94 (P1(f3(f3(a1,a2),a5),a5,a1)), % 0.62/0.94 inference(scs_inference,[],[237,221,19,2,7,9,10])). % 0.62/0.94 cnf(250,plain, % 0.62/0.94 (P1(a2,f3(a2,f6(a4)),f6(a4))), % 0.62/0.94 inference(scs_inference,[],[74,133,2,9])). % 0.62/0.94 cnf(258,plain, % 0.62/0.94 (P1(f3(a1,a2),f3(a2,f3(a2,a4)),a5)), % 0.62/0.94 inference(scs_inference,[],[232,90,240,9])). % 0.62/0.94 cnf(263,plain, % 0.62/0.94 (P1(f3(f3(a2,a4),a5),f3(a1,a2),a2)), % 0.62/0.94 inference(scs_inference,[],[141,158,7,9])). % 0.62/0.94 cnf(279,plain, % 0.62/0.94 (P1(a2,f3(a2,a4),f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[129,82,2,9])). % 0.62/0.94 cnf(285,plain, % 0.62/0.94 (P1(a2,f3(a2,a4),f6(a4))), % 0.62/0.94 inference(scs_inference,[],[279,250,2,9])). % 0.62/0.94 cnf(291,plain, % 0.62/0.94 (P1(f3(a2,a5),f3(a2,a4),a1)), % 0.62/0.94 inference(scs_inference,[],[285,244,3,9])). % 0.62/0.94 cnf(301,plain, % 0.62/0.94 (P1(a1,a5,f6(a4))), % 0.62/0.94 inference(scs_inference,[],[1,291,74,172,78,7,9,10])). % 0.62/0.94 cnf(303,plain, % 0.62/0.94 (P1(f6(a4),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[1,158,301,9])). % 0.62/0.94 cnf(309,plain, % 0.62/0.94 (P1(f3(f6(a4),a5),f6(a4),a5)), % 0.62/0.94 inference(scs_inference,[],[303,19,7,9])). % 0.62/0.94 cnf(312,plain, % 0.62/0.94 (P1(f6(a4),a5,f3(a1,a2))), % 0.62/0.94 inference(scs_inference,[],[303,258,19,90,7,9,10])). % 0.62/0.94 cnf(314,plain, % 0.62/0.94 (P1(f3(f3(a1,a2),a4),f3(a2,a4),f3(a2,a1))), % 0.62/0.94 inference(scs_inference,[],[147,279,111,9])). % 0.62/0.94 cnf(316,plain, % 0.62/0.94 (P1(f3(f6(a4),a5),a5,f6(a4))), % 0.62/0.94 inference(scs_inference,[],[309,147,279,111,2,4,9,10])). % 0.62/0.94 cnf(320,plain, % 0.62/0.94 (P1(f3(a2,a1),a1,a2)), % 0.62/0.94 inference(scs_inference,[],[210,23,7,9])). % 0.62/0.94 cnf(327,plain, % 0.62/0.94 (P1(f6(a4),f3(a2,f3(a1,a2)),a5)), % 0.62/0.94 inference(scs_inference,[],[103,309,316,9])). % 0.62/0.94 cnf(332,plain, % 0.62/0.94 (P1(f3(a1,a2),f6(a4),a5)), % 0.62/0.94 inference(scs_inference,[],[327,94,312,9])). % 0.62/0.94 cnf(334,plain, % 0.62/0.94 (P1(f3(a2,a1),a5,f3(a2,a4))), % 0.62/0.94 inference(scs_inference,[],[1,327,94,320,312,7,9,10])). % 0.62/0.94 cnf(337,plain, % 0.62/0.94 (P1(f3(a1,a2),f3(a2,a4),a5)), % 0.62/0.94 inference(scs_inference,[],[332,285,3,9])). % 0.62/0.94 cnf(343,plain, % 0.62/0.94 (P1(f3(a2,a4),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[226,86,334,9])). % 0.62/0.94 cnf(352,plain, % 0.62/0.94 (P1(f3(a1,a2),a5,f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[337,343,314,178,129,4,9,10])). % 0.62/0.94 cnf(354,plain, % 0.62/0.94 (P1(f3(a2,f6(a4)),f3(a1,a2),a5)), % 0.62/0.94 inference(scs_inference,[],[337,78,352,9])). % 0.62/0.94 cnf(359,plain, % 0.62/0.94 (P1(x3591,x3592,f3(x3591,x3592))), % 0.62/0.94 inference(rename_variables,[],[7])). % 0.62/0.94 cnf(361,plain, % 0.62/0.94 (P1(f3(a2,a5),a5,f3(a1,f3(a1,a2)))), % 0.62/0.94 inference(scs_inference,[],[354,291,196,137,7,359,9,10])). % 0.62/0.94 cnf(364,plain, % 0.62/0.94 (P1(a2,a1,f3(a2,f3(a1,a2)))), % 0.62/0.94 inference(scs_inference,[],[94,70,5,9])). % 0.62/0.94 cnf(374,plain, % 0.62/0.94 (P1(a1,f3(a2,f6(a4)),a5)), % 0.62/0.94 inference(scs_inference,[],[221,133,247,9])). % 0.62/0.94 cnf(383,plain, % 0.62/0.94 (P1(f6(a4),f3(a1,a2),f3(f3(a4,a4),a5))), % 0.62/0.94 inference(scs_inference,[],[67,158,301,9])). % 0.62/0.94 cnf(391,plain, % 0.62/0.94 (P1(f3(a1,a2),f3(a2,a4),f3(f3(a4,a4),a5))), % 0.62/0.94 inference(scs_inference,[],[383,82,312,9])). % 0.62/0.94 cnf(393,plain, % 0.62/0.94 (P1(a1,a5,f3(a2,f6(a4)))), % 0.62/0.94 inference(scs_inference,[],[383,354,374,82,129,312,9,10])). % 0.62/0.95 cnf(395,plain, % 0.62/0.95 (P1(f3(f3(a2,a4),a5),f6(a4),a5)), % 0.62/0.95 inference(scs_inference,[],[343,19,7,9])). % 0.62/0.95 cnf(400,plain, % 0.62/0.95 (P1(f3(a2,f6(a4)),f3(a2,a4),a2)), % 0.62/0.95 inference(scs_inference,[],[391,154,115,9])). % 0.62/0.95 cnf(402,plain, % 0.62/0.95 (P1(f3(f3(a2,a4),a5),a5,f6(a4))), % 0.62/0.95 inference(scs_inference,[],[391,395,154,115,2,4,9,10])). % 0.62/0.95 cnf(408,plain, % 0.62/0.95 (P1(f3(a2,f6(a4)),a5,a1)), % 0.62/0.95 inference(scs_inference,[],[400,118,374,343,237,393,9,10])). % 0.62/0.95 cnf(410,plain, % 0.62/0.95 (P1(a1,f3(a1,a2),a2)), % 0.62/0.95 inference(scs_inference,[],[400,78,408,9])). % 0.62/0.95 cnf(426,plain, % 0.62/0.95 (P1(f6(a4),f3(a2,f6(a4)),a2)), % 0.62/0.95 inference(scs_inference,[],[263,133,402,9])). % 0.62/0.95 cnf(435,plain, % 0.62/0.95 (P1(f3(a2,f6(a4)),a4,a2)), % 0.62/0.95 inference(scs_inference,[],[410,26,393,9])). % 0.62/0.95 cnf(442,plain, % 0.62/0.95 (P1(f6(a4),a2,a4)), % 0.62/0.95 inference(scs_inference,[],[435,291,426,78,361,4,9,10])). % 0.62/0.95 cnf(445,plain, % 0.62/0.95 ($false), % 0.62/0.95 inference(scs_inference,[],[327,364,442,8,9]), % 0.62/0.95 ['proof']). % 0.62/0.95 % SZS output end Proof % 0.62/0.95 % Total time :0.270000s %------------------------------------------------------------------------------