%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD018-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n019.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 05:55:14 EDT 2024
% Result : Unsatisfiable 198.82s 198.80s
% Output : CNFRefutation 198.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : FLD018-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Jun 19 11:13:09 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.49/0.58 start to proof:theBenchmark
% 198.77/198.79 %-------------------------------------------
% 198.77/198.79 % File :CSE---1.7
% 198.77/198.79 % Problem :theBenchmark
% 198.77/198.79 % Transform :cnf
% 198.77/198.79 % Format :tptp:raw
% 198.77/198.79 % Command :java -jar mcs_scs.jar %d %s
% 198.77/198.79
% 198.77/198.79 % Result :Theorem 198.130000s
% 198.77/198.79 % Output :CNFRefutation 198.130000s
% 198.77/198.79 %-------------------------------------------
% 198.77/198.80 %--------------------------------------------------------------------------
% 198.77/198.80 % File : FLD018-1 : TPTP v8.2.0. Bugfixed v2.1.0.
% 198.77/198.80 % Domain : Field Theory (Ordered fields)
% 198.77/198.80 % Problem : If a is zero, the additive inverse of a is also zero
% 198.77/198.80 % Version : [Dra93] axioms : Especial.
% 198.77/198.80 % Theorem formulation : Functional with glxx axiom set.
% 198.77/198.80 % English :
% 198.77/198.80
% 198.77/198.80 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 198.77/198.80 % Source : [Dra93]
% 198.77/198.80 % Names :
% 198.77/198.80
% 198.77/198.80 % Status : Unsatisfiable
% 198.77/198.80 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.4.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.36 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.33 v2.1.0
% 198.77/198.80 % Syntax : Number of clauses : 30 ( 6 unt; 3 nHn; 30 RR)
% 198.77/198.80 % Number of literals : 76 ( 0 equ; 45 neg)
% 198.77/198.80 % Maximal clause size : 4 ( 2 avg)
% 198.77/198.80 % Maximal term depth : 3 ( 1 avg)
% 198.77/198.80 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty)
% 198.77/198.80 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 198.77/198.80 % Number of variables : 50 ( 0 sgn)
% 198.77/198.80 % SPC : CNF_UNS_RFO_NEQ_NHN
% 198.77/198.80
% 198.77/198.80 % Comments :
% 198.77/198.80 % Bugfixes : v2.1.0 - Bugfix in FLD001-0.ax
% 198.77/198.80 %--------------------------------------------------------------------------
% 198.77/198.80 include('Axioms/FLD001-0.ax').
% 198.77/198.80 %--------------------------------------------------------------------------
% 198.77/198.80 cnf(a_is_defined,hypothesis,
% 198.77/198.80 defined(a) ).
% 198.77/198.80
% 198.77/198.80 cnf(a_equals_additive_identity_2,negated_conjecture,
% 198.77/198.80 equalish(a,additive_identity) ).
% 198.77/198.80
% 198.77/198.80 cnf(additive_inverse_not_equal_to_additive_identity_3,negated_conjecture,
% 198.77/198.80 ~ equalish(additive_inverse(a),additive_identity) ).
% 198.82/198.80
% 198.82/198.80 %--------------------------------------------------------------------------
% 198.82/198.80 %-------------------------------------------
% 198.82/198.80 % Proof found
% 198.82/198.80 % SZS status Theorem for theBenchmark
% 198.82/198.80 % SZS output start Proof
% 198.82/198.81 %ClaNum:30(EqnAxiom:0)
% 198.82/198.81 %VarNum:128(SingletonVarNum:50)
% 198.82/198.81 %MaxLitNum:4
% 198.82/198.81 %MaxfuncDepth:2
% 198.82/198.81 %SharedTerms:10
% 198.82/198.81 %goalClause: 4 6
% 198.82/198.81 %singleGoalClaCount:2
% 198.82/198.81 [1]P1(a1)
% 198.82/198.81 [2]P1(a4)
% 198.82/198.81 [3]P1(a2)
% 198.82/198.81 [4]P2(a2,a1)
% 198.82/198.81 [5]~P2(a1,a4)
% 198.82/198.81 [6]~P2(f5(a2),a1)
% 198.82/198.81 [8]~P1(x81)+P2(x81,x81)
% 198.82/198.81 [7]~P1(x71)+P1(f5(x71))
% 198.82/198.81 [12]~P1(x121)+P2(f3(a1,x121),x121)
% 198.82/198.81 [13]~P1(x131)+P2(f7(a4,x131),x131)
% 198.82/198.81 [16]~P1(x161)+P2(f3(x161,f5(x161)),a1)
% 198.82/198.81 [10]~P2(x102,x101)+P2(x101,x102)
% 198.82/198.81 [9]~P1(x91)+P2(x91,a1)+P1(f6(x91))
% 198.82/198.81 [21]~P1(x211)+P2(x211,a1)+P2(f7(x211,f6(x211)),a4)
% 198.82/198.81 [18]~P3(x182,x181)+~P3(x181,x182)+P2(x181,x182)
% 198.82/198.81 [14]~P1(x142)+~P1(x141)+P1(f3(x141,x142))
% 198.82/198.81 [15]~P1(x152)+~P1(x151)+P1(f7(x151,x152))
% 198.82/198.81 [22]~P3(a1,x222)+~P3(a1,x221)+P3(a1,f7(x221,x222))
% 198.82/198.81 [23]~P1(x232)+~P1(x231)+P2(f3(x231,x232),f3(x232,x231))
% 198.82/198.81 [24]~P1(x242)+~P1(x241)+P2(f7(x241,x242),f7(x242,x241))
% 198.82/198.81 [17]~P2(x171,x173)+P2(x171,x172)+~P2(x173,x172)
% 198.82/198.81 [19]~P3(x193,x192)+P3(x191,x192)+~P2(x193,x191)
% 198.82/198.81 [20]~P3(x201,x203)+P3(x201,x202)+~P3(x203,x202)
% 198.82/198.81 [25]~P1(x252)+~P2(x251,x253)+P2(f3(x251,x252),f3(x253,x252))
% 198.82/198.81 [26]~P1(x262)+~P2(x261,x263)+P2(f7(x261,x262),f7(x263,x262))
% 198.82/198.81 [27]~P1(x272)+~P3(x271,x273)+P3(f3(x271,x272),f3(x273,x272))
% 198.82/198.81 [11]P3(x112,x111)+~P1(x111)+~P1(x112)+P3(x111,x112)
% 198.82/198.81 [28]~P1(x283)+~P1(x282)+~P1(x281)+P2(f3(x281,f3(x282,x283)),f3(f3(x281,x282),x283))
% 198.82/198.81 [29]~P1(x293)+~P1(x292)+~P1(x291)+P2(f7(x291,f7(x292,x293)),f7(f7(x291,x292),x293))
% 198.82/198.81 [30]~P1(x303)+~P1(x302)+~P1(x301)+P2(f3(f7(x301,x302),f7(x303,x302)),f7(f3(x301,x303),x302))
% 198.82/198.81 %EqnAxiom
% 198.82/198.81
% 198.82/198.81 %-------------------------------------------
% 198.82/198.83 cnf(31,plain,
% 198.82/198.84 (~P2(a1,f5(a2))),
% 198.82/198.84 inference(scs_inference,[],[6,10])).
% 198.82/198.84 cnf(33,plain,
% 198.82/198.84 (~P2(f5(a2),a2)),
% 198.82/198.84 inference(scs_inference,[],[4,6,10,17])).
% 198.82/198.84 cnf(35,plain,
% 198.82/198.84 (P3(a1,a1)),
% 198.82/198.84 inference(scs_inference,[],[4,6,1,10,17,11])).
% 198.82/198.84 cnf(37,plain,
% 198.82/198.84 (~P3(a2,x371)+P3(a1,x371)),
% 198.82/198.84 inference(scs_inference,[],[4,6,1,10,17,11,19])).
% 198.82/198.84 cnf(39,plain,
% 198.82/198.84 (P2(a1,a1)),
% 198.82/198.84 inference(scs_inference,[],[4,6,1,10,17,11,19,18])).
% 198.82/198.84 cnf(43,plain,
% 198.82/198.84 (P3(a4,a4)),
% 198.82/198.84 inference(scs_inference,[],[33,2,10,11])).
% 198.82/198.84 cnf(45,plain,
% 198.82/198.84 (P2(a4,a4)),
% 198.82/198.84 inference(scs_inference,[],[33,2,10,11,18])).
% 198.82/198.84 cnf(47,plain,
% 198.82/198.84 (~P2(a4,a1)),
% 198.82/198.84 inference(scs_inference,[],[5,10])).
% 198.82/198.84 cnf(49,plain,
% 198.82/198.84 (P3(a2,a2)),
% 198.82/198.84 inference(scs_inference,[],[3,5,10,11])).
% 198.82/198.84 cnf(51,plain,
% 198.82/198.84 (P3(a1,a2)),
% 198.82/198.84 inference(scs_inference,[],[4,3,5,10,11,19])).
% 198.82/198.84 cnf(53,plain,
% 198.82/198.84 (P2(a2,a2)),
% 198.82/198.84 inference(scs_inference,[],[4,3,5,10,11,19,18])).
% 198.82/198.84 cnf(55,plain,
% 198.82/198.84 (P2(a1,a2)+~P3(a2,a1)),
% 198.82/198.84 inference(scs_inference,[],[51,18])).
% 198.82/198.84 cnf(66,plain,
% 198.82/198.84 (P3(a1,f7(a2,a2))),
% 198.82/198.84 inference(scs_inference,[],[49,37,22])).
% 198.82/198.84 cnf(72,plain,
% 198.82/198.84 (~P3(a2,a1)+P2(f7(a1,a1),f7(a2,a1))),
% 198.82/198.84 inference(scs_inference,[],[1,55,26])).
% 198.82/198.84 cnf(73,plain,
% 198.82/198.84 (P2(f3(a1,f5(a4)),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[2,12,7])).
% 198.82/198.84 cnf(74,plain,
% 198.82/198.84 (~P2(x741,f3(a1,f5(a4)))+P2(x741,f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[73,17])).
% 198.82/198.84 cnf(79,plain,
% 198.82/198.84 (P2(f7(a4,f5(a4)),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[2,13,7])).
% 198.82/198.84 cnf(80,plain,
% 198.82/198.84 (~P2(x801,f7(a4,f5(a4)))+P2(x801,f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[79,17])).
% 198.82/198.84 cnf(87,plain,
% 198.82/198.84 (~P1(f5(a4))+P3(f5(a4),f3(a2,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[51,73,19,27])).
% 198.82/198.84 cnf(92,plain,
% 198.82/198.84 (P2(f3(f5(a2),f5(f5(a2))),a1)),
% 198.82/198.84 inference(scs_inference,[],[3,16,7])).
% 198.82/198.84 cnf(97,plain,
% 198.82/198.84 (~P3(f3(f5(a2),f5(f5(a2))),x971)+P3(a1,x971)),
% 198.82/198.84 inference(scs_inference,[],[47,92,17,10,19])).
% 198.82/198.84 cnf(104,plain,
% 198.82/198.84 (P2(f7(a2,a1),f7(a1,a1))+~P3(a2,a1)),
% 198.82/198.84 inference(scs_inference,[],[72,10])).
% 198.82/198.84 cnf(105,plain,
% 198.82/198.84 (P2(f5(a4),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[73,74,10])).
% 198.82/198.84 cnf(110,plain,
% 198.82/198.84 (~P1(f5(a4))+P2(f7(f5(a4),a4),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[2,80,24])).
% 198.82/198.84 cnf(118,plain,
% 198.82/198.84 (P2(f5(a4),f7(f5(a4),a4))+~P1(f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[110,10])).
% 198.82/198.84 cnf(122,plain,
% 198.82/198.84 (P2(f7(a4,f5(a4)),f7(f5(a4),a4))+~P1(f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[79,118,17])).
% 198.82/198.84 cnf(123,plain,
% 198.82/198.84 (~P3(f3(f5(a2),f5(f5(a2))),x1231)+P3(a1,f7(a2,x1231))),
% 198.82/198.84 inference(scs_inference,[],[51,97,22])).
% 198.82/198.84 cnf(124,plain,
% 198.82/198.84 (P2(f7(f5(a4),a4),f7(a4,f5(a4)))+~P1(f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[122,10])).
% 198.82/198.84 cnf(127,plain,
% 198.82/198.84 (~P3(f3(f5(a2),f5(f5(a2))),x1271)+P3(f3(a1,a2),f3(f7(a2,x1271),a2))),
% 198.82/198.84 inference(scs_inference,[],[3,123,27])).
% 198.82/198.84 cnf(133,plain,
% 198.82/198.84 (~P2(a1,f3(f5(a2),f5(f5(a2))))+P3(f3(a1,a2),f3(f7(a2,a2),a2))),
% 198.82/198.84 inference(scs_inference,[],[51,127,19])).
% 198.82/198.84 cnf(134,plain,
% 198.82/198.84 (P3(f3(a1,a2),f3(f7(a2,a2),a2))),
% 198.82/198.84 inference(scs_inference,[],[92,133,10])).
% 198.82/198.84 cnf(156,plain,
% 198.82/198.84 (P1(f6(f5(a2)))),
% 198.82/198.84 inference(scs_inference,[],[6,3,9,7])).
% 198.82/198.84 cnf(195,plain,
% 198.82/198.84 (P1(f5(f6(a4)))),
% 198.82/198.84 inference(scs_inference,[],[47,2,7,9])).
% 198.82/198.84 cnf(214,plain,
% 198.82/198.84 (P3(f5(a4),f3(a2,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[2,7,87])).
% 198.82/198.84 cnf(228,plain,
% 198.82/198.84 (P1(f5(f3(a4,a4)))),
% 198.82/198.84 inference(scs_inference,[],[2,7,14])).
% 198.82/198.84 cnf(229,plain,
% 198.82/198.84 (P3(f5(f3(a4,a4)),f5(f3(a4,a4)))),
% 198.82/198.84 inference(scs_inference,[],[228,11])).
% 198.82/198.84 cnf(231,plain,
% 198.82/198.84 (P2(f7(f5(a4),a4),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[2,7,110])).
% 198.82/198.84 cnf(234,plain,
% 198.82/198.84 (~P2(x2341,f7(f5(a4),a4))+P2(x2341,f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[231,229,18,17])).
% 198.82/198.84 cnf(239,plain,
% 198.82/198.84 (P2(f5(a4),x2391)+~P2(x2391,f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[234,10])).
% 198.82/198.84 cnf(246,plain,
% 198.82/198.84 (P2(f5(a4),f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[105,2,239,26])).
% 198.82/198.84 cnf(247,plain,
% 198.82/198.84 (P3(f7(f5(a4),a4),f3(a2,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[214,246,19])).
% 198.82/198.84 cnf(274,plain,
% 198.82/198.84 (P1(f5(f7(a4,a4)))),
% 198.82/198.84 inference(scs_inference,[],[2,7,15])).
% 198.82/198.84 cnf(275,plain,
% 198.82/198.84 (P3(f5(f7(a4,a4)),f5(f7(a4,a4)))),
% 198.82/198.84 inference(scs_inference,[],[274,11])).
% 198.82/198.84 cnf(277,plain,
% 198.82/198.84 (P2(f7(a4,f5(a4)),f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[2,7,122])).
% 198.82/198.84 cnf(280,plain,
% 198.82/198.84 (~P2(x2801,f7(a4,f5(a4)))+P2(x2801,f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[277,275,18,17])).
% 198.82/198.84 cnf(285,plain,
% 198.82/198.84 (P2(f7(f5(a4),a4),x2851)+~P2(x2851,f7(a4,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[280,10])).
% 198.82/198.84 cnf(296,plain,
% 198.82/198.84 (~P2(a2,a4)),
% 198.82/198.84 inference(scs_inference,[],[47,4,17,10])).
% 198.82/198.84 cnf(314,plain,
% 198.82/198.84 (P2(f7(f5(a4),a4),f7(a4,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[2,7,124])).
% 198.82/198.84 cnf(319,plain,
% 198.82/198.84 (~P3(x3191,f7(a4,f5(a4)))+P3(x3191,f3(a2,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[247,277,314,19,17,20])).
% 198.82/198.84 cnf(341,plain,
% 198.82/198.84 (P2(f3(a2,f5(a4)),f3(a1,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[2,4,7,25])).
% 198.82/198.84 cnf(342,plain,
% 198.82/198.84 (P2(f3(a2,f5(a4)),f5(a4))),
% 198.82/198.84 inference(scs_inference,[],[73,341,17])).
% 198.82/198.84 cnf(344,plain,
% 198.82/198.84 (~P3(f3(a2,f5(a4)),x3441)+P3(f3(a1,f5(a4)),x3441)),
% 198.82/198.84 inference(scs_inference,[],[73,341,17,19])).
% 198.82/198.84 cnf(355,plain,
% 198.82/198.84 (~P2(x3551,f3(a2,f5(a4)))+P2(x3551,f3(a1,f5(a4)))),
% 198.82/198.84 inference(scs_inference,[],[341,17])).
% 198.82/198.84 cnf(361,plain,
% 198.82/198.84 (P2(f3(a1,f5(a4)),f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[73,246,17])).
% 198.82/198.84 cnf(369,plain,
% 198.82/198.84 (P2(f3(a2,f5(a4)),f7(f5(a4),a4))),
% 198.82/198.84 inference(scs_inference,[],[361,341,17])).
% 198.82/198.84 cnf(376,plain,
% 198.82/198.84 (~P2(x3761,f3(a2,f5(a4)))+P2(x3761,f7(f5(a4),a4))),
% 198.89/198.84 inference(scs_inference,[],[369,17])).
% 198.89/198.84 cnf(385,plain,
% 198.89/198.84 (P2(f3(a1,f5(a4)),x3851)+~P2(x3851,f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[355,10])).
% 198.89/198.84 cnf(388,plain,
% 198.89/198.84 (~P1(f5(a4))+P2(f3(f5(a4),a2),f7(f5(a4),a4))),
% 198.89/198.84 inference(scs_inference,[],[3,376,23])).
% 198.89/198.84 cnf(391,plain,
% 198.89/198.84 (~P2(f7(f5(a4),a4),f3(a2,f5(a4)))+P2(f5(a4),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[385,239])).
% 198.89/198.84 cnf(392,plain,
% 198.89/198.84 (P2(f3(f5(a4),a2),f5(a4))+~P1(f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[388,234])).
% 198.89/198.84 cnf(393,plain,
% 198.89/198.84 (P2(f5(a4),f3(f5(a4),a2))+~P1(f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[392,10])).
% 198.89/198.84 cnf(403,plain,
% 198.89/198.84 (P2(f3(a2,f5(a4)),f7(a4,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[369,314,17])).
% 198.89/198.84 cnf(405,plain,
% 198.89/198.84 (~P3(f3(a2,f5(a4)),x4051)+P3(f7(a4,f5(a4)),x4051)),
% 198.89/198.84 inference(scs_inference,[],[369,314,17,19])).
% 198.89/198.84 cnf(410,plain,
% 198.89/198.84 (~P3(f3(a2,f5(a4)),x4101)+P3(f3(f7(a4,f5(a4)),a4),f3(x4101,a4))),
% 198.89/198.84 inference(scs_inference,[],[2,405,27])).
% 198.89/198.84 cnf(429,plain,
% 198.89/198.84 (P2(f5(a4),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[369,391,10])).
% 198.89/198.84 cnf(432,plain,
% 198.89/198.84 (~P3(x4321,f3(a1,f5(a4)))+P3(x4321,f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[214,429,19,20])).
% 198.89/198.84 cnf(471,plain,
% 198.89/198.84 (P2(f3(f5(a4),a2),f7(f5(a4),a4))),
% 198.89/198.84 inference(scs_inference,[],[2,7,388])).
% 198.89/198.84 cnf(472,plain,
% 198.89/198.84 (~P2(x4721,f3(f5(a4),a2))+P2(x4721,f7(f5(a4),a4))),
% 198.89/198.84 inference(scs_inference,[],[471,17])).
% 198.89/198.84 cnf(477,plain,
% 198.89/198.84 (P2(f7(f5(a4),a4),x4771)+~P2(x4771,f3(f5(a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[472,10])).
% 198.89/198.84 cnf(504,plain,
% 198.89/198.84 (P2(f3(f5(a4),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[2,7,392])).
% 198.89/198.84 cnf(505,plain,
% 198.89/198.84 (~P2(x5051,f3(f5(a4),a2))+P2(x5051,f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[504,17])).
% 198.89/198.84 cnf(507,plain,
% 198.89/198.84 (~P3(f3(f5(a4),a2),x5071)+P3(f5(a4),x5071)),
% 198.89/198.84 inference(scs_inference,[],[504,17,19])).
% 198.89/198.84 cnf(509,plain,
% 198.89/198.84 (P2(f3(f3(a2,f5(a4)),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[342,3,505,25])).
% 198.89/198.84 cnf(510,plain,
% 198.89/198.84 (~P2(x5101,f3(f3(a2,f5(a4)),a2))+P2(x5101,f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[509,17])).
% 198.89/198.84 cnf(512,plain,
% 198.89/198.84 (~P3(f3(f3(a2,f5(a4)),a2),x5121)+P3(f5(a4),x5121)),
% 198.89/198.84 inference(scs_inference,[],[509,17,19])).
% 198.89/198.84 cnf(514,plain,
% 198.89/198.84 (P3(f5(a4),f3(f3(a2,f5(a4)),a2))),
% 198.89/198.84 inference(scs_inference,[],[214,3,507,27])).
% 198.89/198.84 cnf(515,plain,
% 198.89/198.84 (~P3(x5151,f5(a4))+P3(x5151,f3(f3(a2,f5(a4)),a2))),
% 198.89/198.84 inference(scs_inference,[],[514,20])).
% 198.89/198.84 cnf(520,plain,
% 198.89/198.84 (~P2(x5201,f3(a2,f5(a4)))+P2(f3(x5201,a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[3,510,25])).
% 198.89/198.84 cnf(523,plain,
% 198.89/198.84 (~P3(f3(a2,f5(a4)),x5231)+P3(f5(a4),f3(x5231,a2))),
% 198.89/198.84 inference(scs_inference,[],[3,512,27])).
% 198.89/198.84 cnf(525,plain,
% 198.89/198.84 (P2(f3(f7(f5(a4),a4),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[403,520,285])).
% 198.89/198.84 cnf(526,plain,
% 198.89/198.84 (~P2(x5261,f3(f7(f5(a4),a4),a2))+P2(x5261,f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[525,17])).
% 198.89/198.84 cnf(531,plain,
% 198.89/198.84 (P2(f5(a4),x5311)+~P2(x5311,f3(f7(f5(a4),a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[526,10])).
% 198.89/198.84 cnf(533,plain,
% 198.89/198.84 (P2(f5(a4),f3(f3(a2,f5(a4)),a2))),
% 198.89/198.84 inference(scs_inference,[],[369,3,531,25])).
% 198.89/198.84 cnf(539,plain,
% 198.89/198.84 (P2(f5(a4),f3(f5(a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[2,7,393])).
% 198.89/198.84 cnf(542,plain,
% 198.89/198.84 (P2(f3(a2,f5(a4)),f3(f5(a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[214,342,539,19,17])).
% 198.89/198.84 cnf(544,plain,
% 198.89/198.84 (P2(f7(f5(a4),a4),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[214,342,539,19,17,477])).
% 198.89/198.84 cnf(556,plain,
% 198.89/198.84 (P2(f3(a1,f5(a4)),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[247,369,544,17,19,385])).
% 198.89/198.84 cnf(565,plain,
% 198.89/198.84 (P2(f7(f5(a4),a4),f3(f5(a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[544,542,17])).
% 198.89/198.84 cnf(573,plain,
% 198.89/198.84 (P2(f5(a4),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[429,556,17])).
% 198.89/198.84 cnf(583,plain,
% 198.89/198.84 (P2(f7(a4,f5(a4)),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[277,544,17])).
% 198.89/198.84 cnf(611,plain,
% 198.89/198.84 (P2(f3(a1,f5(a4)),f3(f5(a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[361,565,17])).
% 198.89/198.84 cnf(622,plain,
% 198.89/198.84 (P2(f3(f5(a4),a2),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[471,544,17])).
% 198.89/198.84 cnf(624,plain,
% 198.89/198.84 (P2(f3(f5(a4),a2),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[471,544,17,355])).
% 198.89/198.84 cnf(651,plain,
% 198.89/198.84 (P2(f7(f3(a1,f5(a4)),f5(a4)),f7(f3(a2,f5(a4)),f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[2,556,7,26])).
% 198.89/198.84 cnf(687,plain,
% 198.89/198.84 (P3(f3(a1,f5(a4)),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[2,35,7,27])).
% 198.89/198.84 cnf(694,plain,
% 198.89/198.84 (P3(f5(a4),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[2,7,11])).
% 198.89/198.84 cnf(710,plain,
% 198.89/198.84 (P3(f3(a1,f5(a4)),f3(f7(a2,a2),f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[2,66,7,27])).
% 198.89/198.84 cnf(722,plain,
% 198.89/198.84 (P2(f3(a1,a4),f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[4,2,10,25])).
% 198.89/198.84 cnf(723,plain,
% 198.89/198.84 (~P3(f3(a1,a4),x7231)+P3(f3(a2,a4),x7231)),
% 198.89/198.84 inference(scs_inference,[],[722,19])).
% 198.89/198.84 cnf(729,plain,
% 198.89/198.84 (~P2(x7291,f3(a1,a4))+P2(x7291,f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[722,17])).
% 198.89/198.84 cnf(733,plain,
% 198.89/198.84 (P2(f3(a2,a4),x7331)+~P2(x7331,f3(a1,a4))),
% 198.89/198.84 inference(scs_inference,[],[729,10])).
% 198.89/198.84 cnf(749,plain,
% 198.89/198.84 (P2(a4,f3(a1,a4))),
% 198.89/198.84 inference(scs_inference,[],[2,10,12])).
% 198.89/198.84 cnf(750,plain,
% 198.89/198.84 (P2(a4,f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[749,729])).
% 198.89/198.84 cnf(752,plain,
% 198.89/198.84 (P2(f3(a2,a4),a4)),
% 198.89/198.84 inference(scs_inference,[],[749,729,733])).
% 198.89/198.84 cnf(791,plain,
% 198.89/198.84 (~P2(a2,f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[296,752,17])).
% 198.89/198.84 cnf(817,plain,
% 198.89/198.84 (P2(a4,f7(a4,a4))),
% 198.89/198.84 inference(scs_inference,[],[2,10,13])).
% 198.89/198.84 cnf(818,plain,
% 198.89/198.84 (P3(f7(a4,a4),a4)),
% 198.89/198.84 inference(scs_inference,[],[817,43,19])).
% 198.89/198.84 cnf(820,plain,
% 198.89/198.84 (P2(f3(a2,a4),f7(a4,a4))),
% 198.89/198.84 inference(scs_inference,[],[817,752,43,19,17])).
% 198.89/198.84 cnf(868,plain,
% 198.89/198.84 (P3(f3(a2,f5(a4)),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[687,556,19])).
% 198.89/198.84 cnf(877,plain,
% 198.89/198.84 (P3(f3(f5(a4),a2),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[687,611,19])).
% 198.89/198.84 cnf(879,plain,
% 198.89/198.84 (~P3(x8791,f3(f5(a4),a2))+P3(x8791,f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[687,611,19,20])).
% 198.89/198.84 cnf(909,plain,
% 198.89/198.84 (P3(f3(a2,f5(a4)),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[694,573,19])).
% 198.89/198.84 cnf(911,plain,
% 198.89/198.84 (P3(f3(a1,f5(a4)),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[694,573,19,344])).
% 198.89/198.84 cnf(925,plain,
% 198.89/198.84 (P3(f3(f5(a4),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[877,911,20])).
% 198.89/198.84 cnf(933,plain,
% 198.89/198.84 (P3(f3(f3(a2,f5(a4)),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[694,533,19])).
% 198.89/198.84 cnf(970,plain,
% 198.89/198.84 (P3(f3(a2,f5(a4)),f3(f7(a2,a2),f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[710,556,19])).
% 198.89/198.84 cnf(988,plain,
% 198.89/198.84 (P2(f3(a2,f5(a4)),f3(f7(a2,a2),f5(a4)))+~P3(f3(f7(a2,a2),f5(a4)),f3(a1,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[970,18,319,432])).
% 198.89/198.84 cnf(1009,plain,
% 198.89/198.84 (P2(f3(a1,a4),f7(a4,a4))),
% 198.89/198.84 inference(scs_inference,[],[722,820,17])).
% 198.89/198.84 cnf(1027,plain,
% 198.89/198.84 (~P2(f3(a1,a4),a2)),
% 198.89/198.84 inference(scs_inference,[],[791,722,17,10])).
% 198.89/198.84 cnf(1058,plain,
% 198.89/198.84 (~P2(a1,f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[5,752,17])).
% 198.89/198.84 cnf(1088,plain,
% 198.89/198.84 (~P3(f3(f7(a2,a2),f5(a4)),f3(a1,f5(a4)))+P2(f3(f7(a2,a2),f5(a4)),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[988,10])).
% 198.89/198.84 cnf(1099,plain,
% 198.89/198.84 (~P3(f3(f7(a2,a2),f5(a4)),f3(f5(a4),a2))+P2(f3(f7(a2,a2),f5(a4)),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[1088,879])).
% 198.89/198.84 cnf(1101,plain,
% 198.89/198.84 (~P2(x11011,f3(f7(a2,a2),f5(a4)))+~P3(x11011,f3(f5(a4),a2))+P2(f3(f7(a2,a2),f5(a4)),f3(a2,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[1099,19])).
% 198.89/198.84 cnf(1185,plain,
% 198.89/198.84 (~P2(a1,f3(a1,a4))),
% 198.89/198.84 inference(scs_inference,[],[1058,722,17])).
% 198.89/198.84 cnf(1193,plain,
% 198.89/198.84 (P2(f7(a4,a4),f3(a2,a4))),
% 198.89/198.84 inference(scs_inference,[],[1009,10,729])).
% 198.89/198.84 cnf(1198,plain,
% 198.89/198.84 (P2(a1,f3(a4,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[2,10,16])).
% 198.89/198.84 cnf(1199,plain,
% 198.89/198.84 (P3(f3(a4,f5(a4)),a2)),
% 198.89/198.84 inference(scs_inference,[],[51,1198,19])).
% 198.89/198.84 cnf(1201,plain,
% 198.89/198.84 (P2(a2,f3(a4,f5(a4)))),
% 198.89/198.84 inference(scs_inference,[],[4,51,1198,19,17])).
% 198.89/198.84 cnf(1210,plain,
% 198.89/198.84 (P3(a2,a1)),
% 198.89/198.84 inference(scs_inference,[],[4,35,10,19])).
% 198.89/198.84 cnf(1211,plain,
% 198.89/198.84 (P2(a1,a2)),
% 198.89/198.84 inference(scs_inference,[],[1210,55])).
% 198.89/198.84 cnf(1212,plain,
% 198.89/198.84 (P2(f7(a1,a1),f7(a2,a1))),
% 198.89/198.84 inference(scs_inference,[],[1210,72])).
% 198.89/198.84 cnf(1213,plain,
% 198.89/198.84 (P2(f7(a2,a1),f7(a1,a1))),
% 198.89/198.84 inference(scs_inference,[],[1210,104])).
% 198.89/198.84 cnf(1216,plain,
% 198.89/198.84 (P3(f3(a4,f5(a4)),a1)),
% 198.89/198.84 inference(scs_inference,[],[1201,1210,19])).
% 198.89/198.84 cnf(1255,plain,
% 198.89/198.84 (P3(a2,f7(a2,a2))),
% 198.89/198.84 inference(scs_inference,[],[66,1211,19])).
% 198.89/198.84 cnf(1285,plain,
% 198.89/198.84 (P2(f5(a4),f3(f7(f5(a4),a4),a2))),
% 198.89/198.84 inference(scs_inference,[],[544,10,520])).
% 198.89/198.84 cnf(1287,plain,
% 198.89/198.84 (P2(a4,f7(a4,f6(a4)))),
% 198.89/198.84 inference(scs_inference,[],[47,2,10,21])).
% 198.89/198.84 cnf(1290,plain,
% 198.89/198.84 (P2(f3(a2,a4),f7(a4,f6(a4)))),
% 198.89/198.84 inference(scs_inference,[],[752,1287,43,19,17])).
% 198.89/198.84 cnf(1375,plain,
% 198.89/198.84 (P3(f3(f7(f5(a4),a4),a2),f5(a4))),
% 198.89/198.84 inference(scs_inference,[],[694,1285,19])).
% 198.89/198.84 cnf(1391,plain,
% 198.89/198.84 (P2(f3(a1,a4),f7(a4,f6(a4)))),
% 198.89/198.84 inference(scs_inference,[],[722,1290,17])).
% 198.89/198.84 cnf(1404,plain,
% 198.89/198.84 (~P2(a2,f7(a4,a4))),
% 198.89/198.84 inference(scs_inference,[],[791,1193,17])).
% 198.89/198.84 cnf(1406,plain,
% 198.89/198.84 (~P2(f7(a4,a4),a2)),
% 198.89/198.84 inference(scs_inference,[],[791,1193,17,10])).
% 198.89/198.84 cnf(1443,plain,
% 198.89/198.84 (~P2(a1,f7(a4,a4))),
% 198.89/198.84 inference(scs_inference,[],[1058,1193,17])).
% 198.89/198.84 cnf(1445,plain,
% 198.89/198.84 (~P2(f7(a4,a4),a1)),
% 198.89/198.84 inference(scs_inference,[],[1058,1193,17,10])).
% 198.89/198.84 cnf(1460,plain,
% 198.89/198.84 (P2(f7(a4,a4),f7(a4,f6(a4)))),
% 198.89/198.84 inference(scs_inference,[],[1193,1290,17])).
% 198.89/198.84 cnf(1482,plain,
% 198.89/198.84 (P2(f7(a2,a1),f7(a2,a1))),
% 198.89/198.84 inference(scs_inference,[],[1213,1212,17])).
% 198.89/198.85 cnf(1593,plain,
% 198.89/198.85 (P3(a1,f7(f7(a2,a2),f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[1255,37,22])).
% 198.89/198.85 cnf(1619,plain,
% 198.89/198.85 (P3(f3(a1,a4),f3(f7(a2,a2),a4))),
% 198.89/198.85 inference(scs_inference,[],[1255,2,37,27])).
% 198.89/198.85 cnf(1620,plain,
% 198.89/198.85 (P3(f3(a2,a4),f3(f7(a2,a2),a4))),
% 198.89/198.85 inference(scs_inference,[],[1619,723])).
% 198.89/198.85 cnf(1712,plain,
% 198.89/198.85 (P3(a2,f7(f7(a2,a2),f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[1210,1593,20])).
% 198.89/198.85 cnf(1768,plain,
% 198.89/198.85 (P3(a4,f3(f7(a2,a2),a4))),
% 198.89/198.85 inference(scs_inference,[],[1620,752,19])).
% 198.89/198.85 cnf(1987,plain,
% 198.89/198.85 (P2(f3(a1,a1),a1)),
% 198.89/198.85 inference(scs_inference,[],[274,1,7,12])).
% 198.89/198.85 cnf(1989,plain,
% 198.89/198.85 (P2(f7(a4,a1),a1)),
% 198.89/198.85 inference(scs_inference,[],[274,1,7,12,13])).
% 198.89/198.85 cnf(1991,plain,
% 198.89/198.85 (P2(f3(a1,f5(a1)),a1)),
% 198.89/198.85 inference(scs_inference,[],[274,1,7,12,13,16])).
% 198.89/198.85 cnf(1997,plain,
% 198.89/198.85 (P2(f7(a4,f6(a4)),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,1,7,12,13,16,520,523,10])).
% 198.89/198.85 cnf(1999,plain,
% 198.89/198.85 (P1(f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,1,7,12,13,16,520,523,10,14])).
% 198.89/198.85 cnf(2001,plain,
% 198.89/198.85 (P1(f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,1,7,12,13,16,520,523,10,14,15])).
% 198.89/198.85 cnf(2003,plain,
% 198.89/198.85 (P1(f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,47,1,2,7,12,13,16,520,523,10,14,15,9])).
% 198.89/198.85 cnf(2005,plain,
% 198.89/198.85 (P2(f3(a1,a1),f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,47,1,2,7,12,13,16,520,523,10,14,15,9,23])).
% 198.89/198.85 cnf(2007,plain,
% 198.89/198.85 (P2(f7(a2,a2),f7(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24])).
% 198.89/198.85 cnf(2013,plain,
% 198.89/198.85 (P2(f7(a4,f6(a4)),a4)),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21])).
% 198.89/198.85 cnf(2015,plain,
% 198.89/198.85 (P3(a1,f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1460,868,583,274,35,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21,22])).
% 198.89/198.85 cnf(2017,plain,
% 198.89/198.85 (~P2(f7(a4,f6(a4)),a1)),
% 198.89/198.85 inference(scs_inference,[],[1445,1460,868,583,274,35,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21,22,17])).
% 198.89/198.85 cnf(2019,plain,
% 198.89/198.85 (P2(f3(a1,f3(a1,a1)),f3(f3(a1,a1),a1))),
% 198.89/198.85 inference(scs_inference,[],[1445,1460,868,583,274,35,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21,22,17,28])).
% 198.89/198.85 cnf(2023,plain,
% 198.89/198.85 (P2(f3(f7(a1,a1),f7(a1,a1)),f7(f3(a1,a1),a1))),
% 198.89/198.85 inference(scs_inference,[],[1445,1460,868,583,274,35,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21,22,17,28,29,30])).
% 198.89/198.85 cnf(2025,plain,
% 198.89/198.85 (P2(f6(a4),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[1445,1460,868,583,274,35,47,1,3,2,7,12,13,16,520,523,10,14,15,9,23,24,25,26,21,22,17,28,29,30,8])).
% 198.89/198.85 cnf(2032,plain,
% 198.89/198.85 (P2(f3(a1,f3(a1,a1)),f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1999,12])).
% 198.89/198.85 cnf(2034,plain,
% 198.89/198.85 (P2(f3(f3(a1,a1),f5(f3(a1,a1))),a1)),
% 198.89/198.85 inference(scs_inference,[],[1999,12,16])).
% 198.89/198.85 cnf(2038,plain,
% 198.89/198.85 (P1(f5(f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[1999,2001,622,12,16,520,7])).
% 198.89/198.85 cnf(2040,plain,
% 198.89/198.85 (P2(f7(a4,f3(a1,a1)),f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1999,2001,622,12,16,520,7,13])).
% 198.89/198.85 cnf(2044,plain,
% 198.89/198.85 (P2(a1,f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1999,2001,1987,622,970,12,16,520,7,13,523,10])).
% 198.89/198.85 cnf(2046,plain,
% 198.89/198.85 (P1(f7(f3(a1,a1),f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[1999,2001,1987,622,970,12,16,520,7,13,523,10,15])).
% 198.89/198.85 cnf(2054,plain,
% 198.89/198.85 (P1(f3(f3(a1,a1),f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2001,1987,622,970,12,16,520,7,13,523,10,15,25,26,24,14])).
% 198.89/198.85 cnf(2058,plain,
% 198.89/198.85 (P3(a1,f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2015,2001,1987,622,970,12,16,520,7,13,523,10,15,25,26,24,14,23,22])).
% 198.89/198.85 cnf(2060,plain,
% 198.89/198.85 (P3(f3(a1,f3(a1,a1)),f3(f7(a1,a1),f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2015,2001,1987,622,970,12,16,520,7,13,523,10,15,25,26,24,14,23,22,27])).
% 198.89/198.85 cnf(2062,plain,
% 198.89/198.85 (P3(a2,f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2015,2001,1987,622,970,1210,12,16,520,7,13,523,10,15,25,26,24,14,23,22,27,20])).
% 198.89/198.85 cnf(2070,plain,
% 198.89/198.85 (P2(f7(a2,f7(a2,a2)),f7(f7(a2,a2),a2))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2015,2001,1987,2019,1027,622,970,1391,1210,3,12,16,520,7,13,523,10,15,25,26,24,14,23,22,27,20,19,17,28,29])).
% 198.89/198.85 cnf(2072,plain,
% 198.89/198.85 (P2(f3(f7(a2,a2),f7(a2,a2)),f7(f3(a2,a2),a2))),
% 198.89/198.85 inference(scs_inference,[],[2007,1999,2015,2001,1987,2019,1027,622,970,1391,1210,3,12,16,520,7,13,523,10,15,25,26,24,14,23,22,27,20,19,17,28,29,30])).
% 198.89/198.85 cnf(2083,plain,
% 198.89/198.85 (P2(f3(a1,f6(a4)),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[2003,16,12])).
% 198.89/198.85 cnf(2087,plain,
% 198.89/198.85 (P2(f7(a4,f6(a4)),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[2003,2046,16,12,7,13])).
% 198.89/198.85 cnf(2091,plain,
% 198.89/198.85 (P3(f5(a4),f3(f5(a4),a2))),
% 198.89/198.85 inference(scs_inference,[],[2003,2046,556,909,16,12,7,13,520,523])).
% 198.89/198.85 cnf(2093,plain,
% 198.89/198.85 (P2(a1,f7(a4,a1))),
% 198.89/198.85 inference(scs_inference,[],[1989,2003,2046,556,909,16,12,7,13,520,523,10])).
% 198.89/198.85 cnf(2097,plain,
% 198.89/198.85 (P1(f7(f6(a4),f6(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2046,556,909,16,12,7,13,520,523,10,25,15])).
% 198.89/198.85 cnf(2099,plain,
% 198.89/198.85 (P1(f3(f6(a4),f6(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2046,556,909,16,12,7,13,520,523,10,25,15,14])).
% 198.89/198.85 cnf(2109,plain,
% 198.89/198.85 (P3(f3(a4,f5(a4)),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2062,2046,1199,556,909,16,12,7,13,520,523,10,25,15,14,23,26,24,27,20])).
% 198.89/198.85 cnf(2111,plain,
% 198.89/198.85 (P3(f3(a1,a1),f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2044,2062,2046,2058,1199,556,909,16,12,7,13,520,523,10,25,15,14,23,26,24,27,20,19])).
% 198.89/198.85 cnf(2113,plain,
% 198.89/198.85 (P2(f7(a4,a1),f3(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2044,2062,2046,2058,1199,556,909,16,12,7,13,520,523,10,25,15,14,23,26,24,27,20,19,17])).
% 198.89/198.85 cnf(2115,plain,
% 198.89/198.85 (P2(f3(a4,f3(a4,a4)),f3(f3(a4,a4),a4))),
% 198.89/198.85 inference(scs_inference,[],[2005,1989,2003,2044,2062,2046,2058,1199,556,909,2,16,12,7,13,520,523,10,25,15,14,23,26,24,27,20,19,17,28])).
% 198.89/198.85 cnf(2129,plain,
% 198.89/198.85 (P2(f3(a1,f7(a1,a1)),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[2001,12])).
% 198.89/198.85 cnf(2131,plain,
% 198.89/198.85 (P2(f3(f7(a1,a1),f5(f7(a1,a1))),a1)),
% 198.89/198.85 inference(scs_inference,[],[2001,12,16])).
% 198.89/198.85 cnf(2133,plain,
% 198.89/198.85 (P2(f7(a4,f7(a1,a1)),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[2001,12,16,13])).
% 198.89/198.85 cnf(2137,plain,
% 198.89/198.85 (P2(f3(a1,a1),f7(a4,a1))),
% 198.89/198.85 inference(scs_inference,[],[2113,2099,2001,12,16,13,7,10])).
% 198.89/198.85 cnf(2139,plain,
% 198.89/198.85 (P1(f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2113,2099,2001,12,16,13,7,10,15])).
% 198.89/198.85 cnf(2147,plain,
% 198.89/198.85 (P1(f3(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2025,2113,2099,2001,12,16,13,7,10,15,25,26,24,14])).
% 198.89/198.85 cnf(2153,plain,
% 198.89/198.85 (P3(f3(f5(a4),a2),f3(f5(a4),a2))),
% 198.89/198.85 inference(scs_inference,[],[2025,2113,2109,2099,2091,2001,925,12,16,13,7,10,15,25,26,24,14,23,27,20])).
% 198.89/198.85 cnf(2165,plain,
% 198.89/198.85 (P2(f3(a2,f5(a2)),a1)),
% 198.89/198.85 inference(scs_inference,[],[3,16])).
% 198.89/198.85 cnf(2167,plain,
% 198.89/198.85 (P2(f3(a1,a2),a2)),
% 198.89/198.85 inference(scs_inference,[],[3,16,12])).
% 198.89/198.85 cnf(2171,plain,
% 198.89/198.85 (P2(f7(a4,a2),a2)),
% 198.89/198.85 inference(scs_inference,[],[2139,3,16,12,7,13])).
% 198.89/198.85 cnf(2173,plain,
% 198.89/198.85 (P2(f3(a1,a1),f3(a1,f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2032,2139,3,16,12,7,13,10])).
% 198.89/198.85 cnf(2175,plain,
% 198.89/198.85 (P1(f7(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2032,2139,3,16,12,7,13,10,15])).
% 198.89/198.85 cnf(2179,plain,
% 198.89/198.85 (P1(f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2032,2139,3,16,12,7,13,10,15,24,14])).
% 198.89/198.85 cnf(2181,plain,
% 198.89/198.85 (P2(f3(a2,a2),f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2032,2139,3,16,12,7,13,10,15,24,14,23])).
% 198.89/198.85 cnf(2185,plain,
% 198.89/198.85 (P3(a2,f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2032,2139,2111,2058,1210,1999,3,16,12,7,13,10,15,24,14,23,27,20])).
% 198.89/198.85 cnf(2187,plain,
% 198.89/198.85 (P3(f7(a4,a1),f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2137,2032,2139,2111,2058,1210,1999,3,16,12,7,13,10,15,24,14,23,27,20,19])).
% 198.89/198.85 cnf(2189,plain,
% 198.89/198.85 (~P2(f7(a4,a1),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2137,2093,2032,2139,2111,1443,2058,1210,1999,3,16,12,7,13,10,15,24,14,23,27,20,19,17])).
% 198.89/198.85 cnf(2195,plain,
% 198.89/198.85 (P2(f3(a1,f7(a2,a2)),f7(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2175,12])).
% 198.89/198.85 cnf(2201,plain,
% 198.89/198.85 (P1(f5(f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2175,12,16,13,7])).
% 198.89/198.85 cnf(2203,plain,
% 198.89/198.85 (P2(a2,f3(a1,a2))),
% 198.89/198.85 inference(scs_inference,[],[2175,2167,12,16,13,7,10])).
% 198.89/198.85 cnf(2205,plain,
% 198.89/198.85 (P1(f7(f7(a2,a2),f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2175,2167,12,16,13,7,10,15])).
% 198.89/198.85 cnf(2215,plain,
% 198.89/198.85 (P1(f3(f7(a2,a2),f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2175,2181,2179,2167,12,16,13,7,10,15,25,26,24,23,14])).
% 198.89/198.85 cnf(2221,plain,
% 198.89/198.85 (P3(f3(a1,a1),f3(f7(a1,a1),f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2175,2181,2179,2167,2187,2185,2060,2032,1199,12,16,13,7,10,15,25,26,24,23,14,27,20,19])).
% 198.89/198.85 cnf(2223,plain,
% 198.89/198.85 (~P2(f5(a2),f3(a2,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[6,2175,2181,2179,2167,2187,2185,2165,2060,2032,1199,12,16,13,7,10,15,25,26,24,23,14,27,20,19,17])).
% 198.89/198.85 cnf(2233,plain,
% 198.89/198.85 (P2(f3(a1,f3(a2,a2)),f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2179,16,12])).
% 198.89/198.85 cnf(2237,plain,
% 198.89/198.85 (P2(f7(a4,f3(a2,a2)),f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[2201,2179,16,12,7,13])).
% 198.89/198.85 cnf(2239,plain,
% 198.89/198.85 (P2(a2,f7(a4,a2))),
% 198.89/198.85 inference(scs_inference,[],[2171,2201,2179,16,12,7,13,10])).
% 198.89/198.85 cnf(2241,plain,
% 198.89/198.85 (P1(f7(f3(a2,a2),f3(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2171,2201,2179,16,12,7,13,10,15])).
% 198.89/198.85 cnf(2249,plain,
% 198.89/198.85 (P1(f3(f3(a2,a2),f3(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2203,2171,2201,2179,16,12,7,13,10,15,25,26,23,14])).
% 198.89/198.85 cnf(2253,plain,
% 198.89/198.85 (P3(f3(a1,f5(a4)),f3(f5(a4),a2))),
% 198.89/198.85 inference(scs_inference,[],[2203,2171,2201,2221,2153,624,2179,16,12,7,13,10,15,25,26,23,14,27,19])).
% 198.89/198.85 cnf(2255,plain,
% 198.89/198.85 (~P2(f3(a1,a2),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2203,2171,2201,2221,2153,1404,624,2179,16,12,7,13,10,15,25,26,23,14,27,19,17])).
% 198.89/198.85 cnf(2261,plain,
% 198.89/198.85 (P2(f3(a4,f5(a4)),a1)),
% 198.89/198.85 inference(scs_inference,[],[2,16])).
% 198.89/198.85 cnf(2263,plain,
% 198.89/198.85 (P2(f3(a1,a4),a4)),
% 198.89/198.85 inference(scs_inference,[],[2,16,12])).
% 198.89/198.85 cnf(2267,plain,
% 198.89/198.85 (P2(f7(a4,a4),a4)),
% 198.89/198.85 inference(scs_inference,[],[2241,2,16,12,7,13])).
% 198.89/198.85 cnf(2271,plain,
% 198.89/198.85 (P1(f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2129,2241,2,16,12,7,13,10,15])).
% 198.89/198.85 cnf(2275,plain,
% 198.89/198.85 (P1(f3(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2129,2241,2,16,12,7,13,10,15,24,14])).
% 198.89/198.85 cnf(2279,plain,
% 198.89/198.85 (P3(f7(a4,a2),f7(f7(a2,a2),f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2239,2129,2241,2253,1712,868,2,16,12,7,13,10,15,24,14,20,19])).
% 198.89/198.85 cnf(2289,plain,
% 198.89/198.85 (P1(f6(f7(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[6,2239,2129,2241,2253,2131,1712,1445,868,2,16,12,7,13,10,15,24,14,20,19,17,523,1101,21,9])).
% 198.89/198.85 cnf(2308,plain,
% 198.89/198.85 (P2(f3(f7(a4,a4),f5(f7(a4,a4))),a1)),
% 198.89/198.85 inference(scs_inference,[],[2271,2289,8,16])).
% 198.89/198.85 cnf(2310,plain,
% 198.89/198.85 (P1(f5(f6(f7(a4,a4))))),
% 198.89/198.85 inference(scs_inference,[],[2271,2289,8,16,7])).
% 198.89/198.85 cnf(2312,plain,
% 198.89/198.85 (P2(f3(a1,f7(a4,a4)),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2271,2289,8,16,7,12])).
% 198.89/198.85 cnf(2314,plain,
% 198.89/198.85 (P2(f7(a4,f7(a4,a4)),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2271,2289,8,16,7,12,13])).
% 198.89/198.85 cnf(2318,plain,
% 198.89/198.85 (P1(f7(f7(a4,a4),f7(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2271,2133,2289,8,16,7,12,13,10,15])).
% 198.89/198.85 cnf(2324,plain,
% 198.89/198.85 (P2(f7(f3(a1,a4),f7(a4,a4)),f7(a4,f7(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2263,2271,2275,2133,2289,8,16,7,12,13,10,15,25,24,26])).
% 198.89/198.85 cnf(2330,plain,
% 198.89/198.85 (P3(f3(a1,f3(a1,a1)),f7(f7(a1,a1),f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2263,2271,2275,2133,2289,2173,2279,2111,8,16,7,12,13,10,15,25,24,26,14,27,19])).
% 198.89/198.85 cnf(2355,plain,
% 198.89/198.85 (P2(f3(a1,f3(a4,a4)),f3(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2318,2275,16,7,12])).
% 198.89/198.85 cnf(2357,plain,
% 198.89/198.85 (P2(f7(a4,f3(a4,a4)),f3(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[2318,2275,16,7,12,13])).
% 198.89/198.85 cnf(2359,plain,
% 198.89/198.85 (P2(f7(a4,a4),f7(a4,f7(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2314,2318,2275,16,7,12,13,10])).
% 198.89/198.85 cnf(2361,plain,
% 198.89/198.85 (P1(f7(f3(a4,a4),f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2314,2318,2275,16,7,12,13,10,15])).
% 198.89/198.85 cnf(2363,plain,
% 198.89/198.85 (P2(f3(f7(a4,a4),f3(a4,a4)),f3(a4,f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2267,2314,2318,2275,16,7,12,13,10,15,25])).
% 198.89/198.85 cnf(2365,plain,
% 198.89/198.85 (P2(f7(f7(a4,a4),f3(a4,a4)),f7(a4,f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2267,2314,2318,2275,16,7,12,13,10,15,25,26])).
% 198.89/198.85 cnf(2367,plain,
% 198.89/198.85 (P1(f3(f3(a4,a4),f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2267,2314,2318,2275,16,7,12,13,10,15,25,26,14])).
% 198.89/198.85 cnf(2371,plain,
% 198.89/198.85 (~P2(f5(a2),f3(a4,f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[6,2267,2314,2261,2318,2330,2019,2275,16,7,12,13,10,15,25,26,14,19,17])).
% 198.89/198.85 cnf(2380,plain,
% 198.89/198.85 (P3(a1,f3(f7(a1,a1),f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2040,2361,1987,2221,10,7,19])).
% 198.89/198.85 cnf(2382,plain,
% 198.89/198.85 (P2(f7(a4,f3(a1,a1)),a1)),
% 198.89/198.85 inference(scs_inference,[],[2040,2361,1987,2221,10,7,19,17])).
% 198.89/198.85 cnf(2388,plain,
% 198.89/198.85 (P2(f3(a2,a2),f3(a1,f3(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2233,10])).
% 198.89/198.85 cnf(2390,plain,
% 198.89/198.85 (P1(f5(a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2233,10,7])).
% 198.89/198.85 cnf(2398,plain,
% 198.89/198.85 (P1(f3(f5(a1),f5(a1)))),
% 198.89/198.85 inference(scs_inference,[],[1,2233,2013,10,7,25,23,26,14])).
% 198.89/198.85 cnf(2400,plain,
% 198.89/198.85 (P3(f7(a4,f7(a4,a4)),a4)),
% 198.89/198.85 inference(scs_inference,[],[1,2233,2013,2359,818,10,7,25,23,26,14,19])).
% 198.89/198.85 cnf(2404,plain,
% 198.89/198.85 (~P2(f3(a1,a1),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[1,2189,2233,2013,2359,2380,2113,818,1210,10,7,25,23,26,14,19,20,17])).
% 198.89/198.85 cnf(2406,plain,
% 198.89/198.85 (P3(f3(a1,a1),f3(f3(f7(a1,a1),f3(a1,a1)),a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2189,2233,2013,2359,2380,2113,818,1210,10,7,25,23,26,14,19,20,17,27])).
% 198.89/198.85 cnf(2410,plain,
% 198.89/198.85 (P2(f3(a1,f5(a1)),f5(a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2189,2233,2013,2359,2380,2113,818,1210,10,7,25,23,26,14,19,20,17,27,16,12])).
% 198.89/198.85 cnf(2412,plain,
% 198.89/198.85 (P2(f7(a4,f5(a1)),f5(a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2189,2233,2013,2359,2380,2113,818,1210,10,7,25,23,26,14,19,20,17,27,16,12,13])).
% 198.89/198.85 cnf(2429,plain,
% 198.89/198.85 (P2(f7(a4,f3(a2,a2)),f3(a1,f3(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[2390,2237,2388,2400,1768,10,7,25,26,20,17])).
% 198.89/198.85 cnf(2448,plain,
% 198.89/198.85 (P2(f7(f7(a4,f3(a1,a1)),a1),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2083,2398,2382,10,7,25,26])).
% 198.89/198.85 cnf(2462,plain,
% 198.89/198.85 (P2(f7(a4,a4),f3(a1,f7(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2312,10])).
% 198.89/198.85 cnf(2493,plain,
% 198.89/198.85 (~P2(f3(a1,f7(a4,a4)),a2)),
% 198.89/198.85 inference(scs_inference,[],[1,2355,2462,2367,1482,1406,10,7,25,26,17])).
% 198.89/198.85 cnf(2502,plain,
% 198.89/198.85 (P2(f3(a4,a4),f7(a4,f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2357,10])).
% 198.89/198.85 cnf(2522,plain,
% 198.89/198.85 (P2(f3(a4,a1),f3(f3(a2,a4),a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2410,2249,750,10,7,25])).
% 198.89/198.85 cnf(2541,plain,
% 198.89/198.85 (P3(f7(a4,a1),f3(f3(f7(a1,a1),f3(a1,a1)),a1))),
% 198.89/198.85 inference(scs_inference,[],[2412,2406,2205,2137,2275,10,7,25,19])).
% 198.89/198.85 cnf(2543,plain,
% 198.89/198.85 (P2(f7(f7(a4,f5(a1)),f3(a4,a4)),f7(f5(a1),f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2412,2406,2205,2137,2275,10,7,25,19,26])).
% 198.89/198.85 cnf(2570,plain,
% 198.89/198.85 (P2(f3(f3(a2,a4),a1),f3(a4,a1))),
% 198.89/198.85 inference(scs_inference,[],[2522,10])).
% 198.89/198.85 cnf(2578,plain,
% 198.89/198.85 (P2(f3(f7(a4,a4),f3(a4,a4)),f3(f3(a4,a4),a4))),
% 198.89/198.85 inference(scs_inference,[],[1997,2522,2363,2147,2115,2271,10,7,25,26,17])).
% 198.89/198.85 cnf(2591,plain,
% 198.89/198.85 (P2(f7(f3(a1,a2),a1),f7(a2,a1))),
% 198.89/198.85 inference(scs_inference,[],[1,2578,2054,53,2167,10,7,25,26])).
% 198.89/198.85 cnf(2602,plain,
% 198.89/198.85 (P1(f5(a4))),
% 198.89/198.85 inference(scs_inference,[],[2,2591,10,7])).
% 198.89/198.85 cnf(2646,plain,
% 198.89/198.85 (P2(f3(a1,a4),f3(a1,a4))),
% 198.89/198.85 inference(scs_inference,[],[2,2602,2023,39,10,7,25])).
% 198.89/198.85 cnf(2680,plain,
% 198.89/198.85 (P2(f3(f7(a4,a2),a4),f3(a2,a4))),
% 198.89/198.85 inference(scs_inference,[],[2,2072,2038,2171,10,7,25])).
% 198.89/198.85 cnf(2700,plain,
% 198.89/198.85 (P2(f3(f7(a4,a2),a4),f7(a4,f6(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2570,2680,2097,2602,1290,7,10,25,26,17])).
% 198.89/198.85 cnf(2710,plain,
% 198.89/198.85 (P2(f3(f3(a4,f5(a4)),a4),f3(a1,a4))),
% 198.89/198.85 inference(scs_inference,[],[2,2070,2261,156,10,7,25])).
% 198.89/198.85 cnf(2760,plain,
% 198.89/198.85 (P2(f3(f3(a4,a4),f5(a4)),f3(f7(a4,f3(a4,a4)),f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2502,2324,2541,1989,195,2602,7,10,19,25])).
% 198.89/198.85 cnf(2762,plain,
% 198.89/198.85 (P2(f7(f3(a4,a4),f5(a4)),f7(f7(a4,f3(a4,a4)),f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2502,2324,2541,1989,195,2602,7,10,19,25,26])).
% 198.89/198.85 cnf(2806,plain,
% 198.89/198.85 (P1(f5(a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2429,10,7])).
% 198.89/198.85 cnf(2808,plain,
% 198.89/198.85 (P1(f7(f5(a2),f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[3,2429,10,7,15])).
% 198.89/198.85 cnf(2814,plain,
% 198.89/198.85 (P1(f3(f5(a2),f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[3,2429,10,7,15,24,23,14])).
% 198.89/198.85 cnf(2824,plain,
% 198.89/198.85 (P2(f3(a1,f5(a2)),f5(a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2429,2404,2646,2173,10,7,15,24,23,14,25,26,17,8,12])).
% 198.89/198.85 cnf(2826,plain,
% 198.89/198.85 (P2(f7(a4,f5(a2)),f5(a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2429,2404,2646,2173,10,7,15,24,23,14,25,26,17,8,12,13])).
% 198.89/198.85 cnf(2839,plain,
% 198.89/198.85 (P1(f5(f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[2806,2824,10,7])).
% 198.89/198.85 cnf(2858,plain,
% 198.89/198.85 (P2(f5(a2),f7(a4,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[2826,10])).
% 198.89/198.85 cnf(2862,plain,
% 198.89/198.85 (P2(f3(a1,a2),f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2826,2814,1211,10,7,25])).
% 198.89/198.85 cnf(2864,plain,
% 198.89/198.85 (P2(f7(a1,a2),f7(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2826,2814,1211,10,7,25,26])).
% 198.89/198.85 cnf(2880,plain,
% 198.89/198.85 (~P2(f3(a2,a2),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[3,2862,2255,2808,10,7,25,26,17])).
% 198.89/198.85 cnf(2930,plain,
% 198.89/198.85 (P2(f7(f7(a1,a2),a2),f7(f7(a2,a2),a2))),
% 198.89/198.85 inference(scs_inference,[],[3,2700,2864,2179,10,7,25,26])).
% 198.89/198.85 cnf(2934,plain,
% 198.89/198.85 (~P2(f3(a1,f3(a2,a2)),f7(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[3,2880,2700,2388,2864,2400,2179,10,7,25,26,27,17])).
% 198.89/198.85 cnf(2964,plain,
% 198.89/198.85 (~P2(f7(a4,f5(a2)),f3(a2,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[3,2223,2930,2858,45,10,25,26,17])).
% 198.89/198.85 cnf(3134,plain,
% 198.89/198.85 (P2(f7(a1,a1),f7(f7(a4,f3(a1,a1)),a1))),
% 198.89/198.85 inference(scs_inference,[],[2448,10])).
% 198.89/198.85 cnf(3232,plain,
% 198.89/198.85 (P2(f7(f5(a1),f3(a4,a4)),f7(f7(a4,f5(a1)),f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[2543,10])).
% 198.89/198.85 cnf(3244,plain,
% 198.89/198.85 (P3(a2,f3(f7(a2,a2),a2))),
% 198.89/198.85 inference(scs_inference,[],[2762,2167,2087,2017,134,10,17,19])).
% 198.89/198.85 cnf(3246,plain,
% 198.89/198.85 (P3(a1,f3(f7(a2,a2),a2))),
% 198.89/198.85 inference(scs_inference,[],[2762,2167,2087,2017,134,10,17,19,37])).
% 198.89/198.85 cnf(3250,plain,
% 198.89/198.85 (P1(f6(f6(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2762,2167,2087,2017,134,2003,10,17,19,37,21,9])).
% 198.89/198.85 cnf(3273,plain,
% 198.89/198.85 (P3(f3(a1,f5(a1)),f3(f3(f7(a2,a2),a2),f5(a1)))),
% 198.89/198.85 inference(scs_inference,[],[3246,3250,3244,3232,2760,2543,1199,2390,2275,8,7,10,17,20,21,27])).
% 198.89/198.85 cnf(3423,plain,
% 198.89/198.85 (P2(a1,f3(f3(a1,a1),f5(f3(a1,a1))))),
% 198.89/198.85 inference(scs_inference,[],[2034,10])).
% 198.89/198.85 cnf(3461,plain,
% 198.89/198.85 (P2(a1,f3(f7(a4,a4),f5(f7(a4,a4))))),
% 198.89/198.85 inference(scs_inference,[],[2308,10])).
% 198.89/198.85 cnf(3569,plain,
% 198.89/198.85 (P2(a1,f7(a4,f3(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[2382,10])).
% 198.89/198.85 cnf(3597,plain,
% 198.89/198.85 (P2(f6(a4),f7(a4,f6(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2087,10])).
% 198.89/198.85 cnf(3605,plain,
% 198.89/198.85 (P2(a1,f3(a1,f5(a1)))),
% 198.89/198.85 inference(scs_inference,[],[1991,10])).
% 198.89/198.85 cnf(3607,plain,
% 198.89/198.85 (~P2(f7(a4,f3(a1,a1)),f3(a2,a4))),
% 198.89/198.85 inference(scs_inference,[],[3569,1058,1991,10,17])).
% 198.89/198.85 cnf(3613,plain,
% 198.89/198.85 (P2(a1,f3(a2,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[2165,10])).
% 198.89/198.85 cnf(3615,plain,
% 198.89/198.85 (~P2(f3(a1,a1),f3(a2,a4))),
% 198.89/198.85 inference(scs_inference,[],[3607,2040,2165,10,17])).
% 198.89/198.85 cnf(3640,plain,
% 198.89/198.85 (P2(f7(f6(a4),f5(a4)),f7(f7(a4,f6(a4)),f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[3597,3613,1185,1391,2602,10,25,17,26])).
% 198.89/198.85 cnf(3642,plain,
% 198.89/198.85 (P3(f3(a4,f5(a1)),f3(a4,f5(a1)))),
% 198.89/198.85 inference(scs_inference,[],[43,3597,3613,1185,1391,2602,2390,10,25,17,26,27])).
% 198.89/198.85 cnf(3657,plain,
% 198.89/198.85 (P2(f7(f7(a4,f6(a4)),f5(a4)),f7(f6(a4),f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[3640,10])).
% 198.89/198.85 cnf(3661,plain,
% 198.89/198.85 (~P2(f3(f7(a4,a4),f5(f7(a4,a4))),f5(a2))),
% 198.89/198.85 inference(scs_inference,[],[3640,3461,3642,31,10,18,17])).
% 198.89/198.85 cnf(3742,plain,
% 198.89/198.85 (P2(a1,f3(f5(a2),f5(f5(a2))))),
% 198.89/198.85 inference(scs_inference,[],[92,10])).
% 198.89/198.85 cnf(3781,plain,
% 198.89/198.85 (P3(a1,f7(a2,f7(a1,a1)))),
% 198.89/198.85 inference(scs_inference,[],[3742,2015,19,123])).
% 198.89/198.85 cnf(3783,plain,
% 198.89/198.85 (P3(f3(a1,a2),f3(f7(a2,f7(a1,a1)),a2))),
% 198.89/198.85 inference(scs_inference,[],[3742,2015,19,123,127])).
% 198.89/198.85 cnf(3825,plain,
% 198.89/198.85 (P3(a1,f3(f7(a2,f7(a1,a1)),a2))),
% 198.89/198.85 inference(scs_inference,[],[3783,3423,2167,1058,19,17,37])).
% 198.89/198.85 cnf(3989,plain,
% 198.89/198.85 (~P2(f3(a1,f5(a1)),f3(a1,a4))),
% 198.89/198.85 inference(scs_inference,[],[3605,1185,17])).
% 198.89/198.85 cnf(4014,plain,
% 198.89/198.85 (P3(f3(a1,f7(a2,a2)),f3(a2,f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[51,3657,3640,3423,2175,17,19,27])).
% 198.89/198.85 cnf(4041,plain,
% 198.89/198.85 (~P2(f5(a1),f3(a1,a4))),
% 198.89/198.85 inference(scs_inference,[],[3989,2410,17])).
% 198.89/198.85 cnf(4159,plain,
% 198.89/198.85 (P2(f7(f3(a2,f5(a4)),f5(a4)),f7(f3(a1,f5(a4)),f5(a4)))),
% 198.89/198.85 inference(scs_inference,[],[2310,651,2215,868,410,16,8,12,13,7,10])).
% 198.89/198.85 cnf(4203,plain,
% 198.89/198.85 (P3(f7(a2,a2),f3(a2,f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[1216,2195,2404,3781,4014,2710,10,729,733,20,19])).
% 198.89/198.85 cnf(4287,plain,
% 198.89/198.85 (P3(a1,f3(f3(f7(a2,a2),a2),f5(a1)))),
% 198.89/198.85 inference(scs_inference,[],[1375,1991,2017,3273,10,515,19])).
% 198.89/198.85 cnf(4315,plain,
% 198.89/198.85 (P3(f7(a1,a1),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[51,525,1216,2001,933,246,2044,2934,3825,10,515,20,19,17,11])).
% 198.89/198.85 cnf(4347,plain,
% 198.89/198.85 (P2(a2,f3(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[1255,2862,2203,3989,10,19,17])).
% 198.89/198.85 cnf(4387,plain,
% 198.89/198.85 (P3(a2,f3(a2,f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[1255,2410,2371,3273,4203,10,19,20])).
% 198.89/198.85 cnf(4405,plain,
% 198.89/198.85 (P2(f7(a4,a4),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[1216,2087,1460,4041,4287,10,20,17])).
% 198.89/198.85 cnf(4423,plain,
% 198.89/198.85 (P3(a1,f3(a2,f7(a2,a2)))),
% 198.89/198.85 inference(scs_inference,[],[51,4,2093,2189,4387,10,17,20])).
% 198.89/198.85 cnf(4443,plain,
% 198.89/198.85 (P2(f7(f7(a4,a4),f3(a4,a4)),f3(a4,a4))),
% 198.89/198.85 inference(scs_inference,[],[51,1216,2357,3605,2365,3615,4423,10,20,19,17])).
% 198.89/198.85 cnf(4599,plain,
% 198.89/198.85 (P3(f7(a2,a1),f7(a1,a1))),
% 198.89/198.85 inference(scs_inference,[],[1212,2493,4315,10,19])).
% 198.89/198.85 cnf(5039,plain,
% 198.89/198.85 (P3(f3(a2,a2),f7(a2,a2))),
% 198.89/198.85 inference(scs_inference,[],[1255,651,4159,3661,4347,10,17,19])).
% 198.89/198.85 cnf(5417,plain,
% 198.89/198.85 (~P2(f3(a2,f5(a2)),f7(a4,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[2964,10])).
% 198.89/198.85 cnf(5872,plain,
% 198.89/198.85 (P2(f7(a2,a1),f7(f7(a4,f3(a1,a1)),a1))),
% 198.89/198.85 inference(scs_inference,[],[1213,3134,17])).
% 198.89/198.85 cnf(5891,plain,
% 198.89/198.85 (P2(f3(a1,a4),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[1009,4599,4405,5872,19,17])).
% 198.89/198.85 cnf(5899,plain,
% 198.89/198.85 (P2(a4,f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[749,5891,17])).
% 198.89/198.85 cnf(5914,plain,
% 198.89/198.85 (P2(f3(a2,a4),f6(a4))),
% 198.89/198.85 inference(scs_inference,[],[752,5899,17])).
% 198.89/198.85 cnf(5986,plain,
% 198.89/198.85 (P2(f3(a4,a4),f7(f7(a4,a4),f3(a4,a4)))),
% 198.89/198.85 inference(scs_inference,[],[4,1,4443,5039,2003,25,26,27,10])).
% 198.89/198.85 cnf(6201,plain,
% 198.89/198.85 (P2(f3(a1,f7(f5(a2),f5(a2))),f7(f5(a2),f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[1,5986,1593,2808,15,22,25,14,13,26,12])).
% 198.89/198.85 cnf(6224,plain,
% 198.89/198.85 (P2(f7(a4,f5(f5(a2))),f5(f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[4,2275,2839,15,25,14,13])).
% 198.89/198.85 cnf(6487,plain,
% 198.89/198.85 (P2(f3(a2,f5(a2)),f3(a1,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[4,2147,2806,15,25])).
% 198.89/198.85 cnf(6521,plain,
% 198.89/198.85 (~P2(f3(a1,f5(a2)),f7(a4,f5(a2)))),
% 198.89/198.85 inference(scs_inference,[],[1,6201,6487,5914,5417,2201,15,25,13,26,14,12,10,17])).
% 198.89/198.85 cnf(6539,plain,
% 198.89/198.85 ($false),
% 198.89/198.85 inference(scs_inference,[],[6224,6521,2824,2858,2205,15,13,14,12,10,17]),
% 198.89/198.85 ['proof']).
% 198.89/198.85 % SZS output end Proof
% 198.89/198.85 % Total time :198.130000s
%------------------------------------------------------------------------------