%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ056-2.005 : TPTP v8.2.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n008.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 13:42:15 EDT 2024 % Result : Unsatisfiable 56.70s 57.01s % Output : CNFRefutation 56.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PUZ056-2.005 : TPTP v8.2.0. Released v3.5.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n008.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 : Tue Jun 18 10:20:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 56.70/57.00 %------------------------------------------- % 56.70/57.00 % File :CSE---1.7 % 56.70/57.00 % Problem :theBenchmark % 56.70/57.00 % Transform :cnf % 56.70/57.00 % Format :tptp:raw % 56.70/57.00 % Command :java -jar mcs_scs.jar %d %s % 56.70/57.00 % 56.70/57.00 % Result :Theorem 56.170000s % 56.70/57.00 % Output :CNFRefutation 56.170000s % 56.70/57.00 %------------------------------------------- % 56.70/57.00 %------------------------------------------------------------------------------ % 56.70/57.00 % File : PUZ056-2.005 : TPTP v8.2.0. Released v3.5.0. % 56.70/57.01 % Domain : Puzzles % 56.70/57.01 % Problem : Towers of Hanoi k=05 % 56.70/57.01 % Version : Especial. % 56.70/57.01 % English : Each instance encodes Tower of Hanoi with n discs as a % 56.70/57.01 % reachability problem. % 56.70/57.01 % 56.70/57.01 % Refs : [NV07] Navarro (2007), Email to Geoff Sutcliffe % 56.70/57.01 % Source : [NV07] % 56.70/57.01 % Names : hanoi-k05 [NV07a] % 56.70/57.01 % 56.70/57.01 % Status : Unsatisfiable % 56.70/57.01 % Rating : 0.00 v3.5.0 % 56.70/57.01 % Syntax : Number of clauses : 16 ( 11 unt; 0 nHn; 15 RR) % 56.70/57.01 % Number of literals : 41 ( 0 equ; 29 neg) % 56.70/57.01 % Maximal clause size : 10 ( 2 avg) % 56.70/57.01 % Maximal term depth : 1 ( 1 avg) % 56.70/57.01 % Number of predicates : 2 ( 2 usr; 0 prp; 2-5 aty) % 56.70/57.01 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 56.70/57.01 % Number of variables : 30 ( 2 sgn) % 56.70/57.01 % SPC : CNF_UNS_EPR_NEQ_HRN % 56.70/57.01 % 56.70/57.01 % Comments : k >= 13 not solved by any prover in less than 1 hr. (2007) % 56.70/57.01 %------------------------------------------------------------------------------ % 56.70/57.01 cnf(rule1,axiom, % 56.70/57.01 ( ~ p(I,T1,T2,T3,T4) % 56.70/57.01 | p(J,T1,T2,T3,T4) ) ). % 56.70/57.01 % 56.70/57.01 cnf(rule2,axiom, % 56.70/57.01 ( ~ p(T0,I,T2,T3,T4) % 56.70/57.01 | ~ neq(T0,I) % 56.70/57.01 | ~ neq(T0,J) % 56.70/57.01 | p(T0,J,T2,T3,T4) ) ). % 56.70/57.01 % 56.70/57.01 cnf(rule3,axiom, % 56.70/57.01 ( ~ p(T0,T1,I,T3,T4) % 56.70/57.01 | ~ neq(T0,I) % 56.70/57.01 | ~ neq(T0,J) % 56.70/57.01 | ~ neq(T1,I) % 56.70/57.01 | ~ neq(T1,J) % 56.70/57.01 | p(T0,T1,J,T3,T4) ) ). % 56.70/57.01 % 56.70/57.01 cnf(rule4,axiom, % 56.70/57.01 ( ~ p(T0,T1,T2,I,T4) % 56.70/57.01 | ~ neq(T0,I) % 56.70/57.01 | ~ neq(T0,J) % 56.70/57.01 | ~ neq(T1,I) % 56.70/57.01 | ~ neq(T1,J) % 56.70/57.01 | ~ neq(T2,I) % 56.70/57.01 | ~ neq(T2,J) % 56.70/57.01 | p(T0,T1,T2,J,T4) ) ). % 56.70/57.01 % 56.70/57.01 cnf(rule5,axiom, % 56.70/57.01 ( ~ p(T0,T1,T2,T3,I) % 56.70/57.01 | ~ neq(T0,I) % 56.70/57.01 | ~ neq(T0,J) % 56.70/57.01 | ~ neq(T1,I) % 56.70/57.01 | ~ neq(T1,J) % 56.70/57.01 | ~ neq(T2,I) % 56.70/57.01 | ~ neq(T2,J) % 56.70/57.01 | ~ neq(T3,I) % 56.70/57.01 | ~ neq(T3,J) % 56.70/57.01 | p(T0,T1,T2,T3,J) ) ). % 56.70/57.01 % 56.70/57.01 cnf(neq1,axiom, % 56.70/57.01 ~ neq(s0,s0) ). % 56.70/57.01 % 56.70/57.01 cnf(neq2,axiom, % 56.70/57.01 neq(s0,s1) ). % 56.70/57.01 % 56.70/57.01 cnf(neq3,axiom, % 56.70/57.01 neq(s0,s2) ). % 56.70/57.01 % 56.70/57.01 cnf(neq4,axiom, % 56.70/57.01 neq(s1,s0) ). % 56.70/57.01 % 56.70/57.01 cnf(neq5,axiom, % 56.70/57.01 ~ neq(s1,s1) ). % 56.70/57.01 % 56.70/57.01 cnf(neq6,axiom, % 56.70/57.01 neq(s1,s2) ). % 56.70/57.01 % 56.70/57.01 cnf(neq7,axiom, % 56.70/57.01 neq(s2,s0) ). % 56.70/57.01 % 56.70/57.01 cnf(neq8,axiom, % 56.70/57.01 neq(s2,s1) ). % 56.70/57.01 % 56.70/57.01 cnf(neq9,axiom, % 56.70/57.01 ~ neq(s2,s2) ). % 56.70/57.01 % 56.70/57.01 cnf(init,axiom, % 56.70/57.01 p(s0,s0,s0,s0,s0) ). % 56.70/57.01 % 56.70/57.01 cnf(goal,negated_conjecture, % 56.70/57.01 ~ p(s2,s2,s2,s2,s2) ). % 56.70/57.01 % 56.70/57.01 %------------------------------------------------------------------------------ % 56.70/57.01 %------------------------------------------- % 56.70/57.01 % Proof found % 56.70/57.01 % SZS status Theorem for theBenchmark % 56.70/57.01 % SZS output start Proof % 56.70/57.01 %ClaNum:16(EqnAxiom:0) % 56.70/57.01 %VarNum:90(SingletonVarNum:30) % 56.70/57.01 %MaxLitNum:10 % 56.70/57.01 %MaxfuncDepth:0 % 56.70/57.01 %SharedTerms:14 % 56.70/57.01 %goalClause: 11 % 56.70/57.01 %singleGoalClaCount:1 % 56.70/57.01 [1]P1(a1,a2) % 56.70/57.01 [2]P1(a1,a3) % 56.70/57.01 [3]P1(a2,a1) % 56.70/57.01 [4]P1(a2,a3) % 56.70/57.01 [5]P1(a3,a1) % 56.70/57.01 [6]P1(a3,a2) % 56.70/57.01 [7]P2(a1,a1,a1,a1,a1) % 56.70/57.01 [8]~P1(a1,a1) % 56.70/57.01 [9]~P1(a2,a2) % 56.70/57.01 [10]~P1(a3,a3) % 56.70/57.01 [11]~P2(a3,a3,a3,a3,a3) % 56.70/57.01 [12]P2(x121,x122,x123,x124,x125)+~P2(x126,x122,x123,x124,x125) % 56.70/57.01 [13]~P1(x131,x132)+~P2(x131,x136,x133,x134,x135)+P2(x131,x132,x133,x134,x135)+~P1(x131,x136) % 56.70/57.01 [14]~P1(x142,x143)+~P1(x141,x143)+~P1(x141,x146)+~P2(x141,x142,x146,x144,x145)+P2(x141,x142,x143,x144,x145)+~P1(x142,x146) % 56.70/57.01 [15]~P1(x153,x154)+~P1(x152,x154)+~P1(x152,x156)+~P1(x151,x154)+~P1(x151,x156)+~P2(x151,x152,x153,x156,x155)+P2(x151,x152,x153,x154,x155)+~P1(x153,x156) % 56.70/57.01 [16]~P1(x164,x165)+~P1(x163,x165)+~P1(x163,x166)+~P1(x162,x165)+~P1(x162,x166)+~P1(x161,x165)+~P1(x161,x166)+~P2(x161,x162,x163,x164,x166)+P2(x161,x162,x163,x164,x165)+~P1(x164,x166) % 56.70/57.01 %EqnAxiom % 56.70/57.01 % 56.70/57.01 %------------------------------------------- % 56.78/57.09 cnf(17,plain, % 56.78/57.09 (~P2(x171,a3,a3,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[11,12])). % 56.78/57.09 cnf(19,plain, % 56.78/57.09 (~P2(a1,a2,a3,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[11,1,2,12,13])). % 56.78/57.09 cnf(29,plain, % 56.78/57.09 (~P2(a2,a2,a1,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[19,3,4,12,14])). % 56.78/57.09 cnf(38,plain, % 56.78/57.09 (~P2(x381,a2,a1,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[29,12])). % 56.78/57.09 cnf(886,plain, % 56.78/57.09 (~P2(x8861,a3,a1,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[2,38,1,13,12])). % 56.78/57.09 cnf(1810,plain, % 56.78/57.09 (~P2(x18101,a1,a1,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[3,886,4,13,12])). % 56.78/57.09 cnf(1823,plain, % 56.78/57.09 (~P2(x18231,a1,a3,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[3,17,4,13,12])). % 56.78/57.09 cnf(4937,plain, % 56.78/57.09 (~P2(x49371,a3,a2,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[6,886,5,14,12])). % 56.78/57.09 cnf(9330,plain, % 56.78/57.09 (~P2(x93301,a2,a2,a3,a3)), % 56.78/57.09 inference(scs_inference,[],[1823,4937,1,2,13,14,12])). % 56.78/57.09 cnf(11350,plain, % 56.78/57.09 (~P2(x113501,a1,a1,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[1810,1,2,15,12])). % 56.78/57.09 cnf(14265,plain, % 56.78/57.09 (~P2(x142651,a2,a2,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[9330,4,3,15,12])). % 56.78/57.09 cnf(17571,plain, % 56.78/57.09 (~P2(x175711,a3,a2,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[14265,2,1,13,12])). % 56.78/57.09 cnf(22083,plain, % 56.78/57.09 (~P2(x220831,a1,a2,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[3,17571,4,13,12])). % 56.78/57.09 cnf(22097,plain, % 56.78/57.09 (~P2(x220971,a1,a3,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[22083,2,1,14,12])). % 56.78/57.09 cnf(25010,plain, % 56.78/57.09 (~P2(x250101,a2,a1,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[6,11350,5,13,12])). % 56.78/57.09 cnf(25023,plain, % 56.78/57.09 (~P2(a2,a2,a3,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[6,22097,25010,4,3,5,13,14])). % 56.78/57.09 cnf(25026,plain, % 56.78/57.09 (~P2(x250261,a2,a3,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[6,22097,25010,4,3,5,13,14,12])). % 56.78/57.09 cnf(25033,plain, % 56.78/57.09 (~P2(x250331,a2,a3,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[25023,12])). % 56.78/57.09 cnf(27262,plain, % 56.78/57.09 (~P2(x272621,a3,a3,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[25033,2,1,13,12])). % 56.78/57.09 cnf(48907,plain, % 56.78/57.09 (~P2(a2,a2,a1,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[3,25026,27262,4,13,14])). % 56.78/57.09 cnf(48910,plain, % 56.78/57.09 (~P2(x489101,a1,a3,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[3,25026,27262,4,13,14,12])). % 56.78/57.09 cnf(48918,plain, % 56.78/57.09 (~P2(x489181,a2,a1,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[48907,12])). % 56.78/57.09 cnf(49138,plain, % 56.78/57.09 (~P2(x491381,a1,a2,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[48910,1,2,14,12])). % 56.78/57.09 cnf(50692,plain, % 56.78/57.09 (~P2(x506921,a1,a1,a1,a3)), % 56.78/57.09 inference(scs_inference,[],[5,48918,6,13,12])). % 56.78/57.09 cnf(51565,plain, % 56.78/57.09 (~P2(x515651,a2,a2,a2,a3)), % 56.78/57.09 inference(scs_inference,[],[6,49138,5,13,12])). % 56.78/57.09 cnf(52793,plain, % 56.78/57.09 (~P2(x527931,a1,a1,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[50692,1,2,16,12])). % 56.78/57.09 cnf(52802,plain, % 56.78/57.09 (~P2(x528021,a3,a1,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[52793,4,3,13,12])). % 56.78/57.09 cnf(55260,plain, % 56.78/57.09 (~P2(x552601,a2,a2,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[51565,4,3,16,12])). % 56.78/57.09 cnf(56046,plain, % 56.78/57.09 (~P2(x560461,a2,a1,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[52802,1,2,13,12])). % 56.78/57.09 cnf(60035,plain, % 56.78/57.09 (~P2(x600351,a3,a2,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[55260,2,1,13,12])). % 56.78/57.09 cnf(60931,plain, % 56.78/57.09 (~P2(x609311,a2,a3,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[56046,4,3,14,12])). % 56.78/57.09 cnf(63071,plain, % 56.78/57.09 (~P2(x630711,a3,a3,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[60931,2,1,13,12])). % 56.78/57.09 cnf(64080,plain, % 56.78/57.09 (~P2(x640801,a1,a2,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[60035,3,4,13,12])). % 56.78/57.09 cnf(64091,plain, % 56.78/57.09 (~P2(a1,a1,a3,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[63071,64080,3,2,1,4,13,14])). % 56.78/57.09 cnf(64099,plain, % 56.78/57.09 (~P2(x640991,a1,a3,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[64091,12])). % 56.78/57.09 cnf(67054,plain, % 56.78/57.09 (~P2(x670541,a3,a3,a2,a1)), % 56.78/57.09 inference(scs_inference,[],[64099,4,3,13,12])). % 56.78/57.09 cnf(84623,plain, % 56.78/57.09 (~P2(x846231,a3,a3,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[63071,5,6,15,12])). % 56.78/57.09 cnf(87081,plain, % 56.78/57.09 (~P2(x870811,a3,a2,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[52802,6,5,14,12])). % 56.78/57.09 cnf(87228,plain, % 56.78/57.09 (~P2(x872281,a2,a3,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[84623,1,2,13,12])). % 56.78/57.09 cnf(87242,plain, % 56.78/57.09 (~P2(x872421,a2,a2,a1,a2)), % 56.78/57.09 inference(scs_inference,[],[87081,1,2,13,12])). % 56.78/57.09 cnf(88776,plain, % 56.78/57.09 (~P2(x887761,a3,a3,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[67054,5,6,15,12])). % 56.78/57.09 cnf(88789,plain, % 56.78/57.09 (~P2(x887891,a2,a3,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[88776,1,2,13,12])). % 56.78/57.09 cnf(90497,plain, % 56.78/57.09 (~P2(x904971,a1,a3,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[87228,5,6,13,12])). % 56.78/57.09 cnf(90519,plain, % 56.78/57.09 (~P2(x905191,a1,a3,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[88789,5,6,13,12])). % 56.78/57.09 cnf(93459,plain, % 56.78/57.09 (~P2(x934591,a2,a2,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[87242,3,4,15,12])). % 56.78/57.09 cnf(93469,plain, % 56.78/57.09 (~P2(x934691,a3,a2,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[93459,2,1,13,12])). % 56.78/57.09 cnf(94470,plain, % 56.78/57.09 (~P2(a1,a1,a2,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[90497,93469,3,1,2,4,13,14])). % 56.78/57.09 cnf(94473,plain, % 56.78/57.09 (~P2(x944731,a1,a2,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[90497,93469,3,1,2,4,13,14,12])). % 56.78/57.09 cnf(94480,plain, % 56.78/57.09 (~P2(x944801,a1,a2,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[94470,12])). % 56.78/57.09 cnf(94482,plain, % 56.78/57.09 (~P2(a1,a1,a2,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[90519,1,2,94470,12,14])). % 56.78/57.09 cnf(94490,plain, % 56.78/57.09 (~P2(x944901,a1,a2,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[94482,12])). % 56.78/57.09 cnf(94584,plain, % 56.78/57.09 (~P2(x945841,a1,a3,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[94473,2,1,14,12])). % 56.78/57.09 cnf(102917,plain, % 56.78/57.09 (~P2(x1029171,a3,a2,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[94480,4,3,13,12])). % 56.78/57.09 cnf(102925,plain, % 56.78/57.09 (~P2(x1029251,a3,a3,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[94584,4,3,13,12])). % 56.78/57.09 cnf(102933,plain, % 56.78/57.09 (~P2(x1029331,a3,a2,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[94490,4,3,13,12])). % 56.78/57.09 cnf(105426,plain, % 56.78/57.09 (~P2(a3,a3,a3,a3,a1)), % 56.78/57.09 inference(scs_inference,[],[102925,94584,6,5,13,16])). % 56.78/57.09 cnf(105433,plain, % 56.78/57.09 (~P2(x1054331,a3,a3,a3,a1)), % 56.78/57.09 inference(scs_inference,[],[105426,12])). % 56.78/57.09 cnf(106109,plain, % 56.78/57.09 (~P2(x1061091,a3,a1,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[102933,5,6,14,12])). % 56.78/57.09 cnf(106131,plain, % 56.78/57.09 (~P2(x1061311,a3,a1,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[102917,5,6,14,12])). % 56.78/57.09 cnf(106142,plain, % 56.78/57.09 (~P2(x1061421,a3,a1,a3,a2)), % 56.78/57.09 inference(scs_inference,[],[93469,5,6,14,12])). % 56.78/57.09 cnf(110926,plain, % 56.78/57.09 (~P2(x1109261,a2,a3,a3,a1)), % 56.78/57.09 inference(scs_inference,[],[105433,1,2,13,12])). % 56.78/57.09 cnf(112151,plain, % 56.78/57.09 (~P2(a2,a2,a1,a3,a1)), % 56.78/57.09 inference(scs_inference,[],[106142,110926,3,4,13,14])). % 56.78/57.09 cnf(112161,plain, % 56.78/57.09 (~P2(a2,a1,a1,a2,a2)), % 56.78/57.09 inference(scs_inference,[],[106131,3,4,112151,12,13])). % 56.78/57.09 cnf(112171,plain, % 56.78/57.09 (~P2(a2,a1,a3,a3,a1)), % 56.78/57.09 inference(scs_inference,[],[105433,112161,3,4,12,13])). % 56.78/57.09 cnf(112181,plain, % 56.78/57.09 (~P2(a2,a1,a1,a1,a1)), % 56.78/57.09 inference(scs_inference,[],[106109,112171,3,4,12,13])). % 56.78/57.09 cnf(112189,plain, % 56.78/57.09 ($false), % 56.78/57.09 inference(scs_inference,[],[112181,7,12]), % 56.78/57.09 ['proof']). % 56.89/57.14 % SZS output end Proof % 56.89/57.14 % Total time :56.170000s %------------------------------------------------------------------------------