%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO094+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 06:03:47 EDT 2024
% Result : Theorem 60.17s 60.29s
% Output : CNFRefutation 60.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GEO094+1 : TPTP v8.2.0. Released v2.4.0.
% 0.02/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Fri Jun 21 06:10:23 EDT 2024
% 0.09/0.28 % CPUTime :
% 0.14/0.45 start to proof:theBenchmark
% 60.17/60.28 %-------------------------------------------
% 60.17/60.28 % File :CSE---1.7
% 60.17/60.28 % Problem :theBenchmark
% 60.17/60.28 % Transform :cnf
% 60.17/60.28 % Format :tptp:raw
% 60.17/60.28 % Command :java -jar mcs_scs.jar %d %s
% 60.17/60.28
% 60.17/60.28 % Result :Theorem 59.770000s
% 60.17/60.28 % Output :CNFRefutation 59.770000s
% 60.17/60.28 %-------------------------------------------
% 60.17/60.29 %--------------------------------------------------------------------------
% 60.17/60.29 % File : GEO094+1 : TPTP v8.2.0. Released v2.4.0.
% 60.17/60.29 % Domain : Geometry (Oriented curves)
% 60.17/60.29 % Problem : Meeting point is not an endpoint of contianing curve
% 60.17/60.29 % Version : [EHK99] axioms.
% 60.17/60.29 % English : A meeting point of two curves is not an endpoint of any curve
% 60.17/60.29 % that includes both as sub-curves.
% 60.17/60.29
% 60.17/60.29 % Refs : [KE99] Kulik & Eschenbach (1999), A Geometry of Oriented Curv
% 60.17/60.29 % : [EHK99] Eschenbach et al. (1999), Representing Simple Trajecto
% 60.17/60.29 % Source : [KE99]
% 60.17/60.29 % Names : Proposition 2.14 (3) [KE99]
% 60.17/60.29
% 60.17/60.29 % Status : Theorem
% 60.17/60.29 % Rating : 0.39 v8.2.0, 0.36 v7.5.0, 0.41 v7.4.0, 0.37 v7.3.0, 0.34 v7.2.0, 0.31 v7.1.0, 0.30 v7.0.0, 0.27 v6.3.0, 0.33 v6.2.0, 0.40 v6.1.0, 0.43 v6.0.0, 0.48 v5.4.0, 0.50 v5.3.0, 0.48 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.43 v4.0.0, 0.42 v3.7.0, 0.35 v3.5.0, 0.32 v3.3.0, 0.29 v3.2.0, 0.36 v3.1.0, 0.44 v2.7.0, 0.33 v2.6.0, 0.50 v2.4.0
% 60.17/60.29 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 60.17/60.29 % Number of atoms : 71 ( 10 equ)
% 60.17/60.29 % Maximal formula atoms : 12 ( 4 avg)
% 60.17/60.29 % Number of connectives : 59 ( 5 ~; 9 |; 23 &)
% 60.17/60.29 % ( 9 <=>; 13 =>; 0 <=; 0 <~>)
% 60.17/60.29 % Maximal formula depth : 12 ( 7 avg)
% 60.17/60.29 % Maximal term depth : 2 ( 1 avg)
% 60.17/60.29 % Number of predicates : 8 ( 7 usr; 0 prp; 1-3 aty)
% 60.17/60.29 % Number of functors : 1 ( 1 usr; 0 con; 2-2 aty)
% 60.17/60.29 % Number of variables : 57 ( 48 !; 9 ?)
% 60.17/60.29 % SPC : FOF_THM_RFO_SEQ
% 60.17/60.29
% 60.17/60.29 % Comments :
% 60.17/60.29 %--------------------------------------------------------------------------
% 60.17/60.29 %----Include simple curve axioms
% 60.17/60.29 include('Axioms/GEO004+0.ax').
% 60.17/60.29 %--------------------------------------------------------------------------
% 60.17/60.29 fof(proposition_2_14_3,conjecture,
% 60.17/60.29 ! [C,C1,C2,P] :
% 60.17/60.29 ( ( meet(P,C1,C2)
% 60.17/60.29 & part_of(C1,C)
% 60.17/60.29 & part_of(C2,C) )
% 60.17/60.29 => ~ end_point(P,C) ) ).
% 60.17/60.29
% 60.17/60.29 %--------------------------------------------------------------------------
% 60.17/60.29 %-------------------------------------------
% 60.17/60.29 % Proof found
% 60.17/60.29 % SZS status Theorem for theBenchmark
% 60.17/60.29 % SZS output start Proof
% 60.17/60.30 %ClaNum:90(EqnAxiom:43)
% 60.17/60.30 %VarNum:331(SingletonVarNum:113)
% 60.17/60.30 %MaxLitNum:12
% 60.17/60.30 %MaxfuncDepth:2
% 60.17/60.30 %SharedTerms:8
% 60.17/60.30 %goalClause: 44 45 46 48
% 60.17/60.30 %singleGoalClaCount:4
% 60.17/60.30 [44]P1(a1,a2)
% 60.17/60.30 [45]P1(a7,a2)
% 60.17/60.30 [46]P2(a8,a2)
% 60.17/60.30 [48]P6(a8,a1,a7)
% 60.17/60.30 [47]P4(f9(x471),x471)
% 60.17/60.30 [49]P3(x491)+P2(f10(x491),x491)
% 60.17/60.30 [51]~P7(x511)+P2(f16(x511),x511)
% 60.17/60.30 [50]P7(x501)+~P2(x502,x501)
% 60.17/60.30 [53]~P3(x531)+~P2(x532,x531)
% 60.17/60.30 [54]~P2(x541,x542)+P5(x541,x542)
% 60.17/60.30 [55]~P4(x551,x552)+P5(x551,x552)
% 60.17/60.30 [56]~P4(x561,x562)+~P2(x561,x562)
% 60.17/60.30 [57]~P2(x572,x571)+~E(f3(x571,x572),x572)
% 60.17/60.30 [59]P1(x591,x592)+P5(f11(x592,x591),x591)
% 60.17/60.30 [63]~P2(x632,x631)+P2(f3(x631,x632),x631)
% 60.17/60.30 [70]P1(x701,x702)+~P5(f11(x702,x701),x702)
% 60.17/60.30 [77]~P4(x771,x772)+P6(x771,f18(x772,x771),f4(x772,x771))
% 60.17/60.30 [72]~P4(x722,x721)+E(f17(f18(x721,x722),f4(x721,x722)),x721)
% 60.17/60.30 [73]P5(x731,x732)+~P6(x731,x733,x732)
% 60.17/60.30 [74]P5(x741,x742)+~P6(x741,x742,x743)
% 60.17/60.30 [75]~P6(x753,x751,x752)+E(f6(x751,x752),f17(x751,x752))
% 60.17/60.30 [52]P7(x521)+~P1(x521,x522)+E(x521,x522)
% 60.17/60.30 [58]P4(x581,x582)+~P5(x581,x582)+P2(x581,x582)
% 60.17/60.30 [66]~P5(x661,x662)+P2(x661,x662)+P5(x661,f12(x661,x662))
% 60.17/60.30 [67]~P5(x671,x672)+P2(x671,x672)+P5(x671,f14(x671,x672))
% 60.17/60.30 [68]~P5(x681,x682)+P2(x681,x682)+P1(f12(x681,x682),x682)
% 60.17/60.30 [69]~P5(x691,x692)+P2(x691,x692)+P1(f14(x691,x692),x692)
% 60.17/60.30 [71]E(x711,x712)+P5(f5(x711,x712),x712)+P5(f5(x711,x712),x711)
% 60.17/60.30 [76]E(x761,x762)+~P5(f5(x761,x762),x762)+~P5(f5(x761,x762),x761)
% 60.17/60.30 [78]~P5(x781,x782)+P2(x781,x782)+~P1(f12(x781,x782),f14(x781,x782))
% 60.17/60.30 [79]~P5(x791,x792)+P2(x791,x792)+~P1(f14(x791,x792),f12(x791,x792))
% 60.17/60.30 [60]~P5(x601,x603)+P5(x601,x602)+~P1(x603,x602)
% 60.17/60.30 [88]~P5(f13(x881,x882,x883),x883)+~P5(f13(x881,x882,x883),x881)+E(x881,f17(x882,x883))
% 60.17/60.30 [89]~P5(f13(x891,x892,x893),x892)+~P5(f13(x891,x892,x893),x891)+E(x891,f17(x892,x893))
% 60.17/60.30 [61]~P5(x611,x614)+P5(x611,x612)+~E(x612,f17(x613,x614))
% 60.17/60.30 [62]~P5(x621,x623)+P5(x621,x622)+~E(x622,f17(x623,x624))
% 60.17/60.30 [84]~P5(x841,x843)+~P5(x841,x842)+P6(x841,x842,x843)+P5(f15(x841,x842,x843),x843)
% 60.17/60.30 [85]~P5(x851,x853)+~P5(x851,x852)+P6(x851,x852,x853)+P5(f15(x851,x852,x853),x852)
% 60.17/60.30 [87]P5(f13(x871,x872,x873),x873)+P5(f13(x871,x872,x873),x872)+P5(f13(x871,x872,x873),x871)+E(x871,f17(x872,x873))
% 60.17/60.30 [81]~P5(x811,x812)+P2(x811,x812)+~P6(x814,x813,x812)+~P5(x811,x813)
% 60.17/60.30 [82]~P5(x821,x822)+P2(x821,x822)+~P6(x824,x822,x823)+~P5(x821,x823)
% 60.17/60.30 [65]~P5(x651,x654)+P5(x651,x652)+P5(x651,x653)+~E(x654,f17(x653,x652))
% 60.17/60.30 [90]~P5(x901,x903)+~P5(x901,x902)+P6(x901,x902,x903)+~P2(f15(x901,x902,x903),x903)+~P2(f15(x901,x902,x903),x902)
% 60.17/60.30 [83]~P3(x834)+~P2(x831,x832)+P6(x831,x832,x833)+~P6(x835,x832,x833)+~E(x834,f17(x832,x833))
% 60.17/60.30 [64]E(x643,x641)+~P2(x641,x644)+~P2(x643,x644)+E(x641,x642)+E(x643,x642)+~P2(x642,x644)
% 60.17/60.30 [80]P1(x802,x801)+~P1(x802,x803)+~P5(x804,x802)+~P2(x804,x803)+P1(x801,x802)+~P1(x801,x803)+~P5(x804,x801)
% 60.17/60.30 [86]P1(x862,x861)+P1(x862,x863)+P1(x863,x861)+P1(x863,x862)+~P1(x862,x864)+~P1(x863,x864)+~P2(x865,x862)+~P2(x865,x863)+P1(x861,x862)+P1(x861,x863)+~P1(x861,x864)+~P2(x865,x861)
% 60.17/60.30 %EqnAxiom
% 60.17/60.30 [1]E(x11,x11)
% 60.17/60.30 [2]E(x22,x21)+~E(x21,x22)
% 60.17/60.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.17/60.30 [4]~E(x41,x42)+E(f9(x41),f9(x42))
% 60.17/60.30 [5]~E(x51,x52)+E(f10(x51),f10(x52))
% 60.17/60.30 [6]~E(x61,x62)+E(f16(x61),f16(x62))
% 60.17/60.30 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73))
% 60.17/60.30 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82))
% 60.17/60.30 [9]~E(x91,x92)+E(f11(x91,x93),f11(x92,x93))
% 60.17/60.30 [10]~E(x101,x102)+E(f11(x103,x101),f11(x103,x102))
% 60.17/60.30 [11]~E(x111,x112)+E(f17(x111,x113),f17(x112,x113))
% 60.17/60.30 [12]~E(x121,x122)+E(f17(x123,x121),f17(x123,x122))
% 60.17/60.30 [13]~E(x131,x132)+E(f13(x131,x133,x134),f13(x132,x133,x134))
% 60.17/60.30 [14]~E(x141,x142)+E(f13(x143,x141,x144),f13(x143,x142,x144))
% 60.17/60.30 [15]~E(x151,x152)+E(f13(x153,x154,x151),f13(x153,x154,x152))
% 60.17/60.30 [16]~E(x161,x162)+E(f15(x161,x163,x164),f15(x162,x163,x164))
% 60.17/60.30 [17]~E(x171,x172)+E(f15(x173,x171,x174),f15(x173,x172,x174))
% 60.17/60.30 [18]~E(x181,x182)+E(f15(x183,x184,x181),f15(x183,x184,x182))
% 60.17/60.30 [19]~E(x191,x192)+E(f14(x191,x193),f14(x192,x193))
% 60.17/60.30 [20]~E(x201,x202)+E(f14(x203,x201),f14(x203,x202))
% 60.17/60.30 [21]~E(x211,x212)+E(f12(x211,x213),f12(x212,x213))
% 60.17/60.30 [22]~E(x221,x222)+E(f12(x223,x221),f12(x223,x222))
% 60.17/60.30 [23]~E(x231,x232)+E(f4(x231,x233),f4(x232,x233))
% 60.17/60.30 [24]~E(x241,x242)+E(f4(x243,x241),f4(x243,x242))
% 60.17/60.30 [25]~E(x251,x252)+E(f5(x251,x253),f5(x252,x253))
% 60.17/60.30 [26]~E(x261,x262)+E(f5(x263,x261),f5(x263,x262))
% 60.17/60.30 [27]~E(x271,x272)+E(f18(x271,x273),f18(x272,x273))
% 60.17/60.30 [28]~E(x281,x282)+E(f18(x283,x281),f18(x283,x282))
% 60.17/60.30 [29]~E(x291,x292)+E(f6(x291,x293),f6(x292,x293))
% 60.17/60.30 [30]~E(x301,x302)+E(f6(x303,x301),f6(x303,x302))
% 60.17/60.30 [31]P1(x312,x313)+~E(x311,x312)+~P1(x311,x313)
% 60.17/60.30 [32]P1(x323,x322)+~E(x321,x322)+~P1(x323,x321)
% 60.17/60.30 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 60.17/60.30 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 60.17/60.30 [35]P5(x352,x353)+~E(x351,x352)+~P5(x351,x353)
% 60.17/60.30 [36]P5(x363,x362)+~E(x361,x362)+~P5(x363,x361)
% 60.17/60.30 [37]P4(x372,x373)+~E(x371,x372)+~P4(x371,x373)
% 60.17/60.30 [38]P4(x383,x382)+~E(x381,x382)+~P4(x383,x381)
% 60.17/60.30 [39]P6(x392,x393,x394)+~E(x391,x392)+~P6(x391,x393,x394)
% 60.17/60.30 [40]P6(x403,x402,x404)+~E(x401,x402)+~P6(x403,x401,x404)
% 60.17/60.30 [41]P6(x413,x414,x412)+~E(x411,x412)+~P6(x413,x414,x411)
% 60.17/60.30 [42]~P3(x421)+P3(x422)+~E(x421,x422)
% 60.17/60.30 [43]~P7(x431)+P7(x432)+~E(x431,x432)
% 60.17/60.30
% 60.17/60.30 %-------------------------------------------
% 60.17/60.31 cnf(91,plain,
% 60.17/60.31 (~P5(x911,x912)+P5(x911,f17(x913,x912))),
% 60.17/60.31 inference(equality_inference,[],[61])).
% 60.17/60.31 cnf(92,plain,
% 60.17/60.31 (~P5(x921,x922)+P5(x921,f17(x922,x923))),
% 60.17/60.31 inference(equality_inference,[],[62])).
% 60.17/60.31 cnf(93,plain,
% 60.17/60.31 (~P5(x931,f17(x932,x933))+P5(x931,x933)+P5(x931,x932)),
% 60.17/60.31 inference(equality_inference,[],[65])).
% 60.17/60.31 cnf(94,plain,
% 60.17/60.31 (~P3(f17(x941,x942))+P6(x943,x941,x942)+~P2(x943,x941)+~P6(x944,x941,x942)),
% 60.17/60.31 inference(equality_inference,[],[83])).
% 60.17/60.31 cnf(101,plain,
% 60.17/60.31 (~P5(x1011,a1)+P5(x1011,a2)),
% 60.17/60.31 inference(scs_inference,[],[44,46,47,56,37,52,60])).
% 60.17/60.31 cnf(104,plain,
% 60.17/60.31 (P1(a1,x1041)+~E(a2,x1041)),
% 60.17/60.31 inference(scs_inference,[],[44,46,47,56,37,52,60,31,32])).
% 60.17/60.31 cnf(105,plain,
% 60.17/60.31 (~P5(x1051,f17(a1,a1))+P5(x1051,a2)),
% 60.17/60.31 inference(scs_inference,[],[44,46,47,56,37,52,60,31,32,93])).
% 60.17/60.31 cnf(111,plain,
% 60.17/60.31 (P4(f9(x1111),x1112)+~E(x1111,x1112)),
% 60.17/60.31 inference(scs_inference,[],[47,38])).
% 60.17/60.31 cnf(119,plain,
% 60.17/60.31 (P1(x1191,a2)+~E(a7,x1191)),
% 60.17/60.31 inference(scs_inference,[],[45,48,40,60,31])).
% 60.17/60.31 cnf(121,plain,
% 60.17/60.31 (~P5(x1211,f17(a7,a7))+P5(x1211,a2)),
% 60.17/60.31 inference(scs_inference,[],[45,48,40,60,31,41,93])).
% 60.17/60.31 cnf(131,plain,
% 60.17/60.31 (P2(x1311,a2)+~E(a8,x1311)),
% 60.17/60.31 inference(scs_inference,[],[46,33])).
% 60.17/60.31 cnf(136,plain,
% 60.17/60.31 (P6(x1361,a1,a7)+~E(a8,x1361)),
% 60.17/60.31 inference(scs_inference,[],[48,39])).
% 60.17/60.31 cnf(146,plain,
% 60.17/60.31 (P1(a1,a1)+~P5(a8,a1)),
% 60.17/60.31 inference(scs_inference,[],[44,46,94,80])).
% 60.17/60.31 cnf(156,plain,
% 60.17/60.31 (P2(f16(a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[46,50,51])).
% 60.17/60.31 cnf(159,plain,
% 60.17/60.31 (P2(x1591,a2)+~E(f16(a2),x1591)),
% 60.17/60.31 inference(scs_inference,[],[156,56,33])).
% 60.17/60.31 cnf(162,plain,
% 60.17/60.31 (P6(x1621,a2,a2)+~E(f16(a2),f15(x1621,a2,a2))+~P5(x1621,a2)),
% 60.17/60.31 inference(scs_inference,[],[46,156,56,33,90])).
% 60.17/60.31 cnf(184,plain,
% 60.17/60.31 (P2(f10(a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[46,53,49])).
% 60.17/60.31 cnf(190,plain,
% 60.17/60.31 (P6(x1901,a2,a2)+~E(f10(a2),f15(x1901,a2,a2))+~P5(x1901,a2)),
% 60.17/60.31 inference(scs_inference,[],[46,184,56,33,90])).
% 60.17/60.31 cnf(291,plain,
% 60.17/60.31 (P5(f9(x2911),f17(x2911,x2912))),
% 60.17/60.31 inference(scs_inference,[],[47,55,92])).
% 60.17/60.31 cnf(292,plain,
% 60.17/60.31 (P5(f9(x2921),f17(x2922,f17(x2921,x2923)))),
% 60.17/60.31 inference(scs_inference,[],[291,91])).
% 60.17/60.31 cnf(294,plain,
% 60.17/60.31 (P5(f9(x2941),f17(f17(x2941,x2942),x2943))),
% 60.17/60.31 inference(scs_inference,[],[291,91,92])).
% 60.17/60.31 cnf(312,plain,
% 60.17/60.31 (P5(f9(x3121),x3122)+~E(f17(x3121,x3123),x3122)),
% 60.17/60.31 inference(scs_inference,[],[291,36])).
% 60.17/60.31 cnf(321,plain,
% 60.17/60.31 (P5(x3211,f17(x3212,x3213))+~E(f9(x3212),x3211)),
% 60.17/60.31 inference(scs_inference,[],[291,35])).
% 60.17/60.31 cnf(322,plain,
% 60.17/60.31 (P1(x3221,f17(x3222,x3223))+~E(f9(x3222),f11(f17(x3222,x3223),x3221))),
% 60.17/60.31 inference(scs_inference,[],[291,35,70])).
% 60.17/60.31 cnf(387,plain,
% 60.17/60.31 (P1(a7,a7)+~P5(a8,a7)),
% 60.17/60.31 inference(scs_inference,[],[45,46,94,80])).
% 60.17/60.31 cnf(399,plain,
% 60.17/60.31 (P1(x3991,a7)+~E(a7,x3991)+~P5(a8,a7)),
% 60.17/60.31 inference(scs_inference,[],[387,31])).
% 60.17/60.31 cnf(416,plain,
% 60.17/60.31 (P5(a8,f17(x4161,a7))),
% 60.17/60.31 inference(scs_inference,[],[48,73,91])).
% 60.17/60.31 cnf(417,plain,
% 60.17/60.31 (P5(a8,f17(x4171,f17(x4172,a7)))),
% 60.17/60.31 inference(scs_inference,[],[416,91])).
% 60.17/60.31 cnf(421,plain,
% 60.17/60.31 (P5(a8,x4211)+~E(f17(x4212,a7),x4211)),
% 60.17/60.31 inference(scs_inference,[],[416,91,92,36])).
% 60.17/60.31 cnf(441,plain,
% 60.17/60.31 (P5(x4411,f17(x4412,a7))+~E(a8,x4411)),
% 60.17/60.31 inference(scs_inference,[],[416,35])).
% 60.17/60.31 cnf(442,plain,
% 60.17/60.31 (P1(x4421,f17(x4422,a7))+~E(a8,f11(f17(x4422,a7),x4421))),
% 60.17/60.31 inference(scs_inference,[],[416,35,70])).
% 60.17/60.31 cnf(473,plain,
% 60.17/60.31 (P1(a1,a1)),
% 60.17/60.31 inference(scs_inference,[],[48,74,146])).
% 60.17/60.31 cnf(474,plain,
% 60.17/60.31 (P1(a1,x4741)+~E(a1,x4741)),
% 60.17/60.31 inference(scs_inference,[],[473,32])).
% 60.17/60.31 cnf(479,plain,
% 60.17/60.31 (P1(x4791,a1)+~E(a1,x4791)),
% 60.17/60.31 inference(scs_inference,[],[473,31])).
% 60.17/60.31 cnf(650,plain,
% 60.17/60.31 (~E(f3(a2,f3(a2,a8)),f3(a2,a8))),
% 60.17/60.31 inference(scs_inference,[],[46,57,63])).
% 60.17/60.31 cnf(671,plain,
% 60.17/60.31 (P5(f9(f17(a1,a1)),a2)),
% 60.17/60.31 inference(scs_inference,[],[47,105,55])).
% 60.17/60.31 cnf(4025,plain,
% 60.17/60.31 (~P2(f9(x40251),x40251)),
% 60.17/60.31 inference(scs_inference,[],[47,56])).
% 60.17/60.31 cnf(4030,plain,
% 60.17/60.31 (~E(f16(a2),f9(a2))),
% 60.17/60.31 inference(scs_inference,[],[46,47,56,33,52,159])).
% 60.17/60.31 cnf(4041,plain,
% 60.17/60.31 (~P5(f9(f17(a1,a1)),f17(a1,a1))+~P6(x40411,a2,f17(a1,a1))),
% 60.17/60.31 inference(scs_inference,[],[671,4025,4030,52,81])).
% 60.17/60.31 cnf(4130,plain,
% 60.17/60.31 (~E(a8,f3(a2,a8))),
% 60.17/60.31 inference(scs_inference,[],[650,2,8])).
% 60.17/60.31 cnf(4137,plain,
% 60.17/60.31 (P5(a8,a2)),
% 60.17/60.31 inference(scs_inference,[],[46,54])).
% 60.17/60.31 cnf(4149,plain,
% 60.17/60.31 (P5(f16(a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[156,54])).
% 60.17/60.31 cnf(4160,plain,
% 60.17/60.31 (P5(f10(a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[184,54])).
% 60.17/60.31 cnf(4162,plain,
% 60.17/60.31 (P5(f16(a2),f17(a2,x41621))),
% 60.17/60.31 inference(scs_inference,[],[4149,184,54,92])).
% 60.17/60.31 cnf(4170,plain,
% 60.17/60.31 (P5(f10(a2),f17(a2,x41701))),
% 60.17/60.31 inference(scs_inference,[],[4160,92])).
% 60.17/60.31 cnf(4172,plain,
% 60.17/60.31 (P5(f10(a2),f17(x41721,a2))),
% 60.17/60.31 inference(scs_inference,[],[4160,92,91])).
% 60.17/60.31 cnf(4198,plain,
% 60.17/60.31 (P5(f10(a2),f17(f17(x41981,a2),x41982))),
% 60.17/60.31 inference(scs_inference,[],[4172,92])).
% 60.17/60.31 cnf(4716,plain,
% 60.17/60.31 (~P2(f3(a2,a8),a2)+E(a8,f3(a2,f3(a2,a8)))+~P2(f3(a2,f3(a2,a8)),a2)),
% 60.17/60.31 inference(scs_inference,[],[46,650,4130,64])).
% 60.17/60.31 cnf(5311,plain,
% 60.17/60.31 (P5(f9(a1),a2)),
% 60.17/60.31 inference(scs_inference,[],[291,184,57,63,105])).
% 60.17/60.31 cnf(5312,plain,
% 60.17/60.31 (P5(f9(x53121),f17(x53121,x53122))),
% 60.17/60.31 inference(rename_variables,[],[291])).
% 60.17/60.31 cnf(5314,plain,
% 60.17/60.31 (P5(f9(a7),a2)),
% 60.17/60.31 inference(scs_inference,[],[291,5312,184,57,63,105,121])).
% 60.17/60.31 cnf(5317,plain,
% 60.17/60.31 (E(f6(a1,a7),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[291,5312,184,48,57,63,105,121,75])).
% 60.17/60.31 cnf(5330,plain,
% 60.17/60.31 (P5(f9(x53301),x53301)),
% 60.17/60.31 inference(scs_inference,[],[291,5312,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55])).
% 60.17/60.31 cnf(5332,plain,
% 60.17/60.31 (P5(a8,a1)),
% 60.17/60.31 inference(scs_inference,[],[291,5312,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74])).
% 60.17/60.31 cnf(5337,plain,
% 60.17/60.31 (P5(a8,a7)),
% 60.17/60.31 inference(scs_inference,[],[291,5312,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73])).
% 60.17/60.31 cnf(5340,plain,
% 60.17/60.31 (E(f17(a1,a7),f6(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[291,5312,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2])).
% 60.17/60.31 cnf(5346,plain,
% 60.17/60.31 (P5(f9(x53461),f12(f9(x53461),x53461))),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66])).
% 60.17/60.31 cnf(5347,plain,
% 60.17/60.31 (~P2(f9(x53471),x53471)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5349,plain,
% 60.17/60.31 (P5(f9(x53491),f14(f9(x53491),x53491))),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67])).
% 60.17/60.31 cnf(5350,plain,
% 60.17/60.31 (~P2(f9(x53501),x53501)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5352,plain,
% 60.17/60.31 (P1(f12(f9(x53521),x53521),x53521)),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68])).
% 60.17/60.31 cnf(5353,plain,
% 60.17/60.31 (~P2(f9(x53531),x53531)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5355,plain,
% 60.17/60.31 (P1(f14(f9(x53551),x53551),x53551)),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69])).
% 60.17/60.31 cnf(5356,plain,
% 60.17/60.31 (~P2(f9(x53561),x53561)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5359,plain,
% 60.17/60.31 (~P2(f9(x53591),x53591)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5362,plain,
% 60.17/60.31 (~P2(f9(x53621),x53621)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5368,plain,
% 60.17/60.31 (~P2(f9(x53681),x53681)),
% 60.17/60.31 inference(rename_variables,[],[4025])).
% 60.17/60.31 cnf(5370,plain,
% 60.17/60.31 (~P6(x53701,a2,a2)),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,5356,5359,5362,5368,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69,78,79,37,32,33,3,81])).
% 60.17/60.31 cnf(5373,plain,
% 60.17/60.31 (P4(f9(f6(a1,a7)),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,5356,5359,5362,5368,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69,78,79,37,32,33,3,81,111])).
% 60.17/60.31 cnf(5374,plain,
% 60.17/60.31 (P5(a8,f6(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,5356,5359,5362,5368,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69,78,79,37,32,33,3,81,111,421])).
% 60.17/60.31 cnf(5390,plain,
% 60.17/60.31 (P5(f9(a1),f6(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,5356,5359,5362,5368,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69,78,79,37,32,33,3,81,111,421,7,9,10,19,20,21,22,23,24,25,26,27,28,29,30,312])).
% 60.17/60.31 cnf(5391,plain,
% 60.17/60.31 (~E(a7,x53911)+P1(x53911,a7)),
% 60.17/60.31 inference(scs_inference,[],[4198,416,291,5312,4025,5347,5350,5353,5356,5359,5362,5368,47,184,48,57,63,105,121,75,77,13,14,15,16,17,18,12,6,5,55,74,8,56,73,11,2,61,62,66,67,68,69,78,79,37,32,33,3,81,111,421,7,9,10,19,20,21,22,23,24,25,26,27,28,29,30,312,399])).
% 60.17/60.31 cnf(5409,plain,
% 60.17/60.31 (~P6(x54091,a2,f17(a1,a1))),
% 60.17/60.31 inference(scs_inference,[],[5330,4041])).
% 60.17/60.31 cnf(5426,plain,
% 60.17/60.31 (P5(f9(f6(a1,a7)),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5340,5373,156,57,63,111,55])).
% 60.17/60.31 cnf(5431,plain,
% 60.17/60.31 (P5(f9(x54311),x54311)),
% 60.17/60.31 inference(rename_variables,[],[5330])).
% 60.17/60.31 cnf(5432,plain,
% 60.17/60.31 (~P6(x54321,a2,a2)),
% 60.17/60.31 inference(rename_variables,[],[5370])).
% 60.17/60.31 cnf(5435,plain,
% 60.17/60.31 (P5(f9(x54351),x54351)),
% 60.17/60.31 inference(rename_variables,[],[5330])).
% 60.17/60.31 cnf(5436,plain,
% 60.17/60.31 (~P6(x54361,a2,a2)),
% 60.17/60.31 inference(rename_variables,[],[5370])).
% 60.17/60.31 cnf(5438,plain,
% 60.17/60.31 (~P2(f9(f6(a1,a7)),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5370,5432,5330,5431,5340,5373,4025,156,57,63,111,55,56,162,190,34])).
% 60.17/60.31 cnf(5440,plain,
% 60.17/60.31 (P5(f15(f9(a2),a2,a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[5370,5432,5436,5330,5431,5435,5340,5373,4025,156,57,63,111,55,56,162,190,34,85])).
% 60.17/60.31 cnf(5441,plain,
% 60.17/60.31 (P5(f9(x54411),x54411)),
% 60.17/60.31 inference(rename_variables,[],[5330])).
% 60.17/60.31 cnf(5442,plain,
% 60.17/60.31 (~P6(x54421,a2,a2)),
% 60.17/60.31 inference(rename_variables,[],[5370])).
% 60.17/60.31 cnf(5445,plain,
% 60.17/60.31 (~P6(x54451,a2,a2)),
% 60.17/60.31 inference(rename_variables,[],[5370])).
% 60.17/60.31 cnf(5447,plain,
% 60.17/60.31 (P2(a8,a7)),
% 60.17/60.31 inference(scs_inference,[],[5332,5370,5432,5436,5442,5337,5330,5431,5435,5340,5311,5373,4025,156,48,57,63,111,55,56,162,190,34,85,84,81])).
% 60.17/60.31 cnf(5449,plain,
% 60.17/60.31 (P2(a8,a1)),
% 60.17/60.31 inference(scs_inference,[],[5332,5370,5432,5436,5442,5337,5330,5431,5435,5340,5311,5373,4025,156,48,57,63,111,55,56,162,190,34,85,84,81,82])).
% 60.17/60.31 cnf(5451,plain,
% 60.17/60.31 (~P2(f15(f9(a2),a2,a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[5332,5370,5432,5436,5442,5445,5337,5330,5431,5435,5441,5340,5311,5373,4025,156,48,57,63,111,55,56,162,190,34,85,84,81,82,90])).
% 60.17/60.31 cnf(5463,plain,
% 60.17/60.31 (~E(f3(a1,a8),a8)),
% 60.17/60.31 inference(scs_inference,[],[5449,57])).
% 60.17/60.31 cnf(5465,plain,
% 60.17/60.31 (P2(f3(a1,a8),a1)),
% 60.17/60.31 inference(scs_inference,[],[5449,57,63])).
% 60.17/60.31 cnf(5469,plain,
% 60.17/60.31 (P4(f15(f9(a2),a2,a2),a2)),
% 60.17/60.31 inference(scs_inference,[],[5449,5440,5451,57,63,56,58])).
% 60.17/60.31 cnf(5474,plain,
% 60.17/60.31 (~P6(x54741,f17(a1,a7),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5449,5314,5426,5438,5440,5451,5370,57,63,56,58,85,82])).
% 60.17/60.31 cnf(5478,plain,
% 60.17/60.31 (~P6(x54781,f17(a1,a7),f6(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5449,5314,5426,5438,5440,5451,5317,5370,57,63,56,58,85,82,68,41])).
% 60.17/60.31 cnf(5479,plain,
% 60.17/60.31 (~P6(x54791,f6(a1,a7),f17(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5449,5314,5426,5438,5440,5451,5317,5370,57,63,56,58,85,82,68,41,40])).
% 60.17/60.31 cnf(5480,plain,
% 60.17/60.31 (P5(f15(f9(a1),f17(a1,a7),f6(a1,a7)),f6(a1,a7))),
% 60.17/60.31 inference(scs_inference,[],[5449,5314,5390,5426,5438,5440,5451,5317,5370,291,57,63,56,58,85,82,68,41,40,84])).
% 60.17/60.31 cnf(5485,plain,
% 60.17/60.31 (~E(f3(a7,a8),a8)),
% 60.17/60.31 inference(scs_inference,[],[5447,57])).
% 60.17/60.31 cnf(5487,plain,
% 60.17/60.31 (P2(f3(a7,a8),a7)),
% 60.17/60.31 inference(scs_inference,[],[5447,57,63])).
% 60.17/60.31 cnf(5489,plain,
% 60.17/60.31 (~P4(a8,a7)),
% 60.17/60.31 inference(scs_inference,[],[5447,57,63,56])).
% 60.17/60.32 cnf(5491,plain,
% 60.17/60.32 (~P6(x54911,f6(a1,a7),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5447,5478,5317,57,63,56,40])).
% 60.17/60.32 cnf(5492,plain,
% 60.17/60.32 (P5(f15(a8,f6(a1,a7),f6(a1,a7)),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5447,5478,5374,5317,57,63,56,40,85])).
% 60.17/60.32 cnf(5497,plain,
% 60.17/60.32 (~P5(f9(a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5447,5478,5374,5330,5370,5317,4149,4025,48,57,63,56,40,85,84,82])).
% 60.17/60.32 cnf(5501,plain,
% 60.17/60.32 (~P2(f9(a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5447,5478,5374,5330,5370,5317,4149,4025,48,57,63,56,40,85,84,82,54])).
% 60.17/60.32 cnf(5516,plain,
% 60.17/60.32 (~E(f3(a1,f3(a1,a8)),f3(a1,a8))),
% 60.17/60.32 inference(scs_inference,[],[5465,57])).
% 60.17/60.32 cnf(5518,plain,
% 60.17/60.32 (P2(f3(a1,f3(a1,a8)),a1)),
% 60.17/60.32 inference(scs_inference,[],[5465,57,63])).
% 60.17/60.32 cnf(5520,plain,
% 60.17/60.32 (~P4(f3(a1,a8),a1)),
% 60.17/60.32 inference(scs_inference,[],[5465,57,63,56])).
% 60.17/60.32 cnf(5523,plain,
% 60.17/60.32 (P5(f9(x55231),f14(f9(x55231),x55231))),
% 60.17/60.32 inference(rename_variables,[],[5349])).
% 60.17/60.32 cnf(5527,plain,
% 60.17/60.32 (P5(f15(f9(a1),f6(a1,a7),f6(a1,a7)),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5491,5497,5465,5349,5390,5330,57,63,56,60,35,85])).
% 60.17/60.32 cnf(5543,plain,
% 60.17/60.32 (P5(f15(f9(a1),a2,f17(a1,a1)),a1)),
% 60.17/60.32 inference(scs_inference,[],[5491,5497,5409,5465,5349,5523,5390,5330,5311,291,57,63,56,60,35,85,65,84,5391,105,69,93])).
% 60.17/60.32 cnf(5547,plain,
% 60.17/60.32 (~E(f3(a7,f3(a7,a8)),f3(a7,a8))),
% 60.17/60.32 inference(scs_inference,[],[5487,57])).
% 60.17/60.32 cnf(5549,plain,
% 60.17/60.32 (P2(f3(a7,f3(a7,a8)),a7)),
% 60.17/60.32 inference(scs_inference,[],[5487,57,63])).
% 60.17/60.32 cnf(5551,plain,
% 60.17/60.32 (~P4(f3(a7,a8),a7)),
% 60.17/60.32 inference(scs_inference,[],[5487,57,63,56])).
% 60.17/60.32 cnf(5554,plain,
% 60.17/60.32 (P5(f9(x55541),x55541)),
% 60.17/60.32 inference(rename_variables,[],[5330])).
% 60.17/60.32 cnf(5561,plain,
% 60.17/60.32 (~P1(a1,a7)),
% 60.17/60.32 inference(scs_inference,[],[5487,5492,5346,5497,5330,5554,5317,57,63,56,61,36,65,37,60])).
% 60.17/60.32 cnf(5564,plain,
% 60.17/60.32 (E(f3(a1,f3(a1,a8)),a8)),
% 60.17/60.32 inference(scs_inference,[],[5487,5463,5492,5516,5518,5346,5449,5465,5497,5330,5554,5317,57,63,56,61,36,65,37,60,64])).
% 60.17/60.32 cnf(5567,plain,
% 60.17/60.32 (~E(a1,a7)),
% 60.17/60.32 inference(scs_inference,[],[5487,5463,5492,5516,5518,5346,5449,5465,5497,5330,5554,5317,57,63,56,61,36,65,37,60,64,104,474])).
% 60.17/60.32 cnf(5568,plain,
% 60.17/60.32 (P5(f11(a7,a1),a1)),
% 60.17/60.32 inference(scs_inference,[],[5487,5463,5492,5516,5518,5346,5449,5465,5497,5330,5554,5317,57,63,56,61,36,65,37,60,64,104,474,59])).
% 60.17/60.32 cnf(5570,plain,
% 60.17/60.32 (P5(f11(a7,a1),a2)),
% 60.17/60.32 inference(scs_inference,[],[5487,5463,5492,5516,5518,5346,5449,5465,5497,5330,5554,5317,57,63,56,61,36,65,37,60,64,104,474,59,101])).
% 60.17/60.32 cnf(5572,plain,
% 60.17/60.32 (~P5(f11(a7,a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5487,5463,5492,5516,5518,5346,5449,5465,5497,5330,5554,5317,57,63,56,61,36,65,37,60,64,104,474,59,101,70])).
% 60.17/60.32 cnf(5581,plain,
% 60.17/60.32 (P2(f3(a2,a8),a2)),
% 60.17/60.32 inference(scs_inference,[],[46,63])).
% 60.17/60.32 cnf(5583,plain,
% 60.17/60.32 (~P2(f11(a7,a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5572,46,63,54])).
% 60.17/60.32 cnf(5585,plain,
% 60.17/60.32 (E(a8,f3(a1,f3(a1,a8)))),
% 60.17/60.32 inference(scs_inference,[],[5572,5564,46,63,54,2])).
% 60.17/60.32 cnf(5589,plain,
% 60.17/60.32 (~P6(x55891,a2,a2)),
% 60.17/60.32 inference(rename_variables,[],[5370])).
% 60.17/60.32 cnf(5595,plain,
% 60.17/60.32 (~P1(a2,a7)),
% 60.17/60.32 inference(scs_inference,[],[5572,5570,5549,5564,5370,46,63,54,2,56,162,61,62,60])).
% 60.17/60.32 cnf(5598,plain,
% 60.17/60.32 (P4(f9(x55981),x55981)),
% 60.17/60.32 inference(rename_variables,[],[47])).
% 60.17/60.32 cnf(5599,plain,
% 60.17/60.32 (~P5(f11(a7,a1),f17(a7,a7))),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5370,47,46,63,54,2,56,162,61,62,60,37,93])).
% 60.17/60.32 cnf(5606,plain,
% 60.17/60.32 (~P2(f9(a8),f3(a1,f3(a1,a8)))),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34])).
% 60.17/60.32 cnf(5613,plain,
% 60.17/60.32 (P6(f3(a1,f3(a1,a8)),a1,a7)),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136])).
% 60.17/60.32 cnf(5615,plain,
% 60.17/60.32 (P5(f11(a7,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136,441,59])).
% 60.17/60.32 cnf(5618,plain,
% 60.17/60.32 (~P5(f11(a7,a2),a7)),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136,441,59,321,70])).
% 60.17/60.32 cnf(5620,plain,
% 60.17/60.32 (P5(f3(a1,f3(a1,a8)),a1)),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136,441,59,321,70,74])).
% 60.17/60.32 cnf(5622,plain,
% 60.17/60.32 (P5(f9(a8),f3(a1,f3(a1,a8)))),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136,441,59,321,70,74,55])).
% 60.17/60.32 cnf(5624,plain,
% 60.17/60.32 (P5(f3(a1,f3(a1,a8)),a7)),
% 60.17/60.32 inference(scs_inference,[],[5572,5520,5570,5549,5564,5349,5501,5370,5589,5497,4025,47,5598,46,63,54,2,56,162,61,62,60,37,93,38,33,36,34,85,65,136,441,59,321,70,74,55,73])).
% 60.17/60.32 cnf(5636,plain,
% 60.17/60.32 (~P2(f3(a2,f3(a2,a8)),a2)+E(a8,f3(a2,f3(a2,a8)))),
% 60.17/60.32 inference(scs_inference,[],[5581,4716])).
% 60.17/60.32 cnf(5639,plain,
% 60.17/60.32 (P2(f3(a2,f3(a2,a8)),a2)),
% 60.17/60.32 inference(scs_inference,[],[5581,5620,101,63])).
% 60.17/60.32 cnf(5643,plain,
% 60.17/60.32 (~P4(f3(a2,a8),a2)),
% 60.17/60.32 inference(scs_inference,[],[5599,5581,5620,101,63,54,56])).
% 60.17/60.32 cnf(5646,plain,
% 60.17/60.32 (~P6(x56461,a2,a2)),
% 60.17/60.32 inference(rename_variables,[],[5370])).
% 60.17/60.32 cnf(5658,plain,
% 60.17/60.32 (P5(f15(f9(a1),f6(a1,a7),f6(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5595,5599,5581,5615,5527,5352,5585,5620,5624,5568,5489,5564,5447,5370,5317,101,63,54,56,190,61,62,60,37,31,33,36])).
% 60.17/60.32 cnf(5665,plain,
% 60.17/60.32 (P5(f9(x56651),x56651)),
% 60.17/60.32 inference(rename_variables,[],[5330])).
% 60.17/60.32 cnf(5671,plain,
% 60.17/60.32 (P5(f11(f17(a7,a7),a1),a1)),
% 60.17/60.32 inference(scs_inference,[],[5595,5599,5581,5615,5527,5352,5622,5606,5585,5620,5624,5568,5489,5564,5447,5370,5646,5330,5317,101,63,54,56,190,61,62,60,37,31,33,36,85,65,81,322,442,59])).
% 60.17/60.32 cnf(5674,plain,
% 60.17/60.32 (~P5(f11(f17(a7,a7),a1),f17(a7,a7))),
% 60.17/60.32 inference(scs_inference,[],[5595,5599,5581,5615,5527,5352,5622,5606,5585,5620,5624,5568,5489,5564,5447,5370,5646,5330,5317,101,63,54,56,190,61,62,60,37,31,33,36,85,65,81,322,442,59,474,70])).
% 60.17/60.32 cnf(5678,plain,
% 60.17/60.32 (~P6(x56781,a8,a8)),
% 60.17/60.32 inference(scs_inference,[],[5567,5595,5599,5581,5615,5527,5352,5622,5606,5585,5620,5624,5568,5489,5564,5447,5370,5646,5330,5317,101,63,54,56,190,61,62,60,37,31,33,36,85,65,81,322,442,59,474,70,76,41])).
% 60.17/60.32 cnf(5683,plain,
% 60.17/60.32 (~P5(f11(f17(a7,a7),a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5567,5595,5599,5581,5615,5527,5352,5622,5606,5585,5620,5624,5568,5489,5564,5447,5370,5646,5330,5665,5317,101,63,54,56,190,61,62,60,37,31,33,36,85,65,81,322,442,59,474,70,76,41,40,84,91])).
% 60.17/60.32 cnf(5689,plain,
% 60.17/60.32 (E(a8,f3(a2,f3(a2,a8)))),
% 60.17/60.32 inference(scs_inference,[],[5639,5636])).
% 60.17/60.32 cnf(5690,plain,
% 60.17/60.32 (P5(f11(f17(a7,a7),a1),a2)),
% 60.17/60.32 inference(scs_inference,[],[5671,101])).
% 60.17/60.32 cnf(5712,plain,
% 60.17/60.32 (~P5(f9(a7),a1)),
% 60.17/60.32 inference(scs_inference,[],[5618,5643,5674,5639,5671,5613,5543,5469,5479,5583,5549,5374,294,4160,5370,5330,5317,5497,416,4025,101,54,56,61,62,37,33,65,85,84,81])).
% 60.17/60.32 cnf(5716,plain,
% 60.17/60.32 (~E(a7,a2)),
% 60.17/60.32 inference(scs_inference,[],[5618,5643,5674,5639,5671,5613,5543,5469,5479,5595,5583,5549,5374,294,4160,5370,5330,5317,5497,416,4025,101,54,56,61,62,37,33,65,85,84,81,5391])).
% 60.17/60.32 cnf(5743,plain,
% 60.17/60.32 (P6(f3(a2,f3(a2,a8)),a1,a7)),
% 60.17/60.32 inference(scs_inference,[],[5689,136])).
% 60.17/60.32 cnf(5747,plain,
% 60.17/60.32 (P5(f3(a2,f3(a2,a8)),a1)),
% 60.17/60.32 inference(scs_inference,[],[5689,136,111,55,74])).
% 60.17/60.32 cnf(5749,plain,
% 60.17/60.32 (P5(f3(a2,f3(a2,a8)),a7)),
% 60.17/60.32 inference(scs_inference,[],[5689,136,111,55,74,73])).
% 60.17/60.32 cnf(5760,plain,
% 60.17/60.32 (~P1(f12(f9(a7),a7),a1)),
% 60.17/60.32 inference(scs_inference,[],[5712,5689,5690,5518,5674,5346,5314,136,111,55,74,73,54,2,56,61,62,60])).
% 60.17/60.32 cnf(5781,plain,
% 60.17/60.32 (~P2(f11(f17(a7,a7),a1),a7)),
% 60.17/60.32 inference(scs_inference,[],[5683,54])).
% 60.17/60.32 cnf(5788,plain,
% 60.17/60.32 (~E(a7,a1)),
% 60.17/60.32 inference(scs_inference,[],[5749,5747,5760,5683,5352,5690,5618,5674,5317,54,61,62,35,32])).
% 60.17/60.32 cnf(5801,plain,
% 60.17/60.32 (P1(a7,a1)),
% 60.17/60.32 inference(scs_inference,[],[44,5551,5749,5747,5760,5743,5683,5352,5639,5690,5451,5561,5349,5618,5581,5674,5712,5317,45,47,54,61,62,35,32,60,37,33,36,65,81,80])).
% 60.17/60.32 cnf(5818,plain,
% 60.17/60.32 (~P5(f11(f17(a7,a7),a2),a7)),
% 60.17/60.32 inference(scs_inference,[],[44,5716,5551,5749,5747,5760,5743,5683,5352,5639,5690,5451,5561,5615,5349,5618,5581,5674,5712,5370,5317,45,47,54,61,62,35,32,60,37,33,36,65,81,80,322,442,59,70,56,162,76,92])).
% 60.17/60.32 cnf(5848,plain,
% 60.17/60.32 (~P2(f11(f17(a7,a7),a2),a7)),
% 60.17/60.32 inference(scs_inference,[],[5818,54])).
% 60.17/60.32 cnf(5856,plain,
% 60.17/60.32 (~P2(f15(a8,f6(a1,a7),f6(a1,a7)),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5818,5491,5346,5568,5374,5314,5712,54,62,36,68,90])).
% 60.17/60.32 cnf(5868,plain,
% 60.17/60.32 (P4(f15(a8,f6(a1,a7),f6(a1,a7)),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5856,5492,5674,54,58])).
% 60.17/60.32 cnf(5890,plain,
% 60.17/60.32 (~P1(x58901,x58902)+P7(x58901)+E(x58901,x58902)),
% 60.17/60.32 inference(rename_variables,[],[52])).
% 60.17/60.32 cnf(5891,plain,
% 60.17/60.32 (~P5(f11(a7,a2),f17(a7,a7))),
% 60.17/60.32 inference(scs_inference,[],[5801,5788,5618,52,93])).
% 60.17/60.32 cnf(5897,plain,
% 60.17/60.32 (P2(f16(a7),a7)),
% 60.17/60.32 inference(scs_inference,[],[5868,5801,5788,5618,292,5497,5317,52,93,38,60,51])).
% 60.17/60.32 cnf(5905,plain,
% 60.17/60.32 (P2(f3(a7,f16(a7)),a7)),
% 60.17/60.32 inference(scs_inference,[],[5868,5801,5788,5618,292,5497,5317,52,93,38,60,51,5391,57,441,321,63])).
% 60.17/60.32 cnf(5909,plain,
% 60.17/60.32 (~P4(f16(a7),a7)),
% 60.17/60.32 inference(scs_inference,[],[5868,5801,5788,5618,292,5497,5317,52,93,38,60,51,5391,57,441,321,63,54,56])).
% 60.17/60.32 cnf(5914,plain,
% 60.17/60.32 (P7(a1)+E(a1,a2)),
% 60.17/60.32 inference(scs_inference,[],[44,5868,5801,5788,5618,4149,292,5370,5497,5317,52,93,38,60,51,5391,57,441,321,63,54,56,162,5890])).
% 60.17/60.32 cnf(5918,plain,
% 60.17/60.32 (~P4(f3(a7,f16(a7)),a7)),
% 60.17/60.32 inference(scs_inference,[],[5905,56])).
% 60.17/60.32 cnf(5935,plain,
% 60.17/60.32 (P5(f15(a8,a2,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[5848,5897,5891,4137,5330,5370,35,33,85])).
% 60.17/60.32 cnf(5949,plain,
% 60.17/60.32 (P5(f15(f15(a8,a2,a2),a2,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[5935,5918,5370,47,37,84])).
% 60.17/60.32 cnf(5950,plain,
% 60.17/60.32 (~P6(x59501,a2,a2)),
% 60.17/60.32 inference(rename_variables,[],[5370])).
% 60.17/60.32 cnf(5952,plain,
% 60.17/60.32 (~P2(f15(f15(a8,a2,a2),a2,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[5935,5918,5370,5950,47,37,84,90])).
% 60.17/60.32 cnf(5963,plain,
% 60.17/60.32 (~P5(f11(a7,a2),f17(f17(a7,a7),f17(a7,a7)))),
% 60.17/60.32 inference(scs_inference,[],[5891,5390,5497,62,93])).
% 60.17/60.32 cnf(5967,plain,
% 60.17/60.32 (P5(f15(f9(a1),f17(a1,a7),f6(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5480,5891,5615,5390,5497,5317,62,93,60,36])).
% 60.17/60.32 cnf(5968,plain,
% 60.17/60.32 (P5(f15(f9(a1),f17(a1,a7),f17(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5480,5474,5891,5615,5390,5497,291,5317,62,93,60,36,84])).
% 60.17/60.32 cnf(5992,plain,
% 60.17/60.32 (~P1(f17(f17(a7,x59921),x59922),a1)),
% 60.17/60.32 inference(scs_inference,[],[5355,5963,5949,5952,5595,294,5615,5330,5712,61,58,62,31,60])).
% 60.17/60.32 cnf(6034,plain,
% 60.17/60.32 (~P5(f11(a7,a1),f17(f17(a7,a7),f17(a7,a7)))),
% 60.17/60.32 inference(scs_inference,[],[5491,5568,5599,5390,90,69,93])).
% 60.17/60.32 cnf(6038,plain,
% 60.17/60.32 (~P2(f15(f9(a1),f6(a1,a7),f6(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[5491,5568,5599,5340,5390,90,69,93,62,34])).
% 60.17/60.32 cnf(6039,plain,
% 60.17/60.32 (~P1(a1,f17(f17(a7,a7),f17(a7,a7)))),
% 60.17/60.32 inference(scs_inference,[],[5491,5568,5599,5340,5390,90,69,93,62,34,60])).
% 60.17/60.32 cnf(6050,plain,
% 60.17/60.32 (P2(f16(a1),a1)+E(a1,a2)),
% 60.17/60.32 inference(scs_inference,[],[5914,51])).
% 60.17/60.32 cnf(6056,plain,
% 60.17/60.32 (~P1(a2,a1)),
% 60.17/60.32 inference(scs_inference,[],[6034,5314,5330,5712,54,62,60])).
% 60.17/60.32 cnf(6068,plain,
% 60.17/60.32 (P5(f11(a1,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[44,6034,6039,5992,5781,5897,5479,417,5332,5314,5390,5330,291,5712,46,54,62,60,33,85,80,119,59])).
% 60.17/60.32 cnf(6070,plain,
% 60.17/60.32 (~P5(f11(a1,a2),a1)),
% 60.17/60.32 inference(scs_inference,[],[44,6034,6039,5992,5781,5897,5479,417,5332,5314,5390,5330,291,5712,46,54,62,60,33,85,80,119,59,70])).
% 60.17/60.32 cnf(6080,plain,
% 60.17/60.32 (P2(f16(a1),a1)),
% 60.17/60.32 inference(scs_inference,[],[44,6034,6039,5992,5781,5897,5479,417,5332,4162,5314,5390,5330,291,5712,46,54,62,60,33,85,80,119,59,70,479,66,52,36,65,6050])).
% 60.17/60.32 cnf(6090,plain,
% 60.17/60.32 (P2(f3(a1,f16(a1)),a1)),
% 60.17/60.32 inference(scs_inference,[],[6080,57,63])).
% 60.17/60.32 cnf(6099,plain,
% 60.17/60.32 (~P6(x60991,a2,a2)),
% 60.17/60.32 inference(rename_variables,[],[5370])).
% 60.17/60.32 cnf(6106,plain,
% 60.17/60.32 (~P2(f15(f11(a1,a2),a2,a2),a2)),
% 60.17/60.32 inference(scs_inference,[],[6070,6068,6080,5967,5909,292,5370,6099,5497,47,57,63,54,56,37,85,93,65,90])).
% 60.17/60.32 cnf(6137,plain,
% 60.17/60.32 (~P5(f11(f17(a1,a1),a2),f17(a1,a1))),
% 60.17/60.32 inference(scs_inference,[],[5968,6106,6090,6070,5474,5620,6068,5340,416,5370,131,56,190,93,35,60,36,85,65,322,59,321,70])).
% 60.17/60.32 cnf(6159,plain,
% 60.17/60.32 (~P5(f11(f17(a1,a1),a2),a1)),
% 60.17/60.32 inference(scs_inference,[],[6137,92])).
% 60.17/60.32 cnf(6163,plain,
% 60.17/60.32 (P4(f15(f9(a1),f6(a1,a7),f6(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[6038,6137,5658,92,54,58])).
% 60.17/60.32 cnf(6169,plain,
% 60.17/60.32 (~P1(f6(a1,a7),a7)),
% 60.17/60.32 inference(scs_inference,[],[6038,6137,6056,5355,5658,6034,5568,5390,5497,92,54,58,61,31,60])).
% 60.17/60.32 cnf(6171,plain,
% 60.17/60.32 (P5(f11(a7,f6(a1,a7)),f6(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[6038,6137,6056,5355,5658,6034,5568,5390,5497,92,54,58,61,31,60,59])).
% 60.17/60.32 cnf(6173,plain,
% 60.17/60.32 (~P5(f11(a7,f6(a1,a7)),a7)),
% 60.17/60.32 inference(scs_inference,[],[6038,6137,6056,5355,5658,6034,5568,5390,5497,92,54,58,61,31,60,59,70])).
% 60.17/60.32 cnf(6189,plain,
% 60.17/60.32 (~P5(f11(a7,f6(a1,a7)),f17(a7,a7))),
% 60.17/60.32 inference(scs_inference,[],[6159,6173,54,93])).
% 60.17/60.32 cnf(6194,plain,
% 60.17/60.32 (~P1(f6(a1,a7),f17(a7,a7))),
% 60.17/60.32 inference(scs_inference,[],[6169,6171,6159,6173,5340,54,93,62,31,60])).
% 60.17/60.32 cnf(6198,plain,
% 60.17/60.32 (E(f3(a7,f3(a7,a8)),a8)),
% 60.17/60.32 inference(scs_inference,[],[6169,5547,6171,6159,6173,5485,5549,5487,5447,5340,54,93,62,31,60,65,64])).
% 60.17/60.32 cnf(6204,plain,
% 60.17/60.32 (P5(f11(a7,f17(a1,a7)),f17(a1,a7))),
% 60.17/60.32 inference(scs_inference,[],[6169,5547,6171,6159,6173,5485,5549,5487,5447,5340,54,93,62,31,60,65,64,442,322,59])).
% 60.17/60.32 cnf(6208,plain,
% 60.17/60.32 (~P5(f11(a7,f17(a1,a7)),a7)),
% 60.17/60.32 inference(scs_inference,[],[6169,5547,6171,6159,6173,5485,5549,5487,5447,5340,54,93,62,31,60,65,64,442,322,59,441,321,70])).
% 60.17/60.32 cnf(6218,plain,
% 60.17/60.32 (P6(f3(a7,f3(a7,a8)),a1,a7)),
% 60.17/60.32 inference(scs_inference,[],[6169,6163,5547,6171,6159,6173,5485,5549,5487,5447,4170,5340,4025,54,93,62,31,60,65,64,442,322,59,441,321,70,2,66,61,38,34,136])).
% 60.17/60.32 cnf(6220,plain,
% 60.17/60.32 (P5(f3(a7,f3(a7,a8)),a1)),
% 60.17/60.32 inference(scs_inference,[],[6169,6163,5547,6171,6159,6173,5485,5549,5487,5447,4170,5340,4025,54,93,62,31,60,65,64,442,322,59,441,321,70,2,66,61,38,34,136,111,74])).
% 60.17/60.32 cnf(6250,plain,
% 60.17/60.32 ($false),
% 60.17/60.32 inference(scs_inference,[],[6194,6189,6204,6198,6220,6208,6218,5801,5678,5340,5330,5317,5712,101,59,73,70,54,61,40,41,93,31,60]),
% 60.17/60.32 ['proof']).
% 60.17/60.32 % SZS output end Proof
% 60.17/60.32 % Total time :59.770000s
%------------------------------------------------------------------------------