%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ005-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:00 EDT 2024 % Result : Unsatisfiable 58.53s 58.85s % Output : CNFRefutation 58.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : PUZ005-1 : TPTP v8.2.0. Released v1.0.0. % 0.05/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n028.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Tue Jun 18 10:02:23 EDT 2024 % 0.09/0.29 % CPUTime : % 0.15/0.54 start to proof:theBenchmark % 58.53/58.83 %------------------------------------------- % 58.53/58.83 % File :CSE---1.7 % 58.53/58.83 % Problem :theBenchmark % 58.53/58.83 % Transform :cnf % 58.53/58.83 % Format :tptp:raw % 58.53/58.83 % Command :java -jar mcs_scs.jar %d %s % 58.53/58.83 % 58.53/58.83 % Result :Theorem 58.020000s % 58.53/58.83 % Output :CNFRefutation 58.020000s % 58.53/58.83 %------------------------------------------- % 58.53/58.84 %-------------------------------------------------------------------------- % 58.53/58.84 % File : PUZ005-1 : TPTP v8.2.0. Released v1.0.0. % 58.53/58.84 % Domain : Puzzles % 58.53/58.84 % Problem : The Lion and the Unicorn % 58.53/58.84 % Version : Especial. % 58.53/58.84 % English : Lion lies on Monday, Tuesday and Wednesday. Unicorn lies % 58.53/58.84 % on Thursday, Friday and Saturday. Both tell truth on other % 58.53/58.84 % days. Both say yesterday was one of their lying days. Prove % 58.53/58.84 % that today is Thursday. % 58.53/58.84 % 58.53/58.84 % Refs : [Smu78] Smullyan (1978), What is the Name of This Book? The Ri % 58.53/58.84 % : [OS85] Ohlbach & Schmidt-Schauss M. (1985), The Lion and the % 58.53/58.84 % Source : [OS85] % 58.53/58.84 % Names : Lion and the Unicorn [OS85] % 58.53/58.84 % 58.53/58.84 % Status : Unsatisfiable % 58.53/58.84 % Rating : 0.00 v2.5.0, 0.20 v2.4.0, 0.00 v2.2.1, 0.25 v2.1.0, 0.00 v2.0.0 % 58.53/58.84 % Syntax : Number of clauses : 51 ( 3 unt; 6 nHn; 48 RR) % 58.53/58.84 % Number of literals : 112 ( 0 equ; 71 neg) % 58.53/58.84 % Maximal clause size : 7 ( 2 avg) % 58.53/58.84 % Maximal term depth : 2 ( 1 avg) % 58.53/58.84 % Number of predicates : 9 ( 9 usr; 0 prp; 1-3 aty) % 58.53/58.84 % Number of functors : 5 ( 5 usr; 3 con; 0-1 aty) % 58.53/58.84 % Number of variables : 56 ( 0 sgn) % 58.53/58.84 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.53/58.84 % 58.53/58.84 % Comments : % 58.53/58.84 %-------------------------------------------------------------------------- % 58.53/58.84 cnf(it_is_a_day,axiom, % 58.53/58.84 ( monday(X) % 58.53/58.84 | tuesday(X) % 58.53/58.84 | wednesday(X) % 58.53/58.84 | thursday(X) % 58.53/58.84 | friday(X) % 58.53/58.84 | saturday(X) % 58.53/58.84 | sunday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_tuesday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ tuesday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_wednesday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ wednesday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_thursday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ thursday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_friday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ friday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_saturday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ saturday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(monday_not_sunday,axiom, % 58.53/58.84 ( ~ monday(X) % 58.53/58.84 | ~ sunday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(tuesday_not_wednesday,axiom, % 58.53/58.84 ( ~ tuesday(X) % 58.53/58.84 | ~ wednesday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(tuesday_not_thursday,axiom, % 58.53/58.84 ( ~ tuesday(X) % 58.53/58.84 | ~ thursday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(tuesday_not_friday,axiom, % 58.53/58.84 ( ~ tuesday(X) % 58.53/58.84 | ~ friday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(tuesday_not_saturday,axiom, % 58.53/58.84 ( ~ tuesday(X) % 58.53/58.84 | ~ saturday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(tuesday_not_sunday,axiom, % 58.53/58.84 ( ~ tuesday(X) % 58.53/58.84 | ~ sunday(X) ) ). % 58.53/58.84 % 58.53/58.84 cnf(wednesday_not_thursday,axiom, % 58.53/58.84 ( ~ wednesday(X) % 58.53/58.85 | ~ thursday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(wednesday_not_friday,axiom, % 58.53/58.85 ( ~ wednesday(X) % 58.53/58.85 | ~ friday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(wednesday_not_saturday,axiom, % 58.53/58.85 ( ~ wednesday(X) % 58.53/58.85 | ~ saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(wednesday_not_sunday,axiom, % 58.53/58.85 ( ~ wednesday(X) % 58.53/58.85 | ~ sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(thursday_not_friday,axiom, % 58.53/58.85 ( ~ thursday(X) % 58.53/58.85 | ~ friday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(thursday_not_saturday,axiom, % 58.53/58.85 ( ~ thursday(X) % 58.53/58.85 | ~ saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(thursday_not_sunday,axiom, % 58.53/58.85 ( ~ thursday(X) % 58.53/58.85 | ~ sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(friday_not_saturday,axiom, % 58.53/58.85 ( ~ friday(X) % 58.53/58.85 | ~ saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(friday_not_sunday,axiom, % 58.53/58.85 ( ~ friday(X) % 58.53/58.85 | ~ sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(saturday_not_sunday,axiom, % 58.53/58.85 ( ~ saturday(X) % 58.53/58.85 | ~ sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(monday_yesterday,axiom, % 58.53/58.85 ( ~ monday(yesterday(X)) % 58.53/58.85 | tuesday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(tuesday_yesterday,axiom, % 58.53/58.85 ( ~ tuesday(yesterday(X)) % 58.53/58.85 | wednesday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(wednesday_yesterday,axiom, % 58.53/58.85 ( ~ wednesday(yesterday(X)) % 58.53/58.85 | thursday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(thursday_yesterday,axiom, % 58.53/58.85 ( ~ thursday(yesterday(X)) % 58.53/58.85 | friday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(friday_yesterday,axiom, % 58.53/58.85 ( ~ friday(yesterday(X)) % 58.53/58.85 | saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(saturday_yesterday,axiom, % 58.53/58.85 ( ~ saturday(yesterday(X)) % 58.53/58.85 | sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(sunday_yesterday,axiom, % 58.53/58.85 ( ~ sunday(yesterday(X)) % 58.53/58.85 | monday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_monday,axiom, % 58.53/58.85 ( monday(yesterday(X)) % 58.53/58.85 | ~ tuesday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_tuesday,axiom, % 58.53/58.85 ( tuesday(yesterday(X)) % 58.53/58.85 | ~ wednesday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_wednesday,axiom, % 58.53/58.85 ( wednesday(yesterday(X)) % 58.53/58.85 | ~ thursday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_thursday,axiom, % 58.53/58.85 ( thursday(yesterday(X)) % 58.53/58.85 | ~ friday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_friday,axiom, % 58.53/58.85 ( friday(yesterday(X)) % 58.53/58.85 | ~ saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_saturday,axiom, % 58.53/58.85 ( saturday(yesterday(X)) % 58.53/58.85 | ~ sunday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(yesterday_sunday,axiom, % 58.53/58.85 ( sunday(yesterday(X)) % 58.53/58.85 | ~ monday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(lions_lying_days,axiom, % 58.53/58.85 ( ~ member(X,lying_days(lion)) % 58.53/58.85 | monday(X) % 58.53/58.85 | tuesday(X) % 58.53/58.85 | wednesday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(unicorns_lying_days,axiom, % 58.53/58.85 ( ~ member(X,lying_days(unicorn)) % 58.53/58.85 | thursday(X) % 58.53/58.85 | friday(X) % 58.53/58.85 | saturday(X) ) ). % 58.53/58.85 % 58.53/58.85 cnf(lion_lies_on_monday,axiom, % 58.53/58.85 ( ~ monday(X) % 58.53/58.85 | member(X,lying_days(lion)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(lion_lies_on_tuesday,axiom, % 58.53/58.85 ( ~ tuesday(X) % 58.53/58.85 | member(X,lying_days(lion)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(lion_lies_on_wednesday,axiom, % 58.53/58.85 ( ~ wednesday(X) % 58.53/58.85 | member(X,lying_days(lion)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(unicorn_lies_on_thursday,axiom, % 58.53/58.85 ( ~ thursday(X) % 58.53/58.85 | member(X,lying_days(unicorn)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(unicorn_lies_on_friday,axiom, % 58.53/58.85 ( ~ friday(X) % 58.53/58.85 | member(X,lying_days(unicorn)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(unicorn_lies_on_saturday,axiom, % 58.53/58.85 ( ~ saturday(X) % 58.53/58.85 | member(X,lying_days(unicorn)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions1,axiom, % 58.53/58.85 ( member(X,lying_days(T)) % 58.53/58.85 | ~ admits(T,X,Y) % 58.53/58.85 | member(Y,lying_days(T)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions2,axiom, % 58.53/58.85 ( member(X,lying_days(T)) % 58.53/58.85 | admits(T,X,Y) % 58.53/58.85 | ~ member(Y,lying_days(T)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions3,axiom, % 58.53/58.85 ( ~ member(X,lying_days(T)) % 58.53/58.85 | ~ admits(T,X,Y) % 58.53/58.85 | ~ member(Y,lying_days(T)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions4,axiom, % 58.53/58.85 ( ~ member(X,lying_days(T)) % 58.53/58.85 | admits(T,X,Y) % 58.53/58.85 | member(Y,lying_days(T)) ) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions5,axiom, % 58.53/58.85 admits(lion,today,yesterday(today)) ). % 58.53/58.85 % 58.53/58.85 cnf(admissions6,axiom, % 58.53/58.85 admits(unicorn,today,yesterday(today)) ). % 58.53/58.85 % 58.53/58.85 cnf(prove_today_is_thursday,negated_conjecture, % 58.53/58.85 ~ thursday(today) ). % 58.53/58.85 % 58.53/58.85 %-------------------------------------------------------------------------- % 58.53/58.85 %------------------------------------------- % 58.53/58.85 % Proof found % 58.53/58.85 % SZS status Theorem for theBenchmark % 58.53/58.85 % SZS output start Proof % 58.53/58.85 %ClaNum:51(EqnAxiom:0) % 58.53/58.85 %VarNum:125(SingletonVarNum:56) % 58.53/58.85 %MaxLitNum:7 % 58.53/58.85 %MaxfuncDepth:1 % 58.53/58.85 %SharedTerms:9 % 58.53/58.85 %goalClause: 3 % 58.53/58.85 %singleGoalClaCount:1 % 58.53/58.85 [3]~P2(a2) % 58.53/58.85 [1]P1(a1,a2,f4(a2)) % 58.53/58.85 [2]P1(a5,a2,f4(a2)) % 58.53/58.85 [4]~P8(x41)+~P3(x41) % 58.53/58.85 [5]~P9(x51)+~P3(x51) % 58.53/58.85 [6]~P2(x61)+~P3(x61) % 58.53/58.85 [7]~P4(x71)+~P3(x71) % 58.53/58.85 [8]~P6(x81)+~P3(x81) % 58.53/58.85 [9]~P7(x91)+~P3(x91) % 58.53/58.85 [10]~P9(x101)+~P8(x101) % 58.53/58.85 [11]~P2(x111)+~P8(x111) % 58.53/58.85 [12]~P4(x121)+~P8(x121) % 58.53/58.85 [13]~P6(x131)+~P8(x131) % 58.53/58.85 [14]~P7(x141)+~P8(x141) % 58.53/58.85 [15]~P2(x151)+~P9(x151) % 58.53/58.85 [16]~P4(x161)+~P9(x161) % 58.53/58.85 [17]~P6(x171)+~P9(x171) % 58.53/58.85 [18]~P7(x181)+~P9(x181) % 58.53/58.85 [19]~P4(x191)+~P2(x191) % 58.53/58.85 [20]~P6(x201)+~P2(x201) % 58.53/58.85 [21]~P7(x211)+~P2(x211) % 58.53/58.85 [22]~P6(x221)+~P4(x221) % 58.53/58.85 [23]~P7(x231)+~P4(x231) % 58.53/58.85 [24]~P7(x241)+~P6(x241) % 58.53/58.85 [25]~P8(x251)+P3(f4(x251)) % 58.53/58.85 [26]~P9(x261)+P8(f4(x261)) % 58.53/58.85 [27]~P2(x271)+P9(f4(x271)) % 58.53/58.85 [28]~P4(x281)+P2(f4(x281)) % 58.53/58.85 [29]~P6(x291)+P4(f4(x291)) % 58.53/58.85 [30]~P7(x301)+P6(f4(x301)) % 58.53/58.85 [31]~P3(x311)+P7(f4(x311)) % 58.53/58.85 [32]P3(x321)+~P7(f4(x321)) % 58.53/58.85 [33]P8(x331)+~P3(f4(x331)) % 58.53/58.85 [34]P9(x341)+~P8(f4(x341)) % 58.53/58.85 [35]P2(x351)+~P9(f4(x351)) % 58.53/58.85 [36]P4(x361)+~P2(f4(x361)) % 58.53/58.85 [37]P6(x371)+~P4(f4(x371)) % 58.53/58.85 [38]P7(x381)+~P6(f4(x381)) % 58.53/58.85 [39]~P3(x391)+P5(x391,f3(a1)) % 58.53/58.85 [40]~P8(x401)+P5(x401,f3(a1)) % 58.53/58.85 [41]~P9(x411)+P5(x411,f3(a1)) % 58.53/58.85 [42]~P2(x421)+P5(x421,f3(a5)) % 58.53/58.85 [43]~P4(x431)+P5(x431,f3(a5)) % 58.53/58.85 [44]~P6(x441)+P5(x441,f3(a5)) % 58.53/58.85 [48]P1(x481,x482,x483)+P5(x483,f3(x481))+~P5(x482,f3(x481)) % 58.53/58.85 [49]P1(x491,x492,x493)+P5(x492,f3(x491))+~P5(x493,f3(x491)) % 58.53/58.85 [50]~P1(x502,x503,x501)+P5(x501,f3(x502))+P5(x503,f3(x502)) % 58.53/58.85 [51]~P1(x511,x512,x513)+~P5(x513,f3(x511))+~P5(x512,f3(x511)) % 58.53/58.85 [46]P8(x461)+P9(x461)+P3(x461)+~P5(x461,f3(a1)) % 58.53/58.85 [47]P4(x471)+P6(x471)+P2(x471)+~P5(x471,f3(a5)) % 58.53/58.85 [45]P8(x451)+P9(x451)+P2(x451)+P4(x451)+P6(x451)+P7(x451)+P3(x451) % 58.53/58.85 %EqnAxiom % 58.53/58.85 % 58.53/58.85 %------------------------------------------- % 58.53/58.86 cnf(62,plain, % 58.53/58.86 (~P7(x621)+~P3(f4(x621))), % 58.53/58.86 inference(scs_inference,[],[14,33])). % 58.53/58.86 cnf(141,plain, % 58.53/58.86 (P1(a1,f4(a2),x1411)+~P5(x1411,f3(a1))+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[1,49,51])). % 58.53/58.86 cnf(142,plain, % 58.53/58.86 (~P5(x1421,f3(a1))+~P5(f4(a2),f3(a1))+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[141,51])). % 58.53/58.86 cnf(143,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+~P5(a2,f3(a1))), % 58.53/58.86 inference(factoring_inference,[],[142])). % 58.53/58.86 cnf(144,plain, % 58.53/58.86 (~P3(f4(a2))+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[143,39])). % 58.53/58.86 cnf(145,plain, % 58.53/58.86 (~P8(a2)+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[144,25])). % 58.53/58.86 cnf(146,plain, % 58.53/58.86 (~P8(a2)), % 58.53/58.86 inference(scs_inference,[],[145,40])). % 58.53/58.86 cnf(147,plain, % 58.53/58.86 (P3(f4(a2))+P8(f4(a2))+~P5(f4(a2),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[3,46,35])). % 58.53/58.86 cnf(199,plain, % 58.53/58.86 (~P4(f4(x1991))+~P8(x1991)), % 58.53/58.86 inference(scs_inference,[],[7,25])). % 58.53/58.86 cnf(200,plain, % 58.53/58.86 (~P4(f4(f4(x2001)))+~P9(x2001)), % 58.53/58.86 inference(scs_inference,[],[199,26])). % 58.53/58.86 cnf(201,plain, % 58.53/58.86 (P3(a2)+~P4(f4(f4(a2)))+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[146,200,46])). % 58.53/58.86 cnf(266,plain, % 58.53/58.86 (~P7(a2)+~P5(a2,f3(a1))+~P4(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[9,201])). % 58.53/58.86 cnf(267,plain, % 58.53/58.86 (~P6(f4(a2))+~P5(a2,f3(a1))+~P7(a2)), % 58.53/58.86 inference(scs_inference,[],[266,29])). % 58.53/58.86 cnf(268,plain, % 58.53/58.86 (~P7(a2)+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[267,30])). % 58.53/58.86 cnf(269,plain, % 58.53/58.86 (~P5(a2,f3(a1))+~P6(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[268,38])). % 58.53/58.86 cnf(1131,plain, % 58.53/58.86 (~P9(f4(x11311))+~P4(x11311)), % 58.53/58.86 inference(scs_inference,[],[15,28])). % 58.53/58.86 cnf(1147,plain, % 58.53/58.86 (~P9(f4(f4(x11471)))+~P6(x11471)), % 58.53/58.86 inference(scs_inference,[],[1131,29])). % 58.53/58.86 cnf(2257,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+P3(f4(a2))+P3(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[25,147])). % 58.53/58.86 cnf(2522,plain, % 58.53/58.86 (P3(a2)+~P5(a2,f3(a1))+P8(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[146,26,46])). % 58.53/58.86 cnf(2850,plain, % 58.53/58.86 (P6(a2)+~P5(a2,f3(a5))+P2(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[3,28,47])). % 58.53/58.86 cnf(3632,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+P3(f4(f4(a2)))+P7(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[31,2257])). % 58.53/58.86 cnf(3648,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+P7(f4(f4(a2)))+P5(f4(f4(a2)),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[3632,39])). % 58.53/58.86 cnf(3758,plain, % 58.53/58.86 (~P5(a2,f3(a1))+P8(f4(a2))+P7(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[31,2522])). % 58.53/58.86 cnf(3899,plain, % 58.53/58.86 (~P7(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[146,32,33])). % 58.53/58.86 cnf(3903,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+P3(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[3899,3632])). % 58.53/58.86 cnf(3904,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))+P5(f4(f4(a2)),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[3899,3648])). % 58.53/58.86 cnf(4461,plain, % 58.53/58.86 (P5(x44611,f3(a1))+~P8(f4(x44611))), % 58.53/58.86 inference(scs_inference,[],[34,41])). % 58.53/58.86 cnf(4477,plain, % 58.53/58.86 (P5(x44771,f3(a1))+~P3(f4(f4(x44771)))), % 58.53/58.86 inference(scs_inference,[],[4461,33])). % 58.53/58.86 cnf(4524,plain, % 58.53/58.86 (P9(a2)+~P5(a2,f3(a1))+P7(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[34,3758])). % 58.53/58.86 cnf(4711,plain, % 58.53/58.86 (P6(x47111)+~P2(f4(f4(x47111)))), % 58.53/58.86 inference(scs_inference,[],[36,37])). % 58.53/58.86 cnf(4805,plain, % 58.53/58.86 (P5(x48051,f3(a5))+~P2(f4(x48051))), % 58.53/58.86 inference(scs_inference,[],[36,43])). % 58.53/58.86 cnf(4868,plain, % 58.53/58.86 (P4(a2)+~P5(a2,f3(a5))+P6(a2)), % 58.53/58.86 inference(scs_inference,[],[36,2850])). % 58.53/58.86 cnf(5315,plain, % 58.53/58.86 (~P3(f4(f4(a2)))+~P5(a2,f3(a1))+P9(a2)), % 58.53/58.86 inference(scs_inference,[],[62,4524])). % 58.53/58.86 cnf(6031,plain, % 58.53/58.86 (~P8(f4(a2))+~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[40,143])). % 58.53/58.86 cnf(6047,plain, % 58.53/58.86 (~P9(a2)+~P8(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[6031,41])). % 58.53/58.86 cnf(6063,plain, % 58.53/58.86 (~P9(a2)), % 58.53/58.86 inference(scs_inference,[],[6047,26])). % 58.53/58.86 cnf(6072,plain, % 58.53/58.86 (~P5(a2,f3(a1))+~P3(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[6063,5315])). % 58.53/58.86 cnf(6337,plain, % 58.53/58.86 (~P3(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[6072,4477])). % 58.53/58.86 cnf(6338,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[6337,3903])). % 58.53/58.86 cnf(6771,plain, % 58.53/58.86 (~P2(f4(a2))+~P5(a2,f3(a5))), % 58.53/58.86 inference(scs_inference,[],[2,42,51])). % 58.53/58.86 cnf(6787,plain, % 58.53/58.86 (~P4(a2)+~P2(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[6771,43])). % 58.53/58.86 cnf(6803,plain, % 58.53/58.86 (~P4(a2)), % 58.53/58.86 inference(scs_inference,[],[6787,28])). % 58.53/58.86 cnf(6806,plain, % 58.53/58.86 (~P5(a2,f3(a5))+P6(a2)), % 58.53/58.86 inference(scs_inference,[],[6803,4868])). % 58.53/58.86 cnf(6819,plain, % 58.53/58.86 (~P2(f4(a2))+P6(a2)), % 58.53/58.86 inference(scs_inference,[],[6806,4805])). % 58.53/58.86 cnf(6835,plain, % 58.53/58.86 (P6(a2)+~P9(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[6819,35])). % 58.53/58.86 cnf(7215,plain, % 58.53/58.86 (~P9(f4(f4(a2)))+~P2(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[6819,1147])). % 58.53/58.86 cnf(7231,plain, % 58.53/58.86 (~P2(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[7215,27])). % 58.53/58.86 cnf(7529,plain, % 58.53/58.86 (~P4(f4(a2))+~P5(a2,f3(a5))), % 58.53/58.86 inference(scs_inference,[],[2,43,51])). % 58.53/58.86 cnf(7545,plain, % 58.53/58.86 (~P6(a2)+~P4(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[7529,44])). % 58.53/58.86 cnf(7561,plain, % 58.53/58.86 (~P6(a2)), % 58.53/58.86 inference(scs_inference,[],[7545,29])). % 58.53/58.86 cnf(7563,plain, % 58.53/58.86 (~P5(a2,f3(a5))), % 58.53/58.86 inference(scs_inference,[],[7561,6806])). % 58.53/58.86 cnf(7565,plain, % 58.53/58.86 (~P9(f4(f4(a2)))), % 58.53/58.86 inference(scs_inference,[],[7561,6835])). % 58.53/58.86 cnf(8220,plain, % 58.53/58.86 (~P4(f4(a2))), % 58.53/58.86 inference(scs_inference,[],[7561,4711,28])). % 58.53/58.86 cnf(8447,plain, % 58.53/58.86 (~P5(a2,f3(a1))+~P5(f4(a2),f3(a5))), % 58.53/58.86 inference(scs_inference,[],[8220,7231,269,47])). % 58.53/58.86 cnf(8534,plain, % 58.53/58.86 (~P5(f4(f4(a2)),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[6338,7565,6337,4461,46])). % 58.53/58.86 cnf(8535,plain, % 58.53/58.86 (~P5(f4(a2),f3(a1))), % 58.53/58.86 inference(scs_inference,[],[8534,3904])). % 58.53/58.86 cnf(8619,plain, % 58.53/58.86 (~P5(a2,f3(a1))), % 58.53/58.86 inference(scs_inference,[],[2,7563,50,8447])). % 58.53/58.86 cnf(8716,plain, % 58.53/58.86 ($false), % 58.53/58.86 inference(scs_inference,[],[1,8535,8619,50]), % 58.53/58.86 ['proof']). % 58.53/58.86 % SZS output end Proof % 58.53/58.86 % Total time :58.020000s %------------------------------------------------------------------------------