%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN311-1 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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.83s % Output : CNFRefutation 0.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN311-1 : TPTP v8.2.0. Released v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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 19:14:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.57 start to proof:theBenchmark % 0.54/0.82 %------------------------------------------- % 0.54/0.82 % File :CSE---1.7 % 0.54/0.82 % Problem :theBenchmark % 0.54/0.82 % Transform :cnf % 0.54/0.82 % Format :tptp:raw % 0.54/0.82 % Command :java -jar mcs_scs.jar %d %s % 0.54/0.82 % 0.54/0.82 % Result :Theorem 0.210000s % 0.54/0.82 % Output :CNFRefutation 0.210000s % 0.54/0.82 %------------------------------------------- % 0.54/0.82 %-------------------------------------------------------------------------- % 0.54/0.82 % File : SYN311-1 : TPTP v8.2.0. Released v1.2.0. % 0.54/0.82 % Domain : Syntactic % 0.54/0.82 % Problem : Problem for testing satisfiability % 0.54/0.82 % Version : Especial. % 0.54/0.82 % English : % 0.54/0.82 % 0.54/0.82 % Refs : [FL+93] Fermuller et al. (1993), Resolution Methods for the De % 0.54/0.82 % Source : [FL+93] % 0.54/0.82 % Names : H2 [FL+93] % 0.54/0.82 % 0.54/0.82 % Status : Unsatisfiable % 0.54/0.83 % Rating : 0.09 v8.2.0, 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.21 v6.0.0, 0.33 v5.5.0, 0.19 v5.4.0, 0.17 v5.3.0, 0.25 v5.2.0, 0.23 v5.1.0, 0.12 v5.0.0, 0.13 v4.0.1, 0.14 v3.4.0, 0.00 v2.7.0, 0.25 v2.6.0, 0.14 v2.5.0, 0.43 v2.4.0, 0.29 v2.3.0, 0.14 v2.2.1, 0.17 v2.1.0, 0.00 v2.0.0 % 0.54/0.83 % Syntax : Number of clauses : 6 ( 2 unt; 0 nHn; 6 RR) % 0.54/0.83 % Number of literals : 10 ( 0 equ; 5 neg) % 0.54/0.83 % Maximal clause size : 2 ( 1 avg) % 0.54/0.83 % Maximal term depth : 3 ( 1 avg) % 0.54/0.83 % Number of predicates : 1 ( 1 usr; 0 prp; 4-4 aty) % 0.54/0.83 % Number of functors : 6 ( 6 usr; 4 con; 0-1 aty) % 0.54/0.83 % Number of variables : 16 ( 0 sgn) % 0.54/0.83 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.54/0.83 % 0.54/0.83 % Comments : This set belongs to the class PVD [FL+93] p.192. % 0.54/0.83 %-------------------------------------------------------------------------- % 0.54/0.83 cnf(clause1,negated_conjecture, % 0.54/0.83 ( p(X3,X,X1,X2) % 0.54/0.83 | ~ p(X,X1,X2,X3) ) ). % 0.54/0.83 % 0.54/0.83 cnf(clause2,negated_conjecture, % 0.54/0.83 ( p(X3,X2,X1,X) % 0.54/0.83 | ~ p(X,X1,X2,X3) ) ). % 0.54/0.83 % 0.54/0.83 cnf(clause3,negated_conjecture, % 0.54/0.83 ( p(X,X1,X2,g(X3)) % 0.54/0.83 | ~ p(X,X1,X2,X3) ) ). % 0.54/0.83 % 0.54/0.83 cnf(clause4,negated_conjecture, % 0.54/0.83 ( p(f(X),X1,X2,X3) % 0.54/0.83 | ~ p(X,X1,X2,X3) ) ). % 0.54/0.83 % 0.54/0.83 cnf(clause5,negated_conjecture, % 0.54/0.83 p(a,b,c,d) ). % 0.54/0.83 % 0.54/0.83 cnf(clause6,negated_conjecture, % 0.54/0.83 ~ p(f(g(d)),f(g(c)),f(g(b)),f(g(a))) ). % 0.54/0.83 % 0.54/0.83 %-------------------------------------------------------------------------- % 0.54/0.83 %------------------------------------------- % 0.54/0.83 % Proof found % 0.54/0.83 % SZS status Theorem for theBenchmark % 0.54/0.83 % SZS output start Proof % 0.54/0.83 %ClaNum:6(EqnAxiom:0) % 0.54/0.83 %VarNum:32(SingletonVarNum:16) % 0.54/0.83 %MaxLitNum:2 % 0.54/0.83 %MaxfuncDepth:2 % 0.54/0.83 %SharedTerms:14 % 0.54/0.83 %goalClause: 1 2 3 4 5 6 % 0.54/0.83 %singleGoalClaCount:2 % 0.54/0.83 [1]P1(a1,a2,a3,a4) % 0.54/0.83 [2]~P1(f6(f5(a4)),f6(f5(a3)),f6(f5(a2)),f6(f5(a1))) % 0.54/0.83 [3]~P1(x34,x33,x32,x31)+P1(x31,x32,x33,x34) % 0.54/0.83 [4]~P1(x42,x43,x44,x41)+P1(x41,x42,x43,x44) % 0.54/0.83 [5]~P1(x51,x52,x53,x54)+P1(x51,x52,x53,f5(x54)) % 0.54/0.83 [6]~P1(x61,x62,x63,x64)+P1(f6(x61),x62,x63,x64) % 0.54/0.83 %EqnAxiom % 0.54/0.83 % 0.54/0.83 %------------------------------------------- % 0.54/0.83 cnf(7,plain, % 0.54/0.83 (~P1(f6(f5(a1)),f6(f5(a2)),f6(f5(a3)),f6(f5(a4)))), % 0.54/0.83 inference(scs_inference,[],[2,3])). % 0.54/0.83 cnf(9,plain, % 0.54/0.83 (~P1(f6(f5(a3)),f6(f5(a2)),f6(f5(a1)),f6(f5(a4)))), % 0.54/0.83 inference(scs_inference,[],[2,3,4])). % 0.54/0.83 cnf(15,plain, % 0.54/0.83 (~P1(f5(a1),f6(f5(a2)),f6(f5(a3)),f6(f5(a4)))), % 0.54/0.83 inference(scs_inference,[],[7,9,3,6])). % 0.54/0.83 cnf(17,plain, % 0.54/0.83 (~P1(f6(f5(a2)),f6(f5(a3)),f6(f5(a4)),f6(f5(a1)))), % 0.54/0.83 inference(scs_inference,[],[7,9,3,6,4])). % 0.54/0.83 cnf(19,plain, % 0.54/0.83 (~P1(f6(f5(a4)),f6(f5(a3)),f6(f5(a2)),f5(a1))), % 0.54/0.83 inference(scs_inference,[],[15,3])). % 0.54/0.83 cnf(21,plain, % 0.54/0.83 (~P1(f6(f5(a2)),f6(f5(a3)),f6(f5(a4)),f5(a1))), % 0.54/0.83 inference(scs_inference,[],[15,3,4])). % 0.54/0.83 cnf(27,plain, % 0.54/0.83 (~P1(f6(f5(a2)),f6(f5(a3)),f6(f5(a4)),a1)), % 0.54/0.83 inference(scs_inference,[],[21,5])). % 0.54/0.83 cnf(29,plain, % 0.54/0.83 (~P1(f5(a1),f6(f5(a4)),f6(f5(a3)),f6(f5(a2)))), % 0.54/0.83 inference(scs_inference,[],[21,5,3])). % 0.54/0.83 cnf(31,plain, % 0.54/0.83 (~P1(f5(a4),f6(f5(a3)),f6(f5(a2)),f5(a1))), % 0.54/0.83 inference(scs_inference,[],[19,21,5,3,6])). % 0.54/0.83 cnf(33,plain, % 0.54/0.83 (~P1(f6(f5(a3)),f6(f5(a2)),f5(a1),f6(f5(a4)))), % 0.54/0.83 inference(scs_inference,[],[19,21,5,3,6,4])). % 0.54/0.83 cnf(35,plain, % 0.54/0.83 (~P1(f5(a4),f6(f5(a3)),f6(f5(a2)),a1)), % 0.54/0.83 inference(scs_inference,[],[31,5])). % 0.54/0.83 cnf(37,plain, % 0.54/0.83 (~P1(f5(a1),f6(f5(a2)),f6(f5(a3)),f5(a4))), % 0.54/0.83 inference(scs_inference,[],[31,5,3])). % 0.54/0.83 cnf(39,plain, % 0.54/0.83 (~P1(f5(a2),f6(f5(a3)),f6(f5(a4)),a1)), % 0.54/0.83 inference(scs_inference,[],[31,27,5,3,6])). % 0.54/0.83 cnf(43,plain, % 0.54/0.83 (~P1(f5(a1),f6(f5(a2)),f6(f5(a3)),a4)), % 0.54/0.83 inference(scs_inference,[],[37,5])). % 0.54/0.83 cnf(45,plain, % 0.54/0.83 (~P1(a1,f6(f5(a2)),f6(f5(a3)),f5(a4))), % 0.54/0.83 inference(scs_inference,[],[37,35,5,3])). % 0.54/0.83 cnf(47,plain, % 0.54/0.83 (~P1(f5(a3),f6(f5(a2)),f6(f5(a1)),f6(f5(a4)))), % 0.54/0.83 inference(scs_inference,[],[37,35,9,5,3,6])). % 0.54/0.83 cnf(49,plain, % 0.54/0.83 (~P1(f6(f5(a2)),f6(f5(a3)),f5(a4),f5(a1))), % 0.54/0.83 inference(scs_inference,[],[37,35,9,5,3,6,4])). % 0.54/0.83 cnf(51,plain, % 0.54/0.83 (~P1(a1,f6(f5(a2)),f6(f5(a3)),a4)), % 0.54/0.83 inference(scs_inference,[],[45,5])). % 0.54/0.83 cnf(53,plain, % 0.54/0.83 (~P1(f6(f5(a4)),f6(f5(a1)),f6(f5(a2)),f5(a3))), % 0.54/0.83 inference(scs_inference,[],[47,45,5,3])). % 0.54/0.83 cnf(55,plain, % 0.54/0.83 (~P1(f5(a2),f6(f5(a3)),f6(f5(a4)),f5(a1))), % 0.54/0.83 inference(scs_inference,[],[47,45,21,5,3,6])). % 0.54/0.83 cnf(57,plain, % 0.54/0.83 (~P1(f6(f5(a2)),f6(f5(a1)),f6(f5(a4)),f5(a3))), % 0.54/0.83 inference(scs_inference,[],[47,45,21,5,3,6,4])). % 0.54/0.83 cnf(59,plain, % 0.54/0.83 (~P1(f6(f5(a4)),f6(f5(a1)),f6(f5(a2)),a3)), % 0.54/0.83 inference(scs_inference,[],[53,5])). % 0.54/0.83 cnf(61,plain, % 0.54/0.83 (~P1(f5(a4),f6(f5(a1)),f6(f5(a2)),f5(a3))), % 0.54/0.83 inference(scs_inference,[],[53,5,6])). % 0.54/0.83 cnf(63,plain, % 0.54/0.83 (~P1(a1,f6(f5(a4)),f6(f5(a3)),f5(a2))), % 0.54/0.83 inference(scs_inference,[],[39,53,5,6,3])). % 0.54/0.84 cnf(65,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a4)),a1,f5(a2))), % 0.54/0.84 inference(scs_inference,[],[39,53,5,6,3,4])). % 0.54/0.84 cnf(67,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a1)),f6(f5(a2)),a3)), % 0.54/0.84 inference(scs_inference,[],[61,5])). % 0.54/0.84 cnf(69,plain, % 0.54/0.84 (~P1(f5(a1),f6(f5(a4)),f6(f5(a3)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[55,61,5,3])). % 0.54/0.84 cnf(71,plain, % 0.54/0.84 (~P1(f5(a2),f6(f5(a3)),f6(f5(a4)),f6(f5(a1)))), % 0.54/0.84 inference(scs_inference,[],[55,61,17,5,3,6])). % 0.54/0.84 cnf(73,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a4)),f5(a1),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[55,61,17,5,3,6,4])). % 0.54/0.84 cnf(75,plain, % 0.54/0.84 (~P1(f5(a1),f6(f5(a4)),f6(f5(a3)),a2)), % 0.54/0.84 inference(scs_inference,[],[69,5])). % 0.54/0.84 cnf(77,plain, % 0.54/0.84 (~P1(f5(a2),f6(f5(a1)),f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[69,57,5,6])). % 0.54/0.84 cnf(79,plain, % 0.54/0.84 (~P1(a3,f6(f5(a2)),f6(f5(a1)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[67,69,57,5,6,3])). % 0.54/0.84 cnf(81,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f6(f5(a2)),a3,f5(a4))), % 0.54/0.84 inference(scs_inference,[],[67,69,57,5,6,3,4])). % 0.54/0.84 cnf(83,plain, % 0.54/0.84 (~P1(f5(a2),f6(f5(a1)),f6(f5(a4)),a3)), % 0.54/0.84 inference(scs_inference,[],[77,5])). % 0.54/0.84 cnf(85,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f6(f5(a4)),f6(f5(a3)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[71,77,5,3])). % 0.54/0.84 cnf(87,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a2)),f5(a1),f6(f5(a4)))), % 0.54/0.84 inference(scs_inference,[],[71,77,33,5,3,6])). % 0.54/0.84 cnf(89,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a4)),f6(f5(a1)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[71,77,33,5,3,6,4])). % 0.54/0.84 cnf(91,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f6(f5(a4)),f6(f5(a3)),a2)), % 0.54/0.84 inference(scs_inference,[],[85,5])). % 0.54/0.84 cnf(93,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),f6(f5(a1)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[85,89,5,6])). % 0.54/0.84 cnf(95,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f5(a1),f6(f5(a2)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[85,87,89,5,6,3])). % 0.54/0.84 cnf(97,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f6(f5(a3)),f5(a2),f6(f5(a1)))), % 0.54/0.84 inference(scs_inference,[],[85,87,89,5,6,3,4])). % 0.54/0.84 cnf(99,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),f6(f5(a1)),a2)), % 0.54/0.84 inference(scs_inference,[],[93,5])). % 0.54/0.84 cnf(103,plain, % 0.54/0.84 (~P1(f5(a4),f5(a1),f6(f5(a2)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[93,95,59,5,3,6])). % 0.54/0.84 cnf(105,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f6(f5(a1)),f5(a2),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[93,95,59,5,3,6,4])). % 0.54/0.84 cnf(107,plain, % 0.54/0.84 (~P1(f5(a4),f5(a1),f6(f5(a2)),a3)), % 0.54/0.84 inference(scs_inference,[],[103,5])). % 0.54/0.84 cnf(109,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a3)),f5(a2),f6(f5(a1)))), % 0.54/0.84 inference(scs_inference,[],[103,97,5,6])). % 0.54/0.84 cnf(111,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a2)),f5(a1),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[103,97,5,6,3])). % 0.54/0.84 cnf(115,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a2)),f5(a1),a4)), % 0.54/0.84 inference(scs_inference,[],[111,5])). % 0.54/0.84 cnf(117,plain, % 0.54/0.84 (~P1(a2,f6(f5(a3)),f6(f5(a4)),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[75,111,5,3])). % 0.54/0.84 cnf(119,plain, % 0.54/0.84 (~P1(f5(a2),f6(f5(a3)),f5(a4),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[75,111,49,5,3,6])). % 0.54/0.84 cnf(121,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f6(f5(a3)),a2,f5(a1))), % 0.54/0.84 inference(scs_inference,[],[75,111,49,5,3,6,4])). % 0.54/0.84 cnf(123,plain, % 0.54/0.84 (~P1(f5(a2),f6(f5(a3)),f5(a4),a1)), % 0.54/0.84 inference(scs_inference,[],[119,5])). % 0.54/0.84 cnf(125,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),f5(a1),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[119,73,5,6])). % 0.54/0.84 cnf(127,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f5(a2),f6(f5(a3)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[109,119,73,5,6,3])). % 0.54/0.84 cnf(129,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f5(a2),f6(f5(a1)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[109,119,73,5,6,3,4])). % 0.54/0.84 cnf(132,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f5(a2),f6(f5(a3)),a4)), % 0.54/0.84 inference(scs_inference,[],[127,5])). % 0.54/0.84 cnf(134,plain, % 0.54/0.84 (~P1(f5(a2),f5(a1),f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[127,125,5,3])). % 0.54/0.84 cnf(136,plain, % 0.54/0.84 (~P1(f5(a1),f5(a2),f6(f5(a3)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[127,125,5,3,6])). % 0.54/0.84 cnf(140,plain, % 0.54/0.84 (~P1(f5(a2),f5(a1),f6(f5(a4)),a3)), % 0.54/0.84 inference(scs_inference,[],[134,5])). % 0.54/0.84 cnf(142,plain, % 0.54/0.84 (~P1(f5(a1),f5(a2),f6(f5(a3)),a4)), % 0.54/0.84 inference(scs_inference,[],[134,132,5,6])). % 0.54/0.84 cnf(144,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a3)),f5(a2),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[134,136,132,5,6,3])). % 0.54/0.84 cnf(152,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a1)),f5(a2),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[144,91,105,5,3,6])). % 0.54/0.84 cnf(154,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f5(a2),f5(a1),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[144,91,105,5,3,6,4])). % 0.54/0.84 cnf(156,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a1)),f5(a2),a3)), % 0.54/0.84 inference(scs_inference,[],[152,5])). % 0.54/0.84 cnf(158,plain, % 0.54/0.84 (~P1(f5(a3),f5(a2),f6(f5(a1)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[152,129,5,6])). % 0.54/0.84 cnf(160,plain, % 0.54/0.84 (~P1(a4,f6(f5(a3)),f5(a2),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[142,152,129,5,6,3])). % 0.54/0.84 cnf(164,plain, % 0.54/0.84 (~P1(f5(a3),f5(a2),f6(f5(a1)),a4)), % 0.54/0.84 inference(scs_inference,[],[158,5])). % 0.54/0.84 cnf(166,plain, % 0.54/0.84 (~P1(a4,f6(f5(a3)),f6(f5(a2)),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[158,43,5,3])). % 0.54/0.84 cnf(168,plain, % 0.54/0.84 (~P1(f5(a3),f5(a2),f5(a1),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[158,43,154,5,3,6])). % 0.54/0.84 cnf(174,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),a1,f5(a2))), % 0.54/0.84 inference(scs_inference,[],[63,65,5,6])). % 0.54/0.84 cnf(176,plain, % 0.54/0.84 (~P1(f5(a4),f5(a1),f5(a2),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[63,168,65,5,6,3])). % 0.54/0.84 cnf(180,plain, % 0.54/0.84 (~P1(a3,f6(f5(a2)),f6(f5(a1)),a4)), % 0.54/0.84 inference(scs_inference,[],[79,5])). % 0.54/0.84 cnf(182,plain, % 0.54/0.84 (~P1(a3,f6(f5(a4)),f6(f5(a1)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[79,83,5,3])). % 0.54/0.84 cnf(184,plain, % 0.54/0.84 (~P1(f5(a1),f6(f5(a2)),a3,f5(a4))), % 0.54/0.84 inference(scs_inference,[],[79,83,81,5,3,6])). % 0.54/0.84 cnf(190,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a3)),a2,f5(a1))), % 0.54/0.84 inference(scs_inference,[],[117,121,5,6])). % 0.54/0.84 cnf(192,plain, % 0.54/0.84 (~P1(a2,f6(f5(a1)),f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[117,99,121,5,6,3])). % 0.54/0.84 cnf(194,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a4)),f5(a1),a2)), % 0.54/0.84 inference(scs_inference,[],[117,99,121,5,6,3,4])). % 0.54/0.84 cnf(196,plain, % 0.54/0.84 (~P1(a4,f6(f5(a3)),f6(f5(a2)),a1)), % 0.54/0.84 inference(scs_inference,[],[166,5])). % 0.54/0.84 cnf(198,plain, % 0.54/0.84 (~P1(a4,f5(a1),f6(f5(a2)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[166,115,5,3])). % 0.54/0.84 cnf(200,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),f5(a1),a2)), % 0.54/0.84 inference(scs_inference,[],[166,115,194,5,3,6])). % 0.54/0.84 cnf(206,plain, % 0.54/0.84 (~P1(a1,f5(a4),f6(f5(a3)),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[176,123,5,3])). % 0.54/0.84 cnf(210,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),a1,a2)), % 0.54/0.84 inference(scs_inference,[],[174,5])). % 0.54/0.84 cnf(212,plain, % 0.54/0.84 (~P1(f6(f5(a4)),a1,f5(a2),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[174,5,4])). % 0.54/0.84 cnf(218,plain, % 0.54/0.84 (~P1(f5(a1),f6(f5(a2)),a3,a4)), % 0.54/0.84 inference(scs_inference,[],[184,5])). % 0.54/0.84 cnf(220,plain, % 0.54/0.84 (~P1(f5(a4),a3,f6(f5(a2)),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[184,5,3])). % 0.54/0.84 cnf(222,plain, % 0.54/0.84 (~P1(f6(f5(a2)),a3,f5(a4),f5(a1))), % 0.54/0.84 inference(scs_inference,[],[184,5,3,4])). % 0.54/0.84 cnf(226,plain, % 0.54/0.84 (~P1(f5(a4),f6(f5(a3)),a2,a1)), % 0.54/0.84 inference(scs_inference,[],[190,5])). % 0.54/0.84 cnf(234,plain, % 0.54/0.84 (~P1(a3,f6(f5(a4)),f6(f5(a1)),a2)), % 0.54/0.84 inference(scs_inference,[],[182,5])). % 0.54/0.84 cnf(236,plain, % 0.54/0.84 (~P1(a2,f5(a1),f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[200,182,5,3])). % 0.54/0.84 cnf(238,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f5(a1),a2,f5(a3))), % 0.54/0.84 inference(scs_inference,[],[200,182,5,3,4])). % 0.54/0.84 cnf(242,plain, % 0.54/0.84 (~P1(a2,f6(f5(a1)),f6(f5(a4)),a3)), % 0.54/0.84 inference(scs_inference,[],[192,5])). % 0.54/0.84 cnf(244,plain, % 0.54/0.84 (~P1(f6(f5(a1)),f6(f5(a4)),f5(a3),a2)), % 0.54/0.84 inference(scs_inference,[],[192,5,4])). % 0.54/0.84 cnf(250,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a4)),f5(a1),f6(f5(a2)))), % 0.54/0.84 inference(scs_inference,[],[29,3,4])). % 0.54/0.84 cnf(251,plain, % 0.54/0.84 (~P1(a4,f6(f5(a3)),f5(a2),a1)), % 0.54/0.84 inference(scs_inference,[],[160,5])). % 0.54/0.84 cnf(253,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a4)),f5(a1),f6(f5(a2)))), % 0.54/0.84 inference(scs_inference,[],[250,160,5,6])). % 0.54/0.84 cnf(255,plain, % 0.54/0.84 (~P1(f6(f5(a2)),f5(a1),f6(f5(a4)),f6(f5(a3)))), % 0.54/0.84 inference(scs_inference,[],[250,160,5,6,3])). % 0.54/0.84 cnf(257,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f5(a1),f6(f5(a2)),f6(f5(a3)))), % 0.54/0.84 inference(scs_inference,[],[250,160,5,6,3,4])). % 0.54/0.84 cnf(261,plain, % 0.54/0.84 (~P1(f5(a2),f5(a1),f6(f5(a4)),f6(f5(a3)))), % 0.54/0.84 inference(scs_inference,[],[255,198,5,6])). % 0.54/0.84 cnf(263,plain, % 0.54/0.84 (~P1(f6(f5(a2)),f5(a1),f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[255,253,198,5,6,3])). % 0.54/0.84 cnf(265,plain, % 0.54/0.84 (~P1(f6(f5(a4)),f5(a3),a2,f6(f5(a1)))), % 0.54/0.84 inference(scs_inference,[],[255,253,244,198,5,6,3,4])). % 0.54/0.84 cnf(271,plain, % 0.54/0.84 (~P1(a3,f5(a2),f6(f5(a1)),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[263,156,257,5,6,3])). % 0.54/0.84 cnf(277,plain, % 0.54/0.84 (~P1(f5(a4),f5(a3),a2,f6(f5(a1)))), % 0.54/0.84 inference(scs_inference,[],[206,265,5,6])). % 0.54/0.84 cnf(285,plain, % 0.54/0.84 (~P1(a3,f6(f5(a4)),f5(a1),f5(a2))), % 0.54/0.84 inference(scs_inference,[],[140,212,5,3])). % 0.54/0.84 cnf(287,plain, % 0.54/0.84 (~P1(f5(a4),a1,f5(a2),a3)), % 0.54/0.84 inference(scs_inference,[],[140,212,5,3,6])). % 0.54/0.84 cnf(293,plain, % 0.54/0.84 (~P1(f6(f5(a1)),a2,f5(a3),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[277,220,5,3])). % 0.54/0.84 cnf(299,plain, % 0.54/0.84 (~P1(f6(f5(a2)),a3,f5(a4),a1)), % 0.54/0.84 inference(scs_inference,[],[222,5])). % 0.54/0.84 cnf(301,plain, % 0.54/0.84 (~P1(f5(a2),a3,f5(a4),a1)), % 0.54/0.84 inference(scs_inference,[],[222,5,6])). % 0.54/0.84 cnf(303,plain, % 0.54/0.84 (~P1(a3,f5(a2),a1,f5(a4))), % 0.54/0.84 inference(scs_inference,[],[287,222,5,6,3])). % 0.54/0.84 cnf(317,plain, % 0.54/0.84 (~P1(a1,f5(a4),a3,f5(a2))), % 0.54/0.84 inference(scs_inference,[],[301,236,5,3])). % 0.54/0.84 cnf(323,plain, % 0.54/0.84 (~P1(f5(a4),f5(a1),a2,a3)), % 0.54/0.84 inference(scs_inference,[],[238,5,6])). % 0.54/0.84 cnf(325,plain, % 0.54/0.84 (~P1(a3,f6(f5(a2)),f5(a1),f5(a4))), % 0.54/0.84 inference(scs_inference,[],[107,238,5,6,3])). % 0.54/0.84 cnf(331,plain, % 0.54/0.84 (~P1(a4,f6(f5(a1)),f5(a2),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[271,164,5,3])). % 0.54/0.84 cnf(337,plain, % 0.54/0.84 (~P1(f5(a1),a2,a3,f5(a4))), % 0.54/0.84 inference(scs_inference,[],[323,285,5,4])). % 0.54/0.84 cnf(343,plain, % 0.54/0.84 (~P1(f5(a1),a2,f5(a3),a4)), % 0.54/0.84 inference(scs_inference,[],[293,5,6])). % 0.54/0.84 cnf(351,plain, % 0.54/0.84 (~P1(a4,f6(f5(a1)),f6(f5(a2)),a3)), % 0.54/0.84 inference(scs_inference,[],[325,180,5,3])). % 0.54/0.84 cnf(359,plain, % 0.54/0.84 (~P1(a4,f5(a3),a2,f5(a1))), % 0.54/0.84 inference(scs_inference,[],[343,331,5,3])). % 0.54/0.84 cnf(363,plain, % 0.54/0.84 (P1(a4,a3,a2,f5(a1))), % 0.54/0.84 inference(scs_inference,[],[1,3,5])). % 0.54/0.84 cnf(372,plain, % 0.54/0.84 (~P1(a2,a1,f6(f5(a4)),f5(a3))), % 0.54/0.84 inference(scs_inference,[],[210,303,5,3])). % 0.54/0.84 cnf(374,plain, % 0.54/0.84 (~P1(f6(f5(a4)),a1,a2,f5(a3))), % 0.54/0.84 inference(scs_inference,[],[210,303,5,3,4])). % 0.54/0.84 cnf(380,plain, % 0.54/0.84 (~P1(f6(f5(a2)),f6(f5(a3)),a4,a1)), % 0.54/0.84 inference(scs_inference,[],[51,372,5,4])). % 0.54/0.84 cnf(388,plain, % 0.54/0.84 (~P1(f5(a4),a1,a2,a3)), % 0.54/0.84 inference(scs_inference,[],[374,5,6])). % 0.54/0.84 cnf(392,plain, % 0.54/0.84 (~P1(f6(f5(a3)),f6(f5(a2)),a1,a4)), % 0.54/0.84 inference(scs_inference,[],[196,380,374,5,6,3,4])). % 0.54/0.84 cnf(396,plain, % 0.54/0.84 (~P1(f5(a3),f6(f5(a2)),a1,a4)), % 0.54/0.84 inference(scs_inference,[],[317,392,5,6])). % 0.54/0.85 cnf(400,plain, % 0.54/0.85 (~P1(f6(f5(a4)),f6(f5(a1)),a2,a3)), % 0.54/0.85 inference(scs_inference,[],[234,251,317,392,5,6,3,4])). % 0.54/0.85 cnf(402,plain, % 0.54/0.85 (~P1(f5(a1),a2,a3,a4)), % 0.54/0.85 inference(scs_inference,[],[337,5])). % 0.54/0.85 cnf(404,plain, % 0.54/0.85 (~P1(f5(a4),f6(f5(a1)),a2,a3)), % 0.54/0.85 inference(scs_inference,[],[337,400,5,6])). % 0.54/0.85 cnf(406,plain, % 0.54/0.85 (~P1(a3,a2,a1,f5(a4))), % 0.54/0.85 inference(scs_inference,[],[388,337,400,5,6,3])). % 0.54/0.85 cnf(408,plain, % 0.54/0.85 (~P1(f6(f5(a1)),f6(f5(a4)),a3,a2)), % 0.54/0.85 inference(scs_inference,[],[242,388,337,400,5,6,3,4])). % 0.54/0.85 cnf(412,plain, % 0.54/0.85 (~P1(f5(a1),f6(f5(a4)),a3,a2)), % 0.54/0.85 inference(scs_inference,[],[359,408,5,6])). % 0.54/0.85 cnf(422,plain, % 0.54/0.85 (~P1(f6(f5(a1)),f6(f5(a2)),a3,a4)), % 0.54/0.85 inference(scs_inference,[],[351,299,406,5,3,4])). % 0.54/0.85 cnf(426,plain, % 0.54/0.85 (~P1(a1,a2,f6(f5(a3)),f5(a4))), % 0.54/0.85 inference(scs_inference,[],[226,168,5,3])). % 0.83/0.85 cnf(428,plain, % 0.83/0.85 (~P1(f6(f5(a3)),a2,a1,f5(a4))), % 0.83/0.85 inference(scs_inference,[],[226,168,5,3,4])). % 0.83/0.85 cnf(434,plain, % 0.83/0.85 (~P1(a4,a1,f6(f5(a2)),f5(a3))), % 0.83/0.85 inference(scs_inference,[],[396,426,5,3])). % 0.83/0.85 cnf(436,plain, % 0.83/0.85 (~P1(f6(f5(a2)),a1,a4,f5(a3))), % 0.83/0.85 inference(scs_inference,[],[396,426,5,3,4])). % 0.83/0.85 cnf(444,plain, % 0.83/0.85 (~P1(f6(f5(a1)),a2,a3,f5(a4))), % 0.83/0.85 inference(scs_inference,[],[404,428,5,6,4])). % 0.83/0.85 cnf(450,plain, % 0.83/0.85 (~P1(f6(f5(a4)),a3,a2,f5(a1))), % 0.83/0.85 inference(scs_inference,[],[412,434,5,4])). % 0.83/0.85 cnf(460,plain, % 0.83/0.85 (~P1(f6(f5(a2)),a3,a4,f5(a1))), % 0.83/0.85 inference(scs_inference,[],[218,436,5,6,4])). % 0.83/0.85 cnf(466,plain, % 0.83/0.85 (~P1(f5(a2),a3,a4,f5(a1))), % 0.83/0.85 inference(scs_inference,[],[444,460,5,6])). % 0.83/0.85 cnf(476,plain, % 0.83/0.85 (~P1(f6(f5(a2)),a3,a4,f6(f5(a1)))), % 0.83/0.85 inference(scs_inference,[],[422,450,5,6,4])). % 0.83/0.85 cnf(480,plain, % 0.83/0.85 (~P1(f6(f5(a4)),f5(a1),f5(a2),f6(f5(a3)))), % 0.83/0.85 inference(scs_inference,[],[261,3,4])). % 0.83/0.85 cnf(485,plain, % 0.83/0.85 (~P1(a3,a4,f5(a1),f5(a2))), % 0.83/0.85 inference(scs_inference,[],[466,480,5,6,4])). % 0.83/0.85 cnf(495,plain, % 0.83/0.85 ($false), % 0.83/0.85 inference(scs_inference,[],[402,476,485,363,5,6,4,3]), % 0.83/0.85 ['proof']). % 0.83/0.85 % SZS output end Proof % 0.83/0.85 % Total time :0.210000s %------------------------------------------------------------------------------