%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM853+2 : TPTP v8.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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:47 EDT 2024
% Result : Theorem 0.70s 0.81s
% Output : CNFRefutation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUM853+2 : TPTP v8.2.0. Released v4.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n017.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 : Sun Jun 23 03:08:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 0.70/0.80 %-------------------------------------------
% 0.70/0.80 % File :CSE---1.7
% 0.70/0.80 % Problem :theBenchmark
% 0.70/0.80 % Transform :cnf
% 0.70/0.80 % Format :tptp:raw
% 0.70/0.80 % Command :java -jar mcs_scs.jar %d %s
% 0.70/0.80
% 0.70/0.80 % Result :Theorem 0.220000s
% 0.70/0.80 % Output :CNFRefutation 0.220000s
% 0.70/0.80 %-------------------------------------------
% 0.70/0.80 %------------------------------------------------------------------------------
% 0.70/0.80 % File : NUM853+2 : TPTP v8.2.0. Released v4.1.0.
% 0.70/0.80 % Domain : Number Theory
% 0.70/0.80 % Problem : holds(conseq(307),490,0)
% 0.70/0.80 % Version : Especial: Reduced > Especial.
% 0.70/0.80 % English :
% 0.70/0.80
% 0.70/0.80 % Refs : [Lan30] Landau (1930), Grundlagen der Analysis
% 0.70/0.80 % : [Kue09] Kuehlwein (2009), Email to Geoff Sutcliffe
% 0.70/0.80 % : [KC+10] Kuehlwein et al. (2010), Premise Selection in the Napr
% 0.70/0.80 % Source : [Kue09]
% 0.70/0.80 % Names :
% 0.70/0.80
% 0.70/0.80 % Status : Theorem
% 0.70/0.80 % Rating : 0.25 v8.2.0, 0.31 v7.4.0, 0.37 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.35 v7.0.0, 0.30 v6.4.0, 0.38 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.33 v6.0.0, 0.35 v5.5.0, 0.33 v5.4.0, 0.32 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.29 v4.1.0
% 0.70/0.80 % Syntax : Number of formulae : 37 ( 14 unt; 0 def)
% 0.70/0.80 % Number of atoms : 63 ( 37 equ)
% 0.70/0.80 % Maximal formula atoms : 3 ( 1 avg)
% 0.70/0.80 % Number of connectives : 45 ( 19 ~; 10 |; 3 &)
% 0.70/0.80 % ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% 0.70/0.80 % Maximal formula depth : 7 ( 4 avg)
% 0.70/0.80 % Maximal term depth : 3 ( 1 avg)
% 0.70/0.80 % Number of predicates : 5 ( 4 usr; 0 prp; 2-2 aty)
% 0.70/0.80 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 0.70/0.80 % Number of variables : 82 ( 74 !; 8 ?)
% 0.70/0.80 % SPC : FOF_THM_RFO_SEQ
% 0.70/0.80
% 0.70/0.80 % Comments : From the Landau in Naproche 0.45 collection.
% 0.70/0.80 % : This version uses a filtered set of axioms.
% 0.70/0.80 %------------------------------------------------------------------------------
% 0.70/0.80 fof('holds(conseq(307), 490, 0)',conjecture,
% 0.70/0.80 greater(vd486,vd488) ).
% 0.70/0.80
% 0.70/0.80 fof('holds(antec(307), 489, 0)',axiom,
% 0.70/0.80 greater(vmul(vd486,vd487),vmul(vd488,vd487)) ).
% 0.70/0.80
% 0.70/0.80 fof('ass(cond(299, 0), 0)',axiom,
% 0.70/0.80 ! [Vd456,Vd465,Vd466] :
% 0.70/0.80 ( less(Vd465,Vd466)
% 0.70/0.80 => less(vmul(Vd465,Vd456),vmul(Vd466,Vd456)) ) ).
% 0.70/0.80
% 0.70/0.80 fof('ass(cond(299, 0), 1)',axiom,
% 0.70/0.80 ! [Vd456,Vd461,Vd462] :
% 0.70/0.80 ( Vd461 = Vd462
% 0.70/0.80 => vmul(Vd461,Vd456) = vmul(Vd462,Vd456) ) ).
% 0.70/0.80
% 0.70/0.80 fof('ass(cond(299, 0), 2)',axiom,
% 0.70/0.80 ! [Vd456,Vd457,Vd458] :
% 0.70/0.80 ( greater(Vd457,Vd458)
% 0.70/0.80 => greater(vmul(Vd457,Vd456),vmul(Vd458,Vd456)) ) ).
% 0.70/0.80
% 0.70/0.80 fof('ass(cond(290, 0), 0)',axiom,
% 0.70/0.80 ! [Vd444,Vd445,Vd446] : vmul(vmul(Vd444,Vd445),Vd446) = vmul(Vd444,vmul(Vd445,Vd446)) ).
% 0.70/0.80
% 0.70/0.81 fof('ass(cond(281, 0), 0)',axiom,
% 0.70/0.81 ! [Vd432,Vd433,Vd434] : vmul(Vd432,vplus(Vd433,Vd434)) = vplus(vmul(Vd432,Vd433),vmul(Vd432,Vd434)) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(270, 0), 0)',axiom,
% 0.70/0.81 ! [Vd418,Vd419] : vmul(Vd418,Vd419) = vmul(Vd419,Vd418) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(261, 0), 0)',axiom,
% 0.70/0.81 ! [Vd408,Vd409] : vmul(vsucc(Vd408),Vd409) = vplus(vmul(Vd408,Vd409),Vd409) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(253, 0), 0)',axiom,
% 0.70/0.81 ! [Vd400] : vmul(v1,Vd400) = Vd400 ).
% 0.70/0.81
% 0.70/0.81 fof('qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))',axiom,
% 0.70/0.81 ! [Vd396,Vd397] :
% 0.70/0.81 ( vmul(Vd396,vsucc(Vd397)) = vplus(vmul(Vd396,Vd397),Vd396)
% 0.70/0.81 & vmul(Vd396,v1) = Vd396 ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(241, 0), 0)',axiom,
% 0.70/0.81 ! [Vd386,Vd387] :
% 0.70/0.81 ( less(Vd386,vplus(Vd387,v1))
% 0.70/0.81 => leq(Vd386,Vd387) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(234, 0), 0)',axiom,
% 0.70/0.81 ! [Vd375,Vd376] :
% 0.70/0.81 ( greater(Vd375,Vd376)
% 0.70/0.81 => geq(Vd375,vplus(Vd376,v1)) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(228, 0), 0)',axiom,
% 0.70/0.81 ! [Vd369] : geq(Vd369,v1) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(223, 0), 0)',axiom,
% 0.70/0.81 ! [Vd362,Vd363,Vd365,Vd366] :
% 0.70/0.81 ( ( geq(Vd365,Vd366)
% 0.70/0.81 & geq(Vd362,Vd363) )
% 0.70/0.81 => geq(vplus(Vd362,Vd365),vplus(Vd363,Vd366)) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(147, 0), 0)',axiom,
% 0.70/0.81 ! [Vd226,Vd227] :
% 0.70/0.81 ( less(Vd226,Vd227)
% 0.70/0.81 => greater(Vd227,Vd226) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(140, 0), 0)',axiom,
% 0.70/0.81 ! [Vd208,Vd209] :
% 0.70/0.81 ( greater(Vd208,Vd209)
% 0.70/0.81 => less(Vd209,Vd208) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(130), 0), 0)',axiom,
% 0.70/0.81 ! [Vd203,Vd204] :
% 0.70/0.81 ( Vd203 = Vd204
% 0.70/0.81 | greater(Vd203,Vd204)
% 0.70/0.81 | less(Vd203,Vd204) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(130), 0), 1)',axiom,
% 0.70/0.81 ! [Vd203,Vd204] :
% 0.70/0.81 ( Vd203 != Vd204
% 0.70/0.81 | ~ less(Vd203,Vd204) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(130), 0), 2)',axiom,
% 0.70/0.81 ! [Vd203,Vd204] :
% 0.70/0.81 ( ~ greater(Vd203,Vd204)
% 0.70/0.81 | ~ less(Vd203,Vd204) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(130), 0), 3)',axiom,
% 0.70/0.81 ! [Vd203,Vd204] :
% 0.70/0.81 ( Vd203 != Vd204
% 0.70/0.81 | ~ greater(Vd203,Vd204) ) ).
% 0.70/0.81
% 0.70/0.81 fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
% 0.70/0.81 ! [Vd198,Vd199] :
% 0.70/0.81 ( less(Vd199,Vd198)
% 0.70/0.81 <=> ? [Vd201] : Vd198 = vplus(Vd199,Vd201) ) ).
% 0.70/0.81
% 0.70/0.81 fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
% 0.70/0.81 ! [Vd193,Vd194] :
% 0.70/0.81 ( greater(Vd194,Vd193)
% 0.70/0.81 <=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(88), 0), 0)',axiom,
% 0.70/0.81 ! [Vd120,Vd121] :
% 0.70/0.81 ( Vd120 = Vd121
% 0.70/0.81 | ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 0.70/0.81 | ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(88), 0), 1)',axiom,
% 0.70/0.81 ! [Vd120,Vd121] :
% 0.70/0.81 ( Vd120 != Vd121
% 0.70/0.81 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(88), 0), 2)',axiom,
% 0.70/0.81 ! [Vd120,Vd121] :
% 0.70/0.81 ( ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 0.70/0.81 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(goal(88), 0), 3)',axiom,
% 0.70/0.81 ! [Vd120,Vd121] :
% 0.70/0.81 ( Vd120 != Vd121
% 0.70/0.81 | ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(81, 0), 0)',axiom,
% 0.70/0.81 ! [Vd104,Vd105] :
% 0.70/0.81 ( Vd104 != Vd105
% 0.70/0.81 => ! [Vd107] : vplus(Vd107,Vd104) != vplus(Vd107,Vd105) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(73, 0), 0)',axiom,
% 0.70/0.81 ! [Vd92,Vd93] : Vd93 != vplus(Vd92,Vd93) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(61, 0), 0)',axiom,
% 0.70/0.81 ! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(52, 0), 0)',axiom,
% 0.70/0.81 ! [Vd68,Vd69] : vplus(vsucc(Vd68),Vd69) = vsucc(vplus(Vd68,Vd69)) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(43, 0), 0)',axiom,
% 0.70/0.81 ! [Vd59] : vplus(v1,Vd59) = vsucc(Vd59) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(33, 0), 0)',axiom,
% 0.70/0.81 ! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) ).
% 0.70/0.81
% 0.70/0.81 fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
% 0.70/0.81 ! [Vd42,Vd43] :
% 0.70/0.81 ( vplus(Vd42,vsucc(Vd43)) = vsucc(vplus(Vd42,Vd43))
% 0.70/0.81 & vplus(Vd42,v1) = vsucc(Vd42) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(20, 0), 0)',axiom,
% 0.70/0.81 ! [Vd24] :
% 0.70/0.81 ( Vd24 != v1
% 0.70/0.81 => Vd24 = vsucc(vskolem2(Vd24)) ) ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(12, 0), 0)',axiom,
% 0.70/0.81 ! [Vd16] : vsucc(Vd16) != Vd16 ).
% 0.70/0.81
% 0.70/0.81 fof('ass(cond(6, 0), 0)',axiom,
% 0.70/0.81 ! [Vd7,Vd8] :
% 0.70/0.81 ( Vd7 != Vd8
% 0.70/0.81 => vsucc(Vd7) != vsucc(Vd8) ) ).
% 0.70/0.81
% 0.70/0.81 %------------------------------------------------------------------------------
% 0.70/0.81 %-------------------------------------------
% 0.70/0.81 % Proof found
% 0.70/0.81 % SZS status Theorem for theBenchmark
% 0.70/0.81 % SZS output start Proof
% 0.70/0.81 %ClaNum:63(EqnAxiom:24)
% 0.70/0.81 %VarNum:166(SingletonVarNum:79)
% 0.70/0.81 %MaxLitNum:3
% 0.70/0.81 %MaxfuncDepth:2
% 0.70/0.81 %SharedTerms:8
% 0.70/0.81 %goalClause: 39
% 0.70/0.81 %singleGoalClaCount:1
% 0.70/0.81 [39]~P2(a7,a9)
% 0.70/0.81 [31]P2(f6(a7,a8),f6(a9,a8))
% 0.70/0.81 [25]P1(x251,a1)
% 0.70/0.81 [26]E(f6(x261,a1),x261)
% 0.70/0.81 [27]E(f6(a1,x271),x271)
% 0.70/0.81 [40]~E(f10(x401,a1),x401)
% 0.70/0.81 [29]E(f6(x291,x292),f6(x292,x291))
% 0.70/0.81 [30]E(f10(x301,x302),f10(x302,x301))
% 0.70/0.81 [41]~E(f10(x411,x412),x412)
% 0.70/0.81 [33]E(f10(f10(x331,a1),x332),f10(f10(x331,x332),a1))
% 0.70/0.81 [34]E(f10(f6(x341,x342),x341),f6(x341,f10(x342,a1)))
% 0.70/0.81 [35]E(f10(f6(x351,x352),x352),f6(f10(x351,a1),x352))
% 0.70/0.81 [36]E(f6(f6(x361,x362),x363),f6(x361,f6(x362,x363)))
% 0.70/0.81 [37]E(f10(f10(x371,x372),x373),f10(x371,f10(x372,x373)))
% 0.70/0.81 [38]E(f10(f6(x381,x382),f6(x381,x383)),f6(x381,f10(x382,x383)))
% 0.70/0.81 [42]E(x421,a1)+E(f10(f11(x421),a1),x421)
% 0.70/0.81 [43]~P2(x431,x432)+~E(x431,x432)
% 0.70/0.81 [44]~P3(x441,x442)+~E(x441,x442)
% 0.70/0.81 [48]~P3(x482,x481)+P2(x481,x482)
% 0.70/0.81 [49]~P2(x492,x491)+P3(x491,x492)
% 0.70/0.81 [53]~P3(x531,x532)+~P2(x531,x532)
% 0.70/0.81 [52]E(x521,x522)+~E(f10(x521,a1),f10(x522,a1))
% 0.70/0.81 [56]~P2(x561,x562)+P1(x561,f10(x562,a1))
% 0.70/0.81 [59]P4(x591,x592)+~P3(x591,f10(x592,a1))
% 0.70/0.81 [57]~P3(x571,x572)+E(f10(x571,f2(x572,x571)),x572)
% 0.70/0.81 [58]~P2(x582,x581)+E(f10(x581,f3(x581,x582)),x582)
% 0.70/0.81 [45]~E(x451,x452)+~E(x452,f10(x451,x453))
% 0.70/0.81 [46]~E(x461,x462)+~E(x461,f10(x462,x463))
% 0.70/0.81 [50]P2(x501,x502)+~E(x501,f10(x502,x503))
% 0.70/0.81 [51]P3(x511,x512)+~E(x512,f10(x511,x513))
% 0.70/0.81 [54]E(x541,x542)+~E(f10(x543,x541),f10(x543,x542))
% 0.70/0.81 [61]~P2(x611,x613)+P2(f6(x611,x612),f6(x613,x612))
% 0.70/0.81 [62]~P3(x621,x623)+P3(f6(x621,x622),f6(x623,x622))
% 0.70/0.81 [55]~E(x551,f10(x552,x553))+~E(x552,f10(x551,x554))
% 0.70/0.81 [47]P2(x471,x472)+P3(x471,x472)+E(x471,x472)
% 0.70/0.81 [60]E(x601,x602)+E(f10(x601,f4(x601,x602)),x602)+E(f10(x602,f5(x601,x602)),x601)
% 0.70/0.81 [63]~P1(x631,x633)+~P1(x632,x634)+P1(f10(x631,x632),f10(x633,x634))
% 0.70/0.81 %EqnAxiom
% 0.70/0.81 [1]E(x11,x11)
% 0.70/0.81 [2]E(x22,x21)+~E(x21,x22)
% 0.70/0.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.70/0.81 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43))
% 0.70/0.81 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52))
% 0.70/0.81 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63))
% 0.70/0.81 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72))
% 0.70/0.81 [8]~E(x81,x82)+E(f11(x81),f11(x82))
% 0.70/0.81 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 0.70/0.81 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 0.70/0.81 [11]~E(x111,x112)+E(f3(x111,x113),f3(x112,x113))
% 0.70/0.81 [12]~E(x121,x122)+E(f3(x123,x121),f3(x123,x122))
% 0.70/0.81 [13]~E(x131,x132)+E(f4(x131,x133),f4(x132,x133))
% 0.70/0.81 [14]~E(x141,x142)+E(f4(x143,x141),f4(x143,x142))
% 0.70/0.81 [15]~E(x151,x152)+E(f5(x151,x153),f5(x152,x153))
% 0.70/0.81 [16]~E(x161,x162)+E(f5(x163,x161),f5(x163,x162))
% 0.70/0.81 [17]P1(x172,x173)+~E(x171,x172)+~P1(x171,x173)
% 0.70/0.81 [18]P1(x183,x182)+~E(x181,x182)+~P1(x183,x181)
% 0.70/0.81 [19]P2(x192,x193)+~E(x191,x192)+~P2(x191,x193)
% 0.70/0.81 [20]P2(x203,x202)+~E(x201,x202)+~P2(x203,x201)
% 0.70/0.81 [21]P3(x212,x213)+~E(x211,x212)+~P3(x211,x213)
% 0.70/0.81 [22]P3(x223,x222)+~E(x221,x222)+~P3(x223,x221)
% 0.70/0.81 [23]P4(x232,x233)+~E(x231,x232)+~P4(x231,x233)
% 0.70/0.81 [24]P4(x243,x242)+~E(x241,x242)+~P4(x243,x241)
% 0.70/0.81
% 0.70/0.81 %-------------------------------------------
% 0.70/0.81 cnf(64,plain,
% 0.70/0.81 (~P2(x641,x641)),
% 0.70/0.81 inference(equality_inference,[],[43])).
% 0.70/0.81 cnf(65,plain,
% 0.70/0.81 (~P3(x651,x651)),
% 0.70/0.81 inference(equality_inference,[],[44])).
% 0.70/0.81 cnf(66,plain,
% 0.70/0.81 (P2(f10(x661,x662),x661)),
% 0.70/0.81 inference(equality_inference,[],[50])).
% 0.70/0.81 cnf(67,plain,
% 0.70/0.81 (P3(x671,f10(x671,x672))),
% 0.70/0.81 inference(equality_inference,[],[51])).
% 0.70/0.81 cnf(70,plain,
% 0.70/0.81 (~P3(a9,a7)),
% 0.70/0.81 inference(scs_inference,[],[39,48])).
% 0.70/0.81 cnf(72,plain,
% 0.70/0.81 (P2(f10(x721,x722),x722)),
% 0.70/0.81 inference(scs_inference,[],[39,30,48,50])).
% 0.70/0.81 cnf(81,plain,
% 0.70/0.81 (E(f6(x811,a1),x811)),
% 0.70/0.81 inference(rename_variables,[],[26])).
% 0.70/0.81 cnf(83,plain,
% 0.70/0.81 (P3(x831,f10(x832,x831))),
% 0.70/0.81 inference(scs_inference,[],[39,30,26,48,50,43,44,45,46,51])).
% 0.70/0.81 cnf(85,plain,
% 0.70/0.81 (~P3(f10(x851,x852),x851)),
% 0.70/0.81 inference(scs_inference,[],[39,66,30,26,48,50,43,44,45,46,51,53])).
% 0.70/0.82 cnf(89,plain,
% 0.70/0.82 (P4(x891,x891)),
% 0.70/0.82 inference(scs_inference,[],[39,66,67,30,26,48,50,43,44,45,46,51,53,55,59])).
% 0.70/0.82 cnf(90,plain,
% 0.70/0.82 (P3(x901,f10(x901,x902))),
% 0.70/0.82 inference(rename_variables,[],[67])).
% 0.70/0.82 cnf(92,plain,
% 0.70/0.82 (E(x921,f6(x921,a1))),
% 0.70/0.82 inference(scs_inference,[],[39,66,67,30,26,81,48,50,43,44,45,46,51,53,55,59,2])).
% 0.70/0.82 cnf(93,plain,
% 0.70/0.82 (~E(f10(f6(x931,a1),x932),x931)),
% 0.70/0.82 inference(scs_inference,[],[39,66,67,30,26,81,48,50,43,44,45,46,51,53,55,59,2,4])).
% 0.70/0.82 cnf(95,plain,
% 0.70/0.82 (~E(f10(a9,x951),a7)),
% 0.70/0.82 inference(scs_inference,[],[39,66,67,30,26,81,48,50,43,44,45,46,51,53,55,59,2,4,6,19])).
% 0.70/0.82 cnf(96,plain,
% 0.70/0.82 (P2(f10(x961,x962),x961)),
% 0.70/0.82 inference(rename_variables,[],[66])).
% 0.70/0.82 cnf(97,plain,
% 0.70/0.82 (~E(x971,f10(x971,x972))),
% 0.70/0.82 inference(scs_inference,[],[39,66,96,64,67,30,26,81,48,50,43,44,45,46,51,53,55,59,2,4,6,19,20])).
% 0.70/0.82 cnf(101,plain,
% 0.70/0.82 (P1(x1011,f6(a1,a1))),
% 0.70/0.82 inference(scs_inference,[],[39,66,96,64,67,30,41,26,81,25,48,50,43,44,45,46,51,53,55,59,2,4,6,19,20,3,18])).
% 0.70/0.82 cnf(102,plain,
% 0.70/0.82 (~E(f10(x1021,x1022),x1021)),
% 0.70/0.82 inference(scs_inference,[],[39,66,96,64,65,67,90,30,41,26,81,25,48,50,43,44,45,46,51,53,55,59,2,4,6,19,20,3,18,22])).
% 0.70/0.82 cnf(104,plain,
% 0.70/0.82 (P4(f10(f10(x1041,x1042),x1043),f10(x1043,f10(x1041,x1042)))),
% 0.70/0.82 inference(scs_inference,[],[39,66,96,64,65,67,90,30,41,26,81,25,48,50,43,44,45,46,51,53,55,59,2,4,6,19,20,3,18,22,23])).
% 0.70/0.82 cnf(105,plain,
% 0.70/0.82 (E(f10(x1051,x1052),f10(x1052,x1051))),
% 0.70/0.82 inference(rename_variables,[],[30])).
% 0.70/0.82 cnf(106,plain,
% 0.70/0.82 (P4(f10(x1061,f10(x1062,x1063)),f10(f10(x1062,x1063),x1061))),
% 0.70/0.82 inference(scs_inference,[],[39,66,96,64,65,67,90,30,105,41,26,81,25,48,50,43,44,45,46,51,53,55,59,2,4,6,19,20,3,18,22,23,24])).
% 0.70/0.82 cnf(120,plain,
% 0.70/0.82 (E(f6(a1,x1201),x1201)),
% 0.70/0.82 inference(rename_variables,[],[27])).
% 0.70/0.82 cnf(122,plain,
% 0.70/0.82 (~P2(x1221,f10(x1221,x1222))),
% 0.70/0.82 inference(scs_inference,[],[85,93,27,58,45,49])).
% 0.70/0.82 cnf(124,plain,
% 0.70/0.82 (~P2(f6(a1,x1241),x1241)),
% 0.70/0.82 inference(scs_inference,[],[85,93,27,120,58,45,49,43])).
% 0.70/0.82 cnf(126,plain,
% 0.70/0.82 (P4(a1,x1261)),
% 0.70/0.82 inference(scs_inference,[],[83,85,93,27,120,58,45,49,43,59])).
% 0.70/0.82 cnf(129,plain,
% 0.70/0.82 (P3(x1291,f6(a1,f10(x1291,x1292)))),
% 0.70/0.82 inference(scs_inference,[],[83,85,93,27,120,58,45,49,43,59,51])).
% 0.70/0.82 cnf(130,plain,
% 0.70/0.82 (E(f6(a1,x1301),x1301)),
% 0.70/0.82 inference(rename_variables,[],[27])).
% 0.70/0.82 cnf(132,plain,
% 0.70/0.82 (~P3(f10(x1321,x1322),x1322)),
% 0.70/0.82 inference(scs_inference,[],[72,83,85,93,27,120,58,45,49,43,59,51,53])).
% 0.70/0.82 cnf(134,plain,
% 0.70/0.82 (~P3(x1341,f6(x1341,a1))),
% 0.70/0.82 inference(scs_inference,[],[72,83,85,93,92,27,120,58,45,49,43,59,51,53,44])).
% 0.70/0.82 cnf(136,plain,
% 0.70/0.82 (~E(f6(a1,f10(x1361,x1362)),x1361)),
% 0.70/0.82 inference(scs_inference,[],[72,83,85,93,92,27,120,130,58,45,49,43,59,51,53,44,46])).
% 0.70/0.82 cnf(137,plain,
% 0.70/0.82 (E(f6(a1,x1371),x1371)),
% 0.70/0.82 inference(rename_variables,[],[27])).
% 0.70/0.82 cnf(139,plain,
% 0.70/0.82 (P2(f6(a1,f10(x1391,x1392)),x1391)),
% 0.70/0.82 inference(scs_inference,[],[72,83,85,93,92,27,120,130,137,58,45,49,43,59,51,53,44,46,50])).
% 0.70/0.82 cnf(140,plain,
% 0.70/0.82 (E(f6(a1,x1401),x1401)),
% 0.70/0.82 inference(rename_variables,[],[27])).
% 0.70/0.82 cnf(143,plain,
% 0.70/0.82 (E(f6(a1,x1431),x1431)),
% 0.70/0.82 inference(rename_variables,[],[27])).
% 0.70/0.82 cnf(145,plain,
% 0.70/0.82 (E(x1451,f6(a1,x1451))),
% 0.70/0.82 inference(scs_inference,[],[72,83,85,93,92,27,120,130,137,140,143,58,45,49,43,59,51,53,44,46,50,55,2])).
% 0.70/0.82 cnf(149,plain,
% 0.70/0.82 (~E(f10(x1491,a9),a7)),
% 0.70/0.82 inference(scs_inference,[],[39,72,97,83,85,93,92,27,120,130,137,140,143,37,58,45,49,43,59,51,53,44,46,50,55,2,3,19])).
% 0.70/0.82 cnf(152,plain,
% 0.70/0.82 (P4(x1521,x1521)),
% 0.70/0.82 inference(rename_variables,[],[89])).
% 0.70/0.82 cnf(155,plain,
% 0.70/0.82 (~E(f6(a9,a8),f6(a7,a8))),
% 0.70/0.82 inference(scs_inference,[],[39,72,97,89,152,83,85,93,92,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20])).
% 0.70/0.82 cnf(157,plain,
% 0.70/0.82 (P1(x1571,f6(f6(a1,a1),a1))),
% 0.70/0.82 inference(scs_inference,[],[39,72,97,89,152,83,85,93,92,101,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20,18])).
% 0.70/0.82 cnf(161,plain,
% 0.70/0.82 (~P3(f10(a9,x1611),f6(a1,f10(a9,x1611)))),
% 0.70/0.82 inference(scs_inference,[],[39,70,72,97,89,152,83,85,93,92,101,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20,18,22,5,48])).
% 0.70/0.82 cnf(164,plain,
% 0.70/0.82 (~E(x1641,f6(a1,f10(f10(x1641,x1642),x1643)))),
% 0.70/0.82 inference(scs_inference,[],[39,70,72,97,89,152,83,85,93,92,101,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20,18,22,5,48,4,6])).
% 0.70/0.82 cnf(165,plain,
% 0.70/0.82 (E(f10(a7,f5(a9,a7)),a9)),
% 0.70/0.82 inference(scs_inference,[],[39,70,72,97,95,89,152,83,85,93,92,101,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20,18,22,5,48,4,6,60])).
% 0.70/0.82 cnf(168,plain,
% 0.70/0.82 (P2(a9,a7)),
% 0.70/0.82 inference(scs_inference,[],[39,70,72,97,95,89,152,83,85,93,92,101,27,120,130,137,140,143,37,64,31,58,45,49,43,59,51,53,44,46,50,55,2,3,19,23,24,20,18,22,5,48,4,6,60,47])).
% 0.70/0.82 cnf(170,plain,
% 0.70/0.82 (~P3(x1701,f6(a1,x1701))),
% 0.70/0.82 inference(scs_inference,[],[124,48])).
% 0.70/0.82 cnf(172,plain,
% 0.70/0.82 (~P2(x1721,f10(x1722,x1721))),
% 0.70/0.82 inference(scs_inference,[],[132,124,48,49])).
% 0.70/0.82 cnf(182,plain,
% 0.70/0.82 (P3(f10(x1821,x1822),f10(f10(x1821,a1),x1822))),
% 0.70/0.82 inference(scs_inference,[],[139,132,124,145,136,33,48,49,53,43,5,45,51])).
% 0.70/0.82 cnf(184,plain,
% 0.70/0.82 (P2(f10(f10(x1841,a1),x1842),f10(x1841,x1842))),
% 0.70/0.82 inference(scs_inference,[],[139,132,124,145,136,33,48,49,53,43,5,45,51,50])).
% 0.70/0.82 cnf(192,plain,
% 0.70/0.82 (E(a9,f10(a7,f5(a9,a7)))),
% 0.70/0.82 inference(scs_inference,[],[139,132,124,145,136,165,33,48,49,53,43,5,45,51,50,44,55,46,2])).
% 0.70/0.82 cnf(193,plain,
% 0.70/0.82 (~E(a9,f6(a1,a7))),
% 0.70/0.82 inference(scs_inference,[],[139,168,132,124,145,136,165,33,48,49,53,43,5,45,51,50,44,55,46,2,19])).
% 0.70/0.82 cnf(200,plain,
% 0.70/0.82 (E(x2001,f6(a1,x2001))),
% 0.70/0.82 inference(rename_variables,[],[145])).
% 0.70/0.82 cnf(205,plain,
% 0.70/0.82 (P1(x2051,f6(a1,f6(f6(a1,a1),a1)))),
% 0.70/0.82 inference(scs_inference,[],[161,122,139,168,102,132,124,145,200,136,157,165,126,33,89,67,48,49,53,43,5,45,51,50,44,55,46,2,19,24,3,23,20,22,18])).
% 0.70/0.82 cnf(209,plain,
% 0.70/0.82 (~P2(f10(a7,f5(a9,a7)),a9)),
% 0.70/0.82 inference(scs_inference,[],[161,122,139,168,102,132,124,145,200,136,157,165,126,33,89,67,48,49,53,43,5,45,51,50,44,55,46,2,19,24,3,23,20,22,18,57,58])).
% 0.70/0.82 cnf(211,plain,
% 0.70/0.82 (~P3(a9,f10(a7,f5(a9,a7)))),
% 0.70/0.82 inference(scs_inference,[],[209,48])).
% 0.70/0.82 cnf(215,plain,
% 0.70/0.82 (P3(a7,a9)),
% 0.70/0.82 inference(scs_inference,[],[184,209,192,48,53,51])).
% 0.70/0.82 cnf(217,plain,
% 0.70/0.82 (~P2(f6(x2171,a1),x2171)),
% 0.70/0.82 inference(scs_inference,[],[184,134,209,192,48,53,51,49])).
% 0.70/0.82 cnf(223,plain,
% 0.70/0.82 (P2(f6(f10(x2231,x2232),a1),x2231)),
% 0.70/0.82 inference(scs_inference,[],[184,134,164,209,192,26,48,53,51,49,5,43,50])).
% 0.70/0.82 cnf(224,plain,
% 0.70/0.82 (E(f6(x2241,a1),x2241)),
% 0.70/0.82 inference(rename_variables,[],[26])).
% 0.70/0.82 cnf(229,plain,
% 0.70/0.82 (E(f6(x2291,a1),x2291)),
% 0.70/0.82 inference(rename_variables,[],[26])).
% 0.70/0.82 cnf(234,plain,
% 0.70/0.82 (~P3(f10(f10(x2341,x2342),x2343),f10(x2341,f10(x2342,x2343)))),
% 0.70/0.82 inference(scs_inference,[],[184,134,164,209,192,26,224,37,48,53,51,49,5,43,50,45,55,6,46,44])).
% 0.70/0.82 cnf(236,plain,
% 0.70/0.82 (E(f10(x2361,f10(x2362,x2363)),f10(f10(x2361,x2362),x2363))),
% 0.70/0.82 inference(scs_inference,[],[184,134,164,209,192,26,224,37,48,53,51,49,5,43,50,45,55,6,46,44,2])).
% 0.70/0.82 cnf(237,plain,
% 0.70/0.82 (E(f10(a7,f5(f10(a7,a9),a7)),f10(a7,a9))),
% 0.70/0.82 inference(scs_inference,[],[184,149,134,164,209,192,26,224,37,48,53,51,49,5,43,50,45,55,6,46,44,2,60])).
% 0.70/0.82 cnf(241,plain,
% 0.70/0.82 (P4(x2411,x2411)),
% 0.70/0.82 inference(rename_variables,[],[89])).
% 0.70/0.82 cnf(248,plain,
% 0.70/0.82 (~E(f10(x2481,x2482),f10(x2483,f10(f10(x2481,a1),x2482)))),
% 0.70/0.82 inference(scs_inference,[],[172,184,155,149,134,164,209,192,26,224,229,37,64,89,241,31,48,53,51,49,5,43,50,45,55,6,46,44,2,60,24,23,19,3,20])).
% 0.70/0.82 cnf(252,plain,
% 0.70/0.82 (E(f5(f10(a7,a9),a7),a9)),
% 0.70/0.82 inference(scs_inference,[],[170,172,184,155,149,182,134,164,209,192,26,224,229,37,64,89,241,31,48,53,51,49,5,43,50,45,55,6,46,44,2,60,24,23,19,3,20,22,54])).
% 0.70/0.82 cnf(257,plain,
% 0.70/0.82 (~P3(f6(f10(x2571,x2572),a1),x2571)),
% 0.70/0.82 inference(scs_inference,[],[223,236,51,53])).
% 0.70/0.82 cnf(259,plain,
% 0.70/0.82 (P2(f10(x2591,f10(x2592,x2593)),f10(x2591,x2592))),
% 0.70/0.82 inference(scs_inference,[],[223,236,51,53,50])).
% 0.70/0.82 cnf(261,plain,
% 0.70/0.82 (~P2(f10(x2611,f10(x2612,x2613)),f10(f10(x2611,x2612),x2613))),
% 0.70/0.82 inference(scs_inference,[],[223,234,236,51,53,50,49])).
% 0.70/0.82 cnf(267,plain,
% 0.70/0.82 (~P3(f10(x2671,f10(x2672,x2673)),f10(f10(x2671,x2672),x2673))),
% 0.70/0.82 inference(scs_inference,[],[223,234,236,237,51,53,50,49,45,43,44])).
% 0.70/0.82 cnf(273,plain,
% 0.70/0.82 (E(f10(a7,a9),f10(a7,f5(f10(a7,a9),a7)))),
% 0.70/0.82 inference(scs_inference,[],[223,234,236,237,51,53,50,49,45,43,44,46,55,2])).
% 0.70/0.82 cnf(277,plain,
% 0.70/0.82 (P4(x2771,x2771)),
% 0.70/0.82 inference(rename_variables,[],[89])).
% 0.70/0.82 cnf(282,plain,
% 0.70/0.82 (~E(f10(f6(a9,a1),x2821),f5(f10(a7,a9),a7))),
% 0.70/0.82 inference(scs_inference,[],[39,211,223,93,234,236,237,252,83,89,277,51,53,50,49,45,43,44,46,55,2,21,23,24,19,3])).
% 0.70/0.82 cnf(288,plain,
% 0.70/0.82 (E(a9,f5(f10(a7,a9),a7))),
% 0.70/0.82 inference(scs_inference,[],[39,211,223,122,93,234,236,129,237,252,83,89,277,31,51,53,50,49,45,43,44,46,55,2,21,23,24,19,3,20,22,54])).
% 0.70/0.82 cnf(292,plain,
% 0.70/0.82 (~P3(f10(a7,a9),f10(a7,f5(f10(a7,a9),a7)))),
% 0.70/0.82 inference(scs_inference,[],[39,211,223,122,93,234,236,129,237,252,83,89,277,31,51,53,50,49,45,43,44,46,55,2,21,23,24,19,3,20,22,54,58,48])).
% 0.70/0.82 cnf(301,plain,
% 0.70/0.82 (E(f6(x3011,a1),x3011)),
% 0.70/0.82 inference(rename_variables,[],[26])).
% 0.70/0.82 cnf(303,plain,
% 0.70/0.82 (P2(f10(f10(x3031,x3032),x3033),x3031)),
% 0.70/0.82 inference(scs_inference,[],[282,257,26,37,62,57,51,50])).
% 0.70/0.82 cnf(308,plain,
% 0.70/0.82 (~P2(f10(f10(x3081,x3082),x3083),f10(x3081,f10(x3082,x3083)))),
% 0.70/0.82 inference(scs_inference,[],[267,282,257,26,301,37,62,57,51,50,45,49])).
% 0.70/0.82 cnf(310,plain,
% 0.70/0.82 (~P3(f10(x3101,f10(x3102,x3103)),f10(x3101,x3102))),
% 0.70/0.82 inference(scs_inference,[],[259,267,282,257,26,301,37,62,57,51,50,45,49,53])).
% 0.70/0.82 cnf(318,plain,
% 0.70/0.82 (E(f10(f10(x3181,x3182),a1),f10(f10(x3181,a1),x3182))),
% 0.70/0.82 inference(scs_inference,[],[259,267,273,282,257,288,26,301,37,33,62,57,51,50,45,49,53,44,43,55,2])).
% 0.70/0.82 cnf(325,plain,
% 0.70/0.82 (P4(x3251,x3251)),
% 0.70/0.82 inference(rename_variables,[],[89])).
% 0.70/0.82 cnf(330,plain,
% 0.70/0.82 (~E(f10(f6(a9,a1),x3301),f10(a7,f5(a9,a7)))),
% 0.70/0.82 inference(scs_inference,[],[292,259,261,149,93,267,273,282,257,288,83,26,301,165,89,325,37,33,62,57,51,50,45,49,53,44,43,55,2,21,47,23,24,19,3])).
% 0.70/0.82 cnf(335,plain,
% 0.70/0.82 (~P2(f10(a7,f5(a9,a7)),f6(a9,a1))),
% 0.70/0.82 inference(scs_inference,[],[292,259,261,172,139,149,93,267,273,282,257,288,83,26,301,165,89,325,37,33,62,57,51,50,45,49,53,44,43,55,2,21,47,23,24,19,3,20,7,58])).
% 0.70/0.82 cnf(337,plain,
% 0.70/0.82 (~P3(f10(a7,f5(f10(a7,a9),a7)),f10(a7,a9))),
% 0.70/0.82 inference(scs_inference,[],[292,259,261,172,139,149,93,267,273,282,257,288,83,26,301,165,89,325,37,33,62,57,51,50,45,49,53,44,43,55,2,21,47,23,24,19,3,20,7,58,48])).
% 0.70/0.82 cnf(343,plain,
% 0.70/0.82 (~P3(f6(a9,a1),f10(a7,f5(a9,a7)))),
% 0.70/0.82 inference(scs_inference,[],[335,48])).
% 0.70/0.82 cnf(349,plain,
% 0.70/0.82 (P2(f10(f10(x3491,x3492),a1),f10(x3491,a1))),
% 0.70/0.82 inference(scs_inference,[],[335,318,48,51,45,50])).
% 0.70/0.82 cnf(361,plain,
% 0.70/0.82 (~P2(f10(f10(x3611,x3612),a1),f10(f10(x3611,a1),x3612))),
% 0.70/0.82 inference(scs_inference,[],[303,310,330,335,318,48,51,45,50,6,53,49,44,55,43])).
% 0.70/0.82 cnf(363,plain,
% 0.70/0.82 (E(f6(x3631,f10(x3632,x3633)),f10(f6(x3631,x3632),f6(x3631,x3633)))),
% 0.70/0.82 inference(scs_inference,[],[303,310,330,335,318,38,48,51,45,50,6,53,49,44,55,43,2])).
% 0.70/0.82 cnf(367,plain,
% 0.70/0.82 (P4(x3671,x3671)),
% 0.70/0.82 inference(rename_variables,[],[89])).
% 0.70/0.82 cnf(370,plain,
% 0.70/0.82 (~E(f10(f10(a9,x3701),x3702),a7)),
% 0.70/0.82 inference(scs_inference,[],[39,337,303,310,330,335,318,83,89,367,38,48,51,45,50,6,53,49,44,55,43,2,21,23,24,19])).
% 0.70/0.82 cnf(374,plain,
% 0.70/0.82 (~E(f10(f6(f6(x3741,a1),a1),x3742),x3741)),
% 0.70/0.82 inference(scs_inference,[],[39,337,303,93,310,330,335,318,182,83,92,89,367,38,48,51,45,50,6,53,49,44,55,43,2,21,23,24,19,22,3])).
% 0.70/0.82 cnf(382,plain,
% 0.70/0.82 (~P3(f6(f6(x3821,a1),a1),x3821)),
% 0.70/0.82 inference(scs_inference,[],[39,337,308,303,72,93,310,330,335,318,182,83,92,89,367,38,48,51,45,50,6,53,49,44,55,43,2,21,23,24,19,22,3,20,59,58,57])).
% 0.70/0.82 cnf(391,plain,
% 0.70/0.82 (~E(f10(f10(a9,x3911),x3912),a7)),
% 0.70/0.82 inference(rename_variables,[],[370])).
% 0.70/0.82 cnf(395,plain,
% 0.70/0.82 (P3(f6(x3951,x3952),f6(x3951,f10(x3952,x3953)))),
% 0.70/0.82 inference(scs_inference,[],[370,363,361,48,57,45,51])).
% 0.70/0.82 cnf(399,plain,
% 0.70/0.82 (P2(f6(x3991,f10(x3992,x3993)),f6(x3991,x3992))),
% 0.70/0.82 inference(scs_inference,[],[370,363,374,361,48,57,45,51,6,50])).
% 0.70/0.82 cnf(401,plain,
% 0.70/0.82 (~P2(x4011,f6(f10(x4011,x4012),a1))),
% 0.70/0.82 inference(scs_inference,[],[370,257,363,374,361,48,57,45,51,6,50,49])).
% 0.70/0.82 cnf(405,plain,
% 0.70/0.82 (~P3(f6(x4051,f10(x4052,x4053)),f10(f6(x4051,x4052),f6(x4051,x4053)))),
% 0.70/0.82 inference(scs_inference,[],[349,370,257,363,374,361,48,57,45,51,6,50,49,53,44])).
% 0.70/0.82 cnf(407,plain,
% 0.70/0.82 (~P2(f6(x4071,f10(x4072,x4073)),f10(f6(x4071,x4072),f6(x4071,x4073)))),
% 0.70/0.82 inference(scs_inference,[],[349,370,257,363,374,361,48,57,45,51,6,50,49,53,44,43])).
% 0.70/0.82 cnf(411,plain,
% 0.70/0.82 (E(f6(x4111,f6(x4112,x4113)),f6(f6(x4111,x4112),x4113))),
% 0.70/0.82 inference(scs_inference,[],[349,370,257,363,374,361,36,48,57,45,51,6,50,49,53,44,43,55,2])).
% 0.70/0.82 cnf(412,plain,
% 0.70/0.82 (E(f10(a7,f5(f10(a9,x4121),a7)),f10(a9,x4121))),
% 0.70/0.82 inference(scs_inference,[],[95,349,370,391,257,363,374,361,36,48,57,45,51,6,50,49,53,44,43,55,2,60])).
% 0.70/0.82 cnf(415,plain,
% 0.70/0.82 (P2(f10(a9,x4151),a7)),
% 0.70/0.82 inference(scs_inference,[],[95,349,370,391,257,363,374,361,36,48,57,45,51,6,50,49,53,44,43,55,2,60,47])).
% 0.70/0.82 cnf(440,plain,
% 0.70/0.82 (~P3(f10(f6(x4401,x4402),f6(x4401,x4403)),f6(x4401,f10(x4402,x4403)))),
% 0.70/0.82 inference(scs_inference,[],[407,48])).
% 0.70/0.82 cnf(448,plain,
% 0.70/0.82 (P2(f10(a7,f5(f10(a9,x4481),a7)),a9)),
% 0.70/0.82 inference(scs_inference,[],[405,407,412,48,45,51,49,50])).
% 0.70/0.82 cnf(450,plain,
% 0.70/0.82 (~P3(f6(x4501,f10(x4502,x4503)),f6(x4501,x4502))),
% 0.70/0.82 inference(scs_inference,[],[399,405,407,412,48,45,51,49,50,53])).
% 0.70/0.82 cnf(452,plain,
% 0.70/0.82 (~P2(f6(x4521,f6(x4522,x4523)),f6(f6(x4521,x4522),x4523))),
% 0.70/0.82 inference(scs_inference,[],[399,405,407,411,412,48,45,51,49,50,53,43])).
% 0.70/0.82 cnf(456,plain,
% 0.70/0.82 (E(f10(a9,x4561),f10(a7,f5(f10(a9,x4561),a7)))),
% 0.70/0.82 inference(scs_inference,[],[399,405,407,411,412,48,45,51,49,50,53,43,44,2])).
% 0.70/0.82 cnf(460,plain,
% 0.70/0.82 (P1(x4601,f6(f6(a1,f6(a1,a1)),a1))),
% 0.70/0.82 inference(scs_inference,[],[170,399,205,405,407,411,395,412,48,45,51,49,50,53,43,44,2,21,18])).
% 0.70/0.82 cnf(481,plain,
% 0.70/0.82 (~P2(x4811,f6(f6(x4811,a1),a1))),
% 0.70/0.82 inference(scs_inference,[],[382,452,456,48,51,49])).
% 0.70/0.82 cnf(483,plain,
% 0.70/0.82 (~P2(f10(a7,f5(f10(a9,x4831),a7)),f10(a9,x4831))),
% 0.70/0.82 inference(scs_inference,[],[382,412,452,456,48,51,49,43])).
% 0.70/0.82 cnf(489,plain,
% 0.70/0.82 (E(f6(x4891,f10(x4892,a1)),f10(f6(x4891,x4892),x4891))),
% 0.70/0.82 inference(scs_inference,[],[448,382,412,452,456,34,48,51,49,43,53,44,2])).
% 0.70/0.82 cnf(498,plain,
% 0.70/0.82 (~E(f10(a9,x4981),f6(a7,a1))),
% 0.70/0.82 inference(scs_inference,[],[440,217,448,415,382,182,26,412,33,452,460,456,104,106,34,48,51,49,43,53,44,2,18,23,24,22,19])).
% 0.70/0.82 cnf(500,plain,
% 0.70/0.82 (~E(f10(a9,x5001),f6(a1,a7))),
% 0.70/0.82 inference(scs_inference,[],[440,95,217,448,415,382,27,182,26,412,33,452,460,456,104,106,34,48,51,49,43,53,44,2,18,23,24,22,19,3])).
% 0.70/0.82 cnf(504,plain,
% 0.70/0.82 (P4(a7,a9)),
% 0.70/0.82 inference(scs_inference,[],[440,95,217,448,401,415,168,382,27,182,26,412,33,452,460,456,104,106,34,48,51,49,43,53,44,2,18,23,24,22,19,3,20,59])).
% 0.70/0.82 cnf(508,plain,
% 0.70/0.82 (~P3(a9,f6(a1,a7))),
% 0.70/0.82 inference(scs_inference,[],[440,95,217,448,401,415,168,382,27,182,26,412,33,452,460,456,104,106,34,48,51,49,43,53,44,2,18,23,24,22,19,3,20,59,58,57])).
% 0.70/0.82 cnf(519,plain,
% 0.70/0.82 (~E(f10(a9,x5191),f6(a1,a7))),
% 0.70/0.82 inference(rename_variables,[],[500])).
% 0.70/0.82 cnf(543,plain,
% 0.70/0.82 (P3(x5431,f10(x5432,x5431))),
% 0.70/0.82 inference(rename_variables,[],[83])).
% 0.70/0.82 cnf(556,plain,
% 0.70/0.82 ($false),
% 0.70/0.82 inference(scs_inference,[],[343,248,217,193,498,481,259,415,192,33,37,83,543,215,450,489,500,519,483,508,504,92,35,31,58,48,57,51,49,53,43,44,2,60,47,21,23,24,22,19,3,20,62]),
% 0.70/0.82 ['proof']).
% 0.70/0.82 % SZS output end Proof
% 0.70/0.82 % Total time :0.220000s
%------------------------------------------------------------------------------