%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : FLD040-3 : 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 : n002.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:23 EDT 2024
% Result : Unsatisfiable 58.69s 58.75s
% Output : CNFRefutation 58.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : FLD040-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n002.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 10:09:08 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.55/0.57 start to proof:theBenchmark
% 58.69/58.74 %-------------------------------------------
% 58.69/58.74 % File :CSE---1.7
% 58.69/58.74 % Problem :theBenchmark
% 58.69/58.74 % Transform :cnf
% 58.69/58.74 % Format :tptp:raw
% 58.69/58.74 % Command :java -jar mcs_scs.jar %d %s
% 58.69/58.74
% 58.69/58.74 % Result :Theorem 58.140000s
% 58.69/58.74 % Output :CNFRefutation 58.140000s
% 58.69/58.74 %-------------------------------------------
% 58.69/58.75 %--------------------------------------------------------------------------
% 58.69/58.75 % File : FLD040-3 : TPTP v8.2.0. Bugfixed v2.1.0.
% 58.69/58.75 % Domain : Field Theory (Ordered fields)
% 58.69/58.75 % Problem : If a is not 0, then the multiplicative inverse of a is not 0
% 58.69/58.75 % Version : [Dra93] axioms : Especial.
% 58.69/58.75 % Theorem formulation : Functional with re axiom set.
% 58.69/58.75 % English :
% 58.69/58.75
% 58.69/58.75 % Refs : [Dra93] Draeger (1993), Anwendung des Theorembeweisers SETHEO
% 58.69/58.75 % Source : [Dra93]
% 58.69/58.75 % Names :
% 58.69/58.75
% 58.69/58.75 % Status : Unsatisfiable
% 58.69/58.75 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0, 0.20 v2.3.0, 0.00 v2.2.1, 0.33 v2.1.0
% 58.69/58.75 % Syntax : Number of clauses : 29 ( 6 unt; 3 nHn; 29 RR)
% 58.69/58.75 % Number of literals : 80 ( 0 equ; 50 neg)
% 58.69/58.75 % Maximal clause size : 5 ( 2 avg)
% 58.69/58.75 % Maximal term depth : 2 ( 1 avg)
% 58.69/58.75 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty)
% 58.69/58.75 % Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% 58.69/58.75 % Number of variables : 73 ( 0 sgn)
% 58.69/58.75 % SPC : CNF_UNS_RFO_NEQ_NHN
% 58.69/58.75
% 58.69/58.75 % Comments :
% 58.69/58.75 % Bugfixes : v2.1.0 - Bugfix in FLD002-0.ax
% 58.69/58.75 %--------------------------------------------------------------------------
% 58.69/58.75 include('Axioms/FLD002-0.ax').
% 58.69/58.75 %--------------------------------------------------------------------------
% 58.69/58.75 cnf(a_is_defined,hypothesis,
% 58.69/58.75 defined(a) ).
% 58.69/58.75
% 58.69/58.75 cnf(not_sum_2,negated_conjecture,
% 58.69/58.75 ~ sum(additive_identity,a,additive_identity) ).
% 58.69/58.75
% 58.69/58.75 cnf(sum_3,negated_conjecture,
% 58.69/58.75 sum(additive_identity,additive_identity,multiplicative_inverse(a)) ).
% 58.69/58.75
% 58.69/58.75 %--------------------------------------------------------------------------
% 58.69/58.75 %-------------------------------------------
% 58.69/58.75 % Proof found
% 58.69/58.75 % SZS status Theorem for theBenchmark
% 58.69/58.75 % SZS output start Proof
% 58.69/58.75 %ClaNum:29(EqnAxiom:0)
% 58.69/58.75 %VarNum:162(SingletonVarNum:73)
% 58.69/58.75 %MaxLitNum:5
% 58.69/58.75 %MaxfuncDepth:1
% 58.69/58.75 %SharedTerms:10
% 58.69/58.75 %goalClause: 4 6
% 58.69/58.75 %singleGoalClaCount:2
% 58.69/58.76 [1]P1(a1)
% 58.69/58.76 [2]P1(a4)
% 58.69/58.76 [3]P1(a2)
% 58.69/58.76 [5]~P2(a1,a1,a4)
% 58.69/58.76 [6]~P2(a1,a2,a1)
% 58.69/58.76 [4]P2(a1,a1,f6(a2))
% 58.69/58.76 [12]~P1(x121)+P2(a1,x121,x121)
% 58.69/58.76 [13]~P1(x131)+P4(a4,x131,x131)
% 58.69/58.76 [7]~P1(x71)+P1(f5(x71))
% 58.69/58.76 [14]~P1(x141)+P2(f5(x141),x141,a1)
% 58.69/58.76 [21]~P2(x212,x211,x213)+P2(x211,x212,x213)
% 58.69/58.76 [22]~P4(x222,x221,x223)+P4(x221,x222,x223)
% 58.69/58.76 [15]~P1(x151)+P2(a1,x151,a1)+P1(f6(x151))
% 58.69/58.76 [19]~P1(x191)+P4(f6(x191),x191,a4)+P2(a1,x191,a1)
% 58.69/58.76 [18]~P3(x182,x181)+~P3(x181,x182)+P2(a1,x181,x182)
% 58.69/58.76 [9]~P1(x92)+~P1(x91)+P1(f3(x91,x92))
% 58.69/58.76 [10]~P1(x102)+~P1(x101)+P1(f7(x101,x102))
% 58.69/58.76 [16]~P1(x162)+~P1(x161)+P2(x161,x162,f3(x161,x162))
% 58.69/58.76 [17]~P1(x172)+~P1(x171)+P4(x171,x172,f7(x171,x172))
% 58.69/58.76 [11]~P3(x111,x113)+P3(x111,x112)+~P3(x113,x112)
% 58.69/58.76 [8]P3(x82,x81)+~P1(x81)+~P1(x82)+P3(x81,x82)
% 58.69/58.76 [20]~P4(x203,x202,x201)+P3(a1,x201)+~P3(a1,x202)+~P3(a1,x203)
% 58.69/58.76 [23]~P2(x233,x235,x231)+P3(x231,x232)+~P2(x234,x235,x232)+~P3(x233,x234)
% 58.69/58.76 [24]~P2(x241,x246,x244)+P2(x241,x242,x243)+~P2(x244,x245,x243)+~P2(x246,x245,x242)
% 58.69/58.76 [25]~P2(x256,x254,x251)+P2(x251,x252,x253)+~P2(x254,x252,x255)+~P2(x256,x255,x253)
% 58.69/58.76 [26]~P4(x261,x266,x264)+P4(x261,x262,x263)+~P4(x264,x265,x263)+~P4(x266,x265,x262)
% 58.69/58.76 [27]~P4(x276,x274,x271)+P4(x271,x272,x273)+~P4(x274,x272,x275)+~P4(x276,x275,x273)
% 58.69/58.76 [28]~P4(x285,x287,x282)+~P4(x284,x287,x281)+P2(x281,x282,x283)+~P2(x284,x285,x286)+~P4(x286,x287,x283)
% 58.69/58.76 [29]~P4(x297,x292,x295)+~P4(x296,x292,x294)+P4(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x297,x291)
% 58.69/58.76 %EqnAxiom
% 58.69/58.76
% 58.69/58.76 %-------------------------------------------
% 58.69/58.76 cnf(32,plain,
% 58.69/58.76 (P3(a1,a1)),
% 58.69/58.76 inference(scs_inference,[],[6,1,21,8])).
% 58.69/58.76 cnf(38,plain,
% 58.69/58.76 (P2(f6(a2),x381,f6(a2))+~P2(a1,x381,a1)),
% 58.69/58.76 inference(scs_inference,[],[4,6,1,21,8,18,23,25])).
% 58.69/58.76 cnf(42,plain,
% 58.69/58.76 (P3(a4,a4)),
% 58.69/58.76 inference(scs_inference,[],[2,8])).
% 58.69/58.76 cnf(49,plain,
% 58.69/58.76 (P3(a2,a2)),
% 58.69/58.76 inference(scs_inference,[],[3,8])).
% 58.69/58.76 cnf(81,plain,
% 58.69/58.76 (P2(a1,f5(a4),f5(a4))),
% 58.69/58.76 inference(scs_inference,[],[2,12,7])).
% 58.69/58.76 cnf(103,plain,
% 58.69/58.76 (P4(a4,f5(a2),f5(a2))),
% 58.69/58.76 inference(scs_inference,[],[3,13,7])).
% 58.69/58.76 cnf(104,plain,
% 58.69/58.76 (~P4(x1041,a4,a4)+P4(x1041,f5(a2),f5(a2))),
% 58.69/58.76 inference(scs_inference,[],[103,26])).
% 58.69/58.76 cnf(110,plain,
% 58.69/58.76 (P2(f5(a2),f5(a2),f5(a2))+~P2(a4,a4,a4)),
% 58.69/58.76 inference(scs_inference,[],[103,28])).
% 58.69/58.76 cnf(157,plain,
% 58.69/58.76 (P2(f5(f5(a1)),f5(a1),a1)),
% 58.69/58.76 inference(scs_inference,[],[1,14,7])).
% 58.69/58.76 cnf(160,plain,
% 58.69/58.76 (~P2(a2,f5(a1),f5(a1))),
% 58.69/58.76 inference(scs_inference,[],[6,157,25,21])).
% 58.69/58.76 cnf(209,plain,
% 58.69/58.76 (P2(x2091,f6(a2),f6(a2))+~P2(a1,x2091,a1)),
% 58.69/58.76 inference(scs_inference,[],[38,21])).
% 58.69/58.76 cnf(241,plain,
% 58.69/58.76 (P4(f5(a2),x2411,f5(a2))+~P4(x2411,a4,a4)),
% 58.69/58.76 inference(scs_inference,[],[104,22])).
% 58.69/58.76 cnf(779,plain,
% 58.69/58.76 (~P2(x7791,a1,a1)+P2(x7791,f6(a2),f6(a2))),
% 58.69/58.76 inference(scs_inference,[],[4,24])).
% 58.69/58.76 cnf(800,plain,
% 58.69/58.76 (P2(f6(a2),x8001,f6(a2))+~P2(x8001,a1,a1)),
% 58.69/58.76 inference(scs_inference,[],[779,21])).
% 58.69/58.76 cnf(848,plain,
% 58.69/58.76 (~P2(x8481,f6(a2),a1)+P2(x8481,f6(a2),f6(a2))+~P2(a1,a1,a1)),
% 58.69/58.76 inference(scs_inference,[],[4,800,24])).
% 58.69/58.77 cnf(865,plain,
% 58.69/58.77 (P2(f6(a2),f5(a4),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[4,81,25])).
% 58.69/58.77 cnf(877,plain,
% 58.69/58.77 (~P2(f6(a2),f6(a2),x8771)+P2(x8771,f5(a4),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[865,25])).
% 58.69/58.77 cnf(1342,plain,
% 58.69/58.77 (P2(x13421,f6(a2),f6(a2))+~P2(x13421,f6(a2),a1)),
% 58.69/58.77 inference(scs_inference,[],[1,848,12])).
% 58.69/58.77 cnf(1358,plain,
% 58.69/58.77 (P2(f6(a2),x13581,f6(a2))+~P2(x13581,f6(a2),a1)),
% 58.69/58.77 inference(scs_inference,[],[1342,21])).
% 58.69/58.77 cnf(2275,plain,
% 58.69/58.77 (P2(a1,f5(a1),f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[1,7,12])).
% 58.69/58.77 cnf(2276,plain,
% 58.69/58.77 (~P2(a1,a1,a2)),
% 58.69/58.77 inference(scs_inference,[],[160,2275,25])).
% 58.69/58.77 cnf(2311,plain,
% 58.69/58.77 (P4(a4,f5(a1),f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[1,7,13])).
% 58.69/58.77 cnf(2315,plain,
% 58.69/58.77 (~P4(x23151,a4,a4)+P4(x23151,f5(a1),f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[2311,26])).
% 58.69/58.77 cnf(2318,plain,
% 58.69/58.77 (P2(f5(a1),f5(a1),f5(a1))+~P2(a4,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2311,28])).
% 58.69/58.77 cnf(2320,plain,
% 58.69/58.77 (~P2(f5(a1),f5(a1),a2)+~P2(a4,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[160,2311,28,25])).
% 58.69/58.77 cnf(2335,plain,
% 58.69/58.77 (P4(f5(a1),x23351,f5(a1))+~P4(x23351,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2315,22])).
% 58.69/58.77 cnf(2637,plain,
% 58.69/58.77 (P4(a4,f5(a4),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[2,7,13])).
% 58.69/58.77 cnf(2638,plain,
% 58.69/58.77 (~P4(x26381,a4,a4)+P4(x26381,f5(a4),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[2637,26])).
% 58.69/58.77 cnf(2640,plain,
% 58.69/58.77 (P2(f5(a4),f5(a4),f5(a4))+~P2(a4,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2637,26,28])).
% 58.69/58.77 cnf(2659,plain,
% 58.69/58.77 (P2(f5(a4),f5(a4),f5(a4))+~P2(a4,a4,x26591)+~P4(x26591,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2637,2638,28])).
% 58.69/58.77 cnf(2705,plain,
% 58.69/58.77 (P2(f5(a4),f5(a4),f5(a4))+~P4(a4,x27051,a4)+~P2(a4,a4,x27051)),
% 58.69/58.77 inference(scs_inference,[],[2659,22])).
% 58.69/58.77 cnf(2721,plain,
% 58.69/58.77 (P2(f5(a4),f5(a4),f5(a4))+~P4(a4,f3(a4,a4),a4)),
% 58.69/58.77 inference(scs_inference,[],[2,2705,16])).
% 58.69/58.77 cnf(2737,plain,
% 58.69/58.77 (P2(f5(a4),f5(a4),f5(a4))+~P4(f3(a4,a4),a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2721,22])).
% 58.69/58.77 cnf(2816,plain,
% 58.69/58.77 (P2(f5(f5(a4)),f5(a4),a1)),
% 58.69/58.77 inference(scs_inference,[],[2,7,14])).
% 58.69/58.77 cnf(2819,plain,
% 58.69/58.77 (~P2(a2,f5(a4),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[6,2816,25,21])).
% 58.69/58.77 cnf(2821,plain,
% 58.69/58.77 (~P2(a2,f6(a2),f6(a2))),
% 58.69/58.77 inference(scs_inference,[],[6,865,2816,25,21,24])).
% 58.69/58.77 cnf(2823,plain,
% 58.69/58.77 (~P2(f6(a2),f6(a2),a2)),
% 58.69/58.77 inference(scs_inference,[],[6,865,2816,25,21,24,877])).
% 58.69/58.77 cnf(2833,plain,
% 58.69/58.77 (~P2(f6(a2),a1,x28331)+~P2(x28331,a1,a2)),
% 58.69/58.77 inference(scs_inference,[],[4,2823,24])).
% 58.69/58.77 cnf(2866,plain,
% 58.69/58.77 (~P2(f6(a2),a1,a2)+~P2(a1,a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[2833,38])).
% 58.69/58.77 cnf(2914,plain,
% 58.69/58.77 (~P2(f6(a2),a1,a2)),
% 58.69/58.77 inference(scs_inference,[],[1,2866,12])).
% 58.69/58.77 cnf(2915,plain,
% 58.69/58.77 (~P2(a1,f6(a2),a2)),
% 58.69/58.77 inference(scs_inference,[],[2914,21])).
% 58.69/58.77 cnf(3015,plain,
% 58.69/58.77 (~P2(x30151,f6(a2),a2)+~P2(x30151,a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[2276,4,25])).
% 58.69/58.77 cnf(3020,plain,
% 58.69/58.77 (~P2(f5(f5(a1)),x30201,a2)+~P2(f5(a1),f6(a2),x30201)),
% 58.69/58.77 inference(scs_inference,[],[2915,157,25])).
% 58.69/58.77 cnf(3036,plain,
% 58.69/58.77 (~P2(x30361,f6(a2),a4)+~P2(x30361,a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[4,5,25])).
% 58.69/58.77 cnf(3044,plain,
% 58.69/58.77 (~P2(f5(a1),f6(a2),a2)),
% 58.69/58.77 inference(scs_inference,[],[1,3015,14])).
% 58.69/58.77 cnf(3045,plain,
% 58.69/58.77 (~P2(f6(a2),f5(a1),a2)),
% 58.69/58.77 inference(scs_inference,[],[3044,21])).
% 58.69/58.77 cnf(3115,plain,
% 58.69/58.77 (~P2(f6(a2),x31151,a4)+~P2(x31151,a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[3036,21])).
% 58.69/58.77 cnf(3149,plain,
% 58.69/58.77 (~P2(a1,f5(a1),a2)),
% 58.69/58.77 inference(scs_inference,[],[4,3045,2275,25])).
% 58.69/58.77 cnf(3161,plain,
% 58.69/58.77 (~P2(x31611,f5(a1),a2)+~P2(x31611,a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[3149,2275,25])).
% 58.69/58.77 cnf(3192,plain,
% 58.69/58.77 (~P2(f6(a2),a1,a4)),
% 58.69/58.77 inference(scs_inference,[],[1,3115,12])).
% 58.69/58.77 cnf(3193,plain,
% 58.69/58.77 (~P2(a1,f6(a2),a4)),
% 58.69/58.77 inference(scs_inference,[],[3192,21])).
% 58.69/58.77 cnf(3230,plain,
% 58.69/58.77 (~P4(x32301,f5(a1),a2)+~P2(a4,a4,x32301)+~P2(f5(a1),a1,a1)),
% 58.69/58.77 inference(scs_inference,[],[2311,3161,28])).
% 58.69/58.77 cnf(3231,plain,
% 58.69/58.77 (~P4(x32311,f5(a1),a2)+~P2(x32311,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[160,2311,28])).
% 58.69/58.77 cnf(3236,plain,
% 58.69/58.77 (~P4(x32361,f5(a4),a2)+~P2(x32361,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2819,2637,28])).
% 58.69/58.77 cnf(3238,plain,
% 58.69/58.77 (~P4(f5(a4),x32381,a2)+~P2(x32381,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2819,2637,28,22])).
% 58.69/58.77 cnf(3270,plain,
% 58.69/58.77 (~P4(a1,f5(a1),a2)),
% 58.69/58.77 inference(scs_inference,[],[2,3231,12])).
% 58.69/58.77 cnf(3271,plain,
% 58.69/58.77 (~P4(f5(a1),a1,a2)),
% 58.69/58.77 inference(scs_inference,[],[3270,22])).
% 58.69/58.77 cnf(3304,plain,
% 58.69/58.77 (~P4(a1,f5(a4),a2)),
% 58.69/58.77 inference(scs_inference,[],[2,3236,12])).
% 58.69/58.77 cnf(3305,plain,
% 58.69/58.77 (~P4(f5(a4),a1,a2)),
% 58.69/58.77 inference(scs_inference,[],[3304,22])).
% 58.69/58.77 cnf(3322,plain,
% 58.69/58.77 (~P4(a4,x33221,a2)+~P4(f5(a4),x33222,x33221)+~P2(x33222,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[2637,3238,27])).
% 58.69/58.77 cnf(3410,plain,
% 58.69/58.77 (~P2(f5(a4),x34101,a1)+~P2(f5(a4),x34101,a4)),
% 58.69/58.77 inference(scs_inference,[],[3192,865,24])).
% 58.69/58.77 cnf(3412,plain,
% 58.69/58.77 (~P2(f5(a4),x34121,a1)+~P2(x34121,f5(a4),a4)),
% 58.69/58.77 inference(scs_inference,[],[3192,865,24,21])).
% 58.69/58.77 cnf(3435,plain,
% 58.69/58.77 (~P2(f5(a4),x34351,a1)+~P2(f5(a4),x34351,a2)),
% 58.69/58.77 inference(scs_inference,[],[865,2914,24])).
% 58.69/58.77 cnf(3437,plain,
% 58.69/58.77 (~P2(f5(a4),x34371,a1)+~P2(x34371,f5(a4),a2)),
% 58.69/58.77 inference(scs_inference,[],[865,2914,24,21])).
% 58.69/58.77 cnf(3687,plain,
% 58.69/58.77 (P2(f5(a4),f6(a2),f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[865,21])).
% 58.69/58.77 cnf(3698,plain,
% 58.69/58.77 (P2(f5(a4),f5(f5(a4)),a1)),
% 58.69/58.77 inference(scs_inference,[],[2816,21])).
% 58.69/58.77 cnf(3700,plain,
% 58.69/58.77 (~P2(f5(a4),f5(f5(a4)),a4)),
% 58.69/58.77 inference(scs_inference,[],[3192,865,2816,21,24])).
% 58.69/58.77 cnf(3707,plain,
% 58.69/58.77 (P2(f5(a1),a1,f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[2275,21])).
% 58.69/58.77 cnf(3716,plain,
% 58.69/58.77 (P2(f5(a1),f5(f5(a1)),a1)),
% 58.69/58.77 inference(scs_inference,[],[157,21])).
% 58.69/58.77 cnf(3847,plain,
% 58.69/58.77 (P4(f5(a4),a4,f5(a4))),
% 58.69/58.77 inference(scs_inference,[],[2637,22])).
% 58.69/58.77 cnf(3851,plain,
% 58.69/58.77 (~P4(f6(a2),a4,a2)),
% 58.69/58.77 inference(scs_inference,[],[2637,2819,865,3305,22,27,28])).
% 58.69/58.77 cnf(3861,plain,
% 58.69/58.77 (~P4(f5(a1),x38611,a2)+~P4(a4,a1,x38611)),
% 58.69/58.77 inference(scs_inference,[],[160,2311,2275,3271,22,28,27])).
% 58.69/58.77 cnf(3868,plain,
% 58.69/58.77 (~P4(x38681,f5(a1),a2)+~P4(a4,a1,x38681)),
% 58.69/58.77 inference(scs_inference,[],[3861,22])).
% 58.69/58.77 cnf(3873,plain,
% 58.69/58.77 (~P4(f7(a4,a1),f5(a1),a2)),
% 58.69/58.77 inference(scs_inference,[],[1,2,3868,17])).
% 58.69/58.77 cnf(3891,plain,
% 58.69/58.77 (P4(f6(a2),a2,a4)),
% 58.69/58.77 inference(scs_inference,[],[6,3,19])).
% 58.69/58.77 cnf(3904,plain,
% 58.69/58.77 (P4(a2,f6(a2),a4)),
% 58.69/58.77 inference(scs_inference,[],[3891,22])).
% 58.69/58.77 cnf(3936,plain,
% 58.69/58.77 (~P4(x39361,f6(a2),f6(a2))+P4(x39361,a4,a4)),
% 58.69/58.77 inference(scs_inference,[],[3891,26])).
% 58.69/58.77 cnf(3939,plain,
% 58.69/58.77 (~P4(f3(a4,a4),f6(a2),f6(a2))+P4(f3(a4,a4),f5(a2),f5(a2))),
% 58.69/58.77 inference(scs_inference,[],[3891,26,2737,104])).
% 58.69/58.77 cnf(3941,plain,
% 58.69/58.77 (~P4(f3(a4,a4),f6(a2),f6(a2))+P4(f3(a4,a4),f5(a1),f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[3891,26,2737,104,2315])).
% 58.69/58.77 cnf(3943,plain,
% 58.69/58.77 (~P4(f3(a4,a4),f6(a2),f6(a2))+P4(f5(a1),f3(a4,a4),f5(a1))),
% 58.69/58.77 inference(scs_inference,[],[3891,26,2737,104,2315,2335])).
% 58.69/58.77 cnf(3945,plain,
% 58.69/58.77 (~P4(f3(a4,a4),f6(a2),f6(a2))+P4(f3(a4,a4),f5(a4),f5(a4))),
% 58.79/58.77 inference(scs_inference,[],[3891,26,2737,104,2315,2335,2638])).
% 58.79/58.77 cnf(3947,plain,
% 58.79/58.77 (~P4(f3(a4,a4),f6(a2),f6(a2))+P4(f5(a2),f3(a4,a4),f5(a2))),
% 58.79/58.77 inference(scs_inference,[],[3891,26,2737,104,2315,2335,2638,241])).
% 58.79/58.77 cnf(3949,plain,
% 58.79/58.77 (P4(a4,f3(a4,a4),a4)+~P4(f3(a4,a4),f6(a2),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[3891,26,2737,104,2315,2335,2638,241,22])).
% 58.79/58.77 cnf(4249,plain,
% 58.79/58.77 (~P1(f6(a2))+P4(a4,a4,a4)),
% 58.79/58.77 inference(scs_inference,[],[3936,13])).
% 58.79/58.77 cnf(4265,plain,
% 58.79/58.77 (P4(a4,a4,a4)),
% 58.79/58.77 inference(scs_inference,[],[6,3,4249,15])).
% 58.79/58.77 cnf(4355,plain,
% 58.79/58.77 (~P4(x43551,a4,a1)+~P4(x43552,a4,f6(a2))+~P2(x43552,x43551,a4)),
% 58.79/58.77 inference(scs_inference,[],[3192,4265,28])).
% 58.79/58.77 cnf(5181,plain,
% 58.79/58.77 (~P2(f5(f5(a1)),f6(a2),a2)+~P2(a1,f5(a1),a1)),
% 58.79/58.77 inference(scs_inference,[],[3020,209])).
% 58.79/58.77 cnf(5741,plain,
% 58.79/58.77 (~P2(f5(a1),a1,a1)+~P2(f5(f5(a1)),f6(a2),a2)),
% 58.79/58.77 inference(scs_inference,[],[5181,21])).
% 58.79/58.77 cnf(6107,plain,
% 58.79/58.77 (~P2(f5(f5(a1)),f6(a2),a2)),
% 58.79/58.77 inference(scs_inference,[],[1,5741,14])).
% 58.79/58.77 cnf(6571,plain,
% 58.79/58.77 (P2(f5(a1),f5(f5(a1)),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,3716,2275,25])).
% 58.79/58.77 cnf(6573,plain,
% 58.79/58.77 (P2(f5(f5(a1)),f5(a1),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,3716,2275,25,21])).
% 58.79/58.77 cnf(6584,plain,
% 58.79/58.77 (P2(a1,f6(a2),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[6107,3707,6571,6573,24,25,21])).
% 58.79/58.77 cnf(6587,plain,
% 58.79/58.77 (P2(f5(a4),f5(f5(a4)),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,3698,81,25])).
% 58.79/58.77 cnf(6595,plain,
% 58.79/58.77 (P2(f6(a2),f6(a2),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,6584,25])).
% 58.79/58.77 cnf(6677,plain,
% 58.79/58.77 (~P2(f6(a2),f6(a2),a4)),
% 58.79/58.77 inference(scs_inference,[],[3700,865,6587,25])).
% 58.79/58.77 cnf(7131,plain,
% 58.79/58.77 (~P4(a1,a4,x71311)+~P4(x71311,f5(a1),a2)),
% 58.79/58.77 inference(scs_inference,[],[3270,2311,26])).
% 58.79/58.77 cnf(7136,plain,
% 58.79/58.77 (~P4(a4,f6(a2),a2)),
% 58.79/58.77 inference(scs_inference,[],[3851,3891,3904,26])).
% 58.79/58.77 cnf(7173,plain,
% 58.79/58.77 (~P4(a4,x71731,f6(a2))+~P4(a4,x71731,a2)),
% 58.79/58.77 inference(scs_inference,[],[4265,7136,26])).
% 58.79/58.77 cnf(7212,plain,
% 58.79/58.77 (~P4(f5(a1),x72121,a2)+~P4(a1,a4,x72121)),
% 58.79/58.77 inference(scs_inference,[],[7131,22])).
% 58.79/58.77 cnf(7216,plain,
% 58.79/58.77 (P2(f6(a2),a1,a1)),
% 58.79/58.77 inference(scs_inference,[],[865,3698,24])).
% 58.79/58.77 cnf(7218,plain,
% 58.79/58.77 (P2(a1,f6(a2),a1)),
% 58.79/58.77 inference(scs_inference,[],[865,3698,24,21])).
% 58.79/58.77 cnf(7322,plain,
% 58.79/58.77 (~P4(x73221,a4,f6(a2))+~P4(a4,x73221,a2)),
% 58.79/58.77 inference(scs_inference,[],[7173,22])).
% 58.79/58.77 cnf(7338,plain,
% 58.79/58.77 (~P4(f5(a1),f7(a1,a4),a2)),
% 58.79/58.77 inference(scs_inference,[],[2,1,7212,17])).
% 58.79/58.77 cnf(7418,plain,
% 58.79/58.77 (~P4(a2,a4,f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[3,7322,13])).
% 58.79/58.77 cnf(7419,plain,
% 58.79/58.77 (~P4(a4,a2,f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[3891,3904,7418,26])).
% 58.79/58.77 cnf(7424,plain,
% 58.79/58.77 (~P2(x74241,x74242,a4)+~P4(x74242,a2,a1)+~P4(x74241,a2,a1)),
% 58.79/58.77 inference(scs_inference,[],[4,3193,4265,49,7419,29])).
% 58.79/58.77 cnf(7662,plain,
% 58.79/58.77 (P2(f5(a1),a1,a1)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14])).
% 58.79/58.77 cnf(7664,plain,
% 58.79/58.77 (P2(a1,a1,a1)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14,12])).
% 58.79/58.77 cnf(7666,plain,
% 58.79/58.77 (~P2(f6(a2),a2,a1)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14,12,21])).
% 58.79/58.77 cnf(7668,plain,
% 58.79/58.77 (P4(a4,a1,a1)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14,12,21,13])).
% 58.79/58.77 cnf(7670,plain,
% 58.79/58.77 (P1(f3(a1,a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14,12,21,13,9])).
% 58.79/58.77 cnf(7672,plain,
% 58.79/58.77 (P1(f7(a1,a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,1,7,1342,22,14,12,21,13,9,10])).
% 58.79/58.77 cnf(7676,plain,
% 58.79/58.77 (P2(a1,a1,f3(a1,a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6,1,3,7,1342,22,14,12,21,13,9,10,15,16])).
% 58.79/58.77 cnf(7678,plain,
% 58.79/58.77 (P4(a1,a1,f7(a1,a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6,1,3,7,1342,22,14,12,21,13,9,10,15,16,17])).
% 58.79/58.77 cnf(7680,plain,
% 58.79/58.77 (P2(a1,a4,a4)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6,1,3,42,7,1342,22,14,12,21,13,9,10,15,16,17,18])).
% 58.79/58.77 cnf(7686,plain,
% 58.79/58.77 (P4(a4,f7(a1,a1),f7(a1,a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,7218,6,1,3,32,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26])).
% 58.79/58.77 cnf(7690,plain,
% 58.79/58.77 (P2(a4,a4,a4)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6595,7218,6,1,3,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28])).
% 58.79/58.77 cnf(7692,plain,
% 58.79/58.77 (~P2(f5(a1),f5(a1),a2)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6595,7218,6,1,3,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320])).
% 58.79/58.77 cnf(7693,plain,
% 58.79/58.77 (P2(f5(a1),f5(a1),f5(a1))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6595,7218,6,1,3,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320,2318])).
% 58.79/58.77 cnf(7694,plain,
% 58.79/58.77 (P2(f5(a4),f5(a4),f5(a4))),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6595,7218,6,1,3,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320,2318,2640])).
% 58.79/58.77 cnf(7697,plain,
% 58.79/58.77 (~P4(a4,f5(a4),a2)),
% 58.79/58.77 inference(scs_inference,[],[7338,2821,6595,7218,6,1,3,3847,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320,2318,2640,7424,3322])).
% 58.79/58.77 cnf(7699,plain,
% 58.79/58.77 (~P2(a2,a1,f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,7338,2821,6595,7218,7216,6,1,3,3847,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320,2318,2640,7424,3322,24])).
% 58.79/58.77 cnf(7701,plain,
% 58.79/58.77 (~P2(f5(a4),f5(a4),a2)),
% 58.79/58.77 inference(scs_inference,[],[4,7338,2821,6595,7218,7216,2637,6,1,3,3847,32,3891,42,7,1342,22,14,12,21,13,9,10,15,16,17,18,25,20,26,23,28,2320,2318,2640,7424,3322,24,29])).
% 58.79/58.77 cnf(7705,plain,
% 58.79/58.77 (P2(f5(a2),f5(a2),f5(a2))),
% 58.79/58.77 inference(scs_inference,[],[7690,110])).
% 58.79/58.77 cnf(7707,plain,
% 58.79/58.77 (~P4(x77071,f5(a1),a2)+~P2(a4,a4,x77071)),
% 58.79/58.77 inference(scs_inference,[],[7662,3230])).
% 58.79/58.77 cnf(7711,plain,
% 58.79/58.77 (~P4(a4,f5(a1),a2)),
% 58.79/58.77 inference(scs_inference,[],[7690,7707])).
% 58.79/58.77 cnf(7717,plain,
% 58.79/58.77 (P2(f5(a4),a4,a1)),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,2,7707,7,22,14])).
% 58.79/58.77 cnf(7725,plain,
% 58.79/58.77 (P1(f3(a4,a4))),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,7670,7699,2,7707,7,22,14,12,21,13,9])).
% 58.79/58.77 cnf(7727,plain,
% 58.79/58.77 (P1(f7(a4,a4))),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,7670,7699,2,7707,7,22,14,12,21,13,9,10])).
% 58.79/58.77 cnf(7729,plain,
% 58.79/58.77 (P2(a4,a4,f3(a4,a4))),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,7670,7699,2,7707,7,22,14,12,21,13,9,10,16])).
% 58.79/58.77 cnf(7731,plain,
% 58.79/58.77 (P4(a4,a4,f7(a4,a4))),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,7670,7699,2,7707,7,22,14,12,21,13,9,10,16,17])).
% 58.79/58.77 cnf(7733,plain,
% 58.79/58.77 (P2(a1,a2,a2)),
% 58.79/58.77 inference(scs_inference,[],[7690,7697,7670,7699,2,49,7707,7,22,14,12,21,13,9,10,16,17,18])).
% 58.79/58.77 cnf(7737,plain,
% 58.79/58.77 (~P2(f5(a4),f6(a2),a2)),
% 58.79/58.77 inference(scs_inference,[],[7664,7690,7694,7701,7697,7670,7676,7699,2,3687,49,7707,7,22,14,12,21,13,9,10,16,17,18,25,24])).
% 58.79/58.77 cnf(7741,plain,
% 58.79/58.77 (P4(a4,a1,f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,7664,7668,7690,7694,7701,7697,7670,7676,7699,2,3687,49,42,7707,7,22,14,12,21,13,9,10,16,17,18,25,24,23,29])).
% 58.79/58.77 cnf(7745,plain,
% 58.79/58.77 (~P4(a4,a1,a2)),
% 58.79/58.77 inference(scs_inference,[],[4,7664,7668,7690,7694,7701,7697,7670,7678,7676,7699,2,3687,49,42,7707,7,22,14,12,21,13,9,10,16,17,18,25,24,23,29,28,7173])).
% 58.79/58.77 cnf(7757,plain,
% 58.79/58.77 (P4(a4,f6(a2),f6(a2))),
% 58.79/58.77 inference(scs_inference,[],[4,7664,7668,7680,7690,7694,7701,7697,7670,7678,7676,7699,4265,2,3687,49,42,7707,7,22,14,12,21,13,9,10,16,17,18,25,24,23,29,28,7173,3410,3412,3435,3437,4355,26])).
% 58.79/58.77 cnf(7759,plain,
% 58.79/58.77 (P4(f7(a4,a4),a4,f7(a4,a4))),
% 58.79/58.77 inference(scs_inference,[],[4,7664,7668,7680,7690,7694,7701,7697,7670,7678,7676,7699,4265,2,3687,49,42,7707,7,22,14,12,21,13,9,10,16,17,18,25,24,23,29,28,7173,3410,3412,3435,3437,4355,26,27])).
% 58.79/58.77 cnf(7766,plain,
% 58.79/58.77 (P1(f5(a2))),
% 58.79/58.77 inference(scs_inference,[],[3,7])).
% 58.79/58.77 cnf(7768,plain,
% 58.79/58.77 (P2(f5(a2),a2,a1)),
% 58.79/58.77 inference(scs_inference,[],[3,7,14])).
% 58.79/58.77 cnf(7774,plain,
% 58.79/58.77 (~P2(f6(a2),f5(a4),a2)),
% 58.79/58.77 inference(scs_inference,[],[7737,7711,7725,3,7,14,22,12,21])).
% 58.79/58.77 cnf(7778,plain,
% 58.79/58.78 (P1(f3(a2,a2))),
% 58.79/58.78 inference(scs_inference,[],[7737,7711,7725,3,7,14,22,12,21,13,9])).
% 58.79/58.78 cnf(7780,plain,
% 58.79/58.78 (P1(f7(a2,a2))),
% 58.79/58.78 inference(scs_inference,[],[7737,7711,7725,3,7,14,22,12,21,13,9,10])).
% 58.79/58.78 cnf(7786,plain,
% 58.79/58.78 (~P2(a4,a2,a4)),
% 58.79/58.78 inference(scs_inference,[],[7737,7711,7725,7717,6,3,7,14,22,12,21,13,9,10,16,17,25])).
% 58.79/58.78 cnf(7790,plain,
% 58.79/58.78 (~P2(a4,a2,f6(a2))),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7725,7759,7731,7717,6,3,7,14,22,12,21,13,9,10,16,17,25,26,24])).
% 58.79/58.78 cnf(7792,plain,
% 58.79/58.78 (P4(f6(a2),a2,f7(a4,a4))),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7731,7717,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27])).
% 58.79/58.78 cnf(7794,plain,
% 58.79/58.78 (P4(f3(a4,a4),f6(a2),f6(a2))),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29])).
% 58.79/58.78 cnf(7796,plain,
% 58.79/58.78 (~P4(f3(a4,a4),f6(a2),a4)),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6677,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29,28])).
% 58.79/58.78 cnf(7798,plain,
% 58.79/58.78 (P4(f3(a4,a4),a4,a4)),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6677,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29,28,3936])).
% 58.79/58.78 cnf(7800,plain,
% 58.79/58.78 (P4(a4,f3(a4,a4),a4)),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6677,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29,28,3936,3949])).
% 58.79/58.78 cnf(7803,plain,
% 58.79/58.78 (P4(f5(a1),f3(a4,a4),f5(a1))),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6677,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29,28,3936,3949,3939,3941,3943])).
% 58.79/58.78 cnf(7805,plain,
% 58.79/58.78 (P4(f5(a2),f3(a4,a4),f5(a2))),
% 58.79/58.78 inference(scs_inference,[],[7733,7737,7711,7757,7725,7759,7729,7731,7717,6677,6595,6,3,3891,7,14,22,12,21,13,9,10,16,17,25,26,24,27,29,28,3936,3949,3939,3941,3943,3945,3947])).
% 58.79/58.78 cnf(7810,plain,
% 58.79/58.78 (~P4(f6(a2),f3(a4,a4),a4)),
% 58.79/58.78 inference(scs_inference,[],[7796,22])).
% 58.79/58.78 cnf(7818,plain,
% 58.79/58.78 (~P2(a2,a2,a2)),
% 58.79/58.78 inference(scs_inference,[],[7786,7672,7778,7796,7768,6,22,12,21,13,25])).
% 58.79/58.78 cnf(7842,plain,
% 58.79/58.78 (~P2(a1,f5(a4),a2)),
% 58.79/58.78 inference(scs_inference,[],[4,7774,7727,7792,7790,7733,7794,3873,22,12,21,13,26,25])).
% 58.79/58.78 cnf(7844,plain,
% 58.79/58.78 (P2(f5(a2),a1,a1)),
% 58.79/58.78 inference(scs_inference,[],[4,7705,7774,7727,7792,7790,7733,7768,7794,3873,22,12,21,13,26,25,24])).
% 58.79/58.78 cnf(7848,plain,
% 58.79/58.78 (~P4(f5(a1),f3(a4,a4),a2)),
% 58.79/58.78 inference(scs_inference,[],[4,7705,7774,7692,7803,7727,7792,7800,7790,7693,7733,7768,7759,7794,3873,22,12,21,13,26,25,24,27,28])).
% 58.79/58.78 cnf(7857,plain,
% 58.79/58.78 (P2(a1,f5(a2),f5(a2))),
% 58.79/58.78 inference(scs_inference,[],[7766,7848,22,12])).
% 58.79/58.78 cnf(7861,plain,
% 58.79/58.78 (P4(a4,f7(a2,a2),f7(a2,a2))),
% 58.79/58.78 inference(scs_inference,[],[7842,7766,7780,7848,22,12,21,13])).
% 58.79/58.78 cnf(7867,plain,
% 58.79/58.78 (~P2(a1,f5(a2),f6(a2))),
% 58.79/58.78 inference(scs_inference,[],[7842,7666,7686,7766,7780,7848,7844,7798,7768,22,12,21,13,25,26,24])).
% 58.79/58.78 cnf(7873,plain,
% 58.79/58.78 (~P4(f5(a2),f3(a4,a4),f6(a2))),
% 58.79/58.78 inference(scs_inference,[],[7842,7805,7666,7686,7810,7766,7780,7848,7844,7741,7705,7800,7798,7768,7690,7678,22,12,21,13,25,26,24,27,29,28])).
% 58.79/58.78 cnf(7907,plain,
% 58.79/58.78 ($false),
% 58.79/58.78 inference(scs_inference,[],[4,7818,7873,7861,7857,7867,7745,7778,7741,7680,7729,7844,7798,7731,7690,7678,3,22,12,21,13,7424,26,25,24,27,29,28,38,1358,800]),
% 58.79/58.78 ['proof']).
% 58.79/58.78 % SZS output end Proof
% 58.79/58.78 % Total time :58.140000s
%------------------------------------------------------------------------------