%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM841+2 : TPTP v8.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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 12:26:42 EDT 2024
% Result : Theorem 2.49s 2.67s
% Output : CNFRefutation 2.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NUM841+2 : TPTP v8.2.0. Released v4.1.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.27 % Computer : n032.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Sun Jun 23 02:09:38 EDT 2024
% 0.08/0.27 % CPUTime :
% 0.12/0.46 start to proof:theBenchmark
% 2.49/2.66 %-------------------------------------------
% 2.49/2.66 % File :CSE---1.7
% 2.49/2.66 % Problem :theBenchmark
% 2.49/2.66 % Transform :cnf
% 2.49/2.66 % Format :tptp:raw
% 2.49/2.66 % Command :java -jar mcs_scs.jar %d %s
% 2.49/2.66
% 2.49/2.66 % Result :Theorem 2.180000s
% 2.49/2.66 % Output :CNFRefutation 2.180000s
% 2.49/2.66 %-------------------------------------------
% 2.49/2.67 %------------------------------------------------------------------------------
% 2.49/2.67 % File : NUM841+2 : TPTP v8.2.0. Released v4.1.0.
% 2.49/2.67 % Domain : Number Theory
% 2.49/2.67 % Problem : holds(214,352,0)
% 2.49/2.67 % Version : Especial: Reduced > Especial.
% 2.49/2.67 % English :
% 2.49/2.67
% 2.49/2.67 % Refs : [Lan30] Landau (1930), Grundlagen der Analysis
% 2.49/2.67 % : [Kue09] Kuehlwein (2009), Email to Geoff Sutcliffe
% 2.49/2.67 % : [KC+10] Kuehlwein et al. (2010), Premise Selection in the Napr
% 2.49/2.67 % Source : [Kue09]
% 2.49/2.67 % Names :
% 2.49/2.67
% 2.49/2.67 % Status : Theorem
% 2.49/2.67 % Rating : 0.44 v7.5.0, 0.47 v7.4.0, 0.43 v7.3.0, 0.45 v7.2.0, 0.41 v7.1.0, 0.43 v7.0.0, 0.50 v6.4.0, 0.58 v6.3.0, 0.46 v6.2.0, 0.52 v6.1.0, 0.50 v6.0.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.63 v5.2.0, 0.45 v5.1.0, 0.48 v5.0.0, 0.62 v4.1.0
% 2.49/2.67 % Syntax : Number of formulae : 26 ( 12 unt; 0 def)
% 2.49/2.67 % Number of atoms : 41 ( 18 equ)
% 2.49/2.67 % Maximal formula atoms : 3 ( 1 avg)
% 2.49/2.67 % Number of connectives : 20 ( 5 ~; 4 |; 1 &)
% 2.49/2.67 % ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% 2.49/2.67 % Maximal formula depth : 6 ( 3 avg)
% 2.49/2.67 % Maximal term depth : 3 ( 1 avg)
% 2.49/2.67 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty)
% 2.49/2.67 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% 2.49/2.67 % Number of variables : 45 ( 43 !; 2 ?)
% 2.49/2.67 % SPC : FOF_THM_RFO_SEQ
% 2.49/2.67
% 2.49/2.67 % Comments : From the Landau in Naproche 0.45 collection.
% 2.49/2.67 % : This version uses a filtered set of axioms.
% 2.49/2.67 %------------------------------------------------------------------------------
% 2.49/2.67 fof('holds(214, 352, 0)',conjecture,
% 2.49/2.67 greater(vplus(vd344,vd347),vplus(vd345,vd348)) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(213, 351, 2)',axiom,
% 2.49/2.67 vplus(vd348,vd345) = vplus(vd345,vd348) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(213, 351, 1)',axiom,
% 2.49/2.67 greater(vplus(vd347,vd345),vplus(vd348,vd345)) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(213, 351, 0)',axiom,
% 2.49/2.67 vplus(vd345,vd347) = vplus(vd347,vd345) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(212, 350, 0)',axiom,
% 2.49/2.67 greater(vplus(vd344,vd347),vplus(vd345,vd347)) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(conjunct2(211), 349, 0)',axiom,
% 2.49/2.67 greater(vd347,vd348) ).
% 2.49/2.67
% 2.49/2.67 fof('holds(conjunct1(211), 346, 0)',axiom,
% 2.49/2.67 greater(vd344,vd345) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(202), 0), 0)',axiom,
% 2.49/2.67 ! [Vd328,Vd329,Vd330] :
% 2.49/2.67 ( less(vplus(Vd328,Vd330),vplus(Vd329,Vd330))
% 2.49/2.67 => less(Vd328,Vd329) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(202), 0), 1)',axiom,
% 2.49/2.67 ! [Vd328,Vd329,Vd330] :
% 2.49/2.67 ( vplus(Vd328,Vd330) = vplus(Vd329,Vd330)
% 2.49/2.67 => Vd328 = Vd329 ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(202), 0), 2)',axiom,
% 2.49/2.67 ! [Vd328,Vd329,Vd330] :
% 2.49/2.67 ( greater(vplus(Vd328,Vd330),vplus(Vd329,Vd330))
% 2.49/2.67 => greater(Vd328,Vd329) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(193), 0), 0)',axiom,
% 2.49/2.67 ! [Vd301,Vd302,Vd303] :
% 2.49/2.67 ( less(Vd301,Vd302)
% 2.49/2.67 => less(vplus(Vd301,Vd303),vplus(Vd302,Vd303)) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(193), 0), 1)',axiom,
% 2.49/2.67 ! [Vd301,Vd302,Vd303] :
% 2.49/2.67 ( Vd301 = Vd302
% 2.49/2.67 => vplus(Vd301,Vd303) = vplus(Vd302,Vd303) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(193), 0), 2)',axiom,
% 2.49/2.67 ! [Vd301,Vd302,Vd303] :
% 2.49/2.67 ( greater(Vd301,Vd302)
% 2.49/2.67 => greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(189, 0), 0)',axiom,
% 2.49/2.67 ! [Vd295,Vd296] : greater(vplus(Vd295,Vd296),Vd295) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(147, 0), 0)',axiom,
% 2.49/2.67 ! [Vd226,Vd227] :
% 2.49/2.67 ( less(Vd226,Vd227)
% 2.49/2.67 => greater(Vd227,Vd226) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(140, 0), 0)',axiom,
% 2.49/2.67 ! [Vd208,Vd209] :
% 2.49/2.67 ( greater(Vd208,Vd209)
% 2.49/2.67 => less(Vd209,Vd208) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(130), 0), 0)',axiom,
% 2.49/2.67 ! [Vd203,Vd204] :
% 2.49/2.67 ( Vd203 = Vd204
% 2.49/2.67 | greater(Vd203,Vd204)
% 2.49/2.67 | less(Vd203,Vd204) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(130), 0), 2)',axiom,
% 2.49/2.67 ! [Vd203,Vd204] :
% 2.49/2.67 ( ~ greater(Vd203,Vd204)
% 2.49/2.67 | ~ less(Vd203,Vd204) ) ).
% 2.49/2.67
% 2.49/2.67 fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
% 2.49/2.67 ! [Vd193,Vd194] :
% 2.49/2.67 ( greater(Vd194,Vd193)
% 2.49/2.67 <=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(goal(88), 0), 3)',axiom,
% 2.49/2.67 ! [Vd120,Vd121] :
% 2.49/2.67 ( Vd120 != Vd121
% 2.49/2.67 | ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(61, 0), 0)',axiom,
% 2.49/2.67 ! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(52, 0), 0)',axiom,
% 2.49/2.67 ! [Vd68,Vd69] : vplus(vsucc(Vd68),Vd69) = vsucc(vplus(Vd68,Vd69)) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(43, 0), 0)',axiom,
% 2.49/2.67 ! [Vd59] : vplus(v1,Vd59) = vsucc(Vd59) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(33, 0), 0)',axiom,
% 2.49/2.67 ! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) ).
% 2.49/2.67
% 2.49/2.67 fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
% 2.49/2.67 ! [Vd42,Vd43] :
% 2.49/2.67 ( vplus(Vd42,vsucc(Vd43)) = vsucc(vplus(Vd42,Vd43))
% 2.49/2.67 & vplus(Vd42,v1) = vsucc(Vd42) ) ).
% 2.49/2.67
% 2.49/2.67 fof('ass(cond(20, 0), 0)',axiom,
% 2.49/2.67 ! [Vd24] :
% 2.49/2.67 ( Vd24 != v1
% 2.49/2.67 => Vd24 = vsucc(vskolem2(Vd24)) ) ).
% 2.49/2.67
% 2.49/2.67 %------------------------------------------------------------------------------
% 2.49/2.67 %-------------------------------------------
% 2.49/2.67 % Proof found
% 2.49/2.67 % SZS status Theorem for theBenchmark
% 2.49/2.67 % SZS output start Proof
% 2.49/2.67 %ClaNum:38(EqnAxiom:12)
% 2.49/2.67 %VarNum:84(SingletonVarNum:41)
% 2.49/2.67 %MaxLitNum:3
% 2.49/2.67 %MaxfuncDepth:2
% 2.49/2.67 %SharedTerms:17
% 2.49/2.67 %goalClause: 25
% 2.49/2.67 %singleGoalClaCount:1
% 2.49/2.67 [13]P1(a1,a4)
% 2.49/2.67 [14]P1(a5,a6)
% 2.49/2.67 [20]P1(f7(a1,a5),f7(a4,a5))
% 2.49/2.67 [21]P1(f7(a5,a4),f7(a6,a4))
% 2.49/2.67 [25]~P1(f7(a1,a5),f7(a4,a6))
% 2.49/2.67 [18]E(f7(x181,x182),f7(x182,x181))
% 2.49/2.67 [19]P1(f7(x191,x192),x191)
% 2.49/2.67 [23]E(f7(f7(x231,a2),x232),f7(f7(x231,x232),a2))
% 2.49/2.67 [24]E(f7(f7(x241,x242),x243),f7(x241,f7(x242,x243)))
% 2.49/2.67 [26]E(x261,a2)+E(f7(f8(x261),a2),x261)
% 2.49/2.67 [29]~P2(x292,x291)+P1(x291,x292)
% 2.49/2.67 [30]~P1(x302,x301)+P2(x301,x302)
% 2.49/2.67 [32]~P2(x321,x322)+~P1(x321,x322)
% 2.49/2.67 [34]~P1(x342,x341)+E(f7(x341,f3(x341,x342)),x342)
% 2.49/2.67 [27]~E(x271,x272)+~E(x271,f7(x272,x273))
% 2.49/2.67 [31]P1(x311,x312)+~E(x311,f7(x312,x313))
% 2.49/2.67 [33]E(x331,x332)+~E(f7(x331,x333),f7(x332,x333))
% 2.49/2.67 [35]~P1(x351,x353)+P1(f7(x351,x352),f7(x353,x352))
% 2.49/2.67 [36]~P2(x361,x363)+P2(f7(x361,x362),f7(x363,x362))
% 2.49/2.67 [37]P1(x371,x372)+~P1(f7(x371,x373),f7(x372,x373))
% 2.49/2.67 [38]P2(x381,x382)+~P2(f7(x381,x383),f7(x382,x383))
% 2.49/2.67 [28]P1(x281,x282)+P2(x281,x282)+E(x281,x282)
% 2.49/2.67 %EqnAxiom
% 2.49/2.67 [1]E(x11,x11)
% 2.49/2.67 [2]E(x22,x21)+~E(x21,x22)
% 2.49/2.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.49/2.67 [4]~E(x41,x42)+E(f7(x41,x43),f7(x42,x43))
% 2.49/2.67 [5]~E(x51,x52)+E(f7(x53,x51),f7(x53,x52))
% 2.49/2.67 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 2.49/2.67 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 2.49/2.67 [8]~E(x81,x82)+E(f8(x81),f8(x82))
% 2.49/2.67 [9]P1(x92,x93)+~E(x91,x92)+~P1(x91,x93)
% 2.49/2.67 [10]P1(x103,x102)+~E(x101,x102)+~P1(x103,x101)
% 2.49/2.67 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 2.49/2.67 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 2.49/2.67
% 2.49/2.67 %-------------------------------------------
% 2.49/2.67 cnf(41,plain,
% 2.49/2.67 (~P2(f7(a4,a6),f7(a1,a5))),
% 2.49/2.67 inference(scs_inference,[],[25,29])).
% 2.49/2.67 cnf(43,plain,
% 2.49/2.67 (P1(f7(x431,x432),x432)),
% 2.49/2.67 inference(scs_inference,[],[25,18,29,31])).
% 2.49/2.67 cnf(47,plain,
% 2.49/2.67 (~P2(f7(x471,x472),x471)),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,29,31,27,32])).
% 2.49/2.67 cnf(49,plain,
% 2.49/2.67 (E(f7(x491,f7(x492,x493)),f7(f7(x491,x492),x493))),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,24,29,31,27,32,2])).
% 2.49/2.67 cnf(50,plain,
% 2.49/2.67 (~E(f7(f7(a4,a6),x501),f7(a1,a5))),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,24,29,31,27,32,2,9])).
% 2.49/2.67 cnf(51,plain,
% 2.49/2.67 (P1(f7(x511,x512),x511)),
% 2.49/2.67 inference(rename_variables,[],[19])).
% 2.49/2.67 cnf(54,plain,
% 2.49/2.67 (~E(f7(f7(a4,a6),x541),f7(a5,a1))),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,51,24,29,31,27,32,2,9,10,3])).
% 2.49/2.67 cnf(56,plain,
% 2.49/2.67 (~P1(f7(a4,a6),f7(f7(a4,a6),x561))),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,51,24,29,31,27,32,2,9,10,3,30])).
% 2.49/2.67 cnf(58,plain,
% 2.49/2.67 (~P1(f7(a5,a1),f7(a4,a6))),
% 2.49/2.67 inference(scs_inference,[],[25,18,19,51,24,29,31,27,32,2,9,10,3,30,34])).
% 2.49/2.67 cnf(67,plain,
% 2.49/2.67 (~P1(x671,f7(x671,x672))),
% 2.49/2.67 inference(scs_inference,[],[50,47,56,35,4,30])).
% 2.49/2.67 cnf(69,plain,
% 2.49/2.67 (P1(f7(x691,f7(x692,x693)),f7(x691,x692))),
% 2.49/2.67 inference(scs_inference,[],[50,47,49,56,35,4,30,31])).
% 2.49/2.67 cnf(73,plain,
% 2.49/2.67 (~P2(f7(x731,x732),x732)),
% 2.49/2.67 inference(scs_inference,[],[43,50,47,49,56,58,35,4,30,31,29,32])).
% 2.49/2.67 cnf(75,plain,
% 2.49/2.67 (~E(f7(x751,f7(x752,x753)),f7(x751,x752))),
% 2.49/2.67 inference(scs_inference,[],[43,50,47,49,56,58,35,4,30,31,29,32,27])).
% 2.49/2.67 cnf(77,plain,
% 2.49/2.67 (E(f7(f7(x771,x772),a2),f7(f7(x771,a2),x772))),
% 2.49/2.67 inference(scs_inference,[],[43,50,47,49,56,58,23,35,4,30,31,29,32,27,2])).
% 2.49/2.67 cnf(78,plain,
% 2.49/2.67 (~E(f7(x781,f7(a4,a6)),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,43,50,47,49,56,58,23,35,4,30,31,29,32,27,2,9])).
% 2.49/2.68 cnf(79,plain,
% 2.49/2.68 (P1(f7(x791,x792),x792)),
% 2.49/2.68 inference(rename_variables,[],[43])).
% 2.49/2.68 cnf(83,plain,
% 2.49/2.68 (~P1(x831,x831)),
% 2.49/2.68 inference(scs_inference,[],[25,43,79,50,47,49,56,58,23,35,4,30,31,29,32,27,2,9,10,5,34])).
% 2.49/2.68 cnf(91,plain,
% 2.49/2.68 (~P1(x911,f7(x912,x911))),
% 2.49/2.68 inference(scs_inference,[],[73,54,4,30])).
% 2.49/2.68 cnf(93,plain,
% 2.49/2.68 (~P2(f7(x931,f7(x932,x933)),f7(x931,x932))),
% 2.49/2.68 inference(scs_inference,[],[69,73,54,4,30,32])).
% 2.49/2.68 cnf(95,plain,
% 2.49/2.68 (P1(f7(f7(x951,x952),a2),f7(x951,a2))),
% 2.49/2.68 inference(scs_inference,[],[69,73,77,54,4,30,32,31])).
% 2.49/2.68 cnf(103,plain,
% 2.49/2.68 (~E(f7(a4,f7(a6,x1031)),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,69,78,18,83,73,77,54,4,30,32,31,29,27,3,9])).
% 2.49/2.68 cnf(110,plain,
% 2.49/2.68 (P1(f7(f7(x1101,x1102),x1103),x1101)),
% 2.49/2.68 inference(scs_inference,[],[93,24,30,31])).
% 2.49/2.68 cnf(112,plain,
% 2.49/2.68 (~P2(f7(f7(x1121,x1122),a2),f7(x1121,a2))),
% 2.49/2.68 inference(scs_inference,[],[95,93,24,30,31,32])).
% 2.49/2.68 cnf(117,plain,
% 2.49/2.68 (~P1(x1171,f7(x1171,x1172))),
% 2.49/2.68 inference(rename_variables,[],[67])).
% 2.49/2.68 cnf(122,plain,
% 2.49/2.68 (~E(x1221,f7(f7(x1221,x1222),a2))),
% 2.49/2.68 inference(scs_inference,[],[95,103,20,18,93,67,117,24,30,31,32,27,9,10,3,4])).
% 2.49/2.68 cnf(123,plain,
% 2.49/2.68 (~P1(f7(x1231,a2),f7(f7(x1231,x1232),a2))),
% 2.49/2.68 inference(scs_inference,[],[112,30])).
% 2.49/2.68 cnf(125,plain,
% 2.49/2.68 (P1(f7(f7(x1251,a2),x1252),f7(x1251,x1252))),
% 2.49/2.68 inference(scs_inference,[],[112,23,30,31])).
% 2.49/2.68 cnf(129,plain,
% 2.49/2.68 (~P2(f7(f7(x1291,x1292),x1293),x1291)),
% 2.49/2.68 inference(scs_inference,[],[110,122,112,23,30,31,4,32])).
% 2.49/2.68 cnf(133,plain,
% 2.49/2.68 (~E(f7(f7(f7(a4,a6),x1331),x1332),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,110,122,112,23,30,31,4,32,27,9])).
% 2.49/2.68 cnf(134,plain,
% 2.49/2.68 (P1(f7(f7(x1341,x1342),x1343),x1341)),
% 2.49/2.68 inference(rename_variables,[],[110])).
% 2.49/2.68 cnf(141,plain,
% 2.49/2.68 (~E(x1411,f7(f7(f7(x1412,x1411),x1413),x1414))),
% 2.49/2.68 inference(scs_inference,[],[25,110,134,75,91,122,112,23,30,31,4,32,27,9,10,3,34,5])).
% 2.49/2.68 cnf(144,plain,
% 2.49/2.68 (P1(f7(f7(a4,a6),x1441),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,110,134,50,75,91,122,112,23,30,31,4,32,27,9,10,3,34,5,29,28])).
% 2.49/2.68 cnf(148,plain,
% 2.49/2.68 (P1(f7(a4,a6),a1)),
% 2.49/2.68 inference(scs_inference,[],[25,110,134,50,75,91,122,112,23,30,31,4,32,27,9,10,3,34,5,29,28,36,37])).
% 2.49/2.68 cnf(152,plain,
% 2.49/2.68 (~P1(x1521,f7(f7(x1521,x1522),x1523))),
% 2.49/2.68 inference(scs_inference,[],[129,30])).
% 2.49/2.68 cnf(154,plain,
% 2.49/2.68 (~P2(f7(f7(x1541,a2),x1542),f7(x1541,x1542))),
% 2.49/2.68 inference(scs_inference,[],[125,129,30,32])).
% 2.49/2.68 cnf(158,plain,
% 2.49/2.68 (~E(f7(f7(a4,a2),a6),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,125,133,129,30,32,4,9])).
% 2.49/2.68 cnf(165,plain,
% 2.49/2.68 (~P1(f7(x1651,x1652),f7(f7(x1651,a2),x1652))),
% 2.49/2.68 inference(scs_inference,[],[154,30])).
% 2.49/2.68 cnf(167,plain,
% 2.49/2.68 (~P2(f7(a5,a4),f7(a6,a4))),
% 2.49/2.68 inference(scs_inference,[],[21,154,30,32])).
% 2.49/2.68 cnf(173,plain,
% 2.49/2.68 (~P1(x1731,f7(f7(x1731,x1732),x1733))),
% 2.49/2.68 inference(rename_variables,[],[152])).
% 2.49/2.68 cnf(178,plain,
% 2.49/2.68 (~P2(a5,a6)),
% 2.49/2.68 inference(scs_inference,[],[148,158,95,21,18,152,173,141,154,30,32,4,9,10,3,36])).
% 2.49/2.68 cnf(182,plain,
% 2.49/2.68 (~P2(f7(a1,a5),f7(a4,a5))),
% 2.49/2.68 inference(scs_inference,[],[20,178,30,32])).
% 2.49/2.68 cnf(193,plain,
% 2.49/2.68 (~P1(f7(a6,a4),f7(a5,a4))),
% 2.49/2.68 inference(scs_inference,[],[167,30])).
% 2.49/2.68 cnf(215,plain,
% 2.49/2.68 (~P1(f7(a4,a5),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[182,30])).
% 2.49/2.68 cnf(221,plain,
% 2.49/2.68 (~E(f7(f7(a4,a6),x2211),f7(a4,a5))),
% 2.49/2.68 inference(scs_inference,[],[144,215,9])).
% 2.49/2.68 cnf(226,plain,
% 2.49/2.68 (~E(f7(f7(a4,a6),x2261),f7(a4,a5))),
% 2.49/2.68 inference(rename_variables,[],[221])).
% 2.49/2.68 cnf(230,plain,
% 2.49/2.68 (~E(f7(f7(a4,a6),x2301),f7(a5,a4))),
% 2.49/2.68 inference(scs_inference,[],[221,226,18,34,29,3])).
% 2.49/2.68 cnf(235,plain,
% 2.49/2.68 (~E(x2351,f7(f7(f7(x2351,x2352),x2353),a2))),
% 2.49/2.68 inference(scs_inference,[],[221,226,110,18,165,34,29,3,10,4])).
% 2.49/2.68 cnf(249,plain,
% 2.49/2.68 (E(f7(a4,a6),f7(a5,a4))+P1(f7(a4,a6),f7(a5,a4))),
% 2.49/2.68 inference(scs_inference,[],[95,123,235,230,34,29,4,10,28])).
% 2.49/2.68 cnf(278,plain,
% 2.49/2.68 (~E(f7(a5,a4),f7(a6,a4))),
% 2.49/2.68 inference(scs_inference,[],[21,83,9])).
% 2.49/2.68 cnf(298,plain,
% 2.49/2.68 (E(f7(a4,a6),f7(a5,a4))),
% 2.49/2.68 inference(scs_inference,[],[193,18,249,9])).
% 2.49/2.68 cnf(325,plain,
% 2.49/2.68 (~E(f7(x3251,f7(x3252,x3253)),x3252)),
% 2.49/2.68 inference(scs_inference,[],[67,43,9])).
% 2.49/2.68 cnf(354,plain,
% 2.49/2.68 (~P1(f7(a1,a5),f7(a6,a4))),
% 2.49/2.68 inference(scs_inference,[],[41,18,11,30])).
% 2.49/2.68 cnf(370,plain,
% 2.49/2.68 (P1(f7(a6,a4),f7(a1,a5))+~E(f7(a5,a4),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[67,278,14,354,29,10,28,31,27,32,2,30,3])).
% 2.49/2.68 cnf(384,plain,
% 2.49/2.68 (~E(f7(a5,a4),f7(a1,a5))+E(f7(f7(a1,a5),f3(f7(a1,a5),f7(a6,a4))),f7(a6,a4))),
% 2.49/2.68 inference(scs_inference,[],[370,34])).
% 2.49/2.68 cnf(430,plain,
% 2.49/2.68 (E(f7(a6,a4),f7(f7(a1,a5),f3(f7(a1,a5),f7(a6,a4))))+~E(f7(a5,a4),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[384,2])).
% 2.49/2.68 cnf(526,plain,
% 2.49/2.68 (E(f7(f7(a5,a4),x5261),f7(f7(a4,a6),x5261))),
% 2.49/2.68 inference(scs_inference,[],[298,2,4])).
% 2.49/2.68 cnf(539,plain,
% 2.49/2.68 (E(f7(a5,a4),f7(a1,a5))+P1(f7(a5,a4),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[25,526,31,32,30,2,9,34,29,28])).
% 2.49/2.68 cnf(546,plain,
% 2.49/2.68 (P1(f7(a5,a4),f7(a1,a5))+~E(f7(a1,a5),f7(a5,a4))),
% 2.49/2.68 inference(scs_inference,[],[25,193,526,31,32,30,2,9,34,29,28,370,384,430,27,10])).
% 2.49/2.68 cnf(554,plain,
% 2.49/2.68 (E(f7(a5,a4),f7(a1,a5))),
% 2.49/2.68 inference(scs_inference,[],[215,18,539,9])).
% 2.49/2.68 cnf(571,plain,
% 2.49/2.68 ($false),
% 2.49/2.68 inference(scs_inference,[],[325,554,18,215,152,31,32,30,2,3,10,546,9]),
% 2.49/2.68 ['proof']).
% 2.49/2.68 % SZS output end Proof
% 2.49/2.68 % Total time :2.180000s
%------------------------------------------------------------------------------