%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ005+1 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n023.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:01 EDT 2024 % Result : Theorem 61.57s 61.72s % Output : CNFRefutation 62.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ005+1 : TPTP v8.2.0. Released v2.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n023.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Tue Jun 18 10:10:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 61.57/61.70 %------------------------------------------- % 61.57/61.70 % File :CSE---1.7 % 61.57/61.70 % Problem :theBenchmark % 61.57/61.70 % Transform :cnf % 61.57/61.70 % Format :tptp:raw % 61.57/61.70 % Command :java -jar mcs_scs.jar %d %s % 61.57/61.70 % 61.57/61.70 % Result :Theorem 61.090000s % 61.57/61.70 % Output :CNFRefutation 61.090000s % 61.57/61.70 %------------------------------------------- % 61.57/61.72 %-------------------------------------------------------------------------- % 61.57/61.72 % File : PUZ005+1 : TPTP v8.2.0. Released v2.2.0. % 61.57/61.72 % Domain : Puzzles % 61.57/61.72 % Problem : The Lion and the Unicorn % 61.57/61.72 % Version : [OS95] axioms. % 61.57/61.72 % English : % 61.57/61.72 % 61.57/61.72 % Refs : [Wei94] Weidenbach (1994), Email to G. Sutcliffe % 61.57/61.72 % : [Wei93] Weidenbach (1993), Extending the Resolution Method wit % 61.57/61.72 % : [Smu78] Smullyan (1978), What is the Name of This Book? The Ri % 61.57/61.72 % : [OS85] Ohlbach & Schmidt-Schauss M. (1985), The Lion and the % 61.57/61.72 % Source : [Wei94] % 61.57/61.72 % Names : % 61.57/61.72 % 61.57/61.72 % Status : Theorem % 61.57/61.72 % Rating : 0.00 v6.3.0, 0.08 v6.2.0, 0.00 v5.5.0, 0.08 v5.4.0, 0.09 v5.3.0, 0.17 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v3.7.0, 0.00 v2.2.1 % 61.57/61.72 % Syntax : Number of formulae : 46 ( 7 unt; 0 def) % 61.57/61.72 % Number of atoms : 110 ( 0 equ) % 61.57/61.72 % Maximal formula atoms : 5 ( 2 avg) % 61.57/61.72 % Number of connectives : 84 ( 20 ~; 0 |; 10 &) % 61.57/61.72 % ( 0 <=>; 54 =>; 0 <=; 0 <~>) % 61.57/61.72 % Maximal formula depth : 8 ( 4 avg) % 61.57/61.72 % Maximal term depth : 2 ( 1 avg) % 61.57/61.72 % Number of predicates : 11 ( 11 usr; 0 prp; 1-3 aty) % 61.57/61.72 % Number of functors : 10 ( 10 usr; 9 con; 0-1 aty) % 61.57/61.72 % Number of variables : 47 ( 46 !; 1 ?) % 61.57/61.72 % SPC : FOF_THM_RFO_NEQ % 61.57/61.72 % 61.57/61.72 % Comments : This problem can be easily solved by sorted theorem provers which % 61.57/61.72 % are able to represent the one place predicates as sorts, but is % 61.57/61.72 % very hard for standard first-order provers. It can be further % 61.57/61.72 % complicated by iterating the 'yesterday' nesting in the theorem, % 61.57/61.72 % e.g. the next iteration would be: -(exists x (day(x) & % 61.57/61.72 % lies(a_lion,x,yesterday(yesterday(x))) & lies(a_unicorn,x, % 61.57/61.72 % yesterday(yesterday(x))))). % 61.57/61.72 %-------------------------------------------------------------------------- % 61.57/61.72 fof(monday,axiom, % 61.57/61.72 monday(a_monday) ). % 61.57/61.72 % 61.57/61.72 fof(tuesday,axiom, % 61.57/61.72 tuesday(a_tuesday) ). % 61.57/61.72 % 61.57/61.72 fof(wednesday,axiom, % 61.57/61.72 wednesday(a_wednesday) ). % 61.57/61.72 % 61.57/61.72 fof(thursday,axiom, % 61.57/61.72 thursday(a_thursday) ). % 61.57/61.72 % 61.57/61.72 fof(friday,axiom, % 61.57/61.72 friday(a_friday) ). % 61.57/61.72 % 61.57/61.72 fof(saturday,axiom, % 61.57/61.72 saturday(a_saturday) ). % 61.57/61.72 % 61.57/61.72 fof(sunday,axiom, % 61.57/61.72 sunday(a_sunday) ). % 61.57/61.72 % 61.57/61.72 fof(monday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( monday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(tuesday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( tuesday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(wednesday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( wednesday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(thursday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( thursday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(friday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( friday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(saturday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( saturday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(sunday_is_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( sunday(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(monday_follows_sunday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( monday(X) % 61.57/61.72 => sunday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(tuesday_follows_monday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( tuesday(X) % 61.57/61.72 => monday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(wednesday_follows_tuesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( wednesday(X) % 61.57/61.72 => tuesday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(thursday_follows_wednesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( thursday(X) % 61.57/61.72 => wednesday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(friday_follows_thursday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( friday(X) % 61.57/61.72 => thursday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(saturday_follows_friday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( saturday(X) % 61.57/61.72 => friday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(sunday_follows_saturday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( sunday(X) % 61.57/61.72 => saturday(yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_monday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( monday(X) % 61.57/61.72 => lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_tuesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( tuesday(X) % 61.57/61.72 => lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_wednesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( wednesday(X) % 61.57/61.72 => lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_does_not_lie_thursday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( thursday(X) % 61.57/61.72 => ~ lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_does_not_lie_friday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( friday(X) % 61.57/61.72 => ~ lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_does_not_lie_saturday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( saturday(X) % 61.57/61.72 => ~ lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_does_not_lie_sunday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( sunday(X) % 61.57/61.72 => ~ lion_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_does_not_lie_monday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( monday(X) % 61.57/61.72 => ~ unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_does_not_lie_tuesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( tuesday(X) % 61.57/61.72 => ~ unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_does_not_lie_wednesday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( wednesday(X) % 61.57/61.72 => ~ unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_thursday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( thursday(X) % 61.57/61.72 => unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_friday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( friday(X) % 61.57/61.72 => unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_saturday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( saturday(X) % 61.57/61.72 => unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_does_not_lie_sunday,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( sunday(X) % 61.57/61.72 => ~ unicorn_lies(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_on_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( lion_lies(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_on_a_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( unicorn_lies(X) % 61.57/61.72 => day(X) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_on_this_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( lion_lies(X) % 61.57/61.72 & lies_on_one_of(a_lion,X,Y) ) % 61.57/61.72 => ~ lion_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_on_other_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( ~ lion_lies(X) % 61.57/61.72 & lies_on_one_of(a_lion,X,Y) ) % 61.57/61.72 => lion_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_on_neither,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( ~ lion_lies(X) % 61.57/61.72 & ~ lies_on_one_of(a_lion,X,Y) ) % 61.57/61.72 => ~ lion_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(lion_lies_on_both,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( lion_lies(X) % 61.57/61.72 & ~ lies_on_one_of(a_lion,X,Y) ) % 61.57/61.72 => lion_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_on_this_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( unicorn_lies(X) % 61.57/61.72 & lies_on_one_of(a_unicorn,X,Y) ) % 61.57/61.72 => ~ unicorn_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_on_other_day,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( ~ unicorn_lies(X) % 61.57/61.72 & lies_on_one_of(a_unicorn,X,Y) ) % 61.57/61.72 => unicorn_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_on_neither,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( ~ unicorn_lies(X) % 61.57/61.72 & ~ lies_on_one_of(a_unicorn,X,Y) ) % 61.57/61.72 => ~ unicorn_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(unicorn_lies_on_both,axiom, % 61.57/61.72 ! [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 => ! [Y] : % 61.57/61.72 ( day(Y) % 61.57/61.72 => ( ( unicorn_lies(X) % 61.57/61.72 & ~ lies_on_one_of(a_unicorn,X,Y) ) % 61.57/61.72 => unicorn_lies(Y) ) ) ) ). % 61.57/61.72 % 61.57/61.72 fof(prove_there_are_close_lying_days,conjecture, % 61.57/61.72 ? [X] : % 61.57/61.72 ( day(X) % 61.57/61.72 & lies_on_one_of(a_lion,X,yesterday(X)) % 61.57/61.72 & lies_on_one_of(a_unicorn,X,yesterday(X)) ) ). % 61.57/61.72 % 61.57/61.72 %-------------------------------------------------------------------------- % 61.57/61.72 %------------------------------------------- % 61.57/61.72 % Proof found % 61.57/61.72 % SZS status Theorem for theBenchmark % 61.57/61.72 % SZS output start Proof % 61.68/61.74 %ClaNum:46(EqnAxiom:0) % 61.68/61.74 %VarNum:113(SingletonVarNum:47) % 61.68/61.74 %MaxLitNum:5 % 61.68/61.74 %MaxfuncDepth:1 % 61.68/61.74 %SharedTerms:16 % 61.68/61.74 %goalClause: 46 % 61.68/61.74 [1]P1(a1) % 61.68/61.74 [2]P6(a4) % 61.68/61.74 [3]P10(a8) % 61.68/61.74 [4]P7(a5) % 61.68/61.74 [5]P2(a2) % 61.68/61.74 [6]P8(a6) % 61.68/61.74 [7]P9(a7) % 61.68/61.74 [8]~P1(x81)+P3(x81) % 61.68/61.74 [9]~P6(x91)+P3(x91) % 61.68/61.74 [10]~P10(x101)+P3(x101) % 61.68/61.74 [11]~P7(x111)+P3(x111) % 61.68/61.74 [12]~P2(x121)+P3(x121) % 61.68/61.74 [13]~P8(x131)+P3(x131) % 61.68/61.74 [14]~P9(x141)+P3(x141) % 61.68/61.74 [15]~P4(x151)+P3(x151) % 61.68/61.74 [16]~P11(x161)+P3(x161) % 61.68/61.74 [17]~P1(x171)+P4(x171) % 61.68/61.74 [18]~P6(x181)+P4(x181) % 61.68/61.74 [19]~P10(x191)+P4(x191) % 61.68/61.74 [20]~P7(x201)+P11(x201) % 61.68/61.74 [21]~P2(x211)+P11(x211) % 61.68/61.74 [22]~P8(x221)+P11(x221) % 61.68/61.74 [23]~P11(x231)+~P1(x231) % 61.68/61.74 [24]~P11(x241)+~P6(x241) % 61.68/61.74 [25]~P11(x251)+~P10(x251) % 61.68/61.74 [26]~P4(x261)+~P7(x261) % 61.68/61.74 [27]~P4(x271)+~P2(x271) % 61.68/61.74 [28]~P4(x281)+~P8(x281) % 61.68/61.74 [29]~P4(x291)+~P9(x291) % 61.68/61.74 [30]~P11(x301)+~P9(x301) % 61.68/61.74 [31]~P6(x311)+P1(f10(x311)) % 61.68/61.74 [32]~P10(x321)+P6(f10(x321)) % 61.68/61.74 [33]~P7(x331)+P10(f10(x331)) % 61.68/61.74 [34]~P2(x341)+P7(f10(x341)) % 61.68/61.74 [35]~P8(x351)+P2(f10(x351)) % 61.68/61.74 [36]~P9(x361)+P8(f10(x361)) % 61.68/61.74 [37]~P1(x371)+P9(f10(x371)) % 61.68/61.74 [46]~P3(x461)+~P5(a3,x461,f10(x461))+~P5(a9,x461,f10(x461)) % 61.68/61.74 [38]~P3(x381)+~P3(x382)+~P4(x382)+P4(x381)+P5(a3,x382,x381) % 61.68/61.74 [39]~P3(x392)+~P3(x391)+~P4(x392)+P4(x391)+P5(a3,x391,x392) % 61.68/61.74 [40]~P3(x401)+~P3(x402)+~P11(x402)+P11(x401)+P5(a9,x402,x401) % 61.68/61.74 [41]~P3(x412)+~P3(x411)+~P11(x412)+P11(x411)+P5(a9,x411,x412) % 61.68/61.74 [42]~P3(x421)+~P3(x422)+P4(x421)+P4(x422)+~P5(a3,x422,x421) % 61.68/61.74 [43]~P3(x431)+~P3(x432)+P11(x431)+P11(x432)+~P5(a9,x432,x431) % 61.68/61.74 [44]~P4(x441)+~P4(x442)+~P3(x441)+~P3(x442)+~P5(a3,x442,x441) % 61.68/61.74 [45]~P11(x451)+~P11(x452)+~P3(x451)+~P3(x452)+~P5(a9,x452,x451) % 61.68/61.74 %EqnAxiom % 61.68/61.74 % 61.68/61.74 %------------------------------------------- % 61.90/61.95 cnf(53,plain, % 61.90/61.95 (~P4(a5)), % 61.90/61.95 inference(scs_inference,[],[1,2,3,4,23,24,25,26])). % 61.90/61.95 cnf(55,plain, % 61.90/61.95 (~P4(a2)), % 61.90/61.95 inference(scs_inference,[],[1,2,3,4,5,23,24,25,26,27])). % 61.90/61.95 cnf(59,plain, % 61.90/61.95 (~P4(a7)), % 61.90/61.95 inference(scs_inference,[],[1,2,3,4,5,6,7,23,24,25,26,27,28,29])). % 61.90/61.95 cnf(61,plain, % 61.90/61.95 (~P11(a7)), % 61.90/61.95 inference(scs_inference,[],[1,2,3,4,5,6,7,23,24,25,26,27,28,29,30])). % 61.90/61.95 cnf(1703,plain, % 61.90/61.95 (P3(a5)), % 61.90/61.95 inference(scs_inference,[],[4,16,20])). % 61.90/61.95 cnf(1884,plain, % 61.90/61.95 (P1(f10(f10(a8)))), % 61.90/61.95 inference(scs_inference,[],[3,31,32])). % 61.90/61.95 cnf(1885,plain, % 61.90/61.95 (~P11(f10(f10(a8)))), % 61.90/61.95 inference(scs_inference,[],[1884,23])). % 61.90/61.95 cnf(1911,plain, % 61.90/61.95 (~P2(f10(a8))), % 61.90/61.95 inference(scs_inference,[],[1885,53,22,20,17,18,19,21,34])). % 61.90/61.95 cnf(1913,plain, % 61.90/61.95 (~P8(f10(a8))), % 61.90/61.95 inference(scs_inference,[],[1885,53,22,20,17,18,19,21,34,35])). % 61.90/61.95 cnf(1915,plain, % 61.90/61.95 (~P9(f10(a8))), % 61.90/61.95 inference(scs_inference,[],[1885,53,22,20,17,18,19,21,34,35,36])). % 61.90/61.95 cnf(2153,plain, % 61.90/61.95 (P10(f10(f10(a2)))), % 61.90/61.95 inference(scs_inference,[],[5,33,34])). % 61.90/61.95 cnf(2154,plain, % 61.90/61.95 (~P11(f10(f10(a2)))), % 61.90/61.95 inference(scs_inference,[],[2153,25])). % 61.90/61.95 cnf(2184,plain, % 61.90/61.95 (~P2(f10(f10(a2)))), % 61.90/61.95 inference(scs_inference,[],[2154,1911,1913,1915,59,35,36,37,19,22,21])). % 61.90/61.95 cnf(2192,plain, % 61.90/61.95 (~P2(f10(a2))), % 61.90/61.95 inference(scs_inference,[],[2154,1911,1913,1915,59,35,36,37,19,22,21,18,20,17,34])). % 61.90/61.95 cnf(2194,plain, % 61.90/61.95 (~P8(f10(a2))), % 61.90/61.95 inference(scs_inference,[],[2184,35])). % 61.90/61.95 cnf(8113,plain, % 61.90/61.95 (P3(f10(a4))), % 61.90/61.95 inference(scs_inference,[],[2,8,31])). % 61.90/61.95 cnf(14325,plain, % 61.90/61.95 (P3(f10(a5))), % 61.90/61.95 inference(scs_inference,[],[4,10,33])). % 61.90/61.95 cnf(18324,plain, % 61.90/61.95 (P3(f10(a7))), % 61.90/61.95 inference(scs_inference,[],[7,13,36])). % 61.90/61.95 cnf(22296,plain, % 61.90/61.95 (P11(f10(a4))+~P4(f10(f10(a8)))+~P5(a9,f10(f10(a8)),f10(a4))), % 61.90/61.95 inference(scs_inference,[],[8113,1885,15,43])). % 61.90/61.95 cnf(22567,plain, % 61.90/61.95 (P11(f10(a4))+~P5(a9,f10(f10(a8)),f10(a4))), % 61.90/61.95 inference(scs_inference,[],[1884,22296,17])). % 61.90/61.95 cnf(22838,plain, % 61.90/61.95 (~P1(f10(a4))+~P5(a9,f10(f10(a8)),f10(a4))), % 61.90/61.95 inference(scs_inference,[],[22567,23])). % 61.90/61.95 cnf(23109,plain, % 61.90/61.95 (~P5(a9,f10(f10(a8)),f10(a4))), % 61.90/61.95 inference(scs_inference,[],[2,22838,31])). % 61.90/61.95 cnf(23128,plain, % 61.90/61.95 (~P11(f10(a4))+~P3(f10(f10(a8)))), % 61.90/61.95 inference(scs_inference,[],[55,8113,23109,1885,2192,2194,1915,61,20,17,35,36,19,37,18,22,21,41])). % 61.90/61.95 cnf(23396,plain, % 61.90/61.95 (~P11(f10(a4))), % 61.90/61.95 inference(scs_inference,[],[1884,23128,8])). % 61.90/61.95 cnf(29108,plain, % 61.90/61.95 (~P11(x291081)+~P5(a3,x291081,f10(x291081))+~P5(a9,x291081,f10(x291081))), % 61.90/61.95 inference(scs_inference,[],[16,46])). % 61.90/61.95 cnf(299370,plain, % 61.90/61.95 (P10(f10(a5))), % 61.90/61.95 inference(scs_inference,[],[4,7,3,14,32,33])). % 61.90/61.95 cnf(299372,plain, % 61.90/61.95 (P8(f10(a7))), % 61.90/61.95 inference(scs_inference,[],[4,7,3,14,32,33,36])). % 61.90/61.95 cnf(299374,plain, % 61.90/61.95 (P2(f10(a6))), % 61.90/61.95 inference(scs_inference,[],[4,6,7,3,14,32,33,36,35])). % 61.90/61.95 cnf(299378,plain, % 61.90/61.95 (P11(a2)), % 61.90/61.95 inference(scs_inference,[],[4,6,7,3,5,2,14,32,33,36,35,31,21])). % 61.90/61.95 cnf(299380,plain, % 61.90/61.95 (P4(a8)), % 61.90/61.95 inference(scs_inference,[],[4,6,7,3,5,2,14,32,33,36,35,31,21,19])). % 61.90/61.95 cnf(299384,plain, % 61.90/61.95 (P11(a5)), % 61.90/61.95 inference(scs_inference,[],[1,4,6,7,3,5,2,14,32,33,36,35,31,21,19,37,20])). % 61.90/61.95 cnf(299386,plain, % 61.90/61.95 (P7(f10(a2))), % 61.90/61.95 inference(scs_inference,[],[1,4,6,7,3,5,2,14,32,33,36,35,31,21,19,37,20,34])). % 61.90/61.95 cnf(299388,plain, % 61.90/61.95 (P4(a4)), % 61.90/61.95 inference(scs_inference,[],[1,4,6,7,3,5,2,14,32,33,36,35,31,21,19,37,20,34,18])). % 61.90/61.95 cnf(299390,plain, % 61.90/61.95 (P4(a1)), % 61.90/61.95 inference(scs_inference,[],[1,4,6,7,3,5,2,14,32,33,36,35,31,21,19,37,20,34,18,17])). % 61.90/61.95 cnf(299452,plain, % 61.90/61.95 (P4(f10(a5))), % 61.90/61.95 inference(scs_inference,[],[299378,299380,299370,299374,299386,30,28,27,24,29,23,26,25,20,21,19])). % 61.90/61.95 cnf(299454,plain, % 61.90/61.95 (P11(f10(a7))), % 61.90/61.95 inference(scs_inference,[],[299378,299380,299370,299372,299374,299386,30,28,27,24,29,23,26,25,20,21,19,22])). % 61.90/61.95 cnf(299699,plain, % 61.90/61.95 (~P5(a9,a5,f10(a5))), % 61.90/61.95 inference(scs_inference,[],[18324,14325,299452,299454,299384,299388,23396,8113,53,1703,30,28,27,23,29,24,26,25,39,41,29108])). % 61.90/61.95 cnf(303210,plain, % 61.90/61.95 (~P11(f10(a5))), % 61.90/61.95 inference(scs_inference,[],[299370,299390,299384,27,28,24,26,25])). % 61.90/61.95 cnf(303401,plain, % 61.90/61.95 ($false), % 61.90/61.95 inference(scs_inference,[],[299699,303210,1703,14325,299384,299388,27,28,26,29,40]), % 61.90/61.95 ['proof']). % 62.05/62.16 % SZS output end Proof % 62.05/62.16 % Total time :61.090000s %------------------------------------------------------------------------------