%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO062-3 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:35 EDT 2024
% Result : Unsatisfiable 1.02s 1.09s
% Output : CNFRefutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO062-3 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 07:23:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 1.02/1.07 %-------------------------------------------
% 1.02/1.07 % File :CSE---1.7
% 1.02/1.07 % Problem :theBenchmark
% 1.02/1.07 % Transform :cnf
% 1.02/1.07 % Format :tptp:raw
% 1.02/1.07 % Command :java -jar mcs_scs.jar %d %s
% 1.02/1.07
% 1.02/1.07 % Result :Theorem 0.470000s
% 1.02/1.07 % Output :CNFRefutation 0.470000s
% 1.02/1.07 %-------------------------------------------
% 1.02/1.08 %--------------------------------------------------------------------------
% 1.02/1.08 % File : GEO062-3 : TPTP v8.2.0. Bugfixed v1.2.1.
% 1.02/1.08 % Domain : Geometry
% 1.02/1.08 % Problem : Insertion identity
% 1.02/1.08 % Version : [Qua89] axioms : Augmented.
% 1.02/1.08 % English :
% 1.02/1.08
% 1.02/1.08 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 1.02/1.08 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 1.02/1.08 % Source : [Qua89]
% 1.02/1.08 % Names : I3 [Qua89]
% 1.02/1.08
% 1.02/1.08 % Status : Unsatisfiable
% 1.02/1.08 % Rating : 0.05 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.00 v7.0.0, 0.13 v6.3.0, 0.00 v6.2.0, 0.20 v6.1.0, 0.36 v6.0.0, 0.20 v5.5.0, 0.65 v5.3.0, 0.67 v5.2.0, 0.56 v5.1.0, 0.53 v5.0.0, 0.57 v4.1.0, 0.46 v4.0.1, 0.45 v4.0.0, 0.36 v3.7.0, 0.20 v3.5.0, 0.27 v3.4.0, 0.33 v3.3.0, 0.36 v3.2.0, 0.31 v3.1.0, 0.27 v2.7.0, 0.33 v2.6.0, 0.22 v2.5.0, 0.36 v2.4.0, 0.50 v2.3.0, 0.25 v2.2.1, 0.43 v2.2.0, 0.20 v2.1.0, 1.00 v2.0.0
% 1.02/1.08 % Syntax : Number of clauses : 75 ( 27 unt; 15 nHn; 54 RR)
% 1.02/1.08 % Number of literals : 196 ( 42 equ; 112 neg)
% 1.02/1.08 % Maximal clause size : 8 ( 2 avg)
% 1.02/1.08 % Maximal term depth : 3 ( 1 avg)
% 1.02/1.08 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 1.02/1.08 % Number of functors : 13 ( 13 usr; 6 con; 0-6 aty)
% 1.02/1.08 % Number of variables : 262 ( 14 sgn)
% 1.02/1.08 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.02/1.08
% 1.02/1.08 % Comments :
% 1.02/1.08 % Bugfixes : v1.2.1 - Clause d12 fixed.
% 1.02/1.08 %--------------------------------------------------------------------------
% 1.02/1.08 %----Include Tarski geometry axioms
% 1.02/1.08 include('Axioms/GEO002-0.ax').
% 1.02/1.08 %----Include definition of reflection
% 1.02/1.08 include('Axioms/GEO002-2.ax').
% 1.02/1.08 %----Include definition of insertion
% 1.02/1.08 include('Axioms/GEO002-3.ax').
% 1.02/1.08 %--------------------------------------------------------------------------
% 1.02/1.08 cnf(d1,axiom,
% 1.02/1.08 equidistant(U,V,U,V) ).
% 1.02/1.08
% 1.02/1.08 cnf(d2,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(W,X,U,V) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d3,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(V,U,W,X) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d4_1,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(U,V,X,W) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d4_2,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(V,U,X,W) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d4_3,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(W,X,V,U) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d4_4,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(X,W,U,V) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d4_5,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | equidistant(X,W,V,U) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d5,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,W,X)
% 1.02/1.08 | ~ equidistant(W,X,Y,Z)
% 1.02/1.08 | equidistant(U,V,Y,Z) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(e1,axiom,
% 1.02/1.08 V = extension(U,V,W,W) ).
% 1.02/1.08
% 1.02/1.08 cnf(b0,axiom,
% 1.02/1.08 ( Y != extension(U,V,W,X)
% 1.02/1.08 | between(U,V,Y) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(r2_1,axiom,
% 1.02/1.08 between(U,V,reflection(U,V)) ).
% 1.02/1.08
% 1.02/1.08 cnf(r2_2,axiom,
% 1.02/1.08 equidistant(V,reflection(U,V),U,V) ).
% 1.02/1.08
% 1.02/1.08 cnf(r3_1,axiom,
% 1.02/1.08 ( U != V
% 1.02/1.08 | V = reflection(U,V) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(r3_2,axiom,
% 1.02/1.08 U = reflection(U,U) ).
% 1.02/1.08
% 1.02/1.08 cnf(r4,axiom,
% 1.02/1.08 ( V != reflection(U,V)
% 1.02/1.08 | U = V ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d7,axiom,
% 1.02/1.08 equidistant(U,U,V,V) ).
% 1.02/1.08
% 1.02/1.08 cnf(d8,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,U1,V1)
% 1.02/1.08 | ~ equidistant(V,W,V1,W1)
% 1.02/1.08 | ~ between(U,V,W)
% 1.02/1.08 | ~ between(U1,V1,W1)
% 1.02/1.08 | equidistant(U,W,U1,W1) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d9,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U,V,X)
% 1.02/1.08 | ~ equidistant(V,W,V,X)
% 1.02/1.08 | U = V
% 1.02/1.08 | W = X ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d10_1,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | U = V
% 1.02/1.08 | W = extension(U,V,V,W) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d10_2,axiom,
% 1.02/1.08 ( ~ equidistant(W,X,Y,Z)
% 1.02/1.08 | extension(U,V,W,X) = extension(U,V,Y,Z)
% 1.02/1.08 | U = V ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d10_3,axiom,
% 1.02/1.08 ( extension(U,V,U,V) = extension(U,V,V,U)
% 1.02/1.08 | U = V ) ).
% 1.02/1.08
% 1.02/1.08 cnf(r5,axiom,
% 1.02/1.08 equidistant(V,U,V,reflection(reflection(U,V),V)) ).
% 1.02/1.08
% 1.02/1.08 cnf(r6,axiom,
% 1.02/1.08 U = reflection(reflection(U,V),V) ).
% 1.02/1.08
% 1.02/1.08 cnf(t3,axiom,
% 1.02/1.08 between(U,V,V) ).
% 1.02/1.08
% 1.02/1.08 cnf(b1,axiom,
% 1.02/1.08 ( ~ between(U,W,X)
% 1.02/1.08 | U != X
% 1.02/1.08 | between(V,W,X) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(t1,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | between(W,V,U) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(t2,axiom,
% 1.02/1.08 between(U,U,V) ).
% 1.02/1.08
% 1.02/1.08 cnf(b2,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(V,U,W)
% 1.02/1.08 | U = V ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b3,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U,W,V)
% 1.02/1.08 | V = W ) ).
% 1.02/1.08
% 1.02/1.08 cnf(t6_1,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(V,U,W)
% 1.02/1.08 | U = V
% 1.02/1.08 | V = W ) ).
% 1.02/1.08
% 1.02/1.08 cnf(t6_2,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U,W,V)
% 1.02/1.08 | U = V
% 1.02/1.08 | V = W ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b4,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(V,W,X)
% 1.02/1.08 | between(U,V,W) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b5,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U,W,X)
% 1.02/1.08 | between(V,W,X) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b6,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(V,W,X)
% 1.02/1.08 | between(U,W,X)
% 1.02/1.08 | V = W ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b7,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(V,W,X)
% 1.02/1.08 | between(U,V,X)
% 1.02/1.08 | V = W ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b8,axiom,
% 1.02/1.08 ( ~ between(U,V,X)
% 1.02/1.08 | ~ between(V,W,X)
% 1.02/1.08 | between(U,W,X) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(b9,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U,W,X)
% 1.02/1.08 | between(U,V,X) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(e2_1,axiom,
% 1.02/1.08 lower_dimension_point_1 != lower_dimension_point_2 ).
% 1.02/1.08
% 1.02/1.08 cnf(e2_2,axiom,
% 1.02/1.08 lower_dimension_point_2 != lower_dimension_point_3 ).
% 1.02/1.08
% 1.02/1.08 cnf(e2_3,axiom,
% 1.02/1.08 lower_dimension_point_1 != lower_dimension_point_3 ).
% 1.02/1.08
% 1.02/1.08 cnf(e3_1,axiom,
% 1.02/1.08 V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2) ).
% 1.02/1.08
% 1.02/1.08 cnf(e3_2,axiom,
% 1.02/1.08 equidistant(V,extension(U,V,lower_dimension_point_1,lower_dimension_point_2),X,extension(W,X,lower_dimension_point_1,lower_dimension_point_2)) ).
% 1.02/1.08
% 1.02/1.08 cnf(e3_3,axiom,
% 1.02/1.08 between(U,V,extension(U,V,lower_dimension_point_1,lower_dimension_point_2)) ).
% 1.02/1.08
% 1.02/1.08 cnf(b10,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ between(U1,V1,W)
% 1.02/1.08 | ~ between(U,X,U1)
% 1.02/1.08 | between(X,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),W)
% 1.02/1.08 | between(V,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),V1) ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d11,axiom,
% 1.02/1.08 ( ~ between(U,V,W)
% 1.02/1.08 | ~ equidistant(U,W,U,W1)
% 1.02/1.08 | ~ equidistant(V,W,V,W1)
% 1.02/1.08 | U = V
% 1.02/1.08 | W = W1 ) ).
% 1.02/1.08
% 1.02/1.08 cnf(d12,axiom,
% 1.02/1.08 ( ~ equidistant(U,V,U1,V1)
% 1.02/1.08 | ~ equidistant(U,W,U1,W1)
% 1.02/1.08 | ~ equidistant(U,X,U1,X1)
% 1.02/1.08 | ~ equidistant(W,X,W1,X1)
% 1.02/1.09 | ~ between(U,V,W)
% 1.02/1.09 | ~ between(U1,V1,W1)
% 1.02/1.09 | equidistant(V,X,V1,X1) ) ).
% 1.02/1.09
% 1.02/1.09 cnf(d13,axiom,
% 1.02/1.09 ( ~ between(U,V,W)
% 1.02/1.09 | ~ between(U1,V1,W1)
% 1.02/1.09 | ~ equidistant(U,V,U1,V1)
% 1.02/1.09 | ~ equidistant(U,W,U1,W1)
% 1.02/1.09 | equidistant(V,W,V1,W1) ) ).
% 1.02/1.09
% 1.02/1.09 cnf(d14,axiom,
% 1.02/1.09 ( ~ equidistant(U,V,U1,V1)
% 1.02/1.09 | ~ equidistant(V,W,V1,W1)
% 1.02/1.09 | ~ equidistant(U,X,U1,X1)
% 1.02/1.09 | ~ equidistant(W,X,W1,X1)
% 1.02/1.09 | ~ between(U,V,W)
% 1.02/1.09 | ~ between(U1,V1,W1)
% 1.02/1.09 | equidistant(V,X,V1,X1) ) ).
% 1.02/1.09
% 1.02/1.09 cnf(d15,axiom,
% 1.02/1.09 ( ~ between(U,V,W)
% 1.02/1.09 | ~ equidistant(U,V,U,X)
% 1.02/1.09 | ~ equidistant(W,V,W,X)
% 1.02/1.09 | V = X ) ).
% 1.02/1.09
% 1.02/1.09 cnf(i2_1,axiom,
% 1.02/1.09 equidistant(U,V,U1,insertion(U1,W1,U,V)) ).
% 1.02/1.09
% 1.02/1.09 cnf(i2_2,axiom,
% 1.02/1.09 ( ~ between(U,V,W)
% 1.02/1.09 | ~ equidistant(U,W,U1,W1)
% 1.02/1.09 | between(U1,insertion(U1,W1,U,V),W1) ) ).
% 1.02/1.09
% 1.02/1.09 cnf(i2_3,axiom,
% 1.02/1.09 ( ~ between(U,V,W)
% 1.02/1.09 | ~ equidistant(U,W,U1,W1)
% 1.02/1.09 | equidistant(V,W,insertion(U1,W1,U,V),W1) ) ).
% 1.02/1.09
% 1.02/1.09 cnf(v_between_u_and_w,hypothesis,
% 1.02/1.09 between(u,v,w) ).
% 1.02/1.09
% 1.02/1.09 cnf(prove_v_equals_insertion,negated_conjecture,
% 1.02/1.09 v != insertion(u,w,u,v) ).
% 1.02/1.09
% 1.02/1.09 %--------------------------------------------------------------------------
% 1.02/1.09 %-------------------------------------------
% 1.02/1.09 % Proof found
% 1.02/1.09 % SZS status Theorem for theBenchmark
% 1.02/1.09 % SZS output start Proof
% 1.02/1.09 %ClaNum:107(EqnAxiom:35)
% 1.02/1.09 %VarNum:664(SingletonVarNum:239)
% 1.02/1.09 %MaxLitNum:8
% 1.02/1.09 %MaxfuncDepth:2
% 1.02/1.09 %SharedTerms:16
% 1.02/1.09 %goalClause: 60
% 1.02/1.09 %singleGoalClaCount:1
% 1.02/1.09 [36]P1(a1,a10,a11)
% 1.02/1.09 [53]~E(a8,a6)
% 1.02/1.09 [54]~E(a9,a6)
% 1.02/1.09 [55]~E(a9,a8)
% 1.02/1.09 [56]~P1(a6,a8,a9)
% 1.02/1.09 [57]~P1(a8,a9,a6)
% 1.02/1.09 [58]~P1(a9,a6,a8)
% 1.02/1.09 [60]~E(f2(f2(a11,a1,a6,a8),a1,a1,a10),a10)
% 1.02/1.09 [37]P1(x371,x372,x372)
% 1.02/1.09 [38]P1(x381,x381,x382)
% 1.02/1.09 [39]P2(x391,x392,x392,x391)
% 1.02/1.09 [40]P2(x401,x402,x401,x402)
% 1.02/1.09 [41]P2(x411,x411,x412,x412)
% 1.02/1.09 [59]~E(f2(x591,x592,a6,a8),x592)
% 1.02/1.09 [50]E(f2(f2(x501,x502,x501,x502),x502,f2(x501,x502,x501,x502),x502),x501)
% 1.02/1.09 [52]P2(x521,x522,x521,f2(f2(x522,x521,x522,x521),x521,f2(x522,x521,x522,x521),x521))
% 1.02/1.09 [42]E(f2(x421,x422,x423,x423),x422)
% 1.02/1.09 [45]P1(x451,x452,f2(x451,x452,x453,x454))
% 1.02/1.09 [47]P2(x471,f2(x472,x471,x473,x474),x473,x474)
% 1.02/1.09 [49]P2(x491,f2(x492,x491,a6,a8),x493,f2(x494,x493,a6,a8))
% 1.02/1.09 [51]P2(x511,x512,x513,f2(f2(x514,x513,a6,a8),x513,x511,x512))
% 1.02/1.09 [61]~P1(x611,x612,x611)+E(x611,x612)
% 1.02/1.09 [73]~E(x731,x732)+E(f2(x731,x732,x731,x732),x732)
% 1.02/1.09 [76]E(x761,x762)+~E(f2(x762,x761,x762,x761),x761)
% 1.02/1.09 [78]E(x781,x782)+E(f2(x781,x782,x781,x782),f2(x781,x782,x782,x781))
% 1.02/1.09 [62]~P1(x623,x622,x621)+P1(x621,x622,x623)
% 1.02/1.09 [75]~P2(x751,x752,x753,x753)+E(x751,x752)
% 1.02/1.09 [80]~P2(x804,x803,x802,x801)+P2(x801,x802,x803,x804)
% 1.02/1.09 [81]~P2(x813,x814,x812,x811)+P2(x811,x812,x813,x814)
% 1.02/1.09 [82]~P2(x824,x823,x821,x822)+P2(x821,x822,x823,x824)
% 1.02/1.09 [83]~P2(x833,x834,x831,x832)+P2(x831,x832,x833,x834)
% 1.02/1.09 [84]~P2(x842,x841,x844,x843)+P2(x841,x842,x843,x844)
% 1.02/1.09 [85]~P2(x852,x851,x853,x854)+P2(x851,x852,x853,x854)
% 1.02/1.09 [86]~P2(x861,x862,x864,x863)+P2(x861,x862,x863,x864)
% 1.02/1.09 [77]P1(x771,x772,x773)+~E(x773,f2(x771,x772,x774,x775))
% 1.02/1.09 [64]~P1(x643,x641,x642)+E(x641,x642)+~P1(x643,x642,x641)
% 1.02/1.09 [65]~P1(x651,x652,x653)+E(x651,x652)+~P1(x652,x651,x653)
% 1.02/1.09 [74]~P1(x741,x742,x743)+E(x741,x742)+E(f2(x741,x742,x742,x743),x743)
% 1.02/1.09 [63]~P1(x634,x632,x633)+P1(x631,x632,x633)+~E(x634,x633)
% 1.02/1.09 [68]~P1(x684,x681,x682)+P1(x681,x682,x683)+~P1(x684,x682,x683)
% 1.02/1.09 [69]~P1(x691,x694,x693)+P1(x691,x692,x693)+~P1(x694,x692,x693)
% 1.02/1.09 [70]~P1(x701,x702,x704)+P1(x701,x702,x703)+~P1(x701,x704,x703)
% 1.02/1.09 [100]~P1(x1005,x1001,x1004)+~P1(x1002,x1003,x1004)+P1(x1001,f7(x1002,x1003,x1004,x1001,x1005),x1002)
% 1.02/1.09 [101]~P1(x1015,x1014,x1013)+~P1(x1012,x1011,x1013)+P1(x1011,f7(x1012,x1011,x1013,x1014,x1015),x1015)
% 1.02/1.09 [98]~P2(x983,x985,x981,x982)+~P1(x983,x984,x985)+P1(x981,f2(f2(x982,x981,a6,a8),x981,x983,x984),x982)
% 1.02/1.09 [99]~P1(x995,x991,x992)+~P2(x995,x992,x994,x993)+P2(x991,x992,f2(f2(x993,x994,a6,a8),x994,x995,x991),x993)
% 1.02/1.09 [90]~P2(x905,x906,x901,x902)+P2(x901,x902,x903,x904)+~P2(x905,x906,x903,x904)
% 1.02/1.09 [91]~P2(x911,x912,x915,x916)+P2(x911,x912,x913,x914)+~P2(x915,x916,x913,x914)
% 1.02/1.09 [89]~P2(x893,x894,x895,x896)+E(x891,x892)+E(f2(x891,x892,x893,x894),f2(x891,x892,x895,x896))
% 1.02/1.09 [71]~P1(x711,x712,x714)+~P1(x713,x711,x712)+E(x711,x712)+P1(x713,x712,x714)
% 1.02/1.09 [72]~P1(x721,x722,x724)+~P1(x723,x721,x722)+E(x721,x722)+P1(x723,x721,x724)
% 1.02/1.09 [87]~P2(x874,x871,x874,x872)+~P2(x873,x871,x873,x872)+E(x871,x872)+~P1(x873,x871,x874)
% 1.02/1.09 [102]~P1(x1024,x1022,x1023)+~P1(x1021,x1022,x1025)+E(x1021,x1022)+P1(x1021,x1023,f3(x1021,x1024,x1022,x1023,x1025))
% 1.02/1.09 [103]~P1(x1033,x1032,x1034)+~P1(x1031,x1032,x1035)+E(x1031,x1032)+P1(x1031,x1033,f4(x1031,x1033,x1032,x1034,x1035))
% 1.02/1.09 [104]~P1(x1043,x1042,x1044)+~P1(x1041,x1042,x1045)+E(x1041,x1042)+P1(f4(x1041,x1043,x1042,x1044,x1045),x1045,f3(x1041,x1043,x1042,x1044,x1045))
% 1.02/1.09 [79]~P1(x793,x794,x792)+~P1(x793,x794,x791)+~P2(x794,x791,x794,x792)+E(x791,x792)+E(x793,x794)
% 1.02/1.09 [88]~P1(x883,x884,x881)+~P2(x884,x881,x884,x882)+~P2(x883,x881,x883,x882)+E(x881,x882)+E(x883,x884)
% 1.02/1.09 [92]~P2(x926,x922,x925,x924)+~P2(x926,x921,x925,x923)+P2(x921,x922,x923,x924)+~P1(x925,x923,x924)+~P1(x926,x921,x922)
% 1.02/1.09 [93]~P2(x936,x932,x935,x934)+~P2(x931,x936,x933,x935)+P2(x931,x932,x933,x934)+~P1(x933,x935,x934)+~P1(x931,x936,x932)
% 1.02/1.09 [105]~P1(x1053,x1054,x1055)+~P1(x1052,x1053,x1055)+~P2(x1052,x1055,x1052,x1056)+~P2(x1052,x1053,x1052,x1051)+P1(x1051,f5(x1052,x1053,x1051,x1054,x1055,x1056),x1056)
% 1.02/1.09 [106]~P1(x1063,x1062,x1065)+~P1(x1061,x1063,x1065)+~P2(x1061,x1065,x1061,x1066)+~P2(x1061,x1063,x1061,x1064)+P2(x1061,x1062,x1061,f5(x1061,x1063,x1064,x1062,x1065,x1066))
% 1.02/1.09 [107]~P1(x1074,x1072,x1075)+~P1(x1073,x1071,x1074)+~P1(x1073,x1076,x1075)+P1(x1071,f7(x1072,f7(x1073,x1071,x1074,x1072,x1075),x1073,x1076,x1075),x1075)+P1(x1076,f7(x1072,f7(x1073,x1071,x1074,x1072,x1075),x1073,x1076,x1075),x1072)
% 1.02/1.09 [94]P1(x945,x943,x944)+P1(x944,x945,x943)+~P2(x943,x941,x943,x942)+~P2(x945,x941,x945,x942)+~P2(x944,x941,x944,x942)+E(x941,x942)+P1(x943,x944,x945)
% 1.02/1.09 [95]~P2(x958,x952,x956,x954)+~P2(x951,x958,x953,x956)+~P2(x957,x952,x955,x954)+~P2(x957,x951,x955,x953)+P2(x951,x952,x953,x954)+~P1(x955,x953,x956)+~P1(x957,x951,x958)
% 1.02/1.09 [96]~P2(x968,x962,x966,x964)+~P2(x967,x962,x965,x964)+~P2(x967,x968,x965,x966)+~P2(x967,x961,x965,x963)+P2(x961,x962,x963,x964)+~P1(x965,x963,x966)+~P1(x967,x961,x968)
% 1.02/1.09 [97]~P1(x971,x972,x973)+~P2(x972,x974,x978,x976)+~P2(x972,x973,x978,x975)+~P2(x971,x974,x977,x976)+~P2(x971,x972,x977,x978)+E(x971,x972)+P2(x973,x974,x975,x976)+~P1(x977,x978,x975)
% 1.02/1.09 %EqnAxiom
% 1.02/1.09 [1]E(x11,x11)
% 1.02/1.09 [2]E(x22,x21)+~E(x21,x22)
% 1.02/1.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.02/1.09 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45))
% 1.02/1.09 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55))
% 1.02/1.09 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65))
% 1.02/1.09 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72))
% 1.02/1.09 [8]~E(x81,x82)+E(f7(x81,x83,x84,x85,x86),f7(x82,x83,x84,x85,x86))
% 1.02/1.09 [9]~E(x91,x92)+E(f7(x93,x91,x94,x95,x96),f7(x93,x92,x94,x95,x96))
% 1.02/1.09 [10]~E(x101,x102)+E(f7(x103,x104,x101,x105,x106),f7(x103,x104,x102,x105,x106))
% 1.02/1.09 [11]~E(x111,x112)+E(f7(x113,x114,x115,x111,x116),f7(x113,x114,x115,x112,x116))
% 1.02/1.09 [12]~E(x121,x122)+E(f7(x123,x124,x125,x126,x121),f7(x123,x124,x125,x126,x122))
% 1.02/1.09 [13]~E(x131,x132)+E(f3(x131,x133,x134,x135,x136),f3(x132,x133,x134,x135,x136))
% 1.02/1.09 [14]~E(x141,x142)+E(f3(x143,x141,x144,x145,x146),f3(x143,x142,x144,x145,x146))
% 1.02/1.09 [15]~E(x151,x152)+E(f3(x153,x154,x151,x155,x156),f3(x153,x154,x152,x155,x156))
% 1.02/1.09 [16]~E(x161,x162)+E(f3(x163,x164,x165,x161,x166),f3(x163,x164,x165,x162,x166))
% 1.02/1.09 [17]~E(x171,x172)+E(f3(x173,x174,x175,x176,x171),f3(x173,x174,x175,x176,x172))
% 1.02/1.09 [18]~E(x181,x182)+E(f4(x181,x183,x184,x185,x186),f4(x182,x183,x184,x185,x186))
% 1.02/1.09 [19]~E(x191,x192)+E(f4(x193,x191,x194,x195,x196),f4(x193,x192,x194,x195,x196))
% 1.02/1.09 [20]~E(x201,x202)+E(f4(x203,x204,x201,x205,x206),f4(x203,x204,x202,x205,x206))
% 1.02/1.09 [21]~E(x211,x212)+E(f4(x213,x214,x215,x211,x216),f4(x213,x214,x215,x212,x216))
% 1.02/1.09 [22]~E(x221,x222)+E(f4(x223,x224,x225,x226,x221),f4(x223,x224,x225,x226,x222))
% 1.02/1.09 [23]~E(x231,x232)+E(f5(x231,x233,x234,x235,x236,x237),f5(x232,x233,x234,x235,x236,x237))
% 1.02/1.09 [24]~E(x241,x242)+E(f5(x243,x241,x244,x245,x246,x247),f5(x243,x242,x244,x245,x246,x247))
% 1.02/1.09 [25]~E(x251,x252)+E(f5(x253,x254,x251,x255,x256,x257),f5(x253,x254,x252,x255,x256,x257))
% 1.02/1.09 [26]~E(x261,x262)+E(f5(x263,x264,x265,x261,x266,x267),f5(x263,x264,x265,x262,x266,x267))
% 1.02/1.09 [27]~E(x271,x272)+E(f5(x273,x274,x275,x276,x271,x277),f5(x273,x274,x275,x276,x272,x277))
% 1.02/1.09 [28]~E(x281,x282)+E(f5(x283,x284,x285,x286,x287,x281),f5(x283,x284,x285,x286,x287,x282))
% 1.02/1.09 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 1.02/1.09 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 1.02/1.09 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 1.02/1.09 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 1.02/1.09 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 1.02/1.09 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 1.02/1.09 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 1.02/1.09
% 1.02/1.09 %-------------------------------------------
% 1.02/1.09 cnf(108,plain,
% 1.02/1.09 (~P1(x1081,x1082,x1081)+P1(x1083,x1082,x1081)),
% 1.02/1.09 inference(equality_inference,[],[63])).
% 1.02/1.09 cnf(111,plain,
% 1.02/1.09 (~P1(f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,f2(f2(a11,a1,a6,a8),a1,a1,a10))),
% 1.02/1.09 inference(scs_inference,[],[60,61])).
% 1.02/1.09 cnf(113,plain,
% 1.02/1.09 (~P2(f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,x1131,x1131)),
% 1.02/1.09 inference(scs_inference,[],[60,61,75])).
% 1.02/1.09 cnf(118,plain,
% 1.02/1.09 (E(x1181,f2(x1182,x1181,x1183,x1183))),
% 1.02/1.09 inference(scs_inference,[],[60,42,50,61,75,76,2])).
% 1.02/1.09 cnf(121,plain,
% 1.02/1.09 (~E(a6,a8)),
% 1.02/1.09 inference(scs_inference,[],[60,42,59,56,50,61,75,76,2,62,73])).
% 1.02/1.09 cnf(122,plain,
% 1.02/1.09 (~E(f2(x1221,x1222,a6,a8),x1222)),
% 1.02/1.09 inference(rename_variables,[],[59])).
% 1.02/1.09 cnf(124,plain,
% 1.02/1.09 (P1(x1241,x1242,f2(x1243,f2(x1241,x1242,x1244,x1245),x1246,x1246))),
% 1.02/1.09 inference(scs_inference,[],[60,42,59,56,50,61,75,76,2,62,73,77])).
% 1.02/1.09 cnf(125,plain,
% 1.02/1.09 (E(f2(x1251,x1252,x1253,x1253),x1252)),
% 1.02/1.09 inference(rename_variables,[],[42])).
% 1.02/1.09 cnf(133,plain,
% 1.02/1.09 (~P1(a10,f2(f2(a11,a1,a6,a8),a1,a1,a10),a10)),
% 1.02/1.09 inference(scs_inference,[],[60,38,42,59,56,50,61,75,76,2,62,73,77,80,81,82,64])).
% 1.02/1.09 cnf(134,plain,
% 1.02/1.09 (P1(x1341,x1341,x1342)),
% 1.02/1.09 inference(rename_variables,[],[38])).
% 1.02/1.09 cnf(136,plain,
% 1.02/1.09 (~P1(f2(x1361,x1362,a6,a8),x1362,f2(x1361,x1362,a6,a8))),
% 1.02/1.09 inference(scs_inference,[],[60,37,38,42,59,122,56,50,61,75,76,2,62,73,77,80,81,82,64,65])).
% 1.02/1.09 cnf(137,plain,
% 1.02/1.09 (~E(f2(x1371,x1372,a6,a8),x1372)),
% 1.02/1.09 inference(rename_variables,[],[59])).
% 1.02/1.09 cnf(138,plain,
% 1.02/1.09 (P1(x1381,x1382,x1382)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(140,plain,
% 1.02/1.09 (~P1(f2(a11,a1,a6,a8),a1,a10)),
% 1.02/1.09 inference(scs_inference,[],[60,37,38,42,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74])).
% 1.02/1.09 cnf(141,plain,
% 1.02/1.09 (~E(f2(x1411,x1412,a6,a8),x1412)),
% 1.02/1.09 inference(rename_variables,[],[59])).
% 1.02/1.09 cnf(144,plain,
% 1.02/1.09 (E(f2(x1441,x1442,x1443,x1443),x1442)),
% 1.02/1.09 inference(rename_variables,[],[42])).
% 1.02/1.09 cnf(145,plain,
% 1.02/1.09 (P2(f2(x1451,x1452,x1453,x1454),x1452,x1453,x1454)),
% 1.02/1.09 inference(scs_inference,[],[60,39,37,38,47,42,125,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90])).
% 1.02/1.09 cnf(146,plain,
% 1.02/1.09 (P2(x1461,f2(x1462,x1461,x1463,x1464),x1463,x1464)),
% 1.02/1.09 inference(rename_variables,[],[47])).
% 1.02/1.09 cnf(147,plain,
% 1.02/1.09 (P2(x1471,x1472,x1472,x1471)),
% 1.02/1.09 inference(rename_variables,[],[39])).
% 1.02/1.09 cnf(149,plain,
% 1.02/1.09 (P2(f2(x1491,x1492,a6,a8),x1492,x1493,f2(x1494,x1493,a6,a8))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,37,38,47,49,42,125,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91])).
% 1.02/1.09 cnf(150,plain,
% 1.02/1.09 (P2(x1501,f2(x1502,x1501,a6,a8),x1503,f2(x1504,x1503,a6,a8))),
% 1.02/1.09 inference(rename_variables,[],[49])).
% 1.02/1.09 cnf(151,plain,
% 1.02/1.09 (P2(x1511,x1512,x1512,x1511)),
% 1.02/1.09 inference(rename_variables,[],[39])).
% 1.02/1.09 cnf(153,plain,
% 1.02/1.09 (~E(x1531,f2(x1531,x1532,a6,a8))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,37,38,47,45,49,42,125,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29])).
% 1.02/1.09 cnf(154,plain,
% 1.02/1.09 (P1(x1541,x1542,f2(x1541,x1542,x1543,x1544))),
% 1.02/1.09 inference(rename_variables,[],[45])).
% 1.02/1.09 cnf(155,plain,
% 1.02/1.09 (P1(x1551,x1552,f2(x1551,f2(x1553,x1552,x1554,x1554),x1555,x1556))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,37,38,47,45,154,49,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30])).
% 1.02/1.09 cnf(156,plain,
% 1.02/1.09 (P1(x1561,x1562,f2(x1561,x1562,x1563,x1564))),
% 1.02/1.09 inference(rename_variables,[],[45])).
% 1.02/1.09 cnf(158,plain,
% 1.02/1.09 (P1(x1581,x1582,x1582)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(159,plain,
% 1.02/1.09 (~E(a10,f2(f2(a11,a1,a6,a8),a1,a1,a10))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,37,138,38,47,45,154,49,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32])).
% 1.02/1.09 cnf(160,plain,
% 1.02/1.09 (P2(x1601,x1602,x1602,x1601)),
% 1.02/1.09 inference(rename_variables,[],[39])).
% 1.02/1.09 cnf(162,plain,
% 1.02/1.09 (P2(x1621,f2(x1622,x1621,f2(x1623,x1624,x1625,x1625),x1626),x1624,x1626)),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,37,138,38,47,146,45,154,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34])).
% 1.02/1.09 cnf(163,plain,
% 1.02/1.09 (P2(x1631,f2(x1632,x1631,x1633,x1634),x1633,x1634)),
% 1.02/1.09 inference(rename_variables,[],[47])).
% 1.02/1.09 cnf(164,plain,
% 1.02/1.09 (P2(x1641,f2(x1642,x1641,x1643,f2(x1644,x1645,x1646,x1646)),x1643,x1645)),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,37,138,38,47,146,163,45,154,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35])).
% 1.02/1.09 cnf(165,plain,
% 1.02/1.09 (P2(x1651,f2(x1652,x1651,x1653,x1654),x1653,x1654)),
% 1.02/1.09 inference(rename_variables,[],[47])).
% 1.02/1.09 cnf(166,plain,
% 1.02/1.09 (~P2(f2(x1661,x1662,a6,a8),f2(x1661,x1662,a6,a8),f2(x1661,x1662,a6,a8),f2(f2(x1661,x1662,a6,a8),x1662,a6,a8))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,37,138,158,38,47,146,163,45,154,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35,87])).
% 1.02/1.09 cnf(167,plain,
% 1.02/1.09 (P1(x1671,x1672,x1672)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(170,plain,
% 1.02/1.09 (E(f2(f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,f2(x1701,a10,x1702,x1702),a10),a10)),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,37,138,158,167,38,47,146,163,45,154,156,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35,87,79])).
% 1.02/1.09 cnf(171,plain,
% 1.02/1.09 (P1(x1711,x1712,x1712)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(172,plain,
% 1.02/1.09 (P1(x1721,x1722,f2(x1721,x1722,x1723,x1724))),
% 1.02/1.09 inference(rename_variables,[],[45])).
% 1.02/1.09 cnf(176,plain,
% 1.02/1.09 (P1(x1761,x1762,x1762)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(179,plain,
% 1.02/1.09 (~P2(f2(a1,f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,f2(x1791,a10,x1792,x1792)),a10,a10,a10)),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,160,40,37,138,158,167,171,176,38,134,47,146,163,165,45,154,156,172,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35,87,79,92,95])).
% 1.02/1.09 cnf(181,plain,
% 1.02/1.09 (P1(x1811,x1812,x1812)),
% 1.02/1.09 inference(rename_variables,[],[37])).
% 1.02/1.09 cnf(189,plain,
% 1.02/1.09 (~P2(a10,f2(a1,f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,f2(x1891,a10,x1892,x1892)),a10,a10)),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,160,40,37,138,158,167,171,176,38,134,47,146,163,165,45,154,156,172,49,150,42,125,144,59,122,137,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35,87,79,92,95,83,84,85])).
% 1.02/1.09 cnf(192,plain,
% 1.02/1.09 (~E(f2(x1921,x1922,a6,a8),x1922)),
% 1.02/1.09 inference(rename_variables,[],[59])).
% 1.02/1.09 cnf(196,plain,
% 1.02/1.09 (E(x1961,f2(x1962,f2(x1963,x1961,a6,a8),a6,a8))+~P2(x1961,x1961,x1961,f2(x1962,f2(x1963,x1961,a6,a8),a6,a8))),
% 1.02/1.09 inference(scs_inference,[],[60,39,147,151,160,40,37,138,158,167,171,176,181,38,134,47,146,163,165,45,154,156,172,49,150,42,125,144,59,122,137,141,192,56,50,61,75,76,2,62,73,77,80,81,82,64,65,74,3,90,91,29,30,31,32,33,34,35,87,79,92,95,83,84,85,71,72,88])).
% 1.02/1.09 cnf(215,plain,
% 1.02/1.09 (~P1(a9,a6,a9)),
% 1.02/1.09 inference(scs_inference,[],[54,153,189,179,196,86,80,81,82,61])).
% 1.02/1.09 cnf(219,plain,
% 1.02/1.10 (~P2(a9,a6,x2191,x2191)),
% 1.02/1.10 inference(scs_inference,[],[54,153,189,179,196,86,80,81,82,61,84,75])).
% 1.02/1.10 cnf(221,plain,
% 1.02/1.10 (~P2(a6,a9,x2211,x2211)),
% 1.02/1.10 inference(scs_inference,[],[54,153,189,179,196,86,80,81,82,61,84,75,85])).
% 1.02/1.10 cnf(227,plain,
% 1.02/1.10 (E(a10,f2(f2(f2(a11,a1,a6,a8),a1,a1,a10),a10,f2(x2271,a10,x2272,x2272),a10))),
% 1.02/1.10 inference(scs_inference,[],[140,170,54,153,189,179,196,86,80,81,82,61,84,75,85,62,83,2])).
% 1.02/1.10 cnf(228,plain,
% 1.02/1.10 (P1(x2281,f2(x2281,x2282,x2283,x2284),f2(x2282,f2(x2281,x2282,x2283,x2284),x2285,x2285))),
% 1.02/1.10 inference(scs_inference,[],[140,170,54,124,153,189,179,45,196,86,80,81,82,61,84,75,85,62,83,2,69])).
% 1.02/1.10 cnf(229,plain,
% 1.02/1.10 (P1(x2291,x2292,f2(x2291,x2292,x2293,x2294))),
% 1.02/1.10 inference(rename_variables,[],[45])).
% 1.02/1.10 cnf(230,plain,
% 1.02/1.10 (P1(x2301,x2302,f2(x2303,f2(x2301,x2302,x2304,x2305),x2306,x2306))),
% 1.02/1.10 inference(rename_variables,[],[124])).
% 1.02/1.10 cnf(232,plain,
% 1.02/1.10 (P1(x2321,x2322,f2(f2(x2323,x2322,x2324,x2324),f2(x2323,x2322,x2324,x2324),x2325,x2325))),
% 1.02/1.10 inference(scs_inference,[],[118,140,170,54,124,155,153,189,179,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63])).
% 1.02/1.10 cnf(233,plain,
% 1.02/1.10 (E(x2331,f2(x2332,x2331,x2333,x2333))),
% 1.02/1.10 inference(rename_variables,[],[118])).
% 1.02/1.10 cnf(236,plain,
% 1.02/1.10 (~P1(a9,a6,f2(x2361,f2(a6,a9,x2362,x2363),x2364,x2364))),
% 1.02/1.10 inference(scs_inference,[],[118,140,170,54,124,230,155,153,189,179,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65])).
% 1.02/1.10 cnf(237,plain,
% 1.02/1.10 (P1(x2371,x2372,f2(x2373,f2(x2371,x2372,x2374,x2375),x2376,x2376))),
% 1.02/1.10 inference(rename_variables,[],[124])).
% 1.02/1.10 cnf(240,plain,
% 1.02/1.10 (P1(x2401,x2401,x2402)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(243,plain,
% 1.02/1.10 (P2(x2431,x2431,x2432,x2432)),
% 1.02/1.10 inference(rename_variables,[],[41])).
% 1.02/1.10 cnf(244,plain,
% 1.02/1.10 (P2(x2441,x2442,x2443,f2(f2(x2444,x2443,a6,a8),x2443,x2441,x2442))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(246,plain,
% 1.02/1.10 (P1(x2461,f2(x2462,x2463,x2464,x2464),f2(x2465,f2(x2461,x2463,x2466,x2467),x2468,x2468))),
% 1.02/1.10 inference(scs_inference,[],[118,233,140,170,51,54,41,124,230,237,155,153,189,179,38,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30])).
% 1.02/1.10 cnf(247,plain,
% 1.02/1.10 (P1(x2471,x2472,f2(x2473,f2(x2471,x2472,x2474,x2475),x2476,x2476))),
% 1.02/1.10 inference(rename_variables,[],[124])).
% 1.02/1.10 cnf(249,plain,
% 1.02/1.10 (P2(x2491,x2491,x2492,x2492)),
% 1.02/1.10 inference(rename_variables,[],[41])).
% 1.02/1.10 cnf(250,plain,
% 1.02/1.10 (P2(f2(x2501,x2502,x2503,x2504),x2502,x2503,f2(x2505,x2504,x2506,x2506))),
% 1.02/1.10 inference(scs_inference,[],[118,233,140,166,170,51,54,41,243,145,124,230,237,155,153,189,179,38,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35])).
% 1.02/1.10 cnf(252,plain,
% 1.02/1.10 (P1(f2(x2521,x2522,x2523,x2523),x2524,f2(x2525,f2(x2522,x2524,x2526,x2527),x2528,x2528))),
% 1.02/1.10 inference(scs_inference,[],[118,233,140,166,170,51,54,41,243,145,124,230,237,247,155,153,189,179,38,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29])).
% 1.02/1.10 cnf(254,plain,
% 1.02/1.10 (P2(x2541,x2541,x2542,f2(f2(x2543,x2542,a6,a8),x2542,x2544,x2544))),
% 1.02/1.10 inference(scs_inference,[],[118,233,140,166,170,51,244,54,41,243,249,145,124,230,237,247,155,153,189,179,38,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91])).
% 1.02/1.10 cnf(255,plain,
% 1.02/1.10 (P2(x2551,x2552,x2553,f2(f2(x2554,x2553,a6,a8),x2553,x2551,x2552))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(257,plain,
% 1.02/1.10 (P2(f2(x2571,x2572,x2573,x2573),x2574,x2575,f2(f2(x2576,x2575,a6,a8),x2575,x2572,x2574))),
% 1.02/1.10 inference(scs_inference,[],[118,233,140,166,170,51,244,255,54,41,243,249,145,124,230,237,247,155,153,189,179,38,45,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91,32])).
% 1.02/1.10 cnf(258,plain,
% 1.02/1.10 (P2(x2581,x2582,x2583,f2(f2(x2584,x2583,a6,a8),x2583,x2581,x2582))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(260,plain,
% 1.02/1.10 (P2(x2601,x2602,x2603,f2(f2(x2604,x2603,a6,a8),x2603,x2601,x2602))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(263,plain,
% 1.02/1.10 (P1(a1,a10,f2(x2631,a11,x2632,x2632))),
% 1.02/1.10 inference(scs_inference,[],[60,118,233,140,166,170,51,244,255,258,54,41,243,249,145,124,230,237,247,155,153,189,179,36,38,45,50,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91,32,33,3,31])).
% 1.02/1.10 cnf(265,plain,
% 1.02/1.10 (~P1(f2(a9,a6,a6,a8),a9,a6)),
% 1.02/1.10 inference(scs_inference,[],[60,118,233,140,136,166,170,51,244,255,258,54,41,243,249,145,124,230,237,247,155,153,189,179,36,38,45,229,50,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91,32,33,3,31,71])).
% 1.02/1.10 cnf(269,plain,
% 1.02/1.10 (~P2(a9,a9,x2691,f2(f2(x2692,x2691,a6,a8),x2691,a9,a6))),
% 1.02/1.10 inference(scs_inference,[],[60,118,233,140,136,166,170,51,244,255,258,260,54,41,243,249,145,124,230,237,247,155,153,189,179,36,37,38,240,45,229,50,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91,32,33,3,31,71,92])).
% 1.02/1.10 cnf(274,plain,
% 1.02/1.10 (~E(f2(x2741,x2742,a6,a8),x2741)),
% 1.02/1.10 inference(scs_inference,[],[60,118,233,140,136,166,170,51,244,255,258,260,54,41,243,249,145,124,230,237,247,155,153,189,179,36,37,38,240,45,229,50,196,86,80,81,82,61,84,75,85,62,83,2,69,63,65,64,90,30,34,35,29,91,32,33,3,31,71,92,4])).
% 1.02/1.10 cnf(302,plain,
% 1.02/1.10 (~P2(f2(x3021,x3022,a6,a8),x3022,x3023,x3023)),
% 1.02/1.10 inference(scs_inference,[],[219,59,121,269,80,86,61,75])).
% 1.02/1.10 cnf(310,plain,
% 1.02/1.10 (~P2(x3101,x3101,x3102,f2(x3103,x3102,a6,a8))),
% 1.02/1.10 inference(scs_inference,[],[219,59,121,269,80,86,61,75,84,83,85,81])).
% 1.02/1.10 cnf(316,plain,
% 1.02/1.10 (E(x3161,f2(f2(x3161,x3162,x3161,x3162),x3162,f2(x3161,x3162,x3161,x3162),x3162))),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,121,269,50,80,86,61,75,84,83,85,81,62,82,2])).
% 1.02/1.10 cnf(317,plain,
% 1.02/1.10 (~P2(a6,a8,x3171,x3171)),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,121,269,37,50,80,86,61,75,84,83,85,81,62,82,2,99])).
% 1.02/1.10 cnf(318,plain,
% 1.02/1.10 (P1(x3181,x3182,x3182)),
% 1.02/1.10 inference(rename_variables,[],[37])).
% 1.02/1.10 cnf(320,plain,
% 1.02/1.10 (P1(f2(f2(x3201,x3202,x3203,x3203),f2(x3201,x3202,x3203,x3203),x3204,x3204),x3202,x3205)),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,232,121,269,37,38,50,80,86,61,75,84,83,85,81,62,82,2,99,70])).
% 1.02/1.10 cnf(321,plain,
% 1.02/1.10 (P1(x3211,x3211,x3212)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(322,plain,
% 1.02/1.10 (P1(x3221,x3222,f2(f2(x3223,x3222,x3224,x3224),f2(x3223,x3222,x3224,x3224),x3225,x3225))),
% 1.02/1.10 inference(rename_variables,[],[232])).
% 1.02/1.10 cnf(324,plain,
% 1.02/1.10 (P1(x3241,f2(f2(x3242,x3241,x3243,x3243),f2(x3242,x3241,x3243,x3243),x3244,x3244),x3245)),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,232,322,121,269,37,38,321,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68])).
% 1.02/1.10 cnf(325,plain,
% 1.02/1.10 (P1(x3251,x3251,x3252)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(326,plain,
% 1.02/1.10 (P1(x3261,x3262,f2(f2(x3263,x3262,x3264,x3264),f2(x3263,x3262,x3264,x3264),x3265,x3265))),
% 1.02/1.10 inference(rename_variables,[],[232])).
% 1.02/1.10 cnf(329,plain,
% 1.02/1.10 (P1(x3291,x3292,f2(f2(x3293,x3292,x3294,x3294),f2(x3293,x3292,x3294,x3294),x3295,x3295))),
% 1.02/1.10 inference(rename_variables,[],[232])).
% 1.02/1.10 cnf(331,plain,
% 1.02/1.10 (P2(x3311,f2(x3312,x3311,a6,a8),x3313,f2(f2(x3314,x3313,a6,a8),x3313,f2(x3315,x3316,a6,a8),x3316))),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,159,149,51,232,322,326,121,269,37,38,321,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90])).
% 1.02/1.10 cnf(332,plain,
% 1.02/1.10 (P2(x3321,x3322,x3323,f2(f2(x3324,x3323,a6,a8),x3323,x3321,x3322))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(334,plain,
% 1.02/1.10 (P1(x3341,f2(x3342,x3343,x3344,x3344),f2(f2(x3343,x3343,x3345,x3345),f2(x3343,x3343,x3345,x3345),x3346,x3346))),
% 1.02/1.10 inference(scs_inference,[],[219,236,59,159,149,51,232,322,326,329,246,121,269,37,38,321,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69])).
% 1.02/1.10 cnf(336,plain,
% 1.02/1.10 (P1(x3361,x3362,f2(f2(x3363,x3362,x3364,x3364),f2(x3363,x3362,x3364,x3364),x3365,x3365))),
% 1.02/1.10 inference(rename_variables,[],[232])).
% 1.02/1.10 cnf(339,plain,
% 1.02/1.10 (~E(f2(x3391,x3392,a6,a8),x3392)),
% 1.02/1.10 inference(rename_variables,[],[59])).
% 1.02/1.10 cnf(340,plain,
% 1.02/1.10 (P1(x3401,x3401,x3402)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(343,plain,
% 1.02/1.10 (P2(f2(x3431,x3432,a6,a8),x3432,x3433,f2(x3434,x3433,a6,a8))),
% 1.02/1.10 inference(rename_variables,[],[149])).
% 1.02/1.10 cnf(344,plain,
% 1.02/1.10 (P2(x3441,f2(x3442,x3441,x3443,x3444),x3443,x3444)),
% 1.02/1.10 inference(rename_variables,[],[47])).
% 1.02/1.10 cnf(346,plain,
% 1.02/1.10 (P1(x3461,f2(x3462,f2(x3461,x3463,x3464,x3465),x3466,x3466),f2(x3463,f2(x3461,x3463,x3464,x3465),x3467,x3467))),
% 1.02/1.10 inference(scs_inference,[],[219,236,118,59,159,149,47,51,228,232,322,326,329,246,121,269,37,38,321,325,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30])).
% 1.02/1.10 cnf(347,plain,
% 1.02/1.10 (E(x3471,f2(x3472,x3471,x3473,x3473))),
% 1.02/1.10 inference(rename_variables,[],[118])).
% 1.02/1.10 cnf(354,plain,
% 1.02/1.10 (P2(f2(x3541,x3542,a6,a8),x3542,x3543,f2(x3544,x3543,a6,a8))),
% 1.02/1.10 inference(rename_variables,[],[149])).
% 1.02/1.10 cnf(355,plain,
% 1.02/1.10 (P1(f2(x3551,f2(x3552,x3553,x3554,x3554),x3555,x3555),x3556,f2(x3557,f2(x3553,x3556,x3558,x3559),x35510,x35510))),
% 1.02/1.10 inference(scs_inference,[],[113,219,227,236,118,347,59,159,149,343,47,344,51,250,228,232,322,326,329,246,252,121,269,37,38,321,325,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29])).
% 1.02/1.10 cnf(356,plain,
% 1.02/1.10 (E(x3561,f2(x3562,x3561,x3563,x3563))),
% 1.02/1.10 inference(rename_variables,[],[118])).
% 1.02/1.10 cnf(357,plain,
% 1.02/1.10 (~E(f2(f2(x3571,a10,x3572,x3572),f2(x3571,a10,x3572,x3572),x3573,x3573),f2(f2(a11,a1,a6,a8),a1,a1,a10))),
% 1.02/1.10 inference(scs_inference,[],[111,113,219,227,236,118,347,59,159,149,343,47,344,51,250,228,232,322,326,329,336,246,252,121,269,37,38,321,325,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29,31])).
% 1.02/1.10 cnf(367,plain,
% 1.02/1.10 (~P2(a6,a6,x3671,f2(f2(x3672,x3671,a6,a8),x3671,a6,a9))),
% 1.02/1.10 inference(scs_inference,[],[111,113,219,227,236,118,347,356,136,59,339,159,149,343,354,47,344,51,332,250,228,232,322,326,329,336,246,252,121,221,269,37,318,38,321,325,340,45,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29,31,33,3,71,92])).
% 1.02/1.10 cnf(373,plain,
% 1.02/1.10 (~E(f2(x3731,f2(x3732,x3733,a6,a8),x3734,x3734),x3733)),
% 1.02/1.10 inference(scs_inference,[],[111,113,219,227,236,118,347,356,136,59,339,159,149,343,354,47,344,51,332,250,228,232,322,326,329,336,246,252,121,221,269,37,318,38,321,325,340,45,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29,31,33,3,71,92,5])).
% 1.02/1.10 cnf(374,plain,
% 1.02/1.10 (P1(x3741,f2(f2(x3742,x3743,x3744,x3744),f2(x3742,x3743,x3744,x3744),x3745,x3745),x3743)),
% 1.02/1.10 inference(scs_inference,[],[111,113,219,227,236,118,347,356,136,59,339,159,149,343,354,47,344,51,332,250,228,232,322,326,329,336,246,252,121,221,269,37,318,38,321,325,340,45,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29,31,33,3,71,92,5,108])).
% 1.02/1.10 cnf(376,plain,
% 1.02/1.10 (P1(f2(x3761,x3762,x3761,x3762),x3762,x3761)),
% 1.02/1.10 inference(scs_inference,[],[111,113,219,227,236,118,347,356,136,59,339,159,149,343,354,47,344,51,332,250,228,232,322,326,329,336,246,252,121,221,269,37,318,38,321,325,340,45,50,80,86,61,75,84,83,85,81,62,82,2,99,70,68,65,90,69,64,91,30,32,35,34,29,31,33,3,71,92,5,108,77])).
% 1.02/1.10 cnf(408,plain,
% 1.02/1.10 (~P1(f2(x4081,x4082,a6,a8),x4081,f2(x4081,x4082,a6,a8))),
% 1.02/1.10 inference(scs_inference,[],[274,317,80,61])).
% 1.02/1.10 cnf(412,plain,
% 1.02/1.10 (P1(x4121,x4122,f2(x4123,f2(x4122,x4122,x4124,x4124),x4125,x4125))),
% 1.02/1.10 inference(scs_inference,[],[274,355,317,80,61,83,108])).
% 1.02/1.10 cnf(421,plain,
% 1.02/1.10 (~P2(f2(x4211,x4212,a6,a8),x4211,x4213,x4213)),
% 1.02/1.10 inference(scs_inference,[],[274,355,317,367,80,61,83,108,85,81,86,75])).
% 1.02/1.10 cnf(429,plain,
% 1.02/1.10 (~P1(f2(x4291,x4292,x4293,x4293),f2(f2(x4291,x4292,x4293,x4293),x4294,a6,a8),f2(f2(x4292,x4292,x4295,x4295),f2(x4292,x4292,x4295,x4295),x4296,x4296))),
% 1.02/1.10 inference(scs_inference,[],[265,274,153,334,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65])).
% 1.02/1.10 cnf(431,plain,
% 1.02/1.10 (P1(x4311,f2(x4312,x4313,x4314,x4314),f2(f2(x4313,x4313,x4315,x4315),f2(x4313,x4313,x4315,x4315),x4316,x4316))),
% 1.02/1.10 inference(rename_variables,[],[334])).
% 1.02/1.10 cnf(433,plain,
% 1.02/1.10 (P1(f2(f2(x4331,x4332,x4333,x4333),x4334,f2(x4331,x4332,x4333,x4333),x4334),x4334,f2(f2(x4332,x4332,x4335,x4335),f2(x4332,x4332,x4335,x4335),x4336,x4336))),
% 1.02/1.10 inference(scs_inference,[],[265,274,153,376,334,431,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70])).
% 1.02/1.10 cnf(434,plain,
% 1.02/1.10 (P1(x4341,f2(x4342,x4343,x4344,x4344),f2(f2(x4343,x4343,x4345,x4345),f2(x4343,x4343,x4345,x4345),x4346,x4346))),
% 1.02/1.10 inference(rename_variables,[],[334])).
% 1.02/1.10 cnf(435,plain,
% 1.02/1.10 (P1(f2(x4351,x4352,x4351,x4352),x4352,x4351)),
% 1.02/1.10 inference(rename_variables,[],[376])).
% 1.02/1.10 cnf(437,plain,
% 1.02/1.10 (P1(f2(x4371,x4372,x4373,x4373),f2(f2(x4372,x4372,x4374,x4374),f2(x4372,x4372,x4374,x4374),x4375,x4375),x4376)),
% 1.02/1.10 inference(scs_inference,[],[265,274,153,376,334,431,434,320,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68])).
% 1.02/1.10 cnf(439,plain,
% 1.02/1.10 (P1(x4391,f2(x4392,x4393,x4394,x4394),f2(f2(x4393,x4393,x4395,x4395),f2(x4393,x4393,x4395,x4395),x4396,x4396))),
% 1.02/1.10 inference(rename_variables,[],[334])).
% 1.02/1.10 cnf(441,plain,
% 1.02/1.10 (P1(f2(x4411,x4412,x4411,x4412),f2(f2(x4413,x4412,x4414,x4414),f2(x4413,x4412,x4414,x4414),x4415,x4415),x4411)),
% 1.02/1.10 inference(scs_inference,[],[265,274,153,376,435,334,431,434,320,324,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69])).
% 1.02/1.10 cnf(442,plain,
% 1.02/1.10 (P1(x4421,f2(f2(x4422,x4421,x4423,x4423),f2(x4422,x4421,x4423,x4423),x4424,x4424),x4425)),
% 1.02/1.10 inference(rename_variables,[],[324])).
% 1.02/1.10 cnf(444,plain,
% 1.02/1.10 (~P1(f2(f2(x4441,x4442,a6,a8),x4441,f2(x4441,x4442,a6,a8),x4441),f2(x4441,x4442,a6,a8),x4441)),
% 1.02/1.10 inference(scs_inference,[],[265,274,153,376,435,334,431,434,320,324,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69,64])).
% 1.02/1.10 cnf(445,plain,
% 1.02/1.10 (~E(f2(x4451,x4452,a6,a8),x4451)),
% 1.02/1.10 inference(rename_variables,[],[274])).
% 1.02/1.10 cnf(446,plain,
% 1.02/1.10 (P1(f2(x4461,x4462,x4461,x4462),x4462,x4461)),
% 1.02/1.10 inference(rename_variables,[],[376])).
% 1.02/1.10 cnf(449,plain,
% 1.02/1.10 (P2(x4491,x4492,x4493,f2(f2(x4494,x4493,a6,a8),x4493,x4491,x4492))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(452,plain,
% 1.02/1.10 (P2(x4521,x4522,x4523,f2(f2(x4524,x4523,a6,a8),x4523,x4521,x4522))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(455,plain,
% 1.02/1.10 (P1(x4551,f2(f2(x4552,x4551,x4553,x4553),f2(x4552,x4551,x4553,x4553),x4554,x4554),x4555)),
% 1.02/1.10 inference(rename_variables,[],[324])).
% 1.02/1.10 cnf(456,plain,
% 1.02/1.10 (~E(f2(f2(x4561,x4562,a6,a8),x4562,f2(x4563,x4564,a6,a8),x4564),x4562)),
% 1.02/1.10 inference(scs_inference,[],[215,302,265,274,153,47,51,449,452,376,435,334,431,434,320,324,442,355,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69,64,90,91,30,35])).
% 1.02/1.10 cnf(457,plain,
% 1.02/1.10 (P2(x4571,x4572,x4573,f2(f2(x4574,x4573,a6,a8),x4573,x4571,x4572))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(460,plain,
% 1.02/1.10 (~P2(f2(x4601,x4602,a6,a8),x4602,x4603,x4603)),
% 1.02/1.10 inference(rename_variables,[],[302])).
% 1.02/1.10 cnf(465,plain,
% 1.02/1.10 (P2(x4651,f2(x4652,x4651,x4653,x4654),x4653,x4654)),
% 1.02/1.10 inference(rename_variables,[],[47])).
% 1.02/1.10 cnf(468,plain,
% 1.02/1.10 (P1(f2(x4681,x4682,x4681,x4682),x4682,x4681)),
% 1.02/1.10 inference(rename_variables,[],[376])).
% 1.02/1.10 cnf(469,plain,
% 1.02/1.10 (~E(f2(f2(x4691,x4691,x4692,x4692),f2(x4691,x4691,x4692,x4692),x4693,x4693),f2(x4694,f2(x4695,x4691,x4696,x4696),a6,a8))),
% 1.02/1.10 inference(scs_inference,[],[215,302,460,265,136,274,153,47,51,449,452,457,149,376,435,446,334,431,434,439,320,324,442,355,310,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69,64,90,91,30,35,34,33,32,29,31])).
% 1.02/1.10 cnf(473,plain,
% 1.02/1.10 (~E(f2(x4731,x4732,a6,a8),x4731)),
% 1.02/1.10 inference(rename_variables,[],[274])).
% 1.02/1.10 cnf(474,plain,
% 1.02/1.10 (~P2(f2(a6,f2(a8,a6,a6,a8),a6,f2(a8,a6,a6,a8)),f2(a8,a6,a6,a8),f2(a6,f2(a8,a6,a6,a8),a6,f2(a8,a6,a6,a8)),a8)),
% 1.02/1.10 inference(scs_inference,[],[215,302,460,265,118,136,274,445,473,153,47,465,51,449,452,457,149,376,435,446,468,334,431,434,439,320,324,442,355,310,317,367,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69,64,90,91,30,35,34,33,32,29,31,3,87])).
% 1.02/1.10 cnf(486,plain,
% 1.02/1.10 (~E(f2(x4861,f2(x4862,x4863,a6,a8),x4864,x4864),x4862)),
% 1.02/1.10 inference(scs_inference,[],[215,133,302,460,265,118,136,274,445,473,153,47,465,51,449,452,457,149,376,435,446,468,334,431,434,439,320,324,442,455,355,357,310,317,367,45,80,61,83,108,85,81,86,75,84,62,82,65,70,68,69,64,90,91,30,35,34,33,32,29,31,3,87,72,71,4])).
% 1.02/1.10 cnf(518,plain,
% 1.02/1.10 (~P2(x5181,f2(x5181,x5182,a6,a8),x5183,x5183)),
% 1.02/1.10 inference(scs_inference,[],[421,474,153,81,83,86,80,75])).
% 1.02/1.10 cnf(520,plain,
% 1.02/1.10 (~P1(x5201,f2(x5201,x5202,a6,a8),x5201)),
% 1.02/1.10 inference(scs_inference,[],[421,474,153,81,83,86,80,75,61])).
% 1.02/1.10 cnf(525,plain,
% 1.02/1.10 (P1(f2(x5251,x5252,x5253,x5253),f2(f2(x5252,x5252,x5254,x5254),f2(x5252,x5252,x5254,x5254),x5255,x5255),x5256)),
% 1.02/1.10 inference(rename_variables,[],[437])).
% 1.02/1.10 cnf(529,plain,
% 1.02/1.10 (~P2(f2(a8,a6,a6,a8),f2(a6,f2(a8,a6,a6,a8),a6,f2(a8,a6,a6,a8)),f2(a6,f2(a8,a6,a6,a8),a6,f2(a8,a6,a6,a8)),a8)),
% 1.02/1.10 inference(scs_inference,[],[421,474,153,437,81,83,86,80,75,61,82,108,84,85])).
% 1.02/1.10 cnf(541,plain,
% 1.02/1.10 (P1(f2(x5411,x5412,x5411,x5412),x5412,x5411)),
% 1.02/1.10 inference(rename_variables,[],[376])).
% 1.02/1.10 cnf(547,plain,
% 1.02/1.10 (P2(x5471,f2(x5472,x5471,x5473,x5474),x5473,x5474)),
% 1.02/1.10 inference(rename_variables,[],[47])).
% 1.02/1.10 cnf(548,plain,
% 1.02/1.10 (P2(x5481,x5482,x5483,f2(f2(x5484,x5483,a6,a8),x5483,x5481,x5482))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(551,plain,
% 1.02/1.10 (P2(x5511,x5512,x5513,f2(f2(x5514,x5513,a6,a8),x5513,x5511,x5512))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(554,plain,
% 1.02/1.10 (P1(f2(x5541,x5542,x5541,x5542),x5542,x5541)),
% 1.02/1.10 inference(rename_variables,[],[376])).
% 1.02/1.10 cnf(559,plain,
% 1.02/1.10 (P2(x5591,x5592,x5593,f2(f2(x5594,x5593,a6,a8),x5593,x5591,x5592))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(562,plain,
% 1.02/1.10 (~E(x5621,f2(f2(x5622,x5621,x5623,x5623),x5624,a6,a8))),
% 1.02/1.10 inference(scs_inference,[],[118,444,421,474,159,153,54,51,548,551,149,47,547,433,437,525,374,346,412,162,263,376,541,81,83,86,80,75,61,82,108,84,85,62,65,63,69,70,90,91,64,33,35,30,32])).
% 1.02/1.10 cnf(564,plain,
% 1.02/1.10 (~P2(f2(x5641,x5642,a6,a8),x5641,x5643,x5643)),
% 1.02/1.10 inference(rename_variables,[],[421])).
% 1.02/1.10 cnf(574,plain,
% 1.02/1.10 (~P1(f2(x5741,x5742,a6,a8),x5741,f2(x5741,x5742,a6,a8))),
% 1.02/1.10 inference(rename_variables,[],[408])).
% 1.02/1.10 cnf(582,plain,
% 1.02/1.10 (~P2(x5821,x5821,x5821,f2(f2(x5822,x5821,x5823,x5823),f2(x5824,x5821,a6,a8),a6,a8))),
% 1.02/1.10 inference(scs_inference,[],[408,574,316,118,444,421,564,474,59,159,153,54,51,548,551,559,149,47,547,433,441,437,525,374,346,412,162,456,263,376,541,554,155,81,83,86,80,75,61,82,108,84,85,62,65,63,69,70,90,91,64,33,35,30,32,34,31,29,71,72,196])).
% 1.02/1.10 cnf(618,plain,
% 1.02/1.10 (~E(x6181,f2(f2(x6182,x6181,x6183,x6183),x6184,a6,a8))),
% 1.02/1.10 inference(rename_variables,[],[562])).
% 1.02/1.10 cnf(623,plain,
% 1.02/1.10 (P1(x6231,x6232,x6232)),
% 1.02/1.10 inference(rename_variables,[],[37])).
% 1.02/1.10 cnf(636,plain,
% 1.02/1.10 (P1(x6361,x6361,x6362)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(639,plain,
% 1.02/1.10 (P2(x6391,f2(x6392,x6391,x6393,f2(x6394,x6395,x6396,x6396)),x6393,x6395)),
% 1.02/1.10 inference(rename_variables,[],[164])).
% 1.02/1.10 cnf(640,plain,
% 1.02/1.10 (P2(x6401,x6402,x6403,f2(f2(x6404,x6403,a6,a8),x6403,x6401,x6402))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(644,plain,
% 1.02/1.10 (P2(x6441,x6442,x6443,f2(f2(x6444,x6443,a6,a8),x6443,x6441,x6442))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(650,plain,
% 1.02/1.10 (P2(x6501,x6502,x6503,f2(f2(x6504,x6503,a6,a8),x6503,x6501,x6502))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(652,plain,
% 1.02/1.10 (E(x6521,f2(f2(x6521,x6522,x6521,x6522),x6522,f2(x6521,x6522,x6521,x6522),x6522))),
% 1.02/1.10 inference(rename_variables,[],[316])).
% 1.02/1.10 cnf(654,plain,
% 1.02/1.10 (P2(x6541,x6542,x6543,f2(f2(x6544,x6543,a6,a8),x6543,x6541,x6542))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(655,plain,
% 1.02/1.10 (~P2(x6551,f2(x6551,x6552,a6,a8),x6553,x6553)),
% 1.02/1.10 inference(rename_variables,[],[518])).
% 1.02/1.10 cnf(659,plain,
% 1.02/1.10 (E(x6591,f2(f2(x6591,x6592,x6591,x6592),x6592,f2(x6591,x6592,x6591,x6592),x6592))),
% 1.02/1.10 inference(rename_variables,[],[316])).
% 1.02/1.10 cnf(665,plain,
% 1.02/1.10 (P1(x6651,x6652,f2(x6651,f2(x6653,x6652,x6654,x6654),x6655,x6656))),
% 1.02/1.10 inference(rename_variables,[],[155])).
% 1.02/1.10 cnf(668,plain,
% 1.02/1.10 (P2(x6681,x6682,x6683,f2(f2(x6684,x6683,a6,a8),x6683,x6681,x6682))),
% 1.02/1.10 inference(rename_variables,[],[51])).
% 1.02/1.10 cnf(675,plain,
% 1.02/1.10 (~P2(x6751,f2(x6751,x6752,a6,a8),x6753,x6753)),
% 1.02/1.10 inference(rename_variables,[],[518])).
% 1.02/1.10 cnf(676,plain,
% 1.02/1.10 (P1(x6761,x6762,x6762)),
% 1.02/1.10 inference(rename_variables,[],[37])).
% 1.02/1.10 cnf(677,plain,
% 1.02/1.10 (P1(x6771,x6771,x6772)),
% 1.02/1.10 inference(rename_variables,[],[38])).
% 1.02/1.10 cnf(682,plain,
% 1.02/1.10 (P1(x6821,x6822,x6822)),
% 1.02/1.10 inference(rename_variables,[],[37])).
% 1.02/1.10 cnf(697,plain,
% 1.02/1.10 ($false),
% 1.02/1.10 inference(scs_inference,[],[60,520,408,316,652,659,518,655,675,582,429,59,469,36,263,37,623,676,682,38,636,677,159,54,373,486,51,640,644,650,654,668,47,164,639,254,257,331,562,618,529,40,41,334,324,124,310,155,665,45,61,86,81,82,83,62,75,4,85,65,70,68,69,64,91,90,32,35,30,34,33,29,31,71,87,72,92,79,96,84,80,99]),
% 1.02/1.10 ['proof']).
% 1.02/1.10 % SZS output end Proof
% 1.02/1.10 % Total time :0.470000s
%------------------------------------------------------------------------------