%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC001-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %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 : Mon Jun 24 11:52:09 EDT 2024 % Result : Unsatisfiable 233.23s 233.17s % Output : CNFRefutation 233.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : MSC001-1 : TPTP v8.2.0. Released v1.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.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 : Sat Jun 22 05:52:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 233.21/233.15 %------------------------------------------- % 233.21/233.15 % File :CSE---1.7 % 233.21/233.15 % Problem :theBenchmark % 233.21/233.15 % Transform :cnf % 233.21/233.15 % Format :tptp:raw % 233.21/233.15 % Command :java -jar mcs_scs.jar %d %s % 233.21/233.15 % 233.21/233.15 % Result :Theorem 232.570000s % 233.21/233.15 % Output :CNFRefutation 232.570000s % 233.21/233.15 %------------------------------------------- % 233.23/233.17 %-------------------------------------------------------------------------- % 233.23/233.17 % File : MSC001-1 : TPTP v8.2.0. Released v1.0.0. % 233.23/233.17 % Domain : Miscellaneous % 233.23/233.17 % Problem : A Blind Hand Problem % 233.23/233.17 % Version : Especial. % 233.23/233.17 % English : % 233.23/233.17 % 233.23/233.17 % Refs : [Pop70] Popplestone (1970), Freddy, Things and Sets % 233.23/233.17 % : [MRS72] Michie et al. (1972), G-deduction % 233.23/233.17 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S % 233.23/233.17 % Source : [SPRFN] % 233.23/233.17 % Names : APABHP [MRS72] % 233.23/233.17 % : APABHP [WM76] % 233.23/233.17 % 233.23/233.17 % Status : Unsatisfiable % 233.23/233.17 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.33 v7.4.0, 0.00 v7.1.0, 0.33 v7.0.0, 0.38 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.12 v5.4.0, 0.10 v5.1.0, 0.09 v5.0.0, 0.07 v4.1.0, 0.00 v2.1.0, 0.12 v2.0.0 % 233.23/233.17 % Syntax : Number of clauses : 18 ( 5 unt; 1 nHn; 16 RR) % 233.23/233.17 % Number of literals : 36 ( 0 equ; 21 neg) % 233.23/233.17 % Maximal clause size : 3 ( 2 avg) % 233.23/233.17 % Maximal term depth : 3 ( 1 avg) % 233.23/233.17 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty) % 233.23/233.17 % Number of functors : 11 ( 11 usr; 7 con; 0-2 aty) % 233.23/233.17 % Number of variables : 39 ( 6 sgn) % 233.23/233.17 % SPC : CNF_UNS_RFO_NEQ_NHN % 233.23/233.17 % 233.23/233.17 % Comments : The clauses are in the original order except that the query % 233.23/233.17 % has been put last. % 233.23/233.17 % : The symbols are explained in [MRS72]. % 233.23/233.17 %-------------------------------------------------------------------------- % 233.23/233.17 cnf(clause_1,axiom, % 233.23/233.17 ( ~ at(A,there,B) % 233.23/233.17 | ~ at(A,here,B) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_2,axiom, % 233.23/233.17 ~ hold(thing(A),do(let_go,B)) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_3,axiom, % 233.23/233.17 ~ red(hand) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_5,axiom, % 233.23/233.17 at(hand,A,do(go(A),B)) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_6,axiom, % 233.23/233.17 at(thing(s),here,now) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_7,axiom, % 233.23/233.17 ( ~ at(thing(A),B,do(go(B),C)) % 233.23/233.17 | at(thing(A),B,C) % 233.23/233.17 | hold(thing(A),C) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_8,axiom, % 233.23/233.17 ( ~ at(hand,A,B) % 233.23/233.17 | ~ at(thing(C),A,B) % 233.23/233.17 | hold(thing(taken(B)),do(pick_up,B)) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_9,axiom, % 233.23/233.17 ( ~ hold(thing(A),B) % 233.23/233.17 | ~ at(hand,C,B) % 233.23/233.17 | at(thing(A),C,B) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_10,axiom, % 233.23/233.17 ( ~ hold(thing(A),B) % 233.23/233.17 | ~ at(thing(A),C,B) % 233.23/233.17 | at(hand,C,B) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_11,axiom, % 233.23/233.17 ( ~ red(A) % 233.23/233.17 | ~ at(A,there,B) % 233.23/233.17 | answer(B) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_12,axiom, % 233.23/233.17 ( ~ at(thing(A),B,C) % 233.23/233.17 | at(thing(A),B,do(go(B),C)) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_13,axiom, % 233.23/233.17 ( ~ hold(thing(A),B) % 233.23/233.17 | hold(thing(A),do(go(C),B)) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_14,axiom, % 233.23/233.17 ( ~ at(hand,A,B) % 233.23/233.17 | at(thing(taken(B)),A,B) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_15,axiom, % 233.23/233.17 ( ~ at(A,B,C) % 233.23/233.17 | at(A,B,do(pick_up,C)) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_16,axiom, % 233.23/233.17 ( ~ at(A,B,C) % 233.23/233.17 | at(A,B,do(let_go,C)) ) ). % 233.23/233.17 % 233.23/233.17 cnf(clause_17,axiom, % 233.23/233.17 ( ~ at(A,B,do(let_go,C)) % 233.23/233.17 | at(A,B,C) ) ). % 233.23/233.17 % 233.23/233.17 cnf(things_here_now_are_red,hypothesis, % 233.23/233.17 ( ~ at(A,here,now) % 233.23/233.17 | red(A) ) ). % 233.23/233.17 % 233.23/233.17 cnf(prove_there_is_a_red_thing,negated_conjecture, % 233.23/233.17 ~ answer(A) ). % 233.23/233.17 % 233.23/233.17 %-------------------------------------------------------------------------- % 233.23/233.17 %------------------------------------------- % 233.23/233.17 % Proof found % 233.23/233.17 % SZS status Theorem for theBenchmark % 233.23/233.17 % SZS output start Proof % 233.23/233.18 %ClaNum:18(EqnAxiom:0) % 233.23/233.18 %VarNum:81(SingletonVarNum:39) % 233.23/233.18 %MaxLitNum:3 % 233.23/233.18 %MaxfuncDepth:2 % 233.23/233.18 %SharedTerms:10 % 233.23/233.18 %goalClause: 4 % 233.23/233.18 %singleGoalClaCount:1 % 233.23/233.18 [3]~P3(a3) % 233.23/233.18 [1]P1(f9(a1),a2,a6) % 233.23/233.18 [4]~P2(x41) % 233.23/233.18 [5]~P4(f9(x51),f5(a7,x52)) % 233.23/233.18 [2]P1(a3,x21,f5(f4(x21),x22)) % 233.23/233.18 [6]P3(x61)+~P1(x61,a2,a6) % 233.23/233.18 [12]~P1(x121,a2,x122)+~P1(x121,a10,x122) % 233.23/233.18 [9]~P1(a3,x92,x91)+P1(f9(f11(x91)),x92,x91) % 233.23/233.18 [10]~P1(x101,x102,x103)+P1(x101,x102,f5(a7,x103)) % 233.23/233.18 [11]~P1(x111,x112,x113)+P1(x111,x112,f5(a8,x113)) % 233.23/233.18 [13]P1(x131,x132,x133)+~P1(x131,x132,f5(a7,x133)) % 233.23/233.18 [7]~P4(f9(x71),x73)+P4(f9(x71),f5(f4(x72),x73)) % 233.23/233.18 [16]~P1(f9(x161),x162,x163)+P1(f9(x161),x162,f5(f4(x162),x163)) % 233.23/233.18 [8]P2(x81)+~P3(x82)+~P1(x82,a10,x81) % 233.23/233.18 [14]~P1(a3,x142,x143)+P1(f9(x141),x142,x143)+~P4(f9(x141),x143) % 233.23/233.18 [15]P1(a3,x151,x152)+~P1(f9(x153),x151,x152)+~P4(f9(x153),x152) % 233.23/233.18 [17]~P1(a3,x172,x171)+~P1(f9(x173),x172,x171)+P4(f9(f11(x171)),f5(a8,x171)) % 233.23/233.18 [18]P1(f9(x181),x183,x182)+P4(f9(x181),x182)+~P1(f9(x181),x183,f5(f4(x183),x182)) % 233.23/233.18 %EqnAxiom % 233.23/233.18 % 233.23/233.18 %------------------------------------------- % 233.23/233.20 cnf(36,plain, % 233.23/233.20 (~P1(f9(a1),a10,x361)), % 233.23/233.20 inference(scs_inference,[],[1,4,6,8])). % 233.23/233.20 cnf(37,plain, % 233.23/233.20 (~P1(f9(f11(f5(f4(a10),x371))),a2,f5(f4(a10),x371))), % 233.23/233.20 inference(scs_inference,[],[2,12,9])). % 233.23/233.20 cnf(43,plain, % 233.23/233.20 (~P1(f9(x431),a10,f5(f4(a2),x432))+~P4(f9(x431),f5(f4(a2),x432))), % 233.23/233.20 inference(scs_inference,[],[2,12,14])). % 233.23/233.20 cnf(44,plain, % 233.23/233.20 (~P1(f9(x441),a10,f5(f4(a2),x442))+~P4(f9(x441),x442)), % 233.23/233.20 inference(scs_inference,[],[43,7])). % 233.23/233.20 cnf(46,plain, % 233.23/233.20 (~P1(f9(x461),a2,f5(f4(a10),x462))+~P4(f9(x461),f5(f4(a10),x462))), % 233.23/233.20 inference(scs_inference,[],[2,12,15])). % 233.23/233.20 cnf(47,plain, % 233.23/233.20 (~P1(f9(x471),a2,f5(f4(a10),x472))+~P4(f9(x471),x472)), % 233.23/233.20 inference(scs_inference,[],[46,7])). % 233.23/233.20 cnf(48,plain, % 233.23/233.20 (~P1(f9(x481),x482,f5(f4(x482),x483))+~P1(f9(f11(f5(f4(x482),x483))),a2,f5(f4(a10),f5(a8,f5(f4(x482),x483))))), % 233.23/233.20 inference(scs_inference,[],[2,47,17])). % 233.23/233.20 cnf(49,plain, % 233.23/233.20 (P1(f9(f11(f5(f4(x491),x492))),x491,f5(a7,f5(f4(x491),x492)))), % 233.23/233.20 inference(scs_inference,[],[2,9,10])). % 233.23/233.20 cnf(52,plain, % 233.23/233.20 (P1(f9(f11(f5(f4(x521),x522))),x521,f5(a8,f5(f4(x521),x522)))), % 233.23/233.20 inference(scs_inference,[],[2,9,11])). % 233.23/233.20 cnf(53,plain, % 233.23/233.20 (P4(f9(f11(f5(f4(x531),x532))),f5(a8,f5(f4(x531),x532)))), % 233.23/233.20 inference(scs_inference,[],[2,9,17])). % 233.23/233.20 cnf(54,plain, % 233.23/233.20 (~P4(f9(a1),f5(f4(a10),x541))), % 233.23/233.20 inference(scs_inference,[],[36,2,10,14])). % 233.23/233.20 cnf(55,plain, % 233.23/233.20 (~P4(f9(a1),x551)), % 233.23/233.20 inference(scs_inference,[],[54,7])). % 233.23/233.20 cnf(57,plain, % 233.23/233.20 (P1(a3,x571,f5(a8,f5(a7,f5(f4(x571),x572))))), % 233.23/233.20 inference(scs_inference,[],[2,10,11])). % 233.23/233.20 cnf(58,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(f4(a2),f5(a7,a6)))), % 233.23/233.20 inference(scs_inference,[],[1,10,16])). % 233.23/233.20 cnf(63,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(a8,f5(a7,a6)))), % 233.23/233.20 inference(scs_inference,[],[1,10,11])). % 233.23/233.20 cnf(70,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(a7,f5(a8,f5(a8,f5(a7,a6)))))), % 233.23/233.20 inference(scs_inference,[],[63,11,10])). % 233.23/233.20 cnf(78,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(f4(a2),f5(a8,a6)))), % 233.23/233.20 inference(scs_inference,[],[1,11,16])). % 233.23/233.20 cnf(79,plain, % 233.23/233.20 (P1(a3,x791,f5(a7,f5(a8,f5(f4(x791),x792))))), % 233.23/233.20 inference(scs_inference,[],[2,11,10])). % 233.23/233.20 cnf(91,plain, % 233.23/233.20 (~P4(f9(x911),x912)+~P1(f9(x911),a10,f5(a7,f5(f4(a2),x912)))), % 233.23/233.20 inference(scs_inference,[],[44,13])). % 233.23/233.20 cnf(94,plain, % 233.23/233.20 (~P4(f9(x941),x942)+~P1(f9(x941),a2,f5(a7,f5(f4(a10),x942)))), % 233.23/233.20 inference(scs_inference,[],[47,13])). % 233.23/233.20 cnf(106,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(a7,f5(f4(a2),f5(f4(a2),f5(a8,a6)))))), % 233.23/233.20 inference(scs_inference,[],[78,16,10])). % 233.23/233.20 cnf(132,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(a7,f5(a7,a6)))), % 233.23/233.20 inference(scs_inference,[],[5,58,18,10])). % 233.23/233.20 cnf(133,plain, % 233.23/233.20 (~P1(a3,x1331,f5(a7,x1332))+P1(f9(f11(x1332)),x1331,x1332)), % 233.23/233.20 inference(scs_inference,[],[9,13])). % 233.23/233.20 cnf(134,plain, % 233.23/233.20 (P1(f9(f11(x1341)),x1342,f5(a7,x1341))+~P1(a3,x1342,f5(a7,x1341))), % 233.23/233.20 inference(scs_inference,[],[133,10])). % 233.23/233.20 cnf(135,plain, % 233.23/233.20 (~P1(a3,x1351,f5(a7,x1352))+P1(f9(f11(x1352)),x1351,f5(a8,f5(a7,x1352)))), % 233.23/233.20 inference(scs_inference,[],[134,11])). % 233.23/233.20 cnf(136,plain, % 233.23/233.20 (~P1(f9(f11(x1361)),a10,f5(a8,f5(a7,x1361)))+~P1(a3,a2,f5(a7,x1361))), % 233.23/233.20 inference(scs_inference,[],[135,12])). % 233.23/233.20 cnf(137,plain, % 233.23/233.20 (~P1(f9(f11(x1371)),a10,f5(a7,x1371))+~P1(a3,a2,f5(a7,x1371))), % 233.23/233.20 inference(scs_inference,[],[136,11])). % 233.23/233.20 cnf(138,plain, % 233.23/233.20 (~P1(f9(f11(x1381)),a10,x1381)+~P1(a3,a2,f5(a7,x1381))), % 233.23/233.20 inference(scs_inference,[],[137,10])). % 233.23/233.20 cnf(139,plain, % 233.23/233.20 (~P1(f9(f11(f5(a8,x1391))),a10,x1391)+~P1(a3,a2,f5(a7,f5(a8,x1391)))), % 233.23/233.20 inference(scs_inference,[],[138,11])). % 233.23/233.20 cnf(141,plain, % 233.23/233.20 (P1(f9(a1),a2,f5(f4(a2),f5(a7,f5(a7,f5(a7,a6)))))), % 233.23/233.20 inference(scs_inference,[],[132,10,16])). % 233.23/233.20 cnf(142,plain, % 233.23/233.20 (P1(f9(f11(f5(f4(x1421),x1422))),x1421,f5(f4(x1421),x1422))), % 233.23/233.20 inference(scs_inference,[],[2,10,133])). % 233.23/233.20 cnf(150,plain, % 233.23/233.20 (P1(f9(f11(x1501)),x1502,f5(a8,x1501))+~P1(a3,x1502,f5(a7,x1501))), % 233.23/233.20 inference(scs_inference,[],[133,11])). % 233.23/233.20 cnf(154,plain, % 233.23/233.20 (~P1(f9(f11(x1541)),a2,x1541)+~P1(a3,a10,f5(a7,x1541))), % 233.23/233.20 inference(scs_inference,[],[133,12])). % 233.23/233.20 cnf(159,plain, % 233.23/233.20 (~P3(f9(f11(x1591)))+~P1(a3,a10,f5(a7,x1591))), % 233.23/233.20 inference(scs_inference,[],[4,133,8])). % 233.23/233.20 cnf(160,plain, % 233.23/233.20 (~P1(f9(f11(x1601)),a2,a6)+~P1(a3,a10,f5(a7,x1601))), % 233.23/233.20 inference(scs_inference,[],[159,6])). % 233.23/233.20 cnf(161,plain, % 233.23/233.20 (~P1(f9(f11(x1611)),a2,f5(a7,a6))+~P1(a3,a10,f5(a7,x1611))), % 233.23/233.20 inference(scs_inference,[],[160,13])). % 233.23/233.20 cnf(171,plain, % 233.23/233.20 (~P1(f9(f11(x1711)),a2,x1711)+~P1(a3,a10,f5(a7,f5(a7,x1711)))), % 233.23/233.20 inference(scs_inference,[],[154,13])). % 233.23/233.20 cnf(173,plain, % 233.23/233.20 (~P1(f9(f11(x1731)),a2,f5(a7,x1731))+~P1(a3,a10,f5(a7,x1731))), % 233.23/233.20 inference(scs_inference,[],[154,13])). % 233.23/233.20 cnf(174,plain, % 233.23/233.20 (~P1(f9(f11(x1741)),a2,f5(f4(a2),f5(a7,x1741)))+~P1(a3,a10,f5(a7,x1741))), % 233.23/233.20 inference(scs_inference,[],[5,173,18])). % 233.23/233.20 cnf(176,plain, % 233.23/233.20 (~P1(f9(f11(f5(a8,x1761))),a2,x1761)+~P1(a3,a10,f5(a7,f5(a8,x1761)))), % 233.23/233.20 inference(scs_inference,[],[154,11])). % 233.23/233.20 cnf(184,plain, % 233.23/233.20 (P1(f9(f11(x1841)),x1842,f5(a7,x1841))+~P1(a3,x1842,f5(a7,f5(a7,x1841)))), % 233.23/233.20 inference(scs_inference,[],[134,13])). % 233.23/233.20 cnf(185,plain, % 233.23/233.20 (P1(f9(f11(x1851)),x1852,f5(a7,f5(a7,x1851)))+~P1(a3,x1852,f5(a7,f5(a7,x1851)))), % 233.23/233.20 inference(scs_inference,[],[184,10])). % 233.23/233.20 cnf(187,plain, % 233.23/233.20 (~P1(a3,x1871,f5(a7,x1872))+P1(f9(f11(x1872)),x1871,f5(f4(x1871),f5(a7,x1872)))), % 233.23/233.20 inference(scs_inference,[],[134,16])). % 233.23/233.20 cnf(188,plain, % 233.23/233.20 (P1(f9(f11(x1881)),x1882,f5(a7,f5(f4(x1882),f5(a7,x1881))))+~P1(a3,x1882,f5(a7,x1881))), % 233.23/233.20 inference(scs_inference,[],[187,10])). % 233.23/233.20 cnf(190,plain, % 233.23/233.20 (~P1(a3,a2,f5(a7,f5(a7,x1901)))+~P1(f9(f11(x1901)),a10,f5(a7,x1901))), % 233.23/233.20 inference(scs_inference,[],[137,13])). % 233.23/233.20 cnf(191,plain, % 233.23/233.20 (~P1(a3,a10,f5(a7,x1911))+~P1(a3,a2,f5(a7,f5(a7,x1911)))), % 233.23/233.20 inference(scs_inference,[],[190,134])). % 233.23/233.20 cnf(193,plain, % 233.23/233.20 (~P1(f9(f11(x1931)),a10,f5(a7,f5(a7,x1931)))+~P1(a3,a2,f5(a7,x1931))), % 233.23/233.20 inference(scs_inference,[],[137,13])). % 233.23/233.20 cnf(194,plain, % 233.23/233.20 (~P1(a3,a10,f5(a7,f5(a7,x1941)))+~P1(a3,a2,f5(a7,x1941))), % 233.23/233.20 inference(scs_inference,[],[193,185])). % 233.23/233.20 cnf(198,plain, % 233.23/233.20 (P1(f9(f11(x1981)),x1982,f5(a8,x1981))+~P1(a3,x1982,f5(a7,f5(a7,x1981)))), % 233.23/233.20 inference(scs_inference,[],[150,13])). % 233.23/233.20 cnf(199,plain, % 233.23/233.20 (P1(f9(f11(x1991)),x1992,f5(a7,f5(a8,x1991)))+~P1(a3,x1992,f5(a7,f5(a7,x1991)))), % 233.23/233.20 inference(scs_inference,[],[198,10])). % 233.23/233.20 cnf(201,plain, % 233.23/233.20 (~P1(f9(f11(x2011)),a10,f5(a8,x2011))+~P1(a3,a2,f5(a7,x2011))), % 233.23/233.20 inference(scs_inference,[],[150,12])). % 233.23/233.20 cnf(205,plain, % 233.23/233.20 (~P1(f9(f11(x2051)),a2,f5(a8,x2051))+~P1(a3,a10,f5(a7,x2051))), % 233.23/233.20 inference(scs_inference,[],[150,12])). % 233.23/233.20 cnf(206,plain, % 233.23/233.20 (~P1(f9(f11(x2061)),a2,f5(a7,f5(a8,x2061)))+~P1(a3,a10,f5(a7,x2061))), % 233.23/233.20 inference(scs_inference,[],[205,13])). % 233.23/233.20 cnf(210,plain, % 233.23/233.20 (P1(a3,x2101,f5(a8,x2102))+~P1(a3,x2101,f5(a7,x2102))+~P4(f9(f11(x2102)),f5(a8,x2102))), % 233.23/233.20 inference(scs_inference,[],[150,15])). % 233.23/233.20 cnf(222,plain, % 233.23/233.20 (~P1(f9(f11(x2221)),a2,f5(a7,x2221))+~P1(a3,a10,f5(a7,f5(a7,x2221)))), % 233.23/233.20 inference(scs_inference,[],[171,13])). % 233.23/233.20 cnf(223,plain, % 233.23/233.20 (~P1(f9(f11(x2231)),a2,f5(f4(a2),f5(a7,x2231)))+~P1(a3,a10,f5(a7,f5(a7,x2231)))), % 233.23/233.20 inference(scs_inference,[],[5,222,18])). % 233.23/233.20 cnf(224,plain, % 233.23/233.20 (~P1(f9(f11(x2241)),a2,f5(a7,f5(f4(a2),f5(a7,x2241))))+~P1(a3,a10,f5(a7,f5(a7,x2241)))), % 233.23/233.20 inference(scs_inference,[],[223,13])). % 233.23/233.20 cnf(231,plain, % 233.23/233.20 (~P1(a3,a2,f5(a7,f5(a7,x2311)))+~P1(f9(f11(x2311)),a10,f5(a8,x2311))), % 233.23/233.20 inference(scs_inference,[],[201,13])). % 233.23/233.20 cnf(282,plain, % 233.23/233.20 (P1(f9(f11(x2821)),x2822,x2821)+~P1(a3,x2822,f5(a7,f5(a7,x2821)))), % 233.23/233.20 inference(scs_inference,[],[184,13])). % 233.23/233.20 cnf(287,plain, % 233.23/233.20 (P1(f9(f11(x2871)),x2872,x2871)+~P1(a3,x2872,f5(a7,f5(a7,f5(a7,x2871))))), % 233.23/233.20 inference(scs_inference,[],[282,13])). % 233.23/233.21 cnf(306,plain, % 233.23/233.21 (P1(a3,x3061,f5(a8,x3062))+~P1(a3,x3061,f5(a7,f5(a7,x3062)))+~P4(f9(f11(x3062)),f5(a8,x3062))), % 233.23/233.21 inference(scs_inference,[],[198,15])). % 233.23/233.21 cnf(309,plain, % 233.23/233.21 (~P1(a3,a10,f5(a7,f5(a7,f5(a7,x3091))))+~P1(f9(f11(x3091)),a2,f5(a7,x3091))), % 233.23/233.21 inference(scs_inference,[],[222,13])). % 233.23/233.21 cnf(310,plain, % 233.23/233.21 (P4(f9(f11(x3101)),f5(a8,x3101))+~P1(f9(f11(x3101)),a10,f5(f4(a10),f5(a8,x3101)))+~P1(a3,a2,f5(a7,f5(a7,x3101)))), % 233.23/233.21 inference(scs_inference,[],[231,18])). % 233.23/233.21 cnf(333,plain, % 233.23/233.21 (~P4(f9(f11(x3331)),f5(f4(a2),f5(a7,x3331)))+~P1(a3,a10,f5(a7,x3331))), % 233.23/233.21 inference(scs_inference,[],[2,174,14])). % 233.23/233.21 cnf(334,plain, % 233.23/233.21 (P1(f9(f11(x3341)),x3342,f5(f4(a2),f5(a7,x3341)))+~P1(f9(f11(x3341)),x3342,f5(f4(x3342),f5(f4(a2),f5(a7,x3341))))+~P1(a3,a10,f5(a7,x3341))), % 233.23/233.21 inference(scs_inference,[],[333,18])). % 233.23/233.21 cnf(336,plain, % 233.23/233.21 (P1(f9(f11(f5(f4(x3361),x3362))),x3361,f5(f4(x3361),f5(a7,f5(f4(x3361),x3362))))), % 233.23/233.21 inference(scs_inference,[],[2,187,10])). % 233.23/233.21 cnf(392,plain, % 233.23/233.21 (P1(f9(f11(x3921)),x3922,f5(a7,f5(a7,x3921)))+~P1(a3,x3922,f5(a7,f5(a7,f5(a7,x3921))))), % 233.23/233.21 inference(scs_inference,[],[185,13])). % 233.23/233.21 cnf(393,plain, % 233.23/233.21 (P1(f9(f11(x3931)),x3932,f5(a7,f5(a8,x3931)))+~P1(a3,x3932,f5(a7,f5(a7,f5(a7,x3931))))), % 233.23/233.21 inference(scs_inference,[],[199,13])). % 233.23/233.21 cnf(519,plain, % 233.23/233.21 (P4(f9(f11(x5191)),f5(a8,x5191))+~P4(f9(f11(x5191)),f5(f4(a10),f5(a8,x5191)))+~P1(a3,a2,f5(a7,f5(a7,x5191)))), % 233.23/233.21 inference(scs_inference,[],[2,310,14])). % 233.23/233.21 cnf(521,plain, % 233.23/233.21 (~P1(a3,a2,f5(a7,x5211))+~P4(f9(f11(x5211)),f5(f4(a10),f5(a8,x5211)))+P4(f9(f11(x5211)),f5(a8,x5211))), % 233.23/233.21 inference(scs_inference,[],[519,10])). % 233.23/233.21 cnf(592,plain, % 233.23/233.21 (~P4(f9(f11(x5921)),f5(a8,x5921))+P1(a3,x5922,f5(a7,f5(a8,x5921)))+~P1(a3,x5922,f5(a7,x5921))), % 233.23/233.21 inference(scs_inference,[],[10,210])). % 233.23/233.21 cnf(595,plain, % 233.23/233.21 (~P4(f9(f11(x5951)),f5(a8,x5951))+P1(a3,x5952,f5(a8,f5(a8,x5951)))+~P1(a3,x5952,f5(a7,x5951))), % 233.23/233.21 inference(scs_inference,[],[11,210])). % 233.23/233.21 cnf(596,plain, % 233.23/233.21 (~P4(f9(f11(f5(f4(x5961),x5962))),f5(a8,f5(f4(x5961),x5962)))+P1(a3,x5961,f5(a8,f5(a8,f5(f4(x5961),x5962))))), % 233.23/233.21 inference(scs_inference,[],[2,595,10])). % 233.23/233.21 cnf(597,plain, % 233.23/233.21 (~P4(f9(f11(x5971)),f5(a8,x5971))+P1(a3,x5972,f5(a8,f5(a8,x5971)))+~P1(a3,x5972,f5(a7,f5(a7,x5971)))), % 233.23/233.21 inference(scs_inference,[],[11,306])). % 233.23/233.21 cnf(676,plain, % 233.23/233.21 (~P4(f9(f11(x6761)),f5(a8,x6761))+~P1(a3,a2,f5(a7,x6761))+~P1(f9(f11(f5(a8,x6761))),a10,f5(a7,f5(a7,f5(a8,x6761))))), % 233.23/233.21 inference(scs_inference,[],[193,592])). % 233.23/233.21 cnf(679,plain, % 233.23/233.21 (~P4(f9(f11(x6791)),f5(a8,x6791))+~P1(a3,a10,f5(a7,x6791))+~P1(f9(f11(f5(a8,x6791))),a2,f5(a7,f5(a8,f5(a8,x6791))))), % 233.23/233.21 inference(scs_inference,[],[206,592])). % 233.23/233.21 cnf(805,plain, % 233.23/233.21 (~P4(f9(f11(x8051)),f5(a8,x8051))+~P1(a3,a2,f5(a8,f5(a8,x8051)))+~P1(a3,a10,f5(a7,f5(a7,x8051)))), % 233.23/233.21 inference(scs_inference,[],[12,597])). % 233.23/233.21 cnf(808,plain, % 233.23/233.21 (~P4(f9(f11(x8081)),f5(a8,x8081))+~P1(a3,a10,f5(a8,f5(a8,x8081)))+~P1(a3,a2,f5(a7,x8081))), % 233.23/233.21 inference(scs_inference,[],[12,595])). % 233.23/233.21 cnf(823,plain, % 233.23/233.21 (~P4(f9(f11(x8231)),f5(a8,x8231))+P1(a3,x8232,f5(a7,f5(a8,f5(a8,x8231))))+~P1(a3,x8232,f5(a7,x8231))), % 233.23/233.21 inference(scs_inference,[],[10,595])). % 233.23/233.21 cnf(849,plain, % 233.23/233.21 (~P4(f9(f11(x8491)),f5(a8,x8491))+P1(a3,x8492,f5(a8,f5(a7,f5(a8,x8491))))+~P1(a3,x8492,f5(a7,x8491))), % 233.23/233.21 inference(scs_inference,[],[11,592])). % 233.23/233.21 cnf(861,plain, % 233.23/233.21 (~P4(f9(f11(x8611)),f5(f4(a10),f5(a8,x8611)))+~P1(a3,a2,f5(a7,x8611))+P4(f9(f11(x8611)),f5(f4(x8612),f5(a8,x8611)))), % 233.23/233.21 inference(scs_inference,[],[7,521])). % 233.23/233.21 cnf(863,plain, % 233.23/233.21 (~P4(f9(f11(x8631)),f5(f4(a10),f5(a8,x8631)))+~P1(f9(f11(x8631)),a2,f5(f4(a10),f5(f4(x8632),f5(a8,x8631))))+~P1(a3,a2,f5(a7,x8631))), % 233.23/233.21 inference(scs_inference,[],[47,861])). % 233.23/233.21 cnf(874,plain, % 233.23/233.21 (P4(f9(f11(x8741)),f5(f4(x8742),f5(a8,x8741)))+~P4(f9(f11(x8741)),f5(f4(a10),f5(a8,x8741)))+~P1(a3,a2,f5(a7,f5(a7,x8741)))), % 233.23/233.21 inference(scs_inference,[],[861,13])). % 233.23/233.21 cnf(910,plain, % 233.23/233.21 (~P4(f9(f11(x9101)),f5(f4(a10),f5(a8,x9101)))+P1(f9(f11(x9101)),x9102,f5(f4(x9102),f5(a8,x9101)))+~P1(a3,a2,f5(a7,f5(a7,x9101)))), % 233.23/233.21 inference(scs_inference,[],[2,874,14])). % 233.23/233.21 cnf(911,plain, % 233.23/233.21 (P1(f9(f11(x9111)),x9112,f5(f4(x9112),f5(a8,x9111)))+~P4(f9(f11(x9111)),f5(a8,x9111))+~P1(a3,a2,f5(a7,f5(a7,x9111)))), % 233.23/233.21 inference(scs_inference,[],[910,7])). % 233.23/233.21 cnf(943,plain, % 233.23/233.21 (~P1(a3,a2,f5(a8,f5(f4(a2),f5(a8,a6))))+P4(f9(f11(f5(a8,f5(f4(a2),f5(a8,a6))))),f5(a8,f5(a8,f5(f4(a2),f5(a8,a6)))))), % 233.23/233.21 inference(scs_inference,[],[78,11,17])). % 233.23/233.21 cnf(948,plain, % 233.23/233.21 (~P1(a3,a10,f5(a7,f5(a7,f5(a8,f5(f4(a2),x9481)))))), % 233.23/233.21 inference(scs_inference,[],[79,224,188])). % 233.23/233.21 cnf(950,plain, % 233.23/233.21 (P1(a3,x9501,f5(a7,f5(a8,f5(f4(x9501),x9502))))), % 233.23/233.21 inference(rename_variables,[],[79])). % 233.23/233.21 cnf(953,plain, % 233.23/233.21 (P1(a3,x9531,f5(a7,f5(a8,f5(f4(x9531),x9532))))), % 233.23/233.21 inference(rename_variables,[],[79])). % 233.23/233.21 cnf(958,plain, % 233.23/233.21 (P1(a3,x9581,f5(a7,f5(a8,f5(f4(x9581),x9582))))), % 233.23/233.21 inference(rename_variables,[],[79])). % 233.23/233.21 cnf(961,plain, % 233.23/233.21 (P1(a3,x9611,f5(a7,f5(a8,f5(f4(x9611),x9612))))), % 233.23/233.21 inference(rename_variables,[],[79])). % 233.23/233.21 cnf(968,plain, % 233.23/233.21 (~P1(a3,a2,f5(a8,f5(a7,f5(f4(a10),x9681))))), % 233.23/233.21 inference(scs_inference,[],[57,37,49,948,79,950,953,958,159,161,287,139,176,309,10,12])). % 233.23/233.21 cnf(977,plain, % 233.23/233.21 (P1(a3,x9771,f5(a7,f5(a8,f5(f4(x9771),x9772))))), % 233.23/233.21 inference(rename_variables,[],[79])). % 233.23/233.21 cnf(979,plain, % 233.23/233.21 (~P1(a3,a2,f5(a7,f5(a7,f5(a8,f5(f4(a10),x9791)))))), % 233.23/233.21 inference(scs_inference,[],[141,70,57,37,49,948,55,79,950,953,958,961,977,159,161,287,139,176,309,10,12,13,18,160,191])). % 233.23/233.21 cnf(997,plain, % 233.23/233.21 (P1(a3,x9971,f5(a8,f5(f4(x9971),x9972)))), % 233.23/233.21 inference(scs_inference,[],[106,979,52,53,10,13,15])). % 233.23/233.21 cnf(1013,plain, % 233.23/233.21 (P4(f9(f11(f5(a8,f5(f4(a2),f5(a8,a6))))),f5(a8,f5(a8,f5(f4(a2),f5(a8,a6)))))), % 233.23/233.21 inference(scs_inference,[],[997,943])). % 233.23/233.21 cnf(1036,plain, % 233.23/233.21 (~P1(a3,a2,f5(a7,f5(f4(x10361),x10362)))+~P1(a3,a10,f5(a8,f5(a8,f5(f4(x10361),x10362))))), % 233.23/233.21 inference(scs_inference,[],[53,808])). % 233.23/233.21 cnf(1044,plain, % 233.23/233.21 (~P1(a3,x10441,f5(a7,f5(f4(x10442),x10443)))+P1(a3,x10441,f5(a8,f5(a7,f5(a8,f5(f4(x10442),x10443)))))), % 233.23/233.21 inference(scs_inference,[],[53,805,849])). % 233.23/233.21 cnf(1070,plain, % 233.23/233.21 (P1(f9(f11(f5(f4(x10701),f5(a7,x10702)))),x10701,f5(a7,x10702))), % 233.23/233.21 inference(scs_inference,[],[5,968,142,13,18])). % 233.23/233.21 cnf(1115,plain, % 233.23/233.21 (~P1(a3,a10,f5(a8,f5(a8,f5(f4(a2),x11151))))), % 233.23/233.21 inference(scs_inference,[],[2,1036,10])). % 233.23/233.21 cnf(1118,plain, % 233.23/233.21 (~P1(f9(x11181),a10,f5(a8,f5(a8,f5(f4(a2),x11182))))+~P4(f9(x11181),f5(a8,f5(a8,f5(f4(a2),x11182))))), % 233.23/233.21 inference(scs_inference,[],[1115,13,15])). % 233.23/233.21 cnf(1143,plain, % 233.23/233.21 (P1(a3,x11431,f5(a8,f5(a7,f5(a8,f5(f4(x11431),x11432)))))), % 233.23/233.21 inference(scs_inference,[],[2,1044,10])). % 233.23/233.21 cnf(1147,plain, % 233.23/233.21 (~P1(f9(x11471),a2,f5(a8,f5(a7,f5(a8,f5(f4(a10),x11472)))))+~P4(f9(x11471),f5(a8,f5(a7,f5(a8,f5(f4(a10),x11472)))))), % 233.23/233.21 inference(scs_inference,[],[1143,12,15])). % 233.23/233.21 cnf(1306,plain, % 233.23/233.21 (~P1(f9(f11(f5(a8,f5(a8,f5(f4(a2),x13061))))),a10,f5(a7,f5(a7,f5(a8,f5(a8,f5(f4(a2),x13061))))))), % 233.23/233.21 inference(scs_inference,[],[79,997,52,676,17])). % 233.23/233.21 cnf(1307,plain, % 233.23/233.21 (~P1(f9(f11(f5(a8,f5(a8,f5(f4(a10),x13071))))),a2,f5(a7,f5(a8,f5(a8,f5(a8,f5(f4(a10),x13071))))))), % 233.23/233.21 inference(scs_inference,[],[79,997,52,679,17])). % 233.23/233.21 cnf(1382,plain, % 233.23/233.21 (~P1(f9(f11(f5(a8,f5(f4(a2),x13821)))),a2,f5(f4(a10),f5(f4(x13822),f5(a8,f5(a8,f5(f4(a2),x13821))))))+~P4(f9(f11(f5(a8,f5(f4(a2),x13821)))),f5(a8,f5(a8,f5(f4(a2),x13821))))), % 233.23/233.21 inference(scs_inference,[],[79,863,7])). % 233.23/233.21 cnf(1386,plain, % 233.23/233.21 (P1(f9(f11(f5(a8,f5(f4(a10),x13861)))),x13862,f5(f4(a2),f5(a7,f5(a8,f5(f4(a10),x13861)))))+~P1(f9(f11(f5(a8,f5(f4(a10),x13861)))),x13862,f5(a7,f5(f4(x13862),f5(f4(a2),f5(a7,f5(a8,f5(f4(a10),x13861)))))))), % 233.23/233.21 inference(scs_inference,[],[79,334,13])). % 233.23/233.21 cnf(1592,plain, % 233.23/233.21 (P4(f9(f11(f5(a7,f5(a8,f5(f4(x15921),x15922))))),f5(a8,f5(a7,f5(a8,f5(f4(x15921),x15922)))))), % 233.23/233.21 inference(scs_inference,[],[79,134,17])). % 233.23/233.21 cnf(1615,plain, % 233.23/233.21 (~P4(f9(f11(f5(a8,f5(f4(a2),x16151)))),f5(a8,f5(a8,f5(f4(a2),x16151))))+~P1(f9(f11(f5(a8,f5(a8,f5(a8,f5(f4(a2),x16151)))))),a10,f5(a7,f5(a8,f5(a8,f5(a8,f5(f4(a2),x16151))))))), % 233.23/233.21 inference(scs_inference,[],[79,137,823])). % 233.23/233.21 cnf(1620,plain, % 233.23/233.21 (~P1(f9(f11(f5(a8,f5(f4(a10),x16201)))),a2,f5(f4(a2),f5(a7,f5(a8,f5(f4(a10),x16201)))))), % 233.23/233.21 inference(scs_inference,[],[79,5,173,18])). % 233.23/233.21 cnf(1631,plain, % 233.23/233.21 (~P4(f9(f11(f5(a8,f5(f4(a2),x16311)))),f5(a8,f5(a8,f5(f4(a2),x16311))))+~P1(a3,a10,f5(a7,f5(a7,f5(a8,f5(a8,f5(a8,f5(f4(a2),x16311)))))))), % 233.23/233.21 inference(scs_inference,[],[79,194,823])). % 233.23/233.21 cnf(1640,plain, % 233.23/233.21 (~P4(f9(f11(f5(a8,f5(f4(a2),x16401)))),f5(a8,f5(a8,f5(f4(a2),x16401))))+~P1(f9(f11(f5(a8,f5(a8,f5(a8,f5(f4(a2),x16401)))))),a10,f5(a8,f5(a8,f5(a8,f5(a8,f5(f4(a2),x16401))))))), % 233.23/233.21 inference(scs_inference,[],[79,201,823])). % 233.23/233.21 cnf(1719,plain, % 233.23/233.21 (~P3(f9(f11(x17191)))+~P4(f9(f11(x17191)),f5(a8,x17191))+~P1(a3,a2,f5(a7,f5(a7,x17191)))), % 233.23/233.21 inference(scs_inference,[],[4,8,911])). % 233.23/233.21 cnf(1722,plain, % 233.23/233.21 (~P3(f9(f11(x17221)))+~P1(a3,a2,f5(a7,x17221))+~P4(f9(f11(x17221)),f5(a8,x17221))), % 233.23/233.21 inference(scs_inference,[],[1719,10])). % 233.23/233.21 cnf(1723,plain, % 233.23/233.21 (~P4(f9(f11(x17231)),f5(a8,x17231))+~P1(f9(f11(x17231)),a2,a6)+~P1(a3,a2,f5(a7,x17231))), % 233.23/233.21 inference(scs_inference,[],[1722,6])). % 233.23/233.21 cnf(1736,plain, % 233.23/233.21 (~P4(f9(f11(x17361)),f5(a8,x17361))+~P1(f9(f11(x17361)),a2,f5(a7,a6))+~P1(a3,a2,f5(a7,x17361))), % 233.23/233.21 inference(scs_inference,[],[1723,13])). % 233.23/233.21 cnf(1738,plain, % 233.23/233.21 (~P4(f9(f11(f5(f4(a2),x17381))),f5(a8,f5(f4(a2),x17381)))+~P1(f9(f11(f5(f4(a2),x17381))),a2,a6)), % 233.23/233.21 inference(scs_inference,[],[2,1723,10])). % 233.23/233.21 cnf(1751,plain, % 233.23/233.21 (~P4(f9(f11(f5(f4(a2),x17511))),f5(a8,f5(f4(a2),x17511)))+~P1(f9(f11(f5(f4(a2),x17511))),a2,f5(a7,a6))), % 233.23/233.21 inference(scs_inference,[],[2,1736,10])). % 233.23/233.21 cnf(1917,plain, % 233.23/233.21 (P4(f9(f11(f5(f4(x19171),x19172))),f5(a8,f5(f4(x19171),x19172)))), % 233.23/233.21 inference(rename_variables,[],[53])). % 233.23/233.21 cnf(1919,plain, % 233.23/233.21 ($false), % 233.23/233.21 inference(scs_inference,[],[336,1620,1306,1307,1070,1013,1592,53,1917,47,48,91,94,185,392,393,596,1118,1147,1382,1386,1615,1631,1640,1738,1751]), % 233.23/233.21 ['proof']). % 233.23/233.21 % SZS output end Proof % 233.23/233.21 % Total time :232.570000s %------------------------------------------------------------------------------