%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO036-3 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : 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:26 EDT 2024
% Result : Unsatisfiable 0.65s 0.75s
% Output : CNFRefutation 0.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : GEO036-3 : TPTP v8.2.0. Released v1.0.0.
% 0.02/0.08 % 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 : Fri Jun 21 07:46:23 EDT 2024
% 0.08/0.27 % CPUTime :
% 0.13/0.45 start to proof:theBenchmark
% 0.65/0.74 %-------------------------------------------
% 0.65/0.74 % File :CSE---1.7
% 0.65/0.74 % Problem :theBenchmark
% 0.65/0.74 % Transform :cnf
% 0.65/0.74 % Format :tptp:raw
% 0.65/0.74 % Command :java -jar mcs_scs.jar %d %s
% 0.65/0.74
% 0.65/0.74 % Result :Theorem 0.260000s
% 0.65/0.74 % Output :CNFRefutation 0.260000s
% 0.65/0.74 %-------------------------------------------
% 0.65/0.74 %--------------------------------------------------------------------------
% 0.65/0.74 % File : GEO036-3 : TPTP v8.2.0. Released v1.0.0.
% 0.65/0.74 % Domain : Geometry
% 0.65/0.74 % Problem : The 3 axiom set points are distinct
% 0.65/0.74 % Version : [Qua89] axioms : Augmented.
% 0.65/0.74 % English :
% 0.65/0.74
% 0.65/0.74 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 0.65/0.74 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 0.65/0.74 % Source : [Qua89]
% 0.65/0.74 % Names : E2 [Qua89]
% 0.65/0.74
% 0.65/0.74 % Status : Unsatisfiable
% 0.65/0.74 % Rating : 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0, 0.15 v4.0.1, 0.27 v3.7.0, 0.00 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.07 v3.2.0, 0.08 v3.1.0, 0.00 v2.1.0, 0.11 v2.0.0
% 0.65/0.74 % Syntax : Number of clauses : 58 ( 17 unt; 14 nHn; 41 RR)
% 0.65/0.74 % Number of literals : 150 ( 36 equ; 78 neg)
% 0.65/0.74 % Maximal clause size : 8 ( 2 avg)
% 0.65/0.74 % Maximal term depth : 3 ( 1 avg)
% 0.65/0.74 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 0.65/0.74 % Number of functors : 9 ( 9 usr; 3 con; 0-6 aty)
% 0.65/0.74 % Number of variables : 200 ( 10 sgn)
% 0.65/0.74 % SPC : CNF_UNS_RFO_SEQ_NHN
% 0.65/0.74
% 0.65/0.74 % Comments :
% 0.65/0.74 %--------------------------------------------------------------------------
% 0.65/0.74 %----Include Tarski geometry axioms
% 0.65/0.74 include('Axioms/GEO002-0.ax').
% 0.65/0.74 %----Include definition of reflection
% 0.65/0.74 include('Axioms/GEO002-2.ax').
% 0.65/0.74 %--------------------------------------------------------------------------
% 0.65/0.74 cnf(d1,axiom,
% 0.65/0.75 equidistant(U,V,U,V) ).
% 0.65/0.75
% 0.65/0.75 cnf(d2,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(W,X,U,V) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d3,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(V,U,W,X) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d4_1,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(U,V,X,W) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d4_2,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(V,U,X,W) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d4_3,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(W,X,V,U) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d4_4,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(X,W,U,V) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d4_5,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | equidistant(X,W,V,U) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d5,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,W,X)
% 0.65/0.75 | ~ equidistant(W,X,Y,Z)
% 0.65/0.75 | equidistant(U,V,Y,Z) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(e1,axiom,
% 0.65/0.75 V = extension(U,V,W,W) ).
% 0.65/0.75
% 0.65/0.75 cnf(b0,axiom,
% 0.65/0.75 ( Y != extension(U,V,W,X)
% 0.65/0.75 | between(U,V,Y) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(r2_1,axiom,
% 0.65/0.75 between(U,V,reflection(U,V)) ).
% 0.65/0.75
% 0.65/0.75 cnf(r2_2,axiom,
% 0.65/0.75 equidistant(V,reflection(U,V),U,V) ).
% 0.65/0.75
% 0.65/0.75 cnf(r3_1,axiom,
% 0.65/0.75 ( U != V
% 0.65/0.75 | V = reflection(U,V) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(r3_2,axiom,
% 0.65/0.75 U = reflection(U,U) ).
% 0.65/0.75
% 0.65/0.75 cnf(r4,axiom,
% 0.65/0.75 ( V != reflection(U,V)
% 0.65/0.75 | U = V ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d7,axiom,
% 0.65/0.75 equidistant(U,U,V,V) ).
% 0.65/0.75
% 0.65/0.75 cnf(d8,axiom,
% 0.65/0.75 ( ~ equidistant(U,V,U1,V1)
% 0.65/0.75 | ~ equidistant(V,W,V1,W1)
% 0.65/0.75 | ~ between(U,V,W)
% 0.65/0.75 | ~ between(U1,V1,W1)
% 0.65/0.75 | equidistant(U,W,U1,W1) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d9,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(U,V,X)
% 0.65/0.75 | ~ equidistant(V,W,V,X)
% 0.65/0.75 | U = V
% 0.65/0.75 | W = X ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d10_1,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | U = V
% 0.65/0.75 | W = extension(U,V,V,W) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d10_2,axiom,
% 0.65/0.75 ( ~ equidistant(W,X,Y,Z)
% 0.65/0.75 | extension(U,V,W,X) = extension(U,V,Y,Z)
% 0.65/0.75 | U = V ) ).
% 0.65/0.75
% 0.65/0.75 cnf(d10_3,axiom,
% 0.65/0.75 ( extension(U,V,U,V) = extension(U,V,V,U)
% 0.65/0.75 | U = V ) ).
% 0.65/0.75
% 0.65/0.75 cnf(r5,axiom,
% 0.65/0.75 equidistant(V,U,V,reflection(reflection(U,V),V)) ).
% 0.65/0.75
% 0.65/0.75 cnf(r6,axiom,
% 0.65/0.75 U = reflection(reflection(U,V),V) ).
% 0.65/0.75
% 0.65/0.75 cnf(t3,axiom,
% 0.65/0.75 between(U,V,V) ).
% 0.65/0.75
% 0.65/0.75 cnf(b1,axiom,
% 0.65/0.75 ( ~ between(U,W,X)
% 0.65/0.75 | U != X
% 0.65/0.75 | between(V,W,X) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(t1,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | between(W,V,U) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(t2,axiom,
% 0.65/0.75 between(U,U,V) ).
% 0.65/0.75
% 0.65/0.75 cnf(b2,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(V,U,W)
% 0.65/0.75 | U = V ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b3,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(U,W,V)
% 0.65/0.75 | V = W ) ).
% 0.65/0.75
% 0.65/0.75 cnf(t6_1,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(V,U,W)
% 0.65/0.75 | U = V
% 0.65/0.75 | V = W ) ).
% 0.65/0.75
% 0.65/0.75 cnf(t6_2,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(U,W,V)
% 0.65/0.75 | U = V
% 0.65/0.75 | V = W ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b4,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(V,W,X)
% 0.65/0.75 | between(U,V,W) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b5,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(U,W,X)
% 0.65/0.75 | between(V,W,X) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b6,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(V,W,X)
% 0.65/0.75 | between(U,W,X)
% 0.65/0.75 | V = W ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b7,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(V,W,X)
% 0.65/0.75 | between(U,V,X)
% 0.65/0.75 | V = W ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b8,axiom,
% 0.65/0.75 ( ~ between(U,V,X)
% 0.65/0.75 | ~ between(V,W,X)
% 0.65/0.75 | between(U,W,X) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(b9,axiom,
% 0.65/0.75 ( ~ between(U,V,W)
% 0.65/0.75 | ~ between(U,W,X)
% 0.65/0.75 | between(U,V,X) ) ).
% 0.65/0.75
% 0.65/0.75 cnf(prove_axioms_points_are_distinct,negated_conjecture,
% 0.65/0.75 ( lower_dimension_point_1 = lower_dimension_point_2
% 0.65/0.75 | lower_dimension_point_2 = lower_dimension_point_3
% 0.65/0.75 | lower_dimension_point_1 = lower_dimension_point_3 ) ).
% 0.65/0.75
% 0.65/0.75 %--------------------------------------------------------------------------
% 0.65/0.75 %-------------------------------------------
% 0.65/0.75 % Proof found
% 0.65/0.75 % SZS status Theorem for theBenchmark
% 0.65/0.75 % SZS output start Proof
% 0.65/0.75 %ClaNum:91(EqnAxiom:35)
% 0.65/0.75 %VarNum:489(SingletonVarNum:183)
% 0.65/0.75 %MaxLitNum:8
% 0.65/0.75 %MaxfuncDepth:2
% 0.65/0.75 %SharedTerms:9
% 0.65/0.75 %goalClause: 52
% 0.65/0.75 [49]~P1(a5,a7,a8)
% 0.65/0.75 [50]~P1(a7,a8,a5)
% 0.65/0.75 [51]~P1(a8,a5,a7)
% 0.65/0.75 [36]P1(x361,x362,x362)
% 0.65/0.75 [37]P1(x371,x371,x372)
% 0.65/0.75 [38]P2(x381,x382,x382,x381)
% 0.65/0.75 [39]P2(x391,x392,x391,x392)
% 0.65/0.75 [40]P2(x401,x401,x402,x402)
% 0.65/0.75 [47]E(f1(f1(x471,x472,x471,x472),x472,f1(x471,x472,x471,x472),x472),x471)
% 0.65/0.75 [48]P2(x481,x482,x481,f1(f1(x482,x481,x482,x481),x481,f1(x482,x481,x482,x481),x481))
% 0.65/0.75 [41]E(f1(x411,x412,x413,x413),x412)
% 0.65/0.75 [43]P1(x431,x432,f1(x431,x432,x433,x434))
% 0.65/0.75 [45]P2(x451,f1(x452,x451,x453,x454),x453,x454)
% 0.65/0.75 [53]~P1(x531,x532,x531)+E(x531,x532)
% 0.65/0.75 [65]~E(x651,x652)+E(f1(x651,x652,x651,x652),x652)
% 0.65/0.75 [68]E(x681,x682)+~E(f1(x682,x681,x682,x681),x681)
% 0.65/0.75 [70]E(x701,x702)+E(f1(x701,x702,x701,x702),f1(x701,x702,x702,x701))
% 0.65/0.75 [54]~P1(x543,x542,x541)+P1(x541,x542,x543)
% 0.65/0.75 [67]~P2(x671,x672,x673,x673)+E(x671,x672)
% 0.65/0.75 [72]~P2(x724,x723,x722,x721)+P2(x721,x722,x723,x724)
% 0.65/0.75 [73]~P2(x733,x734,x732,x731)+P2(x731,x732,x733,x734)
% 0.65/0.75 [74]~P2(x744,x743,x741,x742)+P2(x741,x742,x743,x744)
% 0.65/0.75 [75]~P2(x753,x754,x751,x752)+P2(x751,x752,x753,x754)
% 0.65/0.75 [76]~P2(x762,x761,x764,x763)+P2(x761,x762,x763,x764)
% 0.65/0.75 [77]~P2(x772,x771,x773,x774)+P2(x771,x772,x773,x774)
% 0.65/0.75 [78]~P2(x781,x782,x784,x783)+P2(x781,x782,x783,x784)
% 0.65/0.75 [69]P1(x691,x692,x693)+~E(x693,f1(x691,x692,x694,x695))
% 0.65/0.75 [52]E(a5,a7)+E(a8,a5)+E(a8,a7)
% 0.65/0.75 [56]~P1(x563,x561,x562)+E(x561,x562)+~P1(x563,x562,x561)
% 0.65/0.75 [57]~P1(x571,x572,x573)+E(x571,x572)+~P1(x572,x571,x573)
% 0.65/0.75 [66]~P1(x661,x662,x663)+E(x661,x662)+E(f1(x661,x662,x662,x663),x663)
% 0.65/0.75 [55]~P1(x554,x552,x553)+P1(x551,x552,x553)+~E(x554,x553)
% 0.65/0.75 [60]~P1(x604,x601,x602)+P1(x601,x602,x603)+~P1(x604,x602,x603)
% 0.65/0.75 [61]~P1(x611,x614,x613)+P1(x611,x612,x613)+~P1(x614,x612,x613)
% 0.65/0.75 [62]~P1(x621,x622,x624)+P1(x621,x622,x623)+~P1(x621,x624,x623)
% 0.65/0.75 [85]~P1(x855,x851,x854)+~P1(x852,x853,x854)+P1(x851,f6(x852,x853,x854,x851,x855),x852)
% 0.65/0.75 [86]~P1(x865,x864,x863)+~P1(x862,x861,x863)+P1(x861,f6(x862,x861,x863,x864,x865),x865)
% 0.65/0.75 [80]~P2(x805,x806,x801,x802)+P2(x801,x802,x803,x804)+~P2(x805,x806,x803,x804)
% 0.65/0.75 [81]~P2(x811,x812,x815,x816)+P2(x811,x812,x813,x814)+~P2(x815,x816,x813,x814)
% 0.65/0.75 [79]~P2(x793,x794,x795,x796)+E(x791,x792)+E(f1(x791,x792,x793,x794),f1(x791,x792,x795,x796))
% 0.65/0.75 [63]~P1(x631,x632,x634)+~P1(x633,x631,x632)+E(x631,x632)+P1(x633,x632,x634)
% 0.65/0.75 [64]~P1(x641,x642,x644)+~P1(x643,x641,x642)+E(x641,x642)+P1(x643,x641,x644)
% 0.65/0.75 [87]~P1(x874,x872,x873)+~P1(x871,x872,x875)+E(x871,x872)+P1(x871,x873,f2(x871,x874,x872,x873,x875))
% 0.65/0.75 [88]~P1(x883,x882,x884)+~P1(x881,x882,x885)+E(x881,x882)+P1(x881,x883,f3(x881,x883,x882,x884,x885))
% 0.65/0.75 [89]~P1(x893,x892,x894)+~P1(x891,x892,x895)+E(x891,x892)+P1(f3(x891,x893,x892,x894,x895),x895,f2(x891,x893,x892,x894,x895))
% 0.65/0.75 [71]~P1(x713,x714,x712)+~P1(x713,x714,x711)+~P2(x714,x711,x714,x712)+E(x711,x712)+E(x713,x714)
% 0.65/0.75 [82]~P2(x826,x822,x825,x824)+~P2(x821,x826,x823,x825)+P2(x821,x822,x823,x824)+~P1(x823,x825,x824)+~P1(x821,x826,x822)
% 0.65/0.75 [90]~P1(x903,x904,x905)+~P1(x902,x903,x905)+~P2(x902,x905,x902,x906)+~P2(x902,x903,x902,x901)+P1(x901,f4(x902,x903,x901,x904,x905,x906),x906)
% 0.65/0.75 [91]~P1(x913,x912,x915)+~P1(x911,x913,x915)+~P2(x911,x915,x911,x916)+~P2(x911,x913,x911,x914)+P2(x911,x912,x911,f4(x911,x913,x914,x912,x915,x916))
% 0.65/0.75 [83]P1(x835,x833,x834)+P1(x834,x835,x833)+~P2(x833,x831,x833,x832)+~P2(x835,x831,x835,x832)+~P2(x834,x831,x834,x832)+E(x831,x832)+P1(x833,x834,x835)
% 0.65/0.75 [84]~P1(x841,x842,x843)+~P2(x842,x844,x848,x846)+~P2(x842,x843,x848,x845)+~P2(x841,x844,x847,x846)+~P2(x841,x842,x847,x848)+E(x841,x842)+P2(x843,x844,x845,x846)+~P1(x847,x848,x845)
% 0.65/0.75 %EqnAxiom
% 0.65/0.75 [1]E(x11,x11)
% 0.65/0.75 [2]E(x22,x21)+~E(x21,x22)
% 0.65/0.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.65/0.76 [4]~E(x41,x42)+E(f1(x41,x43,x44,x45),f1(x42,x43,x44,x45))
% 0.65/0.76 [5]~E(x51,x52)+E(f1(x53,x51,x54,x55),f1(x53,x52,x54,x55))
% 0.65/0.76 [6]~E(x61,x62)+E(f1(x63,x64,x61,x65),f1(x63,x64,x62,x65))
% 0.65/0.76 [7]~E(x71,x72)+E(f1(x73,x74,x75,x71),f1(x73,x74,x75,x72))
% 0.65/0.76 [8]~E(x81,x82)+E(f4(x81,x83,x84,x85,x86,x87),f4(x82,x83,x84,x85,x86,x87))
% 0.65/0.76 [9]~E(x91,x92)+E(f4(x93,x91,x94,x95,x96,x97),f4(x93,x92,x94,x95,x96,x97))
% 0.65/0.76 [10]~E(x101,x102)+E(f4(x103,x104,x101,x105,x106,x107),f4(x103,x104,x102,x105,x106,x107))
% 0.65/0.76 [11]~E(x111,x112)+E(f4(x113,x114,x115,x111,x116,x117),f4(x113,x114,x115,x112,x116,x117))
% 0.65/0.76 [12]~E(x121,x122)+E(f4(x123,x124,x125,x126,x121,x127),f4(x123,x124,x125,x126,x122,x127))
% 0.65/0.76 [13]~E(x131,x132)+E(f4(x133,x134,x135,x136,x137,x131),f4(x133,x134,x135,x136,x137,x132))
% 0.65/0.76 [14]~E(x141,x142)+E(f6(x141,x143,x144,x145,x146),f6(x142,x143,x144,x145,x146))
% 0.65/0.76 [15]~E(x151,x152)+E(f6(x153,x151,x154,x155,x156),f6(x153,x152,x154,x155,x156))
% 0.65/0.76 [16]~E(x161,x162)+E(f6(x163,x164,x161,x165,x166),f6(x163,x164,x162,x165,x166))
% 0.65/0.76 [17]~E(x171,x172)+E(f6(x173,x174,x175,x171,x176),f6(x173,x174,x175,x172,x176))
% 0.65/0.76 [18]~E(x181,x182)+E(f6(x183,x184,x185,x186,x181),f6(x183,x184,x185,x186,x182))
% 0.65/0.76 [19]~E(x191,x192)+E(f2(x191,x193,x194,x195,x196),f2(x192,x193,x194,x195,x196))
% 0.65/0.76 [20]~E(x201,x202)+E(f2(x203,x201,x204,x205,x206),f2(x203,x202,x204,x205,x206))
% 0.65/0.76 [21]~E(x211,x212)+E(f2(x213,x214,x211,x215,x216),f2(x213,x214,x212,x215,x216))
% 0.65/0.76 [22]~E(x221,x222)+E(f2(x223,x224,x225,x221,x226),f2(x223,x224,x225,x222,x226))
% 0.65/0.76 [23]~E(x231,x232)+E(f2(x233,x234,x235,x236,x231),f2(x233,x234,x235,x236,x232))
% 0.65/0.76 [24]~E(x241,x242)+E(f3(x241,x243,x244,x245,x246),f3(x242,x243,x244,x245,x246))
% 0.65/0.76 [25]~E(x251,x252)+E(f3(x253,x251,x254,x255,x256),f3(x253,x252,x254,x255,x256))
% 0.65/0.76 [26]~E(x261,x262)+E(f3(x263,x264,x261,x265,x266),f3(x263,x264,x262,x265,x266))
% 0.65/0.76 [27]~E(x271,x272)+E(f3(x273,x274,x275,x271,x276),f3(x273,x274,x275,x272,x276))
% 0.65/0.76 [28]~E(x281,x282)+E(f3(x283,x284,x285,x286,x281),f3(x283,x284,x285,x286,x282))
% 0.65/0.76 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 0.65/0.76 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 0.65/0.76 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 0.65/0.76 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 0.65/0.76 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 0.65/0.76 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 0.65/0.76 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 0.65/0.76
% 0.65/0.76 %-------------------------------------------
% 0.65/0.76 cnf(92,plain,
% 0.65/0.76 (~P1(x921,x922,x921)+P1(x923,x922,x921)),
% 0.65/0.76 inference(equality_inference,[],[55])).
% 0.65/0.76 cnf(95,plain,
% 0.65/0.76 (E(x951,f1(x952,x951,x953,x953))),
% 0.65/0.76 inference(scs_inference,[],[41,2])).
% 0.65/0.76 cnf(96,plain,
% 0.65/0.76 (~P1(a8,a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[41,49,2,54])).
% 0.65/0.76 cnf(98,plain,
% 0.65/0.76 (P1(x981,x982,f1(x983,f1(x981,x982,x984,x985),x986,x986))),
% 0.65/0.76 inference(scs_inference,[],[41,49,2,54,69])).
% 0.65/0.76 cnf(99,plain,
% 0.65/0.76 (E(f1(x991,x992,x993,x993),x992)),
% 0.65/0.76 inference(rename_variables,[],[41])).
% 0.65/0.76 cnf(101,plain,
% 0.65/0.76 (E(f1(x1011,f1(x1012,x1013,x1014,x1015),x1016,x1016),f1(x1017,f1(x1012,x1013,x1014,x1015),x1018,x1018))),
% 0.65/0.76 inference(scs_inference,[],[41,99,49,2,54,69,3])).
% 0.65/0.76 cnf(102,plain,
% 0.65/0.76 (E(f1(x1021,x1022,x1023,x1023),x1022)),
% 0.65/0.76 inference(rename_variables,[],[41])).
% 0.65/0.76 cnf(103,plain,
% 0.65/0.76 (~E(a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[37,41,99,49,2,54,69,3,29])).
% 0.65/0.76 cnf(104,plain,
% 0.65/0.76 (P1(x1041,x1041,x1042)),
% 0.65/0.76 inference(rename_variables,[],[37])).
% 0.65/0.76 cnf(105,plain,
% 0.65/0.76 (~E(a8,a7)),
% 0.65/0.76 inference(scs_inference,[],[36,37,41,99,49,2,54,69,3,29,30])).
% 0.65/0.76 cnf(106,plain,
% 0.65/0.76 (P1(x1061,x1062,x1062)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(107,plain,
% 0.65/0.76 (~E(a7,a8)),
% 0.65/0.76 inference(scs_inference,[],[36,106,37,41,99,49,2,54,69,3,29,30,31])).
% 0.65/0.76 cnf(108,plain,
% 0.65/0.76 (P1(x1081,x1082,x1082)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(109,plain,
% 0.65/0.76 (P2(x1091,x1092,x1092,f1(x1093,x1091,x1094,x1094))),
% 0.65/0.76 inference(scs_inference,[],[36,106,38,37,41,99,102,49,2,54,69,3,29,30,31,32])).
% 0.65/0.76 cnf(110,plain,
% 0.65/0.76 (P2(x1101,x1102,x1102,x1101)),
% 0.65/0.76 inference(rename_variables,[],[38])).
% 0.65/0.76 cnf(111,plain,
% 0.65/0.76 (P2(x1111,x1112,f1(x1113,x1112,x1114,x1114),x1111)),
% 0.65/0.76 inference(scs_inference,[],[36,106,38,110,37,41,99,102,49,2,54,69,3,29,30,31,32,33])).
% 0.65/0.76 cnf(112,plain,
% 0.65/0.76 (P2(x1121,x1122,x1122,x1121)),
% 0.65/0.76 inference(rename_variables,[],[38])).
% 0.65/0.76 cnf(113,plain,
% 0.65/0.76 (~P1(a5,a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,106,38,110,37,104,41,99,102,49,2,54,69,3,29,30,31,32,33,56])).
% 0.65/0.76 cnf(121,plain,
% 0.65/0.76 (P2(x1211,x1212,x1212,x1211)),
% 0.65/0.76 inference(rename_variables,[],[38])).
% 0.65/0.76 cnf(126,plain,
% 0.65/0.76 (P2(x1261,f1(x1262,x1263,x1264,x1264),x1263,x1261)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34])).
% 0.65/0.76 cnf(127,plain,
% 0.65/0.76 (P2(x1271,x1272,x1272,x1271)),
% 0.65/0.76 inference(rename_variables,[],[38])).
% 0.65/0.76 cnf(130,plain,
% 0.65/0.76 (~P1(a8,a7,a8)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,127,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34,35,53])).
% 0.65/0.76 cnf(132,plain,
% 0.65/0.76 (~P2(a7,a5,x1321,x1321)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,127,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34,35,53,67])).
% 0.65/0.76 cnf(134,plain,
% 0.65/0.76 (~P2(x1341,x1341,a5,a7)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,127,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34,35,53,67,72])).
% 0.65/0.76 cnf(136,plain,
% 0.65/0.76 (~P2(a5,a7,x1361,x1361)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,127,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34,35,53,67,72,73])).
% 0.65/0.76 cnf(138,plain,
% 0.65/0.76 (~P2(x1381,x1381,a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,106,108,38,110,112,121,127,37,104,45,41,99,102,48,49,2,54,69,3,29,30,31,32,33,56,57,80,81,34,35,53,67,72,73,74])).
% 0.65/0.76 cnf(148,plain,
% 0.65/0.76 (E(a5,a7)+E(a8,a5)),
% 0.65/0.76 inference(scs_inference,[],[105,52])).
% 0.65/0.76 cnf(155,plain,
% 0.65/0.76 (E(x1551,f1(f1(x1551,x1552,x1551,x1552),x1552,f1(x1551,x1552,x1551,x1552),x1552))),
% 0.65/0.76 inference(scs_inference,[],[105,47,67,72,74,2])).
% 0.65/0.76 cnf(164,plain,
% 0.65/0.76 (P2(x1641,x1642,x1641,f1(x1643,f1(x1644,x1642,x1645,x1645),x1646,x1646))),
% 0.65/0.76 inference(scs_inference,[],[109,111,101,105,107,47,50,67,72,74,2,53,69,73,54,81])).
% 0.65/0.76 cnf(165,plain,
% 0.65/0.76 (P2(x1651,x1652,x1652,f1(x1653,x1651,x1654,x1654))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(167,plain,
% 0.65/0.76 (P2(f1(x1671,x1672,x1673,x1673),x1674,x1674,f1(x1675,x1672,x1676,x1676))),
% 0.65/0.76 inference(scs_inference,[],[109,165,111,95,101,105,107,47,50,67,72,74,2,53,69,73,54,81,32])).
% 0.65/0.76 cnf(168,plain,
% 0.65/0.76 (P2(x1681,x1682,x1682,f1(x1683,x1681,x1684,x1684))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(170,plain,
% 0.65/0.76 (P2(x1701,x1702,f1(x1703,x1702,x1704,x1704),x1701)),
% 0.65/0.76 inference(rename_variables,[],[111])).
% 0.65/0.76 cnf(172,plain,
% 0.65/0.76 (P1(f1(x1721,x1722,x1723,x1723),x1724,f1(x1722,x1724,x1725,x1726))),
% 0.65/0.76 inference(scs_inference,[],[109,165,168,111,95,101,105,107,47,43,50,67,72,74,2,53,69,73,54,81,32,80,29])).
% 0.65/0.76 cnf(173,plain,
% 0.65/0.76 (P1(x1731,x1732,f1(x1731,x1732,x1733,x1734))),
% 0.65/0.76 inference(rename_variables,[],[43])).
% 0.65/0.76 cnf(174,plain,
% 0.65/0.76 (~E(a5,a7)),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,111,95,101,105,107,47,43,96,50,67,72,74,2,53,69,73,54,81,32,80,29,30])).
% 0.65/0.76 cnf(176,plain,
% 0.65/0.76 (~E(f1(a8,a7,x1761,x1762),a5)),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,111,95,101,105,107,47,43,173,96,50,67,72,74,2,53,69,73,54,81,32,80,29,30,31])).
% 0.65/0.76 cnf(178,plain,
% 0.65/0.76 (~E(f1(x1781,a7,x1782,x1782),a5)),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,111,95,101,105,107,47,43,173,96,50,132,67,72,74,2,53,69,73,54,81,32,80,29,30,31,33])).
% 0.65/0.76 cnf(179,plain,
% 0.65/0.76 (P2(x1791,x1792,x1792,f1(x1793,x1791,x1794,x1794))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(180,plain,
% 0.65/0.76 (~P2(a7,a5,x1801,x1801)),
% 0.65/0.76 inference(rename_variables,[],[132])).
% 0.65/0.76 cnf(181,plain,
% 0.65/0.76 (~E(a7,f1(f1(a5,x1811,a5,x1811),x1811,f1(a5,x1811,a5,x1811),x1811))),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,111,95,101,103,105,107,47,43,173,96,50,132,67,72,74,2,53,69,73,54,81,32,80,29,30,31,33,3])).
% 0.65/0.76 cnf(183,plain,
% 0.65/0.76 (~E(a5,f1(x1831,a7,x1832,x1832))),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,179,111,95,101,103,105,107,47,43,173,96,50,132,180,67,72,74,2,53,69,73,54,81,32,80,29,30,31,33,3,34])).
% 0.65/0.76 cnf(185,plain,
% 0.65/0.76 (~P2(a7,a5,x1851,x1851)),
% 0.65/0.76 inference(rename_variables,[],[132])).
% 0.65/0.76 cnf(189,plain,
% 0.65/0.76 (E(a8,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,179,111,170,95,101,103,105,107,47,43,173,96,50,132,180,185,67,72,74,2,53,69,73,54,81,32,80,29,30,31,33,3,34,35,148])).
% 0.65/0.76 cnf(190,plain,
% 0.65/0.76 (P1(x1901,x1902,f1(x1902,x1902,x1903,x1903))),
% 0.65/0.76 inference(scs_inference,[],[36,109,165,168,179,111,170,95,101,103,105,107,47,43,173,96,50,132,180,185,67,72,74,2,53,69,73,54,81,32,80,29,30,31,33,3,34,35,148,92])).
% 0.65/0.76 cnf(210,plain,
% 0.65/0.76 (P1(f1(x2101,x2102,x2101,x2102),x2102,x2101)),
% 0.65/0.76 inference(scs_inference,[],[155,181,67,74,53,69])).
% 0.65/0.76 cnf(212,plain,
% 0.65/0.76 (~P2(x2121,x2121,f1(f1(a5,x2122,a5,x2122),x2122,f1(a5,x2122,a5,x2122),x2122),a7)),
% 0.65/0.76 inference(scs_inference,[],[155,181,67,74,53,69,72])).
% 0.65/0.76 cnf(214,plain,
% 0.65/0.76 (~P1(a7,a5,a8)),
% 0.65/0.76 inference(scs_inference,[],[155,181,51,67,74,53,69,72,54])).
% 0.65/0.76 cnf(220,plain,
% 0.65/0.76 (P2(x2201,x2202,x2202,f1(x2203,x2201,x2204,x2204))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(222,plain,
% 0.65/0.76 (~P1(f1(f1(a5,x2221,a5,x2221),x2221,f1(a5,x2221,a5,x2221),x2221),a7,f1(f1(a5,x2221,a5,x2221),x2221,f1(a5,x2221,a5,x2221),x2221))),
% 0.65/0.76 inference(scs_inference,[],[189,167,155,181,109,51,37,67,74,53,69,72,54,73,2,81,56])).
% 0.65/0.76 cnf(225,plain,
% 0.65/0.76 (~P1(f1(x2251,a7,x2252,x2252),a5,f1(x2251,a7,x2252,x2252))),
% 0.65/0.76 inference(scs_inference,[],[36,189,167,155,181,109,51,178,37,67,74,53,69,72,54,73,2,81,56,57])).
% 0.65/0.76 cnf(226,plain,
% 0.65/0.76 (P1(x2261,x2262,x2262)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(228,plain,
% 0.65/0.76 (P2(a5,x2281,x2281,f1(x2282,a8,x2283,x2283))),
% 0.65/0.76 inference(scs_inference,[],[36,189,167,155,181,109,220,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32])).
% 0.65/0.76 cnf(229,plain,
% 0.65/0.76 (P2(x2291,x2292,x2292,f1(x2293,x2291,x2294,x2294))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(230,plain,
% 0.65/0.76 (P2(x2301,f1(x2302,x2303,x2304,x2304),x2301,f1(x2305,f1(x2306,x2303,x2307,x2307),x2308,x2308))),
% 0.65/0.76 inference(scs_inference,[],[36,189,167,155,181,109,220,229,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80])).
% 0.65/0.76 cnf(231,plain,
% 0.65/0.76 (P2(x2311,x2312,x2312,f1(x2313,x2311,x2314,x2314))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(233,plain,
% 0.65/0.76 (P1(x2331,a5,f1(x2332,f1(x2331,a8,x2333,x2334),x2335,x2335))),
% 0.65/0.76 inference(scs_inference,[],[36,189,167,155,181,109,220,229,98,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30])).
% 0.65/0.76 cnf(234,plain,
% 0.65/0.76 (P1(x2341,x2342,f1(x2343,f1(x2341,x2342,x2344,x2345),x2346,x2346))),
% 0.65/0.76 inference(rename_variables,[],[98])).
% 0.65/0.76 cnf(236,plain,
% 0.65/0.76 (P2(f1(x2361,x2362,x2363,x2363),x2364,x2364,f1(x2365,x2362,x2366,x2366))),
% 0.65/0.76 inference(rename_variables,[],[167])).
% 0.65/0.76 cnf(237,plain,
% 0.65/0.76 (~E(f1(x2371,f1(a5,a7,a5,a7),x2372,x2372),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7))),
% 0.65/0.76 inference(scs_inference,[],[36,189,167,172,155,181,109,220,229,98,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29])).
% 0.65/0.76 cnf(239,plain,
% 0.65/0.76 (~E(f1(a7,a7,x2391,x2391),a8)),
% 0.65/0.76 inference(scs_inference,[],[36,189,190,167,172,155,181,109,220,229,98,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31])).
% 0.65/0.76 cnf(240,plain,
% 0.65/0.76 (P1(x2401,x2402,f1(x2402,x2402,x2403,x2403))),
% 0.65/0.76 inference(rename_variables,[],[190])).
% 0.65/0.76 cnf(243,plain,
% 0.65/0.76 (~P2(x2431,x2431,a5,a7)),
% 0.65/0.76 inference(rename_variables,[],[134])).
% 0.65/0.76 cnf(244,plain,
% 0.65/0.76 (P2(f1(x2441,x2442,x2443,x2443),a5,a8,f1(x2444,x2442,x2445,x2445))),
% 0.65/0.76 inference(scs_inference,[],[36,189,190,167,236,172,155,181,109,220,229,231,134,98,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31,35,33])).
% 0.65/0.76 cnf(248,plain,
% 0.65/0.76 (P1(x2481,x2482,x2482)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(252,plain,
% 0.65/0.76 (E(a5,f1(x2521,f1(a7,a5,x2522,x2522),x2523,x2523))),
% 0.65/0.76 inference(scs_inference,[],[36,226,248,189,103,190,240,167,236,172,155,181,109,220,229,231,134,243,126,98,234,164,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31,35,33,82,71])).
% 0.65/0.76 cnf(261,plain,
% 0.65/0.76 (~P2(a5,a7,f1(a7,a7,x2611,x2611),a7)),
% 0.65/0.76 inference(scs_inference,[],[36,226,248,189,103,190,240,167,236,172,155,181,109,220,229,231,134,243,126,98,234,164,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31,35,33,82,71,77,78,75])).
% 0.65/0.76 cnf(263,plain,
% 0.65/0.76 (~P2(a7,f1(a7,a7,x2631,x2631),a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,226,248,189,103,190,240,167,236,172,155,181,109,220,229,231,134,243,126,98,234,164,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31,35,33,82,71,77,78,75,76])).
% 0.65/0.76 cnf(265,plain,
% 0.65/0.76 (E(a8,f1(x2651,f1(a7,a5,x2652,x2652),x2653,x2653))),
% 0.65/0.76 inference(scs_inference,[],[36,226,248,189,103,190,240,167,236,172,155,181,109,220,229,231,134,243,126,98,234,164,130,51,178,37,67,74,53,69,72,54,73,2,81,56,57,32,80,30,34,29,31,35,33,82,71,77,78,75,76,3])).
% 0.65/0.76 cnf(278,plain,
% 0.65/0.76 (~P2(f1(a8,a7,x2781,x2782),a5,x2783,x2783)),
% 0.65/0.76 inference(scs_inference,[],[176,67])).
% 0.65/0.76 cnf(296,plain,
% 0.65/0.76 (E(f1(x2961,f1(a7,a5,x2962,x2962),x2963,x2963),a8)),
% 0.65/0.76 inference(scs_inference,[],[176,265,239,261,263,67,78,77,75,76,72,69,53,73,2])).
% 0.65/0.76 cnf(301,plain,
% 0.65/0.76 (P2(a5,x3011,x3011,f1(x3012,a8,x3013,x3013))),
% 0.65/0.76 inference(rename_variables,[],[228])).
% 0.65/0.76 cnf(302,plain,
% 0.65/0.76 (P2(x3021,x3022,x3022,f1(x3023,x3021,x3024,x3024))),
% 0.65/0.76 inference(rename_variables,[],[109])).
% 0.65/0.76 cnf(308,plain,
% 0.65/0.76 (P1(x3081,x3082,x3082)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(310,plain,
% 0.65/0.76 (~E(f1(x3101,f1(a7,a8,x3102,x3103),x3104,x3104),a8)),
% 0.65/0.76 inference(scs_inference,[],[36,103,176,228,301,233,265,239,109,302,210,214,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31])).
% 0.65/0.76 cnf(311,plain,
% 0.65/0.76 (P1(x3111,a5,f1(x3112,f1(x3111,a8,x3113,x3114),x3115,x3115))),
% 0.65/0.76 inference(rename_variables,[],[233])).
% 0.65/0.76 cnf(313,plain,
% 0.65/0.76 (P2(a5,x3131,x3131,f1(x3132,a8,x3133,x3133))),
% 0.65/0.76 inference(rename_variables,[],[228])).
% 0.65/0.76 cnf(314,plain,
% 0.65/0.76 (~P2(a5,a7,x3141,x3141)),
% 0.65/0.76 inference(rename_variables,[],[136])).
% 0.65/0.76 cnf(315,plain,
% 0.65/0.76 (P2(f1(x3151,a5,x3152,x3152),x3153,x3153,f1(x3154,a8,x3155,x3155))),
% 0.65/0.76 inference(scs_inference,[],[36,103,95,176,228,301,313,233,265,239,109,302,136,210,214,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32])).
% 0.65/0.76 cnf(316,plain,
% 0.65/0.76 (E(x3161,f1(x3162,x3161,x3163,x3163))),
% 0.65/0.76 inference(rename_variables,[],[95])).
% 0.65/0.76 cnf(317,plain,
% 0.65/0.76 (P1(x3171,f1(x3172,a5,x3173,x3173),f1(x3174,f1(x3171,a8,x3175,x3176),x3177,x3177))),
% 0.65/0.76 inference(scs_inference,[],[36,103,95,316,176,228,301,313,233,311,265,239,109,302,136,210,214,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32,30])).
% 0.65/0.76 cnf(318,plain,
% 0.65/0.76 (E(x3181,f1(x3182,x3181,x3183,x3183))),
% 0.65/0.76 inference(rename_variables,[],[95])).
% 0.65/0.76 cnf(319,plain,
% 0.65/0.76 (~E(f1(x3191,f1(a5,a7,a5,a7),x3192,x3192),a5)),
% 0.65/0.76 inference(scs_inference,[],[36,103,95,316,176,155,237,228,301,313,233,311,265,239,109,302,136,210,214,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32,30,3])).
% 0.65/0.76 cnf(324,plain,
% 0.65/0.76 (~E(f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7))),
% 0.65/0.76 inference(scs_inference,[],[36,103,95,316,176,155,237,228,301,313,233,311,265,239,109,302,136,314,43,210,214,222,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32,30,3,34,29])).
% 0.65/0.76 cnf(327,plain,
% 0.65/0.76 (P2(f1(x3271,x3272,x3273,x3273),f1(x3274,a5,x3275,x3275),a8,f1(x3276,x3272,x3277,x3277))),
% 0.65/0.76 inference(scs_inference,[],[36,103,95,316,318,176,155,237,228,301,313,233,311,244,265,239,109,302,136,314,43,210,214,222,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32,30,3,34,29,33])).
% 0.65/0.76 cnf(329,plain,
% 0.65/0.76 (~P2(f1(x3291,x3291,a5,a5),x3291,a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,308,103,95,316,318,176,155,237,228,301,313,233,311,244,265,239,190,109,302,136,314,138,45,43,210,214,222,183,261,263,67,78,77,75,76,72,69,53,73,2,56,81,80,57,31,35,32,30,3,34,29,33,82])).
% 0.65/0.76 cnf(350,plain,
% 0.65/0.76 (~P2(f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),x3501,x3501)),
% 0.65/0.76 inference(scs_inference,[],[324,67])).
% 0.65/0.76 cnf(362,plain,
% 0.65/0.76 (~P1(f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),f1(a5,a7,a5,a7))),
% 0.65/0.76 inference(scs_inference,[],[324,329,67,76,75,78,77,72,53])).
% 0.65/0.76 cnf(364,plain,
% 0.65/0.76 (P1(x3641,f1(a7,a5,x3642,x3642),a5)),
% 0.65/0.76 inference(scs_inference,[],[324,252,329,67,76,75,78,77,72,53,69])).
% 0.65/0.76 cnf(366,plain,
% 0.65/0.76 (~P2(a7,a5,x3661,f1(x3661,x3661,a5,a5))),
% 0.65/0.76 inference(scs_inference,[],[324,252,329,67,76,75,78,77,72,53,69,73])).
% 0.65/0.76 cnf(368,plain,
% 0.65/0.76 (~P2(x3681,x3681,f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7))),
% 0.65/0.76 inference(scs_inference,[],[324,252,329,67,76,75,78,77,72,53,69,73,74])).
% 0.65/0.76 cnf(370,plain,
% 0.65/0.76 (E(f1(x3701,f1(a7,a5,x3702,x3702),x3703,x3703),a5)),
% 0.65/0.76 inference(scs_inference,[],[324,252,329,67,76,75,78,77,72,53,69,73,74,2])).
% 0.65/0.76 cnf(371,plain,
% 0.65/0.76 (~P1(f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7))),
% 0.65/0.76 inference(scs_inference,[],[324,37,252,329,67,76,75,78,77,72,53,69,73,74,2,56])).
% 0.65/0.76 cnf(375,plain,
% 0.65/0.76 (P2(f1(x3751,a5,x3752,x3752),x3753,x3753,f1(x3754,a8,x3755,x3755))),
% 0.65/0.76 inference(rename_variables,[],[315])).
% 0.65/0.76 cnf(381,plain,
% 0.65/0.76 (~P1(f1(x3811,f1(a5,a7,a5,a7),x3812,x3812),a5,f1(x3811,f1(a5,a7,a5,a7),x3812,x3812))),
% 0.65/0.76 inference(scs_inference,[],[36,324,315,375,319,228,111,37,252,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57])).
% 0.65/0.76 cnf(382,plain,
% 0.65/0.76 (P1(x3821,x3822,x3822)),
% 0.65/0.76 inference(rename_variables,[],[36])).
% 0.65/0.76 cnf(384,plain,
% 0.65/0.76 (P2(f1(x3841,f1(x3842,a5,x3843,x3843),x3844,x3844),x3845,x3845,f1(x3846,a8,x3847,x3847))),
% 0.65/0.76 inference(scs_inference,[],[36,95,324,315,375,319,228,111,37,252,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32])).
% 0.65/0.76 cnf(385,plain,
% 0.65/0.76 (E(x3851,f1(x3852,x3851,x3853,x3853))),
% 0.65/0.76 inference(rename_variables,[],[95])).
% 0.65/0.76 cnf(392,plain,
% 0.65/0.76 (P2(f1(x3921,a5,x3922,x3922),x3923,x3923,f1(x3924,a8,x3925,x3925))),
% 0.65/0.76 inference(rename_variables,[],[315])).
% 0.65/0.76 cnf(393,plain,
% 0.65/0.76 (~E(f1(a7,a5,x3931,x3932),f1(x3933,a7,x3934,x3934))),
% 0.65/0.76 inference(scs_inference,[],[36,189,172,95,385,324,317,315,375,319,228,244,111,37,252,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31])).
% 0.65/0.76 cnf(394,plain,
% 0.65/0.76 (P1(f1(x3941,x3942,x3943,x3943),x3944,f1(x3942,x3944,x3945,x3946))),
% 0.65/0.76 inference(rename_variables,[],[172])).
% 0.65/0.76 cnf(395,plain,
% 0.65/0.76 (P1(a5,f1(x3951,a5,x3952,x3952),f1(x3953,f1(a8,a8,x3954,x3955),x3956,x3956))),
% 0.65/0.76 inference(scs_inference,[],[36,189,172,95,385,324,317,315,375,319,228,244,111,37,252,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31,29])).
% 0.65/0.76 cnf(397,plain,
% 0.65/0.76 (~E(f1(a5,a7,a5,a7),a5)),
% 0.65/0.76 inference(scs_inference,[],[36,189,172,95,385,155,324,317,315,375,319,228,244,111,37,252,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31,29,3])).
% 0.65/0.76 cnf(399,plain,
% 0.65/0.76 (P2(f1(x3991,a5,x3992,x3992),a5,a8,f1(x3993,a8,x3994,x3994))),
% 0.65/0.76 inference(scs_inference,[],[36,189,172,95,385,155,324,317,315,375,392,319,228,244,111,37,252,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31,29,3,33])).
% 0.65/0.76 cnf(403,plain,
% 0.65/0.76 (P1(x4031,x4032,f1(x4032,x4032,x4033,x4033))),
% 0.65/0.76 inference(rename_variables,[],[190])).
% 0.65/0.76 cnf(405,plain,
% 0.65/0.76 (~P2(f1(a5,a5,x4051,x4051),a5,a7,a5)),
% 0.65/0.76 inference(scs_inference,[],[36,382,189,172,394,174,95,385,155,324,317,315,375,392,319,228,244,190,111,126,138,37,252,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31,29,3,33,64,82])).
% 0.65/0.76 cnf(411,plain,
% 0.65/0.76 (E(f1(a7,a7,x4111,x4111),f1(x4112,f1(a8,a7,x4113,x4113),x4114,x4114))),
% 0.65/0.76 inference(scs_inference,[],[36,382,189,105,172,394,174,95,385,155,324,317,315,375,392,319,228,244,190,403,111,126,138,98,37,252,230,278,225,329,67,76,75,78,77,72,53,69,73,74,2,56,81,80,57,32,30,35,34,31,29,3,33,64,82,71])).
% 0.65/0.76 cnf(426,plain,
% 0.65/0.76 (~P2(f1(a7,a5,x4261,x4262),f1(x4263,a7,x4264,x4264),x4265,x4265)),
% 0.65/0.76 inference(scs_inference,[],[393,67])).
% 0.65/0.76 cnf(430,plain,
% 0.65/0.76 (~P2(x4301,x4301,f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),f1(a5,a7,a5,a7))),
% 0.65/0.76 inference(scs_inference,[],[393,350,368,67,77,78])).
% 0.65/0.76 cnf(440,plain,
% 0.65/0.76 (~P1(f1(a7,a5,x4401,x4402),f1(x4403,a7,x4404,x4404),f1(a7,a5,x4401,x4402))),
% 0.65/0.76 inference(scs_inference,[],[393,350,368,411,405,67,77,78,75,72,69,76,53])).
% 0.65/0.76 cnf(448,plain,
% 0.65/0.77 (~E(f1(a7,a5,x4481,x4482),f1(x4483,a7,x4484,x4484))),
% 0.65/0.77 inference(rename_variables,[],[393])).
% 0.65/0.77 cnf(451,plain,
% 0.65/0.77 (P2(f1(x4511,f1(x4512,a5,x4513,x4513),x4514,x4514),x4515,x4515,f1(x4516,a8,x4517,x4517))),
% 0.65/0.77 inference(rename_variables,[],[384])).
% 0.65/0.77 cnf(452,plain,
% 0.65/0.77 (P2(f1(x4521,a5,x4522,x4522),x4523,x4523,f1(x4524,a8,x4525,x4525))),
% 0.65/0.77 inference(rename_variables,[],[315])).
% 0.65/0.77 cnf(454,plain,
% 0.65/0.77 (~P1(f1(x4541,a7,x4542,x4542),f1(a7,a5,x4543,x4544),f1(x4541,a7,x4542,x4542))),
% 0.65/0.77 inference(scs_inference,[],[103,384,393,448,315,37,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56])).
% 0.65/0.77 cnf(460,plain,
% 0.65/0.77 (~P1(f1(a5,a7,a5,a7),a5,f1(a5,a7,a5,a7))),
% 0.65/0.77 inference(scs_inference,[],[36,103,384,393,448,397,399,315,452,37,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57])).
% 0.65/0.77 cnf(461,plain,
% 0.65/0.77 (P1(x4611,x4612,x4612)),
% 0.65/0.77 inference(rename_variables,[],[36])).
% 0.65/0.77 cnf(464,plain,
% 0.65/0.77 (E(x4641,f1(x4642,x4641,x4643,x4643))),
% 0.65/0.77 inference(rename_variables,[],[95])).
% 0.65/0.77 cnf(465,plain,
% 0.65/0.77 (~E(x4651,f1(x4652,x4651,a5,a7))),
% 0.65/0.77 inference(scs_inference,[],[36,103,95,384,393,448,395,397,399,315,452,45,134,37,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32])).
% 0.65/0.77 cnf(471,plain,
% 0.65/0.77 (P1(x4711,x4712,x4712)),
% 0.65/0.77 inference(rename_variables,[],[36])).
% 0.65/0.77 cnf(472,plain,
% 0.65/0.77 (P1(a5,x4721,f1(x4722,f1(a8,x4721,x4723,x4724),x4725,x4725))),
% 0.65/0.77 inference(scs_inference,[],[36,461,189,103,95,464,384,451,393,448,395,397,399,315,452,45,134,98,37,362,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29])).
% 0.65/0.77 cnf(473,plain,
% 0.65/0.77 (P1(x4731,x4732,f1(x4733,f1(x4731,x4732,x4734,x4735),x4736,x4736))),
% 0.65/0.77 inference(rename_variables,[],[98])).
% 0.65/0.77 cnf(475,plain,
% 0.65/0.77 (P2(f1(x4751,f1(x4752,a5,x4753,x4753),x4754,x4754),x4755,x4755,f1(x4756,a8,x4757,x4757))),
% 0.65/0.77 inference(rename_variables,[],[384])).
% 0.65/0.77 cnf(476,plain,
% 0.65/0.77 (~E(f1(a8,a7,x4761,x4762),a8)),
% 0.65/0.77 inference(scs_inference,[],[36,461,189,176,103,95,464,384,451,393,448,395,397,399,315,452,45,134,98,37,362,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29,34,3])).
% 0.65/0.77 cnf(477,plain,
% 0.65/0.77 (P2(f1(x4771,f1(x4772,a5,x4773,x4773),x4774,x4774),a5,a8,f1(x4775,a8,x4776,x4776))),
% 0.65/0.77 inference(scs_inference,[],[36,461,189,176,103,95,464,384,451,475,393,448,395,397,399,315,452,45,134,98,37,362,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29,34,3,33])).
% 0.65/0.77 cnf(479,plain,
% 0.65/0.77 (~P1(a7,f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),f1(a5,a7,a5,a7))),
% 0.65/0.77 inference(scs_inference,[],[36,461,189,176,103,95,464,384,451,475,393,448,395,397,399,315,452,181,43,45,134,98,37,362,350,368,411,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29,34,3,33,63])).
% 0.65/0.77 cnf(485,plain,
% 0.65/0.77 (P1(x4851,x4852,f1(x4853,f1(x4851,x4852,x4854,x4855),x4856,x4856))),
% 0.65/0.77 inference(rename_variables,[],[98])).
% 0.65/0.77 cnf(487,plain,
% 0.65/0.77 (~P2(f1(a7,a7,x4871,x4871),a7,f1(f1(a5,x4872,a5,x4872),x4872,f1(a5,x4872,a5,x4872),x4872),a7)),
% 0.65/0.77 inference(scs_inference,[],[36,461,471,189,176,103,172,174,95,464,384,451,475,393,448,395,397,399,315,452,181,43,126,45,134,98,473,37,362,350,368,411,212,381,405,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29,34,3,33,63,64,82])).
% 0.65/0.77 cnf(489,plain,
% 0.65/0.77 (P1(x4891,x4892,x4892)),
% 0.65/0.77 inference(rename_variables,[],[36])).
% 0.65/0.77 cnf(493,plain,
% 0.65/0.77 (E(a7,f1(x4931,f1(a8,a7,x4932,x4932),x4933,x4933))),
% 0.65/0.77 inference(scs_inference,[],[36,461,471,489,189,105,176,103,172,174,95,464,384,451,475,393,448,395,397,399,315,452,181,43,126,45,134,98,473,485,37,362,350,368,411,212,381,405,164,67,77,78,75,72,69,76,53,73,74,2,66,81,56,80,57,30,32,35,31,29,34,3,33,63,64,82,71])).
% 0.65/0.77 cnf(510,plain,
% 0.65/0.77 (~P2(x5101,f1(x5102,x5101,a5,a7),x5103,x5103)),
% 0.65/0.77 inference(scs_inference,[],[465,67])).
% 0.65/0.77 cnf(516,plain,
% 0.65/0.77 (~P1(x5161,f1(x5162,x5161,a5,a7),x5161)),
% 0.65/0.77 inference(scs_inference,[],[465,426,493,67,72,69,53])).
% 0.65/0.77 cnf(534,plain,
% 0.65/0.77 (P2(x5341,x5342,x5342,f1(x5343,x5341,x5344,x5344))),
% 0.65/0.77 inference(rename_variables,[],[109])).
% 0.65/0.77 cnf(537,plain,
% 0.65/0.77 (P1(f1(x5371,x5372,x5371,x5372),x5372,x5371)),
% 0.65/0.77 inference(rename_variables,[],[210])).
% 0.65/0.77 cnf(540,plain,
% 0.65/0.77 (P2(f1(x5401,a5,x5402,x5402),x5403,x5403,f1(x5404,a8,x5405,x5405))),
% 0.65/0.77 inference(rename_variables,[],[315])).
% 0.65/0.77 cnf(543,plain,
% 0.65/0.77 (~P1(f1(x5431,f1(a7,a8,x5432,x5433),x5434,x5434),a8,f1(x5431,f1(a7,a8,x5432,x5433),x5434,x5434))),
% 0.65/0.77 inference(scs_inference,[],[36,105,228,109,534,465,310,315,210,426,479,493,487,67,72,69,53,75,78,76,77,73,74,54,2,81,56,80,57])).
% 0.65/0.77 cnf(544,plain,
% 0.65/0.77 (P1(x5441,x5442,x5442)),
% 0.65/0.77 inference(rename_variables,[],[36])).
% 0.65/0.77 cnf(546,plain,
% 0.65/0.77 (~E(a7,f1(a7,a5,x5461,x5462))),
% 0.65/0.77 inference(scs_inference,[],[36,105,190,228,109,534,465,310,315,210,426,454,479,493,487,67,72,69,53,75,78,76,77,73,74,54,2,81,56,80,57,30])).
% 0.65/0.77 cnf(547,plain,
% 0.65/0.77 (P1(x5471,x5472,f1(x5472,x5472,x5473,x5473))),
% 0.65/0.77 inference(rename_variables,[],[190])).
% 0.65/0.77 cnf(548,plain,
% 0.65/0.77 (~P1(f1(x5481,a7,x5482,x5482),f1(a7,a5,x5483,x5484),f1(x5481,a7,x5482,x5482))),
% 0.65/0.77 inference(rename_variables,[],[454])).
% 0.65/0.77 cnf(552,plain,
% 0.65/0.77 (~E(f1(a7,f1(a7,a5,x5521,x5522),x5523,x5524),f1(x5525,a7,x5526,x5526))),
% 0.65/0.77 inference(scs_inference,[],[36,105,190,172,228,109,534,465,310,477,315,210,426,454,548,479,493,366,487,67,72,69,53,75,78,76,77,73,74,54,2,81,56,80,57,30,32,31])).
% 0.65/0.77 cnf(553,plain,
% 0.65/0.77 (P1(f1(x5531,x5532,x5533,x5533),x5534,f1(x5532,x5534,x5535,x5536))),
% 0.65/0.77 inference(rename_variables,[],[172])).
% 0.65/0.77 cnf(556,plain,
% 0.65/0.77 (~P2(f1(a7,a5,x5561,x5562),f1(x5563,a7,x5564,x5564),x5565,x5565)),
% 0.65/0.77 inference(rename_variables,[],[426])).
% 0.65/0.77 cnf(568,plain,
% 0.65/0.77 (~P1(f1(a7,a5,x5681,x5682),f1(a8,a7,x5683,x5683),a5)),
% 0.65/0.77 inference(scs_inference,[],[36,105,176,103,107,190,172,553,296,228,109,534,465,310,477,327,315,540,167,210,537,98,426,556,454,548,440,460,479,493,366,487,67,72,69,53,75,78,76,77,73,74,54,2,81,56,80,57,30,32,31,35,3,29,34,33,63,64])).
% 0.65/0.77 cnf(573,plain,
% 0.65/0.77 (~P2(f1(f1(a5,a7,a5,a7),f1(a5,a7,a5,a7),x5731,x5731),f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7),f1(a5,a7,a5,a7))),
% 0.65/0.77 inference(scs_inference,[],[36,544,105,176,103,107,190,547,172,553,296,228,109,534,465,310,477,327,315,540,167,126,210,537,98,430,426,556,454,548,440,460,479,493,366,487,67,72,69,53,75,78,76,77,73,74,54,2,81,56,80,57,30,32,31,35,3,29,34,33,63,64,82])).
% 0.65/0.77 cnf(591,plain,
% 0.65/0.77 (~P2(f1(a8,a7,x5911,x5912),a8,x5913,x5913)),
% 0.65/0.77 inference(scs_inference,[],[476,67])).
% 0.65/0.77 cnf(612,plain,
% 0.65/0.77 (~E(f1(a7,f1(a7,a5,x6121,x6122),x6123,x6124),f1(x6125,a7,x6126,x6126))),
% 0.65/0.77 inference(rename_variables,[],[552])).
% 0.65/0.77 cnf(616,plain,
% 0.65/0.77 (P2(a5,x6161,x6161,f1(x6162,a8,x6163,x6163))),
% 0.65/0.77 inference(rename_variables,[],[228])).
% 0.65/0.77 cnf(622,plain,
% 0.65/0.77 (P2(x6221,x6222,f1(x6223,x6222,x6224,x6224),x6221)),
% 0.65/0.77 inference(rename_variables,[],[111])).
% 0.65/0.77 cnf(625,plain,
% 0.65/0.77 (P1(x6251,x6252,x6252)),
% 0.65/0.77 inference(rename_variables,[],[36])).
% 0.65/0.77 cnf(628,plain,
% 0.65/0.77 (P1(x6281,x6282,f1(x6282,x6282,x6283,x6283))),
% 0.65/0.77 inference(rename_variables,[],[190])).
% 0.65/0.77 cnf(630,plain,
% 0.65/0.77 (~E(x6301,f1(x6302,x6301,a7,a5))),
% 0.65/0.77 inference(scs_inference,[],[36,190,476,228,616,552,612,546,384,111,45,37,138,573,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32])).
% 0.65/0.77 cnf(631,plain,
% 0.65/0.77 (P2(x6311,f1(x6312,x6311,x6313,x6314),x6313,x6314)),
% 0.65/0.77 inference(rename_variables,[],[45])).
% 0.65/0.77 cnf(634,plain,
% 0.65/0.77 (P2(f1(x6341,a5,x6342,x6342),x6343,x6343,f1(x6344,a8,x6345,x6345))),
% 0.65/0.77 inference(rename_variables,[],[315])).
% 0.65/0.77 cnf(635,plain,
% 0.65/0.77 (~P2(x6351,f1(x6352,x6351,a5,a7),x6353,x6353)),
% 0.65/0.77 inference(rename_variables,[],[510])).
% 0.65/0.77 cnf(638,plain,
% 0.65/0.77 (~E(f1(a8,a7,x6381,x6382),f1(x6383,f1(a7,a5,x6384,x6384),x6385,x6385))),
% 0.65/0.77 inference(scs_inference,[],[36,176,190,472,370,476,228,616,552,612,546,384,111,315,45,37,138,573,113,510,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32,35,31,3])).
% 0.65/0.77 cnf(641,plain,
% 0.65/0.77 (~P2(x6411,f1(x6412,x6411,a5,a7),x6413,x6413)),
% 0.65/0.77 inference(rename_variables,[],[510])).
% 0.65/0.77 cnf(642,plain,
% 0.65/0.77 (~E(x6421,f1(x6422,f1(x6423,x6421,x6424,x6424),a5,a7))),
% 0.65/0.77 inference(scs_inference,[],[36,176,190,472,370,476,228,616,552,612,546,384,111,622,315,634,45,37,138,573,113,510,635,641,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32,35,31,3,34,33])).
% 0.65/0.77 cnf(649,plain,
% 0.65/0.77 (~P1(a7,f1(a5,a7,a5,a7),f1(f1(a5,a7,a5,a7),a7,f1(a5,a7,a5,a7),a7))),
% 0.65/0.77 inference(scs_inference,[],[36,176,190,472,370,476,228,616,552,612,546,384,465,111,622,315,634,364,45,37,138,210,573,371,113,510,635,641,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32,35,31,3,34,33,64,63])).
% 0.65/0.77 cnf(653,plain,
% 0.65/0.77 (~P2(f1(x6531,x6531,a7,a7),x6531,a5,a7)),
% 0.65/0.77 inference(scs_inference,[],[36,625,176,190,628,472,370,476,228,616,552,612,546,384,465,111,622,315,634,364,45,631,37,138,134,210,573,371,113,510,635,641,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32,35,31,3,34,33,64,63,82])).
% 0.65/0.77 cnf(659,plain,
% 0.65/0.77 (~E(x6591,f1(f1(x6592,x6591,a5,a7),f1(x6592,x6591,a5,a7),x6593,x6593))),
% 0.65/0.77 inference(scs_inference,[],[36,625,176,190,628,472,370,476,228,616,552,612,546,384,465,111,622,315,634,364,45,631,37,138,134,210,573,371,113,510,635,641,516,568,67,75,78,77,76,53,73,72,74,54,66,81,56,80,57,30,32,35,31,3,34,33,64,63,82,5])).
% 0.65/0.77 cnf(722,plain,
% 0.65/0.77 ($false),
% 0.65/0.77 inference(scs_inference,[],[36,172,105,109,659,630,638,477,327,111,167,41,37,642,591,649,543,653,67,5,76,53,77,78,72,73,75,74,54,66,81,56,80,57,32,30]),
% 0.65/0.77 ['proof']).
% 0.65/0.77 % SZS output end Proof
% 0.65/0.77 % Total time :0.260000s
%------------------------------------------------------------------------------