%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO053-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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:03:32 EDT 2024
% Result : Unsatisfiable 1.10s 1.19s
% Output : CNFRefutation 1.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GEO053-3 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n017.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Jun 21 06:10:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.52/0.63 start to proof:theBenchmark
% 1.00/1.17 %-------------------------------------------
% 1.00/1.17 % File :CSE---1.7
% 1.00/1.17 % Problem :theBenchmark
% 1.00/1.17 % Transform :cnf
% 1.00/1.17 % Format :tptp:raw
% 1.00/1.17 % Command :java -jar mcs_scs.jar %d %s
% 1.00/1.17
% 1.00/1.17 % Result :Theorem 0.490000s
% 1.00/1.17 % Output :CNFRefutation 0.490000s
% 1.00/1.17 %-------------------------------------------
% 1.10/1.17 %--------------------------------------------------------------------------
% 1.10/1.19 % File : GEO053-3 : TPTP v8.2.0. Bugfixed v1.2.1.
% 1.10/1.19 % Domain : Geometry
% 1.10/1.19 % Problem : Unique endpoint
% 1.10/1.19 % Version : [Qua89] axioms : Augmented.
% 1.10/1.19 % English :
% 1.10/1.19
% 1.10/1.19 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 1.10/1.19 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 1.10/1.19 % Source : [Qua89]
% 1.10/1.19 % Names : B15 [Qua89]
% 1.10/1.19
% 1.10/1.19 % Status : Unsatisfiable
% 1.10/1.19 % Rating : 0.05 v8.2.0, 0.10 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.18 v7.3.0, 0.08 v7.1.0, 0.00 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.30 v5.3.0, 0.28 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.11 v2.5.0, 0.18 v2.4.0, 0.12 v2.2.1, 0.14 v2.2.0, 0.00 v2.1.0, 0.25 v2.0.0
% 1.10/1.19 % Syntax : Number of clauses : 85 ( 28 unt; 20 nHn; 63 RR)
% 1.10/1.19 % Number of literals : 233 ( 47 equ; 131 neg)
% 1.10/1.19 % Maximal clause size : 8 ( 2 avg)
% 1.10/1.19 % Maximal term depth : 3 ( 1 avg)
% 1.10/1.19 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 1.10/1.19 % Number of functors : 13 ( 13 usr; 6 con; 0-6 aty)
% 1.10/1.19 % Number of variables : 302 ( 14 sgn)
% 1.10/1.19 % SPC : CNF_UNS_RFO_SEQ_NHN
% 1.10/1.19
% 1.10/1.19 % Comments :
% 1.10/1.19 % Bugfixes : v1.2.1 - Clause d12 fixed.
% 1.10/1.19 %--------------------------------------------------------------------------
% 1.10/1.19 %----Include Tarski geometry axioms
% 1.10/1.19 include('Axioms/GEO002-0.ax').
% 1.10/1.19 %----Include definition of reflection
% 1.10/1.19 include('Axioms/GEO002-2.ax').
% 1.10/1.19 %----Include definition of insertion
% 1.10/1.19 include('Axioms/GEO002-3.ax').
% 1.10/1.19 %--------------------------------------------------------------------------
% 1.10/1.19 cnf(d1,axiom,
% 1.10/1.19 equidistant(U,V,U,V) ).
% 1.10/1.19
% 1.10/1.19 cnf(d2,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(W,X,U,V) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d3,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(V,U,W,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d4_1,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(U,V,X,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d4_2,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(V,U,X,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d4_3,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(W,X,V,U) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d4_4,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(X,W,U,V) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d4_5,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | equidistant(X,W,V,U) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d5,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,W,X)
% 1.10/1.19 | ~ equidistant(W,X,Y,Z)
% 1.10/1.19 | equidistant(U,V,Y,Z) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(e1,axiom,
% 1.10/1.19 V = extension(U,V,W,W) ).
% 1.10/1.19
% 1.10/1.19 cnf(b0,axiom,
% 1.10/1.19 ( Y != extension(U,V,W,X)
% 1.10/1.19 | between(U,V,Y) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(r2_1,axiom,
% 1.10/1.19 between(U,V,reflection(U,V)) ).
% 1.10/1.19
% 1.10/1.19 cnf(r2_2,axiom,
% 1.10/1.19 equidistant(V,reflection(U,V),U,V) ).
% 1.10/1.19
% 1.10/1.19 cnf(r3_1,axiom,
% 1.10/1.19 ( U != V
% 1.10/1.19 | V = reflection(U,V) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(r3_2,axiom,
% 1.10/1.19 U = reflection(U,U) ).
% 1.10/1.19
% 1.10/1.19 cnf(r4,axiom,
% 1.10/1.19 ( V != reflection(U,V)
% 1.10/1.19 | U = V ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d7,axiom,
% 1.10/1.19 equidistant(U,U,V,V) ).
% 1.10/1.19
% 1.10/1.19 cnf(d8,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,U1,V1)
% 1.10/1.19 | ~ equidistant(V,W,V1,W1)
% 1.10/1.19 | ~ between(U,V,W)
% 1.10/1.19 | ~ between(U1,V1,W1)
% 1.10/1.19 | equidistant(U,W,U1,W1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d9,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,V,X)
% 1.10/1.19 | ~ equidistant(V,W,V,X)
% 1.10/1.19 | U = V
% 1.10/1.19 | W = X ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d10_1,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | U = V
% 1.10/1.19 | W = extension(U,V,V,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d10_2,axiom,
% 1.10/1.19 ( ~ equidistant(W,X,Y,Z)
% 1.10/1.19 | extension(U,V,W,X) = extension(U,V,Y,Z)
% 1.10/1.19 | U = V ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d10_3,axiom,
% 1.10/1.19 ( extension(U,V,U,V) = extension(U,V,V,U)
% 1.10/1.19 | U = V ) ).
% 1.10/1.19
% 1.10/1.19 cnf(r5,axiom,
% 1.10/1.19 equidistant(V,U,V,reflection(reflection(U,V),V)) ).
% 1.10/1.19
% 1.10/1.19 cnf(r6,axiom,
% 1.10/1.19 U = reflection(reflection(U,V),V) ).
% 1.10/1.19
% 1.10/1.19 cnf(t3,axiom,
% 1.10/1.19 between(U,V,V) ).
% 1.10/1.19
% 1.10/1.19 cnf(b1,axiom,
% 1.10/1.19 ( ~ between(U,W,X)
% 1.10/1.19 | U != X
% 1.10/1.19 | between(V,W,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t1,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | between(W,V,U) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t2,axiom,
% 1.10/1.19 between(U,U,V) ).
% 1.10/1.19
% 1.10/1.19 cnf(b2,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(V,U,W)
% 1.10/1.19 | U = V ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b3,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,W,V)
% 1.10/1.19 | V = W ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t6_1,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(V,U,W)
% 1.10/1.19 | U = V
% 1.10/1.19 | V = W ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t6_2,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,W,V)
% 1.10/1.19 | U = V
% 1.10/1.19 | V = W ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b4,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | between(U,V,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b5,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,W,X)
% 1.10/1.19 | between(V,W,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b6,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | between(U,W,X)
% 1.10/1.19 | V = W ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b7,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | between(U,V,X)
% 1.10/1.19 | V = W ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b8,axiom,
% 1.10/1.19 ( ~ between(U,V,X)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | between(U,W,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b9,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,W,X)
% 1.10/1.19 | between(U,V,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(e2_1,axiom,
% 1.10/1.19 lower_dimension_point_1 != lower_dimension_point_2 ).
% 1.10/1.19
% 1.10/1.19 cnf(e2_2,axiom,
% 1.10/1.19 lower_dimension_point_2 != lower_dimension_point_3 ).
% 1.10/1.19
% 1.10/1.19 cnf(e2_3,axiom,
% 1.10/1.19 lower_dimension_point_1 != lower_dimension_point_3 ).
% 1.10/1.19
% 1.10/1.19 cnf(e3_1,axiom,
% 1.10/1.19 V != extension(U,V,lower_dimension_point_1,lower_dimension_point_2) ).
% 1.10/1.19
% 1.10/1.19 cnf(e3_2,axiom,
% 1.10/1.19 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.10/1.19
% 1.10/1.19 cnf(e3_3,axiom,
% 1.10/1.19 between(U,V,extension(U,V,lower_dimension_point_1,lower_dimension_point_2)) ).
% 1.10/1.19
% 1.10/1.19 cnf(b10,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U1,V1,W)
% 1.10/1.19 | ~ between(U,X,U1)
% 1.10/1.19 | between(X,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),W)
% 1.10/1.19 | between(V,inner_pasch(V1,inner_pasch(U,X,U1,V1,W),U,V,W),V1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d11,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ equidistant(U,W,U,W1)
% 1.10/1.19 | ~ equidistant(V,W,V,W1)
% 1.10/1.19 | U = V
% 1.10/1.19 | W = W1 ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d12,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,U1,V1)
% 1.10/1.19 | ~ equidistant(U,W,U1,W1)
% 1.10/1.19 | ~ equidistant(U,X,U1,X1)
% 1.10/1.19 | ~ equidistant(W,X,W1,X1)
% 1.10/1.19 | ~ between(U,V,W)
% 1.10/1.19 | ~ between(U1,V1,W1)
% 1.10/1.19 | equidistant(V,X,V1,X1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d13,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U1,V1,W1)
% 1.10/1.19 | ~ equidistant(U,V,U1,V1)
% 1.10/1.19 | ~ equidistant(U,W,U1,W1)
% 1.10/1.19 | equidistant(V,W,V1,W1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d14,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,U1,V1)
% 1.10/1.19 | ~ equidistant(V,W,V1,W1)
% 1.10/1.19 | ~ equidistant(U,X,U1,X1)
% 1.10/1.19 | ~ equidistant(W,X,W1,X1)
% 1.10/1.19 | ~ between(U,V,W)
% 1.10/1.19 | ~ between(U1,V1,W1)
% 1.10/1.19 | equidistant(V,X,V1,X1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(d15,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ equidistant(U,V,U,X)
% 1.10/1.19 | ~ equidistant(W,V,W,X)
% 1.10/1.19 | V = X ) ).
% 1.10/1.19
% 1.10/1.19 cnf(i2_1,axiom,
% 1.10/1.19 equidistant(U,V,U1,insertion(U1,W1,U,V)) ).
% 1.10/1.19
% 1.10/1.19 cnf(i2_2,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ equidistant(U,W,U1,W1)
% 1.10/1.19 | between(U1,insertion(U1,W1,U,V),W1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(i2_3,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ equidistant(U,W,U1,W1)
% 1.10/1.19 | equidistant(V,W,insertion(U1,W1,U,V),W1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(i3,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | V = insertion(U,W,U,V) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(i4,axiom,
% 1.10/1.19 ( ~ equidistant(W,X,Y,Z)
% 1.10/1.19 | insertion(U,V,W,X) = insertion(U,V,Y,Z) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b11,axiom,
% 1.10/1.19 ( ~ equidistant(U,V,U1,V1)
% 1.10/1.19 | ~ equidistant(V,W,V1,W1)
% 1.10/1.19 | ~ equidistant(U,W,U1,W1)
% 1.10/1.19 | ~ between(U,V,W)
% 1.10/1.19 | between(U1,V1,W1) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b12,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,V,X)
% 1.10/1.19 | U = V
% 1.10/1.19 | between(U,W,X)
% 1.10/1.19 | between(U,X,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b13,axiom,
% 1.10/1.19 ( ~ between(U,V,W)
% 1.10/1.19 | ~ between(U,V,X)
% 1.10/1.19 | U = V
% 1.10/1.19 | between(V,W,X)
% 1.10/1.19 | between(V,X,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t7,axiom,
% 1.10/1.19 ( ~ between(U,W,X)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | W = X
% 1.10/1.19 | between(U,V,W)
% 1.10/1.19 | between(V,U,W) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t9,axiom,
% 1.10/1.19 ( ~ between(U,V,X)
% 1.10/1.19 | ~ between(U,W,X)
% 1.10/1.19 | between(U,V,W)
% 1.10/1.19 | between(U,W,V) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(b14,axiom,
% 1.10/1.19 ( ~ between(U,V,X)
% 1.10/1.19 | ~ between(U,W,X)
% 1.10/1.19 | between(V,W,X)
% 1.10/1.19 | between(W,V,X) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(t8,axiom,
% 1.10/1.19 ( ~ between(U,V,Y)
% 1.10/1.19 | ~ between(V,W,X)
% 1.10/1.19 | ~ between(U,X,Y)
% 1.10/1.19 | between(U,W,Y) ) ).
% 1.10/1.19
% 1.10/1.19 cnf(v_between_u_and_w,hypothesis,
% 1.10/1.19 between(u,v,w) ).
% 1.10/1.19
% 1.10/1.19 cnf(u_to_v_equals_u_to_w,hypothesis,
% 1.10/1.19 equidistant(u,v,u,w) ).
% 1.10/1.19
% 1.10/1.19 cnf(prove_v_equals_w,negated_conjecture,
% 1.10/1.19 v != w ).
% 1.10/1.19
% 1.10/1.19 %--------------------------------------------------------------------------
% 1.10/1.19 %-------------------------------------------
% 1.10/1.19 % Proof found
% 1.10/1.19 % SZS status Theorem for theBenchmark
% 1.10/1.19 % SZS output start Proof
% 1.10/1.19 %ClaNum:117(EqnAxiom:35)
% 1.10/1.19 %VarNum:783(SingletonVarNum:279)
% 1.10/1.19 %MaxLitNum:8
% 1.10/1.19 %MaxfuncDepth:2
% 1.10/1.19 %SharedTerms:15
% 1.10/1.19 %goalClause: 57
% 1.10/1.19 %singleGoalClaCount:1
% 1.10/1.19 [36]P1(a1,a10,a11)
% 1.10/1.19 [39]P2(a1,a10,a1,a11)
% 1.10/1.19 [54]~E(a8,a6)
% 1.10/1.19 [55]~E(a9,a6)
% 1.10/1.19 [56]~E(a9,a8)
% 1.10/1.19 [57]~E(a11,a10)
% 1.10/1.19 [58]~P1(a6,a8,a9)
% 1.10/1.19 [59]~P1(a8,a9,a6)
% 1.10/1.19 [60]~P1(a9,a6,a8)
% 1.10/1.19 [37]P1(x371,x372,x372)
% 1.10/1.19 [38]P1(x381,x381,x382)
% 1.10/1.19 [40]P2(x401,x402,x402,x401)
% 1.10/1.19 [41]P2(x411,x412,x411,x412)
% 1.10/1.19 [42]P2(x421,x421,x422,x422)
% 1.10/1.19 [61]~E(f2(x611,x612,a6,a8),x612)
% 1.10/1.19 [51]E(f2(f2(x511,x512,x511,x512),x512,f2(x511,x512,x511,x512),x512),x511)
% 1.10/1.19 [53]P2(x531,x532,x531,f2(f2(x532,x531,x532,x531),x531,f2(x532,x531,x532,x531),x531))
% 1.10/1.19 [43]E(f2(x431,x432,x433,x433),x432)
% 1.10/1.19 [46]P1(x461,x462,f2(x461,x462,x463,x464))
% 1.10/1.19 [48]P2(x481,f2(x482,x481,x483,x484),x483,x484)
% 1.10/1.19 [50]P2(x501,f2(x502,x501,a6,a8),x503,f2(x504,x503,a6,a8))
% 1.10/1.19 [52]P2(x521,x522,x523,f2(f2(x524,x523,a6,a8),x523,x521,x522))
% 1.10/1.19 [62]~P1(x621,x622,x621)+E(x621,x622)
% 1.10/1.19 [74]~E(x741,x742)+E(f2(x741,x742,x741,x742),x742)
% 1.10/1.19 [83]E(x831,x832)+~E(f2(x832,x831,x832,x831),x831)
% 1.10/1.19 [85]E(x851,x852)+E(f2(x851,x852,x851,x852),f2(x851,x852,x852,x851))
% 1.10/1.19 [63]~P1(x633,x632,x631)+P1(x631,x632,x633)
% 1.10/1.19 [82]~P2(x821,x822,x823,x823)+E(x821,x822)
% 1.10/1.19 [94]~P1(x942,x943,x941)+E(f2(f2(x941,x942,a6,a8),x942,x942,x943),x943)
% 1.10/1.19 [87]~P2(x874,x873,x872,x871)+P2(x871,x872,x873,x874)
% 1.10/1.19 [88]~P2(x883,x884,x882,x881)+P2(x881,x882,x883,x884)
% 1.10/1.19 [89]~P2(x894,x893,x891,x892)+P2(x891,x892,x893,x894)
% 1.10/1.19 [90]~P2(x903,x904,x901,x902)+P2(x901,x902,x903,x904)
% 1.10/1.19 [91]~P2(x912,x911,x914,x913)+P2(x911,x912,x913,x914)
% 1.10/1.19 [92]~P2(x922,x921,x923,x924)+P2(x921,x922,x923,x924)
% 1.10/1.19 [93]~P2(x931,x932,x934,x933)+P2(x931,x932,x933,x934)
% 1.10/1.19 [84]P1(x841,x842,x843)+~E(x843,f2(x841,x842,x844,x845))
% 1.10/1.19 [104]~P2(x1043,x1044,x1045,x1046)+E(f2(f2(x1041,x1042,a6,a8),x1042,x1043,x1044),f2(f2(x1041,x1042,a6,a8),x1042,x1045,x1046))
% 1.10/1.19 [65]~P1(x653,x651,x652)+E(x651,x652)+~P1(x653,x652,x651)
% 1.10/1.19 [66]~P1(x661,x662,x663)+E(x661,x662)+~P1(x662,x661,x663)
% 1.10/1.19 [81]~P1(x811,x812,x813)+E(x811,x812)+E(f2(x811,x812,x812,x813),x813)
% 1.10/1.19 [64]~P1(x644,x642,x643)+P1(x641,x642,x643)+~E(x644,x643)
% 1.10/1.19 [69]~P1(x694,x691,x692)+P1(x691,x692,x693)+~P1(x694,x692,x693)
% 1.10/1.19 [70]~P1(x701,x704,x703)+P1(x701,x702,x703)+~P1(x704,x702,x703)
% 1.10/1.19 [71]~P1(x711,x712,x714)+P1(x711,x712,x713)+~P1(x711,x714,x713)
% 1.10/1.19 [110]~P1(x1105,x1101,x1104)+~P1(x1102,x1103,x1104)+P1(x1101,f7(x1102,x1103,x1104,x1101,x1105),x1102)
% 1.10/1.19 [111]~P1(x1115,x1114,x1113)+~P1(x1112,x1111,x1113)+P1(x1111,f7(x1112,x1111,x1113,x1114,x1115),x1115)
% 1.10/1.19 [108]~P2(x1083,x1085,x1081,x1082)+~P1(x1083,x1084,x1085)+P1(x1081,f2(f2(x1082,x1081,a6,a8),x1081,x1083,x1084),x1082)
% 1.10/1.19 [109]~P1(x1095,x1091,x1092)+~P2(x1095,x1092,x1094,x1093)+P2(x1091,x1092,f2(f2(x1093,x1094,a6,a8),x1094,x1095,x1091),x1093)
% 1.10/1.19 [98]~P2(x985,x986,x981,x982)+P2(x981,x982,x983,x984)+~P2(x985,x986,x983,x984)
% 1.10/1.19 [99]~P2(x991,x992,x995,x996)+P2(x991,x992,x993,x994)+~P2(x995,x996,x993,x994)
% 1.10/1.19 [97]~P2(x973,x974,x975,x976)+E(x971,x972)+E(f2(x971,x972,x973,x974),f2(x971,x972,x975,x976))
% 1.10/1.19 [72]~P1(x721,x722,x724)+~P1(x723,x721,x722)+E(x721,x722)+P1(x723,x722,x724)
% 1.10/1.19 [73]~P1(x731,x732,x734)+~P1(x733,x731,x732)+E(x731,x732)+P1(x733,x731,x734)
% 1.10/1.19 [75]P1(x752,x751,x753)+~P1(x754,x752,x753)+P1(x751,x752,x753)+~P1(x754,x751,x753)
% 1.10/1.19 [76]P1(x761,x763,x762)+~P1(x761,x763,x764)+P1(x761,x762,x763)+~P1(x761,x762,x764)
% 1.10/1.19 [95]~P2(x954,x951,x954,x952)+~P2(x953,x951,x953,x952)+E(x951,x952)+~P1(x953,x951,x954)
% 1.10/1.19 [80]~P1(x801,x805,x803)+~P1(x801,x804,x803)+P1(x801,x802,x803)+~P1(x804,x802,x805)
% 1.10/1.19 [112]~P1(x1124,x1122,x1123)+~P1(x1121,x1122,x1125)+E(x1121,x1122)+P1(x1121,x1123,f3(x1121,x1124,x1122,x1123,x1125))
% 1.10/1.19 [113]~P1(x1133,x1132,x1134)+~P1(x1131,x1132,x1135)+E(x1131,x1132)+P1(x1131,x1133,f4(x1131,x1133,x1132,x1134,x1135))
% 1.10/1.19 [114]~P1(x1143,x1142,x1144)+~P1(x1141,x1142,x1145)+E(x1141,x1142)+P1(f4(x1141,x1143,x1142,x1144,x1145),x1145,f3(x1141,x1143,x1142,x1144,x1145))
% 1.10/1.19 [77]P1(x774,x773,x771)+~P1(x773,x771,x772)+~P1(x774,x771,x772)+E(x771,x772)+P1(x773,x774,x771)
% 1.10/1.19 [78]P1(x782,x784,x783)+~P1(x781,x782,x783)+~P1(x781,x782,x784)+E(x781,x782)+P1(x782,x783,x784)
% 1.10/1.19 [79]P1(x791,x794,x793)+~P1(x791,x792,x793)+~P1(x791,x792,x794)+E(x791,x792)+P1(x791,x793,x794)
% 1.10/1.19 [86]~P1(x863,x864,x862)+~P1(x863,x864,x861)+~P2(x864,x861,x864,x862)+E(x861,x862)+E(x863,x864)
% 1.10/1.19 [96]~P1(x963,x964,x961)+~P2(x964,x961,x964,x962)+~P2(x963,x961,x963,x962)+E(x961,x962)+E(x963,x964)
% 1.10/1.19 [100]~P2(x1006,x1002,x1005,x1004)+~P2(x1006,x1001,x1005,x1003)+P2(x1001,x1002,x1003,x1004)+~P1(x1005,x1003,x1004)+~P1(x1006,x1001,x1002)
% 1.10/1.19 [101]~P2(x1016,x1012,x1015,x1014)+~P2(x1011,x1016,x1013,x1015)+P2(x1011,x1012,x1013,x1014)+~P1(x1013,x1015,x1014)+~P1(x1011,x1016,x1012)
% 1.10/1.19 [102]~P2(x1025,x1026,x1022,x1023)+~P2(x1024,x1026,x1021,x1023)+~P2(x1024,x1025,x1021,x1022)+P1(x1021,x1022,x1023)+~P1(x1024,x1025,x1026)
% 1.10/1.19 [115]~P1(x1153,x1154,x1155)+~P1(x1152,x1153,x1155)+~P2(x1152,x1155,x1152,x1156)+~P2(x1152,x1153,x1152,x1151)+P1(x1151,f5(x1152,x1153,x1151,x1154,x1155,x1156),x1156)
% 1.10/1.19 [116]~P1(x1163,x1162,x1165)+~P1(x1161,x1163,x1165)+~P2(x1161,x1165,x1161,x1166)+~P2(x1161,x1163,x1161,x1164)+P2(x1161,x1162,x1161,f5(x1161,x1163,x1164,x1162,x1165,x1166))
% 1.10/1.19 [117]~P1(x1174,x1172,x1175)+~P1(x1173,x1171,x1174)+~P1(x1173,x1176,x1175)+P1(x1171,f7(x1172,f7(x1173,x1171,x1174,x1172,x1175),x1173,x1176,x1175),x1175)+P1(x1176,f7(x1172,f7(x1173,x1171,x1174,x1172,x1175),x1173,x1176,x1175),x1172)
% 1.10/1.19 [103]P1(x1035,x1033,x1034)+P1(x1034,x1035,x1033)+~P2(x1033,x1031,x1033,x1032)+~P2(x1035,x1031,x1035,x1032)+~P2(x1034,x1031,x1034,x1032)+E(x1031,x1032)+P1(x1033,x1034,x1035)
% 1.10/1.19 [105]~P2(x1058,x1052,x1056,x1054)+~P2(x1051,x1058,x1053,x1056)+~P2(x1057,x1052,x1055,x1054)+~P2(x1057,x1051,x1055,x1053)+P2(x1051,x1052,x1053,x1054)+~P1(x1055,x1053,x1056)+~P1(x1057,x1051,x1058)
% 1.10/1.19 [106]~P2(x1068,x1062,x1066,x1064)+~P2(x1067,x1062,x1065,x1064)+~P2(x1067,x1068,x1065,x1066)+~P2(x1067,x1061,x1065,x1063)+P2(x1061,x1062,x1063,x1064)+~P1(x1065,x1063,x1066)+~P1(x1067,x1061,x1068)
% 1.10/1.19 [107]~P1(x1071,x1072,x1073)+~P2(x1072,x1074,x1078,x1076)+~P2(x1072,x1073,x1078,x1075)+~P2(x1071,x1074,x1077,x1076)+~P2(x1071,x1072,x1077,x1078)+E(x1071,x1072)+P2(x1073,x1074,x1075,x1076)+~P1(x1077,x1078,x1075)
% 1.10/1.19 %EqnAxiom
% 1.10/1.19 [1]E(x11,x11)
% 1.10/1.19 [2]E(x22,x21)+~E(x21,x22)
% 1.10/1.19 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.10/1.19 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45))
% 1.10/1.19 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55))
% 1.10/1.19 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65))
% 1.10/1.19 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72))
% 1.10/1.19 [8]~E(x81,x82)+E(f7(x81,x83,x84,x85,x86),f7(x82,x83,x84,x85,x86))
% 1.10/1.19 [9]~E(x91,x92)+E(f7(x93,x91,x94,x95,x96),f7(x93,x92,x94,x95,x96))
% 1.10/1.19 [10]~E(x101,x102)+E(f7(x103,x104,x101,x105,x106),f7(x103,x104,x102,x105,x106))
% 1.10/1.19 [11]~E(x111,x112)+E(f7(x113,x114,x115,x111,x116),f7(x113,x114,x115,x112,x116))
% 1.10/1.19 [12]~E(x121,x122)+E(f7(x123,x124,x125,x126,x121),f7(x123,x124,x125,x126,x122))
% 1.10/1.19 [13]~E(x131,x132)+E(f3(x131,x133,x134,x135,x136),f3(x132,x133,x134,x135,x136))
% 1.10/1.19 [14]~E(x141,x142)+E(f3(x143,x141,x144,x145,x146),f3(x143,x142,x144,x145,x146))
% 1.10/1.19 [15]~E(x151,x152)+E(f3(x153,x154,x151,x155,x156),f3(x153,x154,x152,x155,x156))
% 1.10/1.19 [16]~E(x161,x162)+E(f3(x163,x164,x165,x161,x166),f3(x163,x164,x165,x162,x166))
% 1.10/1.19 [17]~E(x171,x172)+E(f3(x173,x174,x175,x176,x171),f3(x173,x174,x175,x176,x172))
% 1.10/1.19 [18]~E(x181,x182)+E(f4(x181,x183,x184,x185,x186),f4(x182,x183,x184,x185,x186))
% 1.10/1.19 [19]~E(x191,x192)+E(f4(x193,x191,x194,x195,x196),f4(x193,x192,x194,x195,x196))
% 1.10/1.19 [20]~E(x201,x202)+E(f4(x203,x204,x201,x205,x206),f4(x203,x204,x202,x205,x206))
% 1.10/1.19 [21]~E(x211,x212)+E(f4(x213,x214,x215,x211,x216),f4(x213,x214,x215,x212,x216))
% 1.10/1.19 [22]~E(x221,x222)+E(f4(x223,x224,x225,x226,x221),f4(x223,x224,x225,x226,x222))
% 1.10/1.19 [23]~E(x231,x232)+E(f5(x231,x233,x234,x235,x236,x237),f5(x232,x233,x234,x235,x236,x237))
% 1.10/1.19 [24]~E(x241,x242)+E(f5(x243,x241,x244,x245,x246,x247),f5(x243,x242,x244,x245,x246,x247))
% 1.10/1.19 [25]~E(x251,x252)+E(f5(x253,x254,x251,x255,x256,x257),f5(x253,x254,x252,x255,x256,x257))
% 1.10/1.19 [26]~E(x261,x262)+E(f5(x263,x264,x265,x261,x266,x267),f5(x263,x264,x265,x262,x266,x267))
% 1.10/1.19 [27]~E(x271,x272)+E(f5(x273,x274,x275,x276,x271,x277),f5(x273,x274,x275,x276,x272,x277))
% 1.10/1.19 [28]~E(x281,x282)+E(f5(x283,x284,x285,x286,x287,x281),f5(x283,x284,x285,x286,x287,x282))
% 1.10/1.19 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 1.10/1.19 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 1.10/1.19 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 1.10/1.19 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 1.10/1.19 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 1.10/1.19 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 1.10/1.19 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 1.10/1.19
% 1.10/1.19 %-------------------------------------------
% 1.10/1.19 cnf(118,plain,
% 1.10/1.19 (~P1(x1181,x1182,x1181)+P1(x1183,x1182,x1181)),
% 1.10/1.19 inference(equality_inference,[],[64])).
% 1.10/1.19 cnf(121,plain,
% 1.10/1.19 (~P1(a11,a10,a11)),
% 1.10/1.19 inference(scs_inference,[],[57,62])).
% 1.10/1.19 cnf(123,plain,
% 1.10/1.19 (~P2(a11,a10,x1231,x1231)),
% 1.10/1.19 inference(scs_inference,[],[57,62,82])).
% 1.10/1.19 cnf(128,plain,
% 1.10/1.19 (E(x1281,f2(x1282,x1281,x1283,x1283))),
% 1.10/1.19 inference(scs_inference,[],[57,43,51,62,82,83,2])).
% 1.10/1.19 cnf(129,plain,
% 1.10/1.19 (~P1(a9,a8,a6)),
% 1.10/1.19 inference(scs_inference,[],[57,43,58,51,62,82,83,2,63])).
% 1.10/1.19 cnf(131,plain,
% 1.10/1.19 (~E(a6,a8)),
% 1.10/1.19 inference(scs_inference,[],[57,43,61,58,51,62,82,83,2,63,74])).
% 1.10/1.19 cnf(132,plain,
% 1.10/1.19 (~E(f2(x1321,x1322,a6,a8),x1322)),
% 1.10/1.19 inference(rename_variables,[],[61])).
% 1.10/1.19 cnf(134,plain,
% 1.10/1.19 (P1(x1341,x1342,f2(x1343,f2(x1341,x1342,x1344,x1345),x1346,x1346))),
% 1.10/1.19 inference(scs_inference,[],[57,43,61,58,51,62,82,83,2,63,74,84])).
% 1.10/1.19 cnf(135,plain,
% 1.10/1.19 (E(f2(x1351,x1352,x1353,x1353),x1352)),
% 1.10/1.19 inference(rename_variables,[],[43])).
% 1.10/1.19 cnf(143,plain,
% 1.10/1.19 (~P1(a10,a11,a10)),
% 1.10/1.19 inference(scs_inference,[],[57,38,43,61,58,51,62,82,83,2,63,74,84,87,88,89,65])).
% 1.10/1.19 cnf(146,plain,
% 1.10/1.19 (~P1(f2(x1461,x1462,a6,a8),x1462,f2(x1461,x1462,a6,a8))),
% 1.10/1.19 inference(scs_inference,[],[57,37,38,43,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66])).
% 1.10/1.19 cnf(148,plain,
% 1.10/1.19 (P1(x1481,x1482,x1482)),
% 1.10/1.19 inference(rename_variables,[],[37])).
% 1.10/1.19 cnf(151,plain,
% 1.10/1.19 (E(f2(x1511,x1512,x1513,x1513),x1512)),
% 1.10/1.19 inference(rename_variables,[],[43])).
% 1.10/1.19 cnf(152,plain,
% 1.10/1.19 (P2(f2(x1521,x1522,x1523,x1524),x1522,x1523,x1524)),
% 1.10/1.19 inference(scs_inference,[],[57,40,37,38,48,43,135,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98])).
% 1.10/1.19 cnf(153,plain,
% 1.10/1.19 (P2(x1531,f2(x1532,x1531,x1533,x1534),x1533,x1534)),
% 1.10/1.19 inference(rename_variables,[],[48])).
% 1.10/1.19 cnf(154,plain,
% 1.10/1.19 (P2(x1541,x1542,x1542,x1541)),
% 1.10/1.19 inference(rename_variables,[],[40])).
% 1.10/1.19 cnf(156,plain,
% 1.10/1.19 (P2(f2(x1561,x1562,a6,a8),x1562,x1563,f2(x1564,x1563,a6,a8))),
% 1.10/1.19 inference(scs_inference,[],[57,40,154,37,38,48,50,43,135,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99])).
% 1.10/1.19 cnf(158,plain,
% 1.10/1.19 (P2(x1581,x1582,x1582,x1581)),
% 1.10/1.19 inference(rename_variables,[],[40])).
% 1.10/1.19 cnf(160,plain,
% 1.10/1.19 (~E(x1601,f2(x1601,x1602,a6,a8))),
% 1.10/1.19 inference(scs_inference,[],[57,40,154,37,38,48,46,50,43,135,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29])).
% 1.10/1.19 cnf(161,plain,
% 1.10/1.19 (P1(x1611,x1612,f2(x1611,x1612,x1613,x1614))),
% 1.10/1.19 inference(rename_variables,[],[46])).
% 1.10/1.19 cnf(162,plain,
% 1.10/1.19 (P1(x1621,x1622,f2(x1621,f2(x1623,x1622,x1624,x1624),x1625,x1626))),
% 1.10/1.19 inference(scs_inference,[],[57,40,154,37,38,48,46,161,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30])).
% 1.10/1.19 cnf(163,plain,
% 1.10/1.19 (P1(x1631,x1632,f2(x1631,x1632,x1633,x1634))),
% 1.10/1.19 inference(rename_variables,[],[46])).
% 1.10/1.19 cnf(165,plain,
% 1.10/1.19 (P1(x1651,x1652,x1652)),
% 1.10/1.19 inference(rename_variables,[],[37])).
% 1.10/1.19 cnf(166,plain,
% 1.10/1.19 (~E(a10,a11)),
% 1.10/1.19 inference(scs_inference,[],[57,40,154,158,37,148,38,48,46,161,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32])).
% 1.10/1.20 cnf(169,plain,
% 1.10/1.20 (P2(x1691,f2(x1692,x1691,x1693,x1694),x1693,x1694)),
% 1.10/1.20 inference(rename_variables,[],[48])).
% 1.10/1.20 cnf(170,plain,
% 1.10/1.20 (P2(x1701,f2(x1702,x1701,f2(x1703,x1704,x1705,x1705),x1706),x1704,x1706)),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,37,148,38,48,153,169,46,161,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34])).
% 1.10/1.20 cnf(171,plain,
% 1.10/1.20 (P2(x1711,f2(x1712,x1711,x1713,x1714),x1713,x1714)),
% 1.10/1.20 inference(rename_variables,[],[48])).
% 1.10/1.20 cnf(172,plain,
% 1.10/1.20 (P2(x1721,f2(x1722,x1721,x1723,f2(x1724,x1725,x1726,x1726)),x1723,x1725)),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,37,148,38,48,153,169,171,46,161,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34,35])).
% 1.10/1.20 cnf(174,plain,
% 1.10/1.20 (~P1(f2(a11,f2(x1741,a10,x1742,x1742),a6,a8),a11,f2(x1741,a10,x1742,x1742))),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,37,148,38,48,153,169,171,46,161,163,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34,35,72])).
% 1.10/1.20 cnf(175,plain,
% 1.10/1.20 (P1(x1751,x1752,f2(x1751,x1752,x1753,x1754))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(177,plain,
% 1.10/1.20 (E(f2(a11,a10,f2(x1771,a10,x1772,x1772),a10),a10)),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,37,148,165,38,48,153,169,171,46,161,163,175,50,43,135,151,61,132,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34,35,72,86])).
% 1.10/1.20 cnf(178,plain,
% 1.10/1.20 (P1(x1781,x1782,x1782)),
% 1.10/1.20 inference(rename_variables,[],[37])).
% 1.10/1.20 cnf(179,plain,
% 1.10/1.20 (P1(x1791,x1792,f2(x1791,x1792,x1793,x1794))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(186,plain,
% 1.10/1.20 (~P2(a11,a11,a10,f2(a1,a10,a11,a10))),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,41,37,148,165,178,38,48,153,169,171,46,161,163,175,179,50,43,135,151,61,132,39,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34,35,72,86,105,90])).
% 1.10/1.20 cnf(190,plain,
% 1.10/1.20 (~P2(a11,a11,f2(a1,a10,a11,a10),a10)),
% 1.10/1.20 inference(scs_inference,[],[57,40,154,158,41,37,148,165,178,38,48,153,169,171,46,161,163,175,179,50,43,135,151,61,132,39,58,51,62,82,83,2,63,74,84,87,88,89,65,66,3,98,99,29,30,31,32,33,34,35,72,86,105,90,91,93])).
% 1.10/1.20 cnf(204,plain,
% 1.10/1.20 (~P1(x2041,f2(x2041,x2042,a6,a8),x2041)),
% 1.10/1.20 inference(scs_inference,[],[160,62])).
% 1.10/1.20 cnf(206,plain,
% 1.10/1.20 (E(a10,f2(a11,a10,f2(x2061,a10,x2062,x2062),a10))),
% 1.10/1.20 inference(scs_inference,[],[177,160,62,2])).
% 1.10/1.20 cnf(207,plain,
% 1.10/1.20 (~P2(x2071,f2(x2071,x2072,a6,a8),x2073,x2073)),
% 1.10/1.20 inference(scs_inference,[],[177,160,62,2,82])).
% 1.10/1.20 cnf(209,plain,
% 1.10/1.20 (~P1(f2(x2091,a10,x2092,x2092),a11,f2(a11,f2(x2091,a10,x2092,x2092),a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[174,177,160,62,2,82,63])).
% 1.10/1.20 cnf(211,plain,
% 1.10/1.20 (~P2(x2111,x2111,x2112,f2(x2112,x2113,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[174,177,160,62,2,82,63,89])).
% 1.10/1.20 cnf(213,plain,
% 1.10/1.20 (P1(x2131,x2132,f2(x2131,f2(x2133,f2(x2131,x2132,x2134,x2135),x2136,x2136),x2137,x2138))),
% 1.10/1.20 inference(scs_inference,[],[174,177,134,160,46,62,2,82,63,89,71])).
% 1.10/1.20 cnf(214,plain,
% 1.10/1.20 (P1(x2141,x2142,f2(x2141,x2142,x2143,x2144))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(216,plain,
% 1.10/1.20 (P1(x2161,f2(x2161,x2162,x2163,x2164),f2(x2162,f2(x2161,x2162,x2163,x2164),x2165,x2165))),
% 1.10/1.20 inference(scs_inference,[],[174,177,134,160,46,214,62,2,82,63,89,71,70])).
% 1.10/1.20 cnf(217,plain,
% 1.10/1.20 (P1(x2171,x2172,f2(x2171,x2172,x2173,x2174))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(218,plain,
% 1.10/1.20 (P1(x2181,x2182,f2(x2183,f2(x2181,x2182,x2184,x2185),x2186,x2186))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(220,plain,
% 1.10/1.20 (P1(x2201,x2202,f2(f2(x2203,x2202,x2204,x2204),f2(x2203,x2202,x2204,x2204),x2205,x2205))),
% 1.10/1.20 inference(scs_inference,[],[128,174,177,134,162,160,46,214,62,2,82,63,89,71,70,64])).
% 1.10/1.20 cnf(221,plain,
% 1.10/1.20 (E(x2211,f2(x2212,x2211,x2213,x2213))),
% 1.10/1.20 inference(rename_variables,[],[128])).
% 1.10/1.20 cnf(225,plain,
% 1.10/1.20 (P2(x2251,x2252,x2251,f2(f2(x2252,x2251,x2252,x2251),x2251,f2(x2252,x2251,x2252,x2251),x2251))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(227,plain,
% 1.10/1.20 (~P1(a11,a10,f2(x2271,f2(a10,a11,x2272,x2273),x2274,x2274))),
% 1.10/1.20 inference(scs_inference,[],[57,128,174,177,42,53,134,218,162,160,46,214,62,2,82,63,89,71,70,64,99,66])).
% 1.10/1.20 cnf(228,plain,
% 1.10/1.20 (P1(x2281,x2282,f2(x2283,f2(x2281,x2282,x2284,x2285),x2286,x2286))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(231,plain,
% 1.10/1.20 (~P1(f2(x2311,x2312,a6,a8),x2311,f2(x2311,x2312,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,128,174,177,42,53,134,218,162,160,38,46,214,62,2,82,63,89,71,70,64,99,66,3,65])).
% 1.10/1.20 cnf(232,plain,
% 1.10/1.20 (~E(x2321,f2(x2321,x2322,a6,a8))),
% 1.10/1.20 inference(rename_variables,[],[160])).
% 1.10/1.20 cnf(233,plain,
% 1.10/1.20 (P1(x2331,x2331,x2332)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(239,plain,
% 1.10/1.20 (P2(x2391,x2391,x2392,x2392)),
% 1.10/1.20 inference(rename_variables,[],[42])).
% 1.10/1.20 cnf(240,plain,
% 1.10/1.20 (~E(f2(x2401,f2(a11,a10,x2402,x2403),x2404,x2404),a11)),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,174,177,42,53,52,134,218,228,162,160,190,38,46,214,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31])).
% 1.10/1.20 cnf(241,plain,
% 1.10/1.20 (P1(x2411,x2412,f2(x2413,f2(x2411,x2412,x2414,x2415),x2416,x2416))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(242,plain,
% 1.10/1.20 (P1(x2421,f2(x2422,x2423,x2424,x2424),f2(x2425,f2(x2421,x2423,x2426,x2427),x2428,x2428))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,174,177,42,53,52,134,218,228,241,162,160,190,38,46,214,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30])).
% 1.10/1.20 cnf(243,plain,
% 1.10/1.20 (P1(x2431,x2432,f2(x2433,f2(x2431,x2432,x2434,x2435),x2436,x2436))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(244,plain,
% 1.10/1.20 (P1(f2(x2441,x2442,x2443,x2443),x2444,f2(x2445,f2(x2442,x2444,x2446,x2447),x2448,x2448))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,174,177,42,53,52,134,218,228,241,243,162,160,190,38,46,214,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29])).
% 1.10/1.20 cnf(245,plain,
% 1.10/1.20 (P1(x2451,x2452,f2(x2453,f2(x2451,x2452,x2454,x2455),x2456,x2456))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(247,plain,
% 1.10/1.20 (P2(x2471,x2472,x2471,f2(f2(x2472,x2471,x2472,x2471),x2471,f2(x2472,x2471,x2472,x2471),x2471))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(249,plain,
% 1.10/1.20 (P2(x2491,x2492,x2491,f2(f2(x2492,x2491,x2492,x2491),x2491,f2(x2492,x2491,x2492,x2491),x2491))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(251,plain,
% 1.10/1.20 (P2(x2511,x2511,x2512,x2512)),
% 1.10/1.20 inference(rename_variables,[],[42])).
% 1.10/1.20 cnf(252,plain,
% 1.10/1.20 (P1(x2521,x2522,f2(x2523,f2(x2521,f2(x2521,x2522,x2524,x2525),x2526,x2527),x2528,x2528))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,174,177,42,239,53,225,247,52,134,218,228,241,243,245,162,160,190,38,233,46,214,217,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80])).
% 1.10/1.20 cnf(253,plain,
% 1.10/1.20 (P1(x2531,x2532,f2(x2531,x2532,x2533,x2534))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(254,plain,
% 1.10/1.20 (P1(x2541,x2542,f2(x2543,f2(x2541,x2542,x2544,x2545),x2546,x2546))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(255,plain,
% 1.10/1.20 (P1(x2551,x2551,x2552)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(257,plain,
% 1.10/1.20 (~P2(f2(x2571,f2(a1,a10,x2572,x2573),x2574,x2574),a10,f2(x2571,f2(a1,a10,x2572,x2573),x2574,x2574),a11)),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,174,177,42,239,53,225,247,52,39,134,218,228,241,243,245,254,162,166,160,190,38,233,46,214,217,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95])).
% 1.10/1.20 cnf(258,plain,
% 1.10/1.20 (P1(x2581,x2582,f2(x2583,f2(x2581,x2582,x2584,x2585),x2586,x2586))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(260,plain,
% 1.10/1.20 (~P1(a9,a8,f2(x2601,f2(a9,a6,x2602,x2603),x2604,x2604))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,174,177,42,239,60,53,225,247,52,39,134,218,228,241,243,245,254,258,162,129,166,160,190,38,233,46,214,217,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76])).
% 1.10/1.20 cnf(263,plain,
% 1.10/1.20 (~P1(f2(x2631,f2(x2631,x2632,a6,a8),a6,a8),x2631,f2(x2631,x2632,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,146,174,177,42,239,60,53,225,247,52,39,134,218,228,241,243,245,254,258,162,129,166,160,232,190,38,233,46,214,217,253,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76,72])).
% 1.10/1.20 cnf(264,plain,
% 1.10/1.20 (~E(x2641,f2(x2641,x2642,a6,a8))),
% 1.10/1.20 inference(rename_variables,[],[160])).
% 1.10/1.20 cnf(266,plain,
% 1.10/1.20 (P1(x2661,x2662,f2(x2661,x2662,x2663,x2664))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(268,plain,
% 1.10/1.20 (~P2(a11,a11,a11,f2(f2(a10,a11,a10,a11),a11,f2(a10,a11,a10,a11),a11))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,146,174,123,177,42,239,60,53,225,247,249,52,39,134,218,228,241,243,245,254,258,162,129,166,160,232,190,37,38,233,255,46,214,217,253,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76,72,100])).
% 1.10/1.20 cnf(269,plain,
% 1.10/1.20 (~P2(a11,a10,x2691,x2691)),
% 1.10/1.20 inference(rename_variables,[],[123])).
% 1.10/1.20 cnf(270,plain,
% 1.10/1.20 (P1(x2701,x2702,x2702)),
% 1.10/1.20 inference(rename_variables,[],[37])).
% 1.10/1.20 cnf(274,plain,
% 1.10/1.20 (~P1(a11,a10,f2(f2(a11,a10,a6,a8),a10,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,146,174,123,177,42,239,60,53,225,247,249,52,39,134,218,228,241,243,245,254,258,162,129,166,160,232,264,190,37,38,233,255,46,214,217,253,266,50,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76,72,100,86])).
% 1.10/1.20 cnf(285,plain,
% 1.10/1.20 (~P2(f2(x2851,x2852,a6,a8),x2851,x2853,x2853)),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,146,174,123,269,177,42,239,251,60,53,225,247,249,52,39,134,218,228,241,243,245,254,258,162,129,166,160,232,264,190,41,37,270,38,233,255,46,214,217,253,266,50,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76,72,100,86,106,92])).
% 1.10/1.20 cnf(295,plain,
% 1.10/1.20 (~P2(f2(x2951,f2(a1,a10,x2952,x2953),x2954,x2954),a11,a10,f2(x2951,f2(a1,a10,x2952,x2953),x2954,x2954))),
% 1.10/1.20 inference(scs_inference,[],[57,121,128,221,146,174,123,269,177,42,239,251,60,53,225,247,249,52,39,134,218,228,241,243,245,254,258,162,129,166,160,232,264,190,41,37,270,38,233,255,46,214,217,253,266,50,62,2,82,63,89,71,70,64,99,66,3,65,98,34,31,30,29,32,33,35,80,95,76,72,100,86,106,92,93,87,90,91,88])).
% 1.10/1.20 cnf(317,plain,
% 1.10/1.20 (~P2(a11,f2(x3171,f2(a1,a10,x3172,x3173),x3174,x3174),f2(x3171,f2(a1,a10,x3172,x3173),x3174,x3174),a10)),
% 1.10/1.20 inference(scs_inference,[],[257,295,92,87,91])).
% 1.10/1.20 cnf(327,plain,
% 1.10/1.20 (~P1(f2(x3271,x3272,a6,a8),x3271,f2(x3271,f2(x3271,x3272,a6,a8),a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[263,257,131,295,268,92,87,91,90,93,88,62,63])).
% 1.10/1.20 cnf(329,plain,
% 1.10/1.20 (~P2(f2(x3291,x3292,a6,a8),x3292,x3293,x3293)),
% 1.10/1.20 inference(scs_inference,[],[263,257,61,131,295,268,92,87,91,90,93,88,62,63,82])).
% 1.10/1.20 cnf(331,plain,
% 1.10/1.20 (~P2(x3311,x3311,f2(x3312,x3313,a6,a8),x3313)),
% 1.10/1.20 inference(scs_inference,[],[263,257,61,131,295,268,92,87,91,90,93,88,62,63,82,89])).
% 1.10/1.20 cnf(333,plain,
% 1.10/1.20 (E(x3331,f2(f2(x3331,x3332,x3331,x3332),x3332,f2(x3331,x3332,x3331,x3332),x3332))),
% 1.10/1.20 inference(scs_inference,[],[263,257,61,51,131,295,268,92,87,91,90,93,88,62,63,82,89,2])).
% 1.10/1.20 cnf(335,plain,
% 1.10/1.20 (P1(x3351,x3351,x3352)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(337,plain,
% 1.10/1.20 (P1(x3371,f2(f2(x3372,x3371,x3373,x3373),f2(x3372,x3371,x3373,x3373),x3374,x3374),x3375)),
% 1.10/1.20 inference(scs_inference,[],[263,257,61,51,220,131,295,268,38,335,92,87,91,90,93,88,62,63,82,89,2,109,69])).
% 1.10/1.20 cnf(338,plain,
% 1.10/1.20 (P1(x3381,x3381,x3382)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(339,plain,
% 1.10/1.20 (P1(x3391,x3392,f2(f2(x3393,x3392,x3394,x3394),f2(x3393,x3392,x3394,x3394),x3395,x3395))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(342,plain,
% 1.10/1.20 (P1(x3421,f2(x3421,x3422,x3423,x3424),f2(x3422,f2(x3421,x3422,x3423,x3424),x3425,x3425))),
% 1.10/1.20 inference(rename_variables,[],[216])).
% 1.10/1.20 cnf(343,plain,
% 1.10/1.20 (P1(x3431,x3432,f2(f2(x3433,x3432,x3434,x3434),f2(x3433,x3432,x3434,x3434),x3435,x3435))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(345,plain,
% 1.10/1.20 (P1(x3451,f2(x3452,x3453,x3454,x3454),f2(f2(x3453,x3453,x3455,x3455),f2(x3453,x3453,x3455,x3455),x3456,x3456))),
% 1.10/1.20 inference(scs_inference,[],[263,257,61,51,216,220,339,343,242,131,295,268,38,335,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70])).
% 1.10/1.20 cnf(346,plain,
% 1.10/1.20 (P1(x3461,f2(x3462,x3463,x3464,x3464),f2(x3465,f2(x3461,x3463,x3466,x3467),x3468,x3468))),
% 1.10/1.20 inference(rename_variables,[],[242])).
% 1.10/1.20 cnf(347,plain,
% 1.10/1.20 (P1(x3471,x3472,f2(f2(x3473,x3472,x3474,x3474),f2(x3473,x3472,x3474,x3474),x3475,x3475))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(350,plain,
% 1.10/1.20 (P2(f2(x3501,x3502,a6,a8),x3502,x3503,f2(x3504,x3503,a6,a8))),
% 1.10/1.20 inference(rename_variables,[],[156])).
% 1.10/1.20 cnf(351,plain,
% 1.10/1.20 (P2(f2(x3511,x3512,x3513,x3514),x3512,x3513,x3514)),
% 1.10/1.20 inference(rename_variables,[],[152])).
% 1.10/1.20 cnf(354,plain,
% 1.10/1.20 (P2(x3541,x3542,x3541,f2(f2(x3542,x3541,x3542,x3541),x3541,f2(x3542,x3541,x3542,x3541),x3541))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(357,plain,
% 1.10/1.20 (~E(f2(x3571,x3572,a6,a8),x3572)),
% 1.10/1.20 inference(rename_variables,[],[61])).
% 1.10/1.20 cnf(358,plain,
% 1.10/1.20 (P1(x3581,x3581,x3582)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(361,plain,
% 1.10/1.20 (P1(x3611,x3612,f2(f2(x3613,x3612,x3614,x3614),f2(x3613,x3612,x3614,x3614),x3615,x3615))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(363,plain,
% 1.10/1.20 (~E(f2(x3631,f2(x3632,x3631,a6,a8),x3633,x3633),x3632)),
% 1.10/1.20 inference(scs_inference,[],[57,204,263,257,61,156,350,53,51,152,216,342,220,339,343,347,242,131,295,268,38,335,338,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31])).
% 1.10/1.20 cnf(364,plain,
% 1.10/1.20 (P1(x3641,f2(x3641,x3642,x3643,x3644),f2(x3642,f2(x3641,x3642,x3643,x3644),x3645,x3645))),
% 1.10/1.20 inference(rename_variables,[],[216])).
% 1.10/1.20 cnf(367,plain,
% 1.10/1.20 (~E(x3671,f2(x3672,x3671,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,204,263,257,206,61,357,156,350,53,51,152,216,342,220,339,343,347,242,131,285,295,268,38,335,338,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31,3,34])).
% 1.10/1.20 cnf(373,plain,
% 1.10/1.20 (P1(x3731,f2(x3731,x3732,x3733,x3734),f2(x3732,f2(x3731,x3732,x3733,x3734),x3735,x3735))),
% 1.10/1.20 inference(rename_variables,[],[216])).
% 1.10/1.20 cnf(374,plain,
% 1.10/1.20 (~E(f2(a9,a6,x3741,x3742),a8)),
% 1.10/1.20 inference(scs_inference,[],[57,204,263,257,206,61,357,156,350,53,354,51,152,216,342,364,373,220,339,343,347,242,131,285,295,260,268,38,335,338,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31,3,34,32,29,30])).
% 1.10/1.20 cnf(375,plain,
% 1.10/1.20 (P1(x3751,f2(x3751,x3752,x3753,x3754),f2(x3752,f2(x3751,x3752,x3753,x3754),x3755,x3755))),
% 1.10/1.20 inference(rename_variables,[],[216])).
% 1.10/1.20 cnf(378,plain,
% 1.10/1.20 (P2(x3781,x3782,x3783,f2(f2(x3784,x3783,a6,a8),x3783,x3781,x3782))),
% 1.10/1.20 inference(rename_variables,[],[52])).
% 1.10/1.20 cnf(387,plain,
% 1.10/1.20 (P1(x3871,x3872,f2(f2(x3873,x3872,x3874,x3874),f2(x3873,x3872,x3874,x3874),x3875,x3875))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(389,plain,
% 1.10/1.20 (~P2(f2(f2(x3891,a10,x3892,x3892),f2(x3891,a10,x3892,x3892),x3893,x3893),a10,f2(f2(x3891,a10,x3892,x3892),f2(x3891,a10,x3892,x3892),x3893,x3893),a11)),
% 1.10/1.20 inference(scs_inference,[],[57,204,207,263,257,206,61,357,156,350,60,53,354,52,378,51,39,152,216,342,364,373,375,220,339,343,347,361,387,242,346,252,131,285,295,260,268,129,38,335,338,166,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31,3,34,32,29,30,33,35,80,76,95])).
% 1.10/1.20 cnf(390,plain,
% 1.10/1.20 (P1(x3901,x3902,f2(f2(x3903,x3902,x3904,x3904),f2(x3903,x3902,x3904,x3904),x3905,x3905))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(411,plain,
% 1.10/1.20 (~E(f2(f2(x4111,x4112,x4113,x4113),x4111,a6,a8),x4112)),
% 1.10/1.20 inference(scs_inference,[],[57,204,143,207,231,263,257,206,61,357,156,350,60,53,354,52,378,51,42,39,152,351,216,342,364,373,375,220,339,343,347,361,387,390,242,346,213,252,186,131,285,295,240,260,268,129,41,37,38,335,338,358,166,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31,3,34,32,29,30,33,35,80,76,95,72,73,100,106,5])).
% 1.10/1.20 cnf(412,plain,
% 1.10/1.20 (P1(f2(x4121,x4122,x4121,x4122),x4122,x4121)),
% 1.10/1.20 inference(scs_inference,[],[57,204,143,207,231,263,257,206,61,357,156,350,60,53,354,52,378,51,42,39,152,351,216,342,364,373,375,220,339,343,347,361,387,390,242,346,213,252,186,131,285,295,240,260,268,129,41,37,38,335,338,358,166,92,87,91,90,93,88,62,63,82,89,2,109,69,71,70,99,98,65,66,31,3,34,32,29,30,33,35,80,76,95,72,73,100,106,5,84])).
% 1.10/1.20 cnf(429,plain,
% 1.10/1.20 (P1(x4291,f2(f2(x4292,x4293,x4294,x4294),f2(x4292,x4293,x4294,x4294),x4295,x4295),x4293)),
% 1.10/1.20 inference(scs_inference,[],[337,118])).
% 1.10/1.20 cnf(430,plain,
% 1.10/1.20 (P1(x4301,f2(f2(x4302,x4301,x4303,x4303),f2(x4302,x4301,x4303,x4303),x4304,x4304),x4305)),
% 1.10/1.20 inference(rename_variables,[],[337])).
% 1.10/1.20 cnf(432,plain,
% 1.10/1.20 (~P2(x4321,f2(x4322,x4321,a6,a8),x4323,x4323)),
% 1.10/1.20 inference(scs_inference,[],[329,337,118,92])).
% 1.10/1.20 cnf(446,plain,
% 1.10/1.20 (~P1(f2(x4461,f2(x4462,x4461,a6,a8),x4463,x4463),x4462,f2(x4461,f2(x4462,x4461,a6,a8),x4463,x4463))),
% 1.10/1.20 inference(scs_inference,[],[227,329,389,337,363,118,92,91,90,88,63,87,93,62])).
% 1.10/1.20 cnf(448,plain,
% 1.10/1.20 (~P2(f2(x4481,f2(x4482,x4481,a6,a8),x4483,x4483),x4482,x4484,x4484)),
% 1.10/1.20 inference(scs_inference,[],[227,329,389,337,363,118,92,91,90,88,63,87,93,62,82])).
% 1.10/1.20 cnf(450,plain,
% 1.10/1.20 (~P2(a11,f2(f2(x4501,a10,x4502,x4502),f2(x4501,a10,x4502,x4502),x4503,x4503),f2(f2(x4501,a10,x4502,x4502),f2(x4501,a10,x4502,x4502),x4503,x4503),a10)),
% 1.10/1.20 inference(scs_inference,[],[227,329,389,337,363,118,92,91,90,88,63,87,93,62,82,89])).
% 1.10/1.20 cnf(452,plain,
% 1.10/1.20 (P1(x4521,f2(f2(x4522,a10,x4523,x4523),f2(x4522,a10,x4523,x4523),x4524,x4524),f2(a11,a10,f2(x4525,a10,x4526,x4526),a10))),
% 1.10/1.20 inference(scs_inference,[],[227,206,329,389,337,430,363,118,92,91,90,88,63,87,93,62,82,89,64])).
% 1.10/1.20 cnf(453,plain,
% 1.10/1.20 (P1(x4531,f2(f2(x4532,x4531,x4533,x4533),f2(x4532,x4531,x4533,x4533),x4534,x4534),x4535)),
% 1.10/1.20 inference(rename_variables,[],[337])).
% 1.10/1.20 cnf(462,plain,
% 1.10/1.20 (P1(f2(a11,a1,a11,a1),a10,a11)),
% 1.10/1.20 inference(scs_inference,[],[227,206,329,389,36,412,337,430,453,363,331,37,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70])).
% 1.10/1.20 cnf(463,plain,
% 1.10/1.20 (P1(f2(x4631,x4632,x4631,x4632),x4632,x4631)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(465,plain,
% 1.10/1.20 (P1(x4651,x4652,f2(x4651,f2(x4651,f2(x4653,x4652,x4654,x4654),x4655,x4656),x4657,x4658))),
% 1.10/1.20 inference(scs_inference,[],[227,206,329,389,162,36,46,412,337,430,453,363,331,37,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71])).
% 1.10/1.20 cnf(466,plain,
% 1.10/1.20 (P1(x4661,x4662,f2(x4661,x4662,x4663,x4664))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(469,plain,
% 1.10/1.20 (P2(f2(x4691,x4692,a6,a8),x4692,x4693,f2(x4694,x4693,a6,a8))),
% 1.10/1.20 inference(rename_variables,[],[156])).
% 1.10/1.20 cnf(475,plain,
% 1.10/1.20 (~P1(x4751,f2(x4751,x4752,a6,a8),x4752)),
% 1.10/1.20 inference(scs_inference,[],[227,206,329,389,61,162,156,469,52,36,46,466,412,337,430,453,170,363,331,37,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65])).
% 1.10/1.20 cnf(476,plain,
% 1.10/1.20 (~E(f2(x4761,x4762,a6,a8),x4762)),
% 1.10/1.20 inference(rename_variables,[],[61])).
% 1.10/1.20 cnf(477,plain,
% 1.10/1.20 (P1(x4771,x4772,f2(x4771,x4772,x4773,x4774))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(480,plain,
% 1.10/1.20 (P1(x4801,x4802,f2(x4801,f2(x4803,x4802,x4804,x4804),x4805,x4806))),
% 1.10/1.20 inference(rename_variables,[],[162])).
% 1.10/1.20 cnf(482,plain,
% 1.10/1.20 (~E(f2(x4821,f2(x4822,x4823,x4824,x4824),a6,a8),x4823)),
% 1.10/1.20 inference(scs_inference,[],[57,227,128,206,329,389,61,476,162,156,469,52,36,46,466,412,337,430,453,170,363,331,37,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65,66,3])).
% 1.10/1.20 cnf(485,plain,
% 1.10/1.20 (P1(x4851,x4852,f2(x4851,f2(x4853,x4852,x4854,x4854),x4855,x4856))),
% 1.10/1.20 inference(rename_variables,[],[162])).
% 1.10/1.20 cnf(487,plain,
% 1.10/1.20 (E(x4871,f2(x4872,x4871,x4873,x4873))),
% 1.10/1.20 inference(rename_variables,[],[128])).
% 1.10/1.20 cnf(493,plain,
% 1.10/1.20 (P2(x4931,x4932,x4931,f2(f2(x4932,x4931,x4932,x4931),x4931,f2(x4932,x4931,x4932,x4931),x4931))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(494,plain,
% 1.10/1.20 (~P2(f2(x4941,x4942,a6,a8),x4942,x4943,x4943)),
% 1.10/1.20 inference(rename_variables,[],[329])).
% 1.10/1.20 cnf(495,plain,
% 1.10/1.20 (~E(f2(f2(x4951,f2(x4952,x4951,a6,a8),x4951,f2(x4952,x4951,a6,a8)),f2(x4952,x4951,a6,a8),f2(x4951,f2(x4952,x4951,a6,a8),x4951,f2(x4952,x4951,a6,a8)),f2(x4952,x4951,a6,a8)),f2(x4952,x4951,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,204,227,128,487,206,329,494,389,61,476,162,480,156,469,134,53,493,52,36,46,466,39,412,337,430,453,170,363,331,37,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65,66,3,31,32,29,33,34,35])).
% 1.10/1.20 cnf(500,plain,
% 1.10/1.20 (P1(f2(x5001,x5002,x5001,x5002),x5002,x5001)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(503,plain,
% 1.10/1.20 (P1(x5031,x5032,f2(x5031,f2(x5033,x5032,x5034,x5034),x5035,x5036))),
% 1.10/1.20 inference(rename_variables,[],[162])).
% 1.10/1.20 cnf(506,plain,
% 1.10/1.20 (~P2(f2(f2(x5061,x5062,a6,a8),f2(x5063,x5062,x5064,x5064),x5065,x5066),x5062,f2(f2(x5061,x5062,a6,a8),f2(x5063,x5062,x5064,x5064),x5065,x5066),f2(x5062,f2(x5061,x5062,a6,a8),a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,204,227,128,487,206,329,494,389,61,476,59,162,480,485,503,156,469,134,53,493,52,36,160,46,466,39,412,463,337,430,453,170,363,331,129,37,38,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65,66,3,31,32,29,33,34,35,30,75,80,95])).
% 1.10/1.20 cnf(508,plain,
% 1.10/1.20 (P1(x5081,x5082,f2(x5081,f2(x5083,x5082,x5084,x5084),x5085,x5086))),
% 1.10/1.20 inference(rename_variables,[],[162])).
% 1.10/1.20 cnf(512,plain,
% 1.10/1.20 (~E(x5121,f2(x5122,x5121,a6,a8))),
% 1.10/1.20 inference(rename_variables,[],[367])).
% 1.10/1.20 cnf(513,plain,
% 1.10/1.20 (~P1(x5131,f2(x5131,x5132,a6,a8),x5131)),
% 1.10/1.20 inference(rename_variables,[],[204])).
% 1.10/1.20 cnf(514,plain,
% 1.10/1.20 (P1(x5141,x5142,f2(x5141,x5142,x5143,x5144))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(517,plain,
% 1.10/1.20 (P1(x5171,x5172,f2(x5171,f2(x5173,x5172,x5174,x5174),x5175,x5176))),
% 1.10/1.20 inference(rename_variables,[],[162])).
% 1.10/1.20 cnf(519,plain,
% 1.10/1.20 (~P1(x5191,f2(x5192,x5191,a6,a8),x5192)),
% 1.10/1.20 inference(scs_inference,[],[57,204,513,227,128,487,206,329,494,389,61,476,59,162,480,485,503,508,156,469,134,60,53,493,52,36,160,46,466,477,514,39,412,463,337,430,453,170,363,331,367,512,129,37,38,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65,66,3,31,32,29,33,34,35,30,75,80,95,73,76,72])).
% 1.10/1.20 cnf(530,plain,
% 1.10/1.20 (~E(f2(x5301,f2(x5302,x5301,a6,a8),x5301,f2(x5302,x5301,a6,a8)),f2(x5302,x5301,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,204,513,227,128,487,206,329,494,389,61,476,59,162,480,485,503,508,517,156,469,134,60,53,493,52,36,160,46,466,477,514,39,412,463,500,337,430,453,170,363,211,331,367,512,152,129,37,38,118,92,91,90,88,63,87,93,62,82,89,64,69,109,70,71,99,98,65,66,3,31,32,29,33,34,35,30,75,80,95,73,76,72,100,74])).
% 1.10/1.20 cnf(570,plain,
% 1.10/1.20 (~P2(f2(f2(x5701,x5702,x5703,x5703),x5701,a6,a8),x5702,x5704,x5704)),
% 1.10/1.20 inference(scs_inference,[],[448,274,506,411,482,5,90,91,92,63,93,87,88,62,82])).
% 1.10/1.20 cnf(575,plain,
% 1.10/1.20 (P1(x5751,f2(f2(x5752,x5753,x5754,x5754),f2(x5752,x5753,x5754,x5754),x5755,x5755),x5753)),
% 1.10/1.20 inference(rename_variables,[],[429])).
% 1.10/1.20 cnf(578,plain,
% 1.10/1.20 (P1(f2(x5781,x5782,x5781,x5782),x5782,x5781)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(582,plain,
% 1.10/1.20 (P1(x5821,x5821,x5822)),
% 1.10/1.20 inference(rename_variables,[],[38])).
% 1.10/1.20 cnf(584,plain,
% 1.10/1.20 (P1(a1,f2(f2(x5841,a10,x5842,x5842),f2(x5841,a10,x5842,x5842),x5843,x5843),a11)),
% 1.10/1.20 inference(scs_inference,[],[448,274,506,411,36,429,575,482,317,462,412,38,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71])).
% 1.10/1.20 cnf(585,plain,
% 1.10/1.20 (P1(x5851,f2(f2(x5852,x5853,x5854,x5854),f2(x5852,x5853,x5854,x5854),x5855,x5855),x5853)),
% 1.10/1.20 inference(rename_variables,[],[429])).
% 1.10/1.20 cnf(588,plain,
% 1.10/1.20 (P2(x5881,x5882,x5883,f2(f2(x5884,x5883,a6,a8),x5883,x5881,x5882))),
% 1.10/1.20 inference(rename_variables,[],[52])).
% 1.10/1.20 cnf(590,plain,
% 1.10/1.20 (P2(x5901,f2(x5902,x5901,f2(x5903,x5904,a6,a8),f2(x5905,x5904,x5906,x5906)),x5907,f2(x5908,x5907,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[448,274,506,411,50,156,52,36,429,575,172,482,317,462,412,38,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99])).
% 1.10/1.20 cnf(592,plain,
% 1.10/1.20 (P2(x5921,f2(x5922,x5921,x5923,f2(x5924,x5925,x5926,x5926)),x5923,x5925)),
% 1.10/1.20 inference(rename_variables,[],[172])).
% 1.10/1.20 cnf(595,plain,
% 1.10/1.20 (~E(f2(f2(x5951,x5952,x5953,x5953),x5951,a6,a8),x5952)),
% 1.10/1.20 inference(rename_variables,[],[411])).
% 1.10/1.20 cnf(600,plain,
% 1.10/1.20 (P1(x6001,x6002,f2(x6003,f2(x6001,x6002,x6004,x6005),x6006,x6006))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(602,plain,
% 1.10/1.20 (~E(f2(f2(x6021,f2(x6022,x6023,x6024,x6024),x6025,x6025),x6021,a6,a8),x6023)),
% 1.10/1.20 inference(scs_inference,[],[128,448,274,506,411,595,50,61,156,134,162,52,36,429,575,172,482,317,462,412,38,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99,65,66,3])).
% 1.10/1.20 cnf(603,plain,
% 1.10/1.20 (~E(f2(f2(x6031,x6032,x6033,x6033),x6031,a6,a8),x6032)),
% 1.10/1.20 inference(rename_variables,[],[411])).
% 1.10/1.20 cnf(607,plain,
% 1.10/1.20 (P2(x6071,x6072,x6073,f2(f2(x6074,x6073,a6,a8),x6073,x6071,x6072))),
% 1.10/1.20 inference(rename_variables,[],[52])).
% 1.10/1.20 cnf(608,plain,
% 1.10/1.20 (~P2(f2(x6081,f2(x6082,x6081,a6,a8),x6083,x6083),x6082,x6084,x6084)),
% 1.10/1.20 inference(rename_variables,[],[448])).
% 1.10/1.20 cnf(609,plain,
% 1.10/1.20 (~E(x6091,f2(x6092,f2(x6093,f2(x6092,x6091,x6094,x6095),x6096,x6096),a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[128,448,274,506,475,411,595,50,61,156,134,600,162,52,588,42,36,429,575,172,482,317,462,412,38,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99,65,66,3,32,34,30])).
% 1.10/1.20 cnf(610,plain,
% 1.10/1.20 (P1(x6101,x6102,f2(x6103,f2(x6101,x6102,x6104,x6105),x6106,x6106))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(613,plain,
% 1.10/1.20 (P1(x6131,x6132,f2(x6133,f2(x6131,x6132,x6134,x6135),x6136,x6136))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(619,plain,
% 1.10/1.20 (P1(f2(x6191,x6192,x6191,x6192),x6192,x6191)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(622,plain,
% 1.10/1.20 (P1(x6221,x6222,f2(x6223,f2(x6221,x6222,x6224,x6225),x6226,x6226))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(626,plain,
% 1.10/1.20 (P1(x6261,x6262,f2(x6263,f2(x6261,x6262,x6264,x6265),x6266,x6266))),
% 1.10/1.20 inference(rename_variables,[],[134])).
% 1.10/1.20 cnf(632,plain,
% 1.10/1.20 (~P1(x6321,f2(x6321,f2(x6321,x6321,a6,a8),x6321,f2(x6321,x6321,a6,a8)),f2(x6321,x6321,a6,a8))),
% 1.10/1.20 inference(scs_inference,[],[57,204,446,121,206,128,448,608,274,506,475,411,595,50,61,59,156,134,600,610,613,622,626,162,60,52,588,607,42,36,39,429,575,172,530,482,317,462,412,578,619,38,582,129,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99,65,66,3,32,34,30,31,35,29,33,75,80,76,73,72])).
% 1.10/1.20 cnf(635,plain,
% 1.10/1.20 (P1(f2(x6351,x6352,x6351,x6352),x6352,x6351)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(646,plain,
% 1.10/1.20 (P1(x6461,x6462,f2(x6461,x6462,x6463,x6464))),
% 1.10/1.20 inference(rename_variables,[],[46])).
% 1.10/1.20 cnf(648,plain,
% 1.10/1.20 (~P2(x6481,f2(x6481,f2(x6482,x6481,f2(x6483,x6483,x6483,x6483),f2(x6484,x6483,x6485,x6485)),a6,a8),f2(x6483,x6483,x6483,x6483),x6483)),
% 1.10/1.20 inference(scs_inference,[],[57,204,446,121,206,128,448,608,274,506,475,123,411,595,603,50,61,59,156,134,600,610,613,622,626,162,60,52,588,607,42,46,646,36,39,429,575,585,172,592,530,432,482,317,462,412,578,619,635,337,41,38,582,129,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99,65,66,3,32,34,30,31,35,29,33,75,80,76,73,72,101,86,100])).
% 1.10/1.20 cnf(654,plain,
% 1.10/1.20 (~E(f2(x6541,f2(x6542,f2(x6543,x6541,a6,a8),x6544,x6544),x6545,x6545),x6543)),
% 1.10/1.20 inference(scs_inference,[],[57,204,446,121,206,128,448,608,274,506,475,123,411,595,603,50,61,59,156,134,600,610,613,622,626,162,60,52,588,607,42,46,646,36,39,429,575,585,172,592,530,432,482,317,462,412,578,619,635,337,41,38,582,129,5,90,91,92,63,93,87,88,62,82,89,69,70,109,71,98,99,65,66,3,32,34,30,31,35,29,33,75,80,76,73,72,101,86,100,4])).
% 1.10/1.20 cnf(699,plain,
% 1.10/1.20 (P1(a1,f2(f2(x6991,a10,x6992,x6992),f2(x6991,a10,x6992,x6992),x6993,x6993),a11)),
% 1.10/1.20 inference(rename_variables,[],[584])).
% 1.10/1.20 cnf(700,plain,
% 1.10/1.20 (P1(x7001,f2(x7002,x7003,x7004,x7004),f2(f2(x7003,x7003,x7005,x7005),f2(x7003,x7003,x7005,x7005),x7006,x7006))),
% 1.10/1.20 inference(rename_variables,[],[345])).
% 1.10/1.20 cnf(703,plain,
% 1.10/1.20 (P1(f2(x7031,x7032,x7031,x7032),x7032,x7031)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(706,plain,
% 1.10/1.20 (P1(x7061,f2(f2(x7062,a10,x7063,x7063),f2(x7062,a10,x7063,x7063),x7064,x7064),f2(a11,a10,f2(x7065,a10,x7066,x7066),a10))),
% 1.10/1.20 inference(rename_variables,[],[452])).
% 1.10/1.20 cnf(707,plain,
% 1.10/1.20 (P1(x7071,f2(x7072,x7073,x7074,x7074),f2(f2(x7073,x7073,x7075,x7075),f2(x7073,x7073,x7075,x7075),x7076,x7076))),
% 1.10/1.20 inference(rename_variables,[],[345])).
% 1.10/1.20 cnf(711,plain,
% 1.10/1.20 (P2(x7111,x7112,x7111,f2(f2(x7112,x7111,x7112,x7111),x7111,f2(x7112,x7111,x7112,x7111),x7111))),
% 1.10/1.20 inference(rename_variables,[],[53])).
% 1.10/1.20 cnf(717,plain,
% 1.10/1.20 (P1(f2(x7171,x7172,x7171,x7172),x7172,x7171)),
% 1.10/1.20 inference(rename_variables,[],[412])).
% 1.10/1.20 cnf(721,plain,
% 1.10/1.20 (P1(x7211,f2(x7212,x7213,x7214,x7214),f2(f2(x7213,x7213,x7215,x7215),f2(x7213,x7213,x7215,x7215),x7216,x7216))),
% 1.10/1.20 inference(rename_variables,[],[345])).
% 1.10/1.20 cnf(728,plain,
% 1.10/1.20 (P1(x7281,f2(x7282,x7283,x7284,x7284),f2(f2(x7283,x7283,x7285,x7285),f2(x7283,x7283,x7285,x7285),x7286,x7286))),
% 1.10/1.20 inference(rename_variables,[],[345])).
% 1.10/1.20 cnf(729,plain,
% 1.10/1.20 (~P1(x7291,f2(x7291,x7292,a6,a8),x7291)),
% 1.10/1.20 inference(rename_variables,[],[204])).
% 1.10/1.20 cnf(734,plain,
% 1.10/1.20 (P1(x7341,x7342,x7342)),
% 1.10/1.20 inference(rename_variables,[],[37])).
% 1.10/1.20 cnf(736,plain,
% 1.10/1.20 (P2(x7361,x7362,x7363,f2(f2(x7364,x7363,a6,a8),x7363,x7361,x7362))),
% 1.10/1.20 inference(rename_variables,[],[52])).
% 1.10/1.20 cnf(737,plain,
% 1.10/1.20 (~P2(f2(f2(x7371,x7372,x7373,x7373),x7371,a6,a8),x7372,x7374,x7374)),
% 1.10/1.20 inference(rename_variables,[],[570])).
% 1.10/1.20 cnf(743,plain,
% 1.10/1.20 (P1(x7431,x7432,f2(f2(x7433,x7432,x7434,x7434),f2(x7433,x7432,x7434,x7434),x7435,x7435))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(746,plain,
% 1.10/1.20 (P1(x7461,x7462,f2(f2(x7463,x7462,x7464,x7464),f2(x7463,x7462,x7464,x7464),x7465,x7465))),
% 1.10/1.20 inference(rename_variables,[],[220])).
% 1.10/1.20 cnf(747,plain,
% 1.10/1.20 (~P1(x7471,f2(x7472,x7471,a6,a8),x7472)),
% 1.10/1.20 inference(rename_variables,[],[519])).
% 1.10/1.20 cnf(751,plain,
% 1.10/1.20 (~P1(x7511,f2(x7511,x7512,a6,a8),x7511)),
% 1.10/1.20 inference(rename_variables,[],[204])).
% 1.10/1.20 cnf(776,plain,
% 1.10/1.20 ($false),
% 1.10/1.20 inference(scs_inference,[],[57,204,729,751,446,333,632,570,737,519,747,257,506,389,51,61,495,452,706,374,345,700,707,721,728,220,743,746,53,711,37,734,160,52,736,42,46,39,244,465,654,648,590,602,609,327,209,450,584,699,429,170,48,412,703,717,41,91,92,5,90,93,88,63,87,62,82,89,69,70,71,98,99,65,66,32,3,30,29,31,34,33,35,80,76,73,72,101,79,86,100]),
% 1.10/1.20 ['proof']).
% 1.10/1.20 % SZS output end Proof
% 1.10/1.20 % Total time :0.490000s
%------------------------------------------------------------------------------