%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN312-1 : TPTP v8.2.0. Bugfixed v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.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 19:05:07 EDT 2024 % Result : Unsatisfiable 0.54s 0.77s % Output : CNFRefutation 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN312-1 : TPTP v8.2.0. Bugfixed v2.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 18:44:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 0.54/0.77 %------------------------------------------- % 0.54/0.77 % File :CSE---1.7 % 0.54/0.77 % Problem :theBenchmark % 0.54/0.77 % Transform :cnf % 0.54/0.77 % Format :tptp:raw % 0.54/0.77 % Command :java -jar mcs_scs.jar %d %s % 0.54/0.77 % 0.54/0.77 % Result :Theorem 0.160000s % 0.54/0.77 % Output :CNFRefutation 0.160000s % 0.54/0.77 %------------------------------------------- % 0.54/0.77 %-------------------------------------------------------------------------- % 0.54/0.77 % File : SYN312-1 : TPTP v8.2.0. Bugfixed v2.0.0. % 0.54/0.77 % Domain : Syntactic % 0.54/0.77 % Problem : Problem for testing satisfiability % 0.54/0.77 % Version : Especial. % 0.54/0.77 % English : % 0.54/0.77 % 0.54/0.77 % Refs : [FL+93] Fermuller et al. (1993), Resolution Methods for the De % 0.54/0.77 % Source : [FL+93] % 0.54/0.77 % Names : H3 [FL+93] % 0.54/0.77 % 0.54/0.77 % Status : Unsatisfiable % 0.54/0.77 % Rating : 0.09 v8.2.0, 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.12 v5.0.0, 0.13 v4.0.1, 0.00 v2.6.0, 0.14 v2.5.0, 0.29 v2.4.0, 0.29 v2.3.0, 0.29 v2.2.1, 0.17 v2.1.0 % 0.54/0.77 % Syntax : Number of clauses : 8 ( 3 unt; 0 nHn; 8 RR) % 0.54/0.77 % Number of literals : 14 ( 0 equ; 7 neg) % 0.54/0.77 % Maximal clause size : 3 ( 1 avg) % 0.54/0.77 % Maximal term depth : 3 ( 1 avg) % 0.54/0.77 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 0.54/0.77 % Number of functors : 6 ( 6 usr; 4 con; 0-1 aty) % 0.54/0.77 % Number of variables : 16 ( 0 sgn) % 0.54/0.77 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.54/0.77 % 0.54/0.77 % Comments : % 0.54/0.77 % Bugfixes : v2.0.0 - clause1 fixed. % 0.54/0.77 %-------------------------------------------------------------------------- % 0.54/0.77 cnf(clause1,negated_conjecture, % 0.54/0.77 ( p(X,X3,X2) % 0.54/0.77 | ~ p(X,X1,X2) % 0.54/0.77 | ~ p(X1,X3,X2) ) ). % 0.54/0.77 % 0.54/0.77 cnf(clause2,negated_conjecture, % 0.54/0.77 ( p(X2,X1,X) % 0.54/0.77 | ~ p(X,X1,X2) ) ). % 0.54/0.77 % 0.54/0.77 cnf(clause3,negated_conjecture, % 0.54/0.77 ( p(X1,X,X2) % 0.54/0.77 | ~ p(X,X1,X2) ) ). % 0.54/0.77 % 0.54/0.77 cnf(clause4,negated_conjecture, % 0.54/0.77 ( p(X,X1,f(X2)) % 0.54/0.77 | ~ p(X,X1,X2) ) ). % 0.54/0.77 % 0.54/0.77 cnf(clause5,negated_conjecture, % 0.54/0.77 ( p(g(X),X1,X2) % 0.54/0.77 | ~ p(X,X1,X2) ) ). % 0.54/0.77 % 0.54/0.77 cnf(clause6,negated_conjecture, % 0.54/0.77 p(a,f(b),c) ). % 0.54/0.77 % 0.54/0.77 cnf(clause7,negated_conjecture, % 0.54/0.77 p(f(b),d,c) ). % 0.54/0.77 % 0.54/0.77 cnf(clause8,negated_conjecture, % 0.54/0.77 ~ p(f(g(a)),f(g(d)),f(g(c))) ). % 0.54/0.77 % 0.54/0.77 %-------------------------------------------------------------------------- % 0.54/0.77 %------------------------------------------- % 0.54/0.77 % Proof found % 0.54/0.77 % SZS status Theorem for theBenchmark % 0.54/0.77 % SZS output start Proof % 0.54/0.77 %ClaNum:8(EqnAxiom:0) % 0.54/0.77 %VarNum:33(SingletonVarNum:16) % 0.54/0.77 %MaxLitNum:3 % 0.54/0.77 %MaxfuncDepth:2 % 0.54/0.77 %SharedTerms:14 % 0.54/0.77 %goalClause: 1 2 3 4 5 6 7 8 % 0.54/0.77 %singleGoalClaCount:3 % 0.54/0.77 [1]P1(a1,f3(a2),a4) % 0.54/0.77 [2]P1(f3(a2),a5,a4) % 0.54/0.77 [3]~P1(f3(f6(a1)),f3(f6(a5)),f3(f6(a4))) % 0.54/0.77 [4]~P1(x43,x42,x41)+P1(x41,x42,x43) % 0.54/0.77 [5]~P1(x52,x51,x53)+P1(x51,x52,x53) % 0.54/0.77 [6]~P1(x61,x62,x63)+P1(x61,x62,f3(x63)) % 0.54/0.77 [7]~P1(x71,x72,x73)+P1(f6(x71),x72,x73) % 0.54/0.77 [8]~P1(x81,x84,x83)+P1(x81,x82,x83)+~P1(x84,x82,x83) % 0.54/0.77 %EqnAxiom % 0.54/0.77 % 0.54/0.77 %------------------------------------------- % 0.54/0.78 cnf(9,plain, % 0.54/0.78 (~P1(f3(f6(a4)),f3(f6(a5)),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[3,4])). % 0.54/0.78 cnf(11,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f3(f6(a1)),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[3,4,5])). % 0.54/0.78 cnf(13,plain, % 0.54/0.78 (~P1(f3(f6(a1)),f3(f6(a5)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[3,4,5,6])). % 0.54/0.78 cnf(15,plain, % 0.54/0.78 (P1(a1,a5,a4)), % 0.54/0.78 inference(scs_inference,[],[1,3,2,4,5,6,8])). % 0.54/0.78 cnf(19,plain, % 0.54/0.78 (~P1(f3(f6(a4)),f3(f6(a1)),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[11,4])). % 0.54/0.78 cnf(21,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f3(f6(a4)),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[9,11,4,5])). % 0.54/0.78 cnf(23,plain, % 0.54/0.78 (~P1(f3(f6(a4)),f3(f6(a5)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[9,11,4,5,6])). % 0.54/0.78 cnf(25,plain, % 0.54/0.78 (~P1(x251,a1,a4)+P1(x251,a5,a4)), % 0.54/0.78 inference(scs_inference,[],[9,11,15,4,5,6,8])). % 0.54/0.78 cnf(29,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f3(f6(a1)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[21,13,4,5])). % 0.54/0.78 cnf(31,plain, % 0.54/0.78 (~P1(f3(f6(a4)),f3(f6(a1)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[19,21,13,4,5,6])). % 0.54/0.78 cnf(33,plain, % 0.54/0.78 (~P1(f6(a5),f3(f6(a1)),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[31,4])). % 0.54/0.78 cnf(35,plain, % 0.54/0.78 (~P1(f3(f6(a1)),f3(f6(a4)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[31,4,5])). % 0.54/0.78 cnf(37,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f3(f6(a4)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[31,21,4,5,6])). % 0.54/0.78 cnf(39,plain, % 0.54/0.78 (~P1(a5,f3(f6(a1)),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[31,21,4,5,6,7])). % 0.54/0.78 cnf(41,plain, % 0.54/0.78 (~P1(f6(a4),f3(f6(a1)),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[29,4])). % 0.54/0.78 cnf(45,plain, % 0.54/0.78 (~P1(a5,f3(f6(a1)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[29,39,4,5,6])). % 0.54/0.78 cnf(47,plain, % 0.54/0.78 (~P1(a4,f3(f6(a1)),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[29,39,4,5,6,7])). % 0.54/0.78 cnf(49,plain, % 0.54/0.78 (~P1(f6(a5),f3(f6(a4)),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[35,4])). % 0.54/0.78 cnf(51,plain, % 0.54/0.78 (~P1(a5,f3(f6(a4)),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[35,4,7])). % 0.54/0.78 cnf(55,plain, % 0.54/0.78 (~P1(a4,f3(f6(a1)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[35,47,4,7,5,6])). % 0.54/0.78 cnf(61,plain, % 0.54/0.78 (~P1(f3(f6(a1)),a4,f6(a5))), % 0.54/0.78 inference(scs_inference,[],[55,4,7,5])). % 0.54/0.78 cnf(63,plain, % 0.54/0.78 (~P1(f6(a5),f3(f6(a1)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[55,33,4,7,5,6])). % 0.54/0.78 cnf(65,plain, % 0.54/0.78 (~P1(f6(a4),f3(f6(a1)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[63,4])). % 0.54/0.78 cnf(69,plain, % 0.54/0.78 (~P1(a5,f3(f6(a4)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[63,51,4,5,6])). % 0.54/0.78 cnf(75,plain, % 0.54/0.78 (~P1(f3(f6(a1)),a5,f6(a4))), % 0.54/0.78 inference(scs_inference,[],[45,4,7,5])). % 0.54/0.78 cnf(77,plain, % 0.54/0.78 (~P1(f6(a5),f3(f6(a4)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[45,49,4,7,5,6])). % 0.54/0.78 cnf(79,plain, % 0.54/0.78 (~P1(f6(a1),f3(f6(a4)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[77,4])). % 0.54/0.78 cnf(81,plain, % 0.54/0.78 (~P1(a1,f3(f6(a4)),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[77,4,7])). % 0.54/0.78 cnf(89,plain, % 0.54/0.78 (~P1(a1,f3(f6(a4)),a5)), % 0.54/0.78 inference(scs_inference,[],[69,4,7])). % 0.54/0.78 cnf(93,plain, % 0.54/0.78 (~P1(f6(a1),f3(f6(a5)),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[23,4])). % 0.54/0.78 cnf(95,plain, % 0.54/0.78 (~P1(a1,f3(f6(a5)),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[23,4,7])). % 0.54/0.78 cnf(97,plain, % 0.54/0.78 (~P1(f3(f6(a1)),f6(a4),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[65,23,4,7,5])). % 0.54/0.78 cnf(99,plain, % 0.54/0.78 (~P1(f6(a1),f3(f6(a5)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[65,23,4,7,5,6])). % 0.54/0.78 cnf(101,plain, % 0.54/0.78 (~P1(f6(a1),f3(f6(a4)),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[37,4])). % 0.54/0.78 cnf(103,plain, % 0.54/0.78 (~P1(a1,f3(f6(a5)),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[37,99,4,7])). % 0.54/0.78 cnf(107,plain, % 0.54/0.78 (~P1(f6(a5),a4,f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[61,4])). % 0.54/0.78 cnf(111,plain, % 0.54/0.78 (~P1(f6(a5),a4,f6(a1))), % 0.54/0.78 inference(scs_inference,[],[61,101,4,7,6])). % 0.54/0.78 cnf(113,plain, % 0.54/0.78 (~P1(f3(f6(a4)),f6(a1),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[61,79,101,4,7,6,5])). % 0.54/0.78 cnf(115,plain, % 0.54/0.78 (~P1(f6(a4),a5,f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[75,4])). % 0.54/0.78 cnf(119,plain, % 0.54/0.78 (~P1(f3(f6(a5)),a1,f6(a4))), % 0.54/0.78 inference(scs_inference,[],[75,103,107,4,7,5])). % 0.54/0.78 cnf(121,plain, % 0.54/0.78 (~P1(f6(a4),a5,f6(a1))), % 0.54/0.78 inference(scs_inference,[],[75,103,107,4,7,5,6])). % 0.54/0.78 cnf(123,plain, % 0.54/0.78 (~P1(f6(a5),f3(f6(a4)),a1)), % 0.54/0.78 inference(scs_inference,[],[81,4])). % 0.54/0.78 cnf(125,plain, % 0.54/0.78 (~P1(a5,a4,f6(a1))), % 0.54/0.78 inference(scs_inference,[],[81,111,4,7])). % 0.54/0.78 cnf(127,plain, % 0.54/0.78 (~P1(f3(f6(a4)),a1,f6(a5))), % 0.54/0.78 inference(scs_inference,[],[81,111,4,7,5])). % 0.54/0.78 cnf(132,plain, % 0.54/0.78 (~P1(a4,a5,f6(a1))), % 0.54/0.78 inference(scs_inference,[],[121,4,7])). % 0.54/0.78 cnf(134,plain, % 0.54/0.78 (~P1(a5,f6(a4),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[121,4,7,5])). % 0.54/0.78 cnf(140,plain, % 0.54/0.78 (~P1(f3(f6(a5)),a1,f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[125,95,115,4,7,5])). % 0.54/0.78 cnf(148,plain, % 0.54/0.78 (~P1(f6(a1),a1,a4)), % 0.54/0.78 inference(scs_inference,[],[132,89,123,4,7,5,25])). % 0.54/0.78 cnf(150,plain, % 0.54/0.78 (~P1(f6(a4),a1,f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[119,4])). % 0.54/0.78 cnf(154,plain, % 0.54/0.78 (~P1(f6(a4),a1,f6(a5))), % 0.54/0.78 inference(scs_inference,[],[119,148,4,7,6])). % 0.54/0.78 cnf(156,plain, % 0.54/0.78 (~P1(a1,f6(a1),a4)), % 0.54/0.78 inference(scs_inference,[],[119,148,4,7,6,5])). % 0.54/0.78 cnf(158,plain, % 0.54/0.78 (~P1(f6(a5),f6(a1),f3(f6(a4)))), % 0.54/0.78 inference(scs_inference,[],[113,4])). % 0.54/0.78 cnf(160,plain, % 0.54/0.78 (~P1(a4,a1,f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[113,150,4,7])). % 0.54/0.78 cnf(162,plain, % 0.54/0.78 (~P1(f6(a5),f6(a1),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[113,150,4,7,6])). % 0.54/0.78 cnf(164,plain, % 0.54/0.78 (~P1(f3(f6(a1)),f6(a4),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[113,41,150,4,7,6,5])). % 0.54/0.78 cnf(166,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f6(a4),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[164,4])). % 0.54/0.78 cnf(168,plain, % 0.54/0.78 (~P1(a4,a1,f6(a5))), % 0.54/0.78 inference(scs_inference,[],[164,154,4,7])). % 0.54/0.78 cnf(170,plain, % 0.54/0.78 (~P1(f3(f6(a5)),f6(a4),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[164,154,4,7,6])). % 0.54/0.78 cnf(172,plain, % 0.54/0.78 (~P1(a1,f6(a4),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[164,154,4,7,6,5])). % 0.54/0.78 cnf(174,plain, % 0.54/0.78 (~P1(f6(a5),f6(a4),f3(f6(a1)))), % 0.54/0.78 inference(scs_inference,[],[97,4])). % 0.54/0.78 cnf(176,plain, % 0.54/0.78 (~P1(a5,f6(a1),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[97,162,4,7])). % 0.54/0.78 cnf(178,plain, % 0.54/0.78 (~P1(f6(a5),f6(a4),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[97,162,4,7,6])). % 0.54/0.78 cnf(180,plain, % 0.54/0.78 (~P1(f6(a1),f6(a5),f6(a4))), % 0.54/0.78 inference(scs_inference,[],[97,162,4,7,6,5])). % 0.54/0.78 cnf(182,plain, % 0.54/0.78 (~P1(f6(a5),a1,a4)), % 0.54/0.78 inference(scs_inference,[],[168,4])). % 0.54/0.78 cnf(186,plain, % 0.54/0.78 (~P1(a1,a4,f6(a5))), % 0.54/0.78 inference(scs_inference,[],[168,180,4,7,5])). % 0.54/0.78 cnf(188,plain, % 0.54/0.78 (~P1(f6(a1),f6(a4),f3(f6(a5)))), % 0.54/0.78 inference(scs_inference,[],[170,4])). % 0.54/0.78 cnf(192,plain, % 0.54/0.78 (~P1(f6(a1),f6(a4),f6(a5))), % 0.54/0.78 inference(scs_inference,[],[170,158,4,7,6])). % 0.54/0.78 cnf(194,plain, % 0.54/0.78 (~P1(f6(a4),f3(f6(a5)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[170,158,4,7,6,5])). % 0.54/0.78 cnf(198,plain, % 0.54/0.78 (~P1(a4,f3(f6(a5)),f6(a1))), % 0.54/0.78 inference(scs_inference,[],[134,194,4,7])). % 0.54/0.78 cnf(200,plain, % 0.54/0.78 (~P1(f6(a4),f6(a5),f6(a1))), % 0.54/0.79 inference(scs_inference,[],[178,134,194,4,7,5])). % 0.54/0.79 cnf(206,plain, % 0.54/0.79 (~P1(f6(a4),f6(a1),f6(a5))), % 0.54/0.79 inference(scs_inference,[],[192,176,200,4,7,5])). % 0.54/0.79 cnf(214,plain, % 0.54/0.79 (~P1(f3(f6(a5)),f6(a1),f6(a4))), % 0.54/0.79 inference(scs_inference,[],[172,206,93,4,7,5,6])). % 0.54/0.79 cnf(220,plain, % 0.54/0.79 (~P1(f6(a4),f3(f6(a5)),f3(f6(a1)))), % 0.54/0.79 inference(scs_inference,[],[214,166,174,4,7,5])). % 0.54/0.79 cnf(226,plain, % 0.54/0.79 (~P1(f3(f6(a5)),a4,f6(a1))), % 0.54/0.79 inference(scs_inference,[],[220,140,198,4,7,5])). % 0.54/0.79 cnf(232,plain, % 0.54/0.79 (~P1(f6(a5),a1,f6(a4))), % 0.54/0.79 inference(scs_inference,[],[127,188,4,7,6])). % 0.54/0.79 cnf(243,plain, % 0.54/0.79 (~P1(f6(a1),a4,f3(f6(a5)))), % 0.54/0.79 inference(scs_inference,[],[226,4])). % 0.54/0.79 cnf(245,plain, % 0.54/0.79 (~P1(a5,a1,f6(a4))), % 0.54/0.79 inference(scs_inference,[],[226,232,4,7])). % 0.54/0.79 cnf(257,plain, % 0.54/0.79 (~P1(f6(a4),a1,a5)), % 0.54/0.79 inference(scs_inference,[],[245,4])). % 0.54/0.79 cnf(259,plain, % 0.54/0.79 (~P1(a1,a4,f3(f6(a5)))), % 0.54/0.79 inference(scs_inference,[],[245,243,4,7])). % 0.54/0.79 cnf(263,plain, % 0.54/0.79 (~P1(f6(a5),a4,a1)), % 0.54/0.79 inference(scs_inference,[],[186,4])). % 0.54/0.79 cnf(287,plain, % 0.54/0.79 (~P1(a4,f6(a1),a1)), % 0.54/0.79 inference(scs_inference,[],[156,4])). % 0.54/0.79 cnf(293,plain, % 0.54/0.79 (~P1(f3(f6(a5)),a1,a4)), % 0.54/0.79 inference(scs_inference,[],[160,4])). % 0.54/0.79 cnf(303,plain, % 0.54/0.79 (~P1(a1,f3(f6(a5)),a4)), % 0.54/0.79 inference(scs_inference,[],[259,257,293,4,7,5])). % 0.54/0.79 cnf(307,plain, % 0.54/0.79 (~P1(a5,a1,a4)), % 0.54/0.79 inference(scs_inference,[],[303,182,4,7])). % 0.54/0.79 cnf(309,plain, % 0.54/0.79 (~P1(f6(a1),a4,a1)), % 0.54/0.79 inference(scs_inference,[],[303,182,287,4,7,5])). % 0.54/0.79 cnf(315,plain, % 0.54/0.79 ($false), % 0.54/0.79 inference(scs_inference,[],[15,263,309,307,4,7,5]), % 0.54/0.79 ['proof']). % 0.54/0.79 % SZS output end Proof % 0.54/0.79 % Total time :0.160000s %------------------------------------------------------------------------------