%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET010-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : 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 14:19:58 EDT 2024
% Result : Unsatisfiable 235.84s 235.99s
% Output : CNFRefutation 235.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET010-1 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n017.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 : Sun Jun 23 14:55:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.59 start to proof:theBenchmark
% 235.84/235.98 %-------------------------------------------
% 235.84/235.98 % File :CSE---1.7
% 235.84/235.98 % Problem :theBenchmark
% 235.84/235.98 % Transform :cnf
% 235.84/235.98 % Format :tptp:raw
% 235.84/235.98 % Command :java -jar mcs_scs.jar %d %s
% 235.84/235.98
% 235.84/235.98 % Result :Theorem 235.130000s
% 235.84/235.98 % Output :CNFRefutation 235.130000s
% 235.84/235.98 %-------------------------------------------
% 235.84/235.99 %--------------------------------------------------------------------------
% 235.84/235.99 % File : SET010-1 : TPTP v8.2.0. Released v1.0.0.
% 235.84/235.99 % Domain : Set Theory
% 235.84/235.99 % Problem : X \ Y ^ Z = (X \ Y) U (X \ Z)
% 235.84/235.99 % Version : [LS74] axioms.
% 235.84/235.99 % English :
% 235.84/235.99
% 235.84/235.99 % Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% 235.84/235.99 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 235.84/235.99 % Source : [SPRFN]
% 235.84/235.99 % Names : ls118 [LS74]
% 235.84/235.99 % : ls118 [WM76]
% 235.84/235.99
% 235.84/235.99 % Status : Unsatisfiable
% 235.84/235.99 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.00 v7.4.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v6.0.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.21 v4.1.0, 0.12 v4.0.1, 0.20 v4.0.0, 0.43 v3.4.0, 0.75 v3.3.0, 0.67 v3.2.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.67 v2.5.0, 0.20 v2.4.0, 0.00 v2.2.1, 0.25 v2.1.0, 1.00 v2.0.0
% 235.84/235.99 % Syntax : Number of clauses : 29 ( 5 unt; 9 nHn; 24 RR)
% 235.84/235.99 % Number of literals : 79 ( 0 equ; 38 neg)
% 235.84/235.99 % Maximal clause size : 4 ( 2 avg)
% 235.84/235.99 % Maximal term depth : 2 ( 1 avg)
% 235.84/235.99 % Number of predicates : 6 ( 6 usr; 0 prp; 2-3 aty)
% 235.84/235.99 % Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% 235.84/235.99 % Number of variables : 76 ( 6 sgn)
% 235.84/235.99 % SPC : CNF_UNS_RFO_NEQ_NHN
% 235.84/235.99
% 235.84/235.99 % Comments :
% 235.84/235.99 %--------------------------------------------------------------------------
% 235.84/235.99 %----Include the member and subset axioms
% 235.84/235.99 include('Axioms/SET001-0.ax').
% 235.84/235.99 %----Include the member and union axioms
% 235.84/235.99 include('Axioms/SET001-1.ax').
% 235.84/235.99 %----Include the member and intersection axioms
% 235.84/235.99 include('Axioms/SET001-2.ax').
% 235.84/235.99 %----Include the member and difference axioms
% 235.84/235.99 include('Axioms/SET001-3.ax').
% 235.84/235.99 %--------------------------------------------------------------------------
% 235.84/235.99 cnf(a_intersection_b,hypothesis,
% 235.84/235.99 intersection(a,b,aIb) ).
% 235.84/235.99
% 235.84/235.99 cnf(c_minus_a,hypothesis,
% 235.84/235.99 difference(c,a,cDa) ).
% 235.84/235.99
% 235.84/235.99 cnf(c_minus_b,hypothesis,
% 235.84/235.99 difference(c,b,cDb) ).
% 235.84/235.99
% 235.84/235.99 cnf(c_minus_aIb,hypothesis,
% 235.84/235.99 difference(c,aIb,cD_aIb) ).
% 235.84/235.99
% 235.84/235.99 cnf(prove_cDa_union_cDb_is_cD_aIb,negated_conjecture,
% 235.84/235.99 ~ union(cDa,cDb,cD_aIb) ).
% 235.84/235.99
% 235.84/235.99 %--------------------------------------------------------------------------
% 235.84/235.99 %-------------------------------------------
% 235.84/235.99 % Proof found
% 235.84/235.99 % SZS status Theorem for theBenchmark
% 235.84/235.99 % SZS output start Proof
% 235.84/235.99 %ClaNum:29(EqnAxiom:0)
% 235.84/235.99 %VarNum:210(SingletonVarNum:76)
% 235.84/235.99 %MaxLitNum:4
% 235.84/235.99 %MaxfuncDepth:1
% 235.84/235.99 %SharedTerms:12
% 235.84/235.99 %goalClause: 5
% 235.84/235.99 %singleGoalClaCount:1
% 235.84/235.99 [1]P1(a1,a2,a3)
% 235.84/235.99 [2]P2(a4,a1,a5)
% 235.84/235.99 [3]P2(a4,a2,a7)
% 235.84/235.99 [4]P2(a4,a3,a6)
% 235.84/235.99 [5]~P4(a5,a7,a6)
% 235.84/235.99 [6]~P3(x62,x61)+P5(x61,x62)
% 235.84/235.99 [7]~P3(x71,x72)+P5(x71,x72)
% 235.84/235.99 [8]P5(x81,x82)+P6(f8(x81,x82),x81)
% 235.84/235.99 [11]P5(x111,x112)+~P6(f8(x111,x112),x112)
% 235.84/235.99 [10]~P5(x101,x102)+~P5(x102,x101)+P3(x101,x102)
% 235.84/235.99 [9]~P5(x93,x92)+P6(x91,x92)+~P6(x91,x93)
% 235.84/235.99 [21]P1(x211,x212,x213)+P6(f9(x211,x212,x213),x213)+P6(f9(x211,x212,x213),x212)
% 235.84/235.99 [22]P1(x221,x222,x223)+P6(f9(x221,x222,x223),x223)+P6(f9(x221,x222,x223),x221)
% 235.84/235.99 [23]P2(x231,x232,x233)+P6(f11(x231,x232,x233),x233)+P6(f11(x231,x232,x233),x231)
% 235.84/235.99 [24]P2(x241,x242,x243)+P6(f11(x241,x242,x243),x243)+~P6(f11(x241,x242,x243),x242)
% 235.84/235.99 [26]P4(x261,x262,x263)+~P6(f10(x261,x262,x263),x263)+~P6(f10(x261,x262,x263),x262)
% 235.84/235.99 [27]P4(x271,x272,x273)+~P6(f10(x271,x272,x273),x273)+~P6(f10(x271,x272,x273),x271)
% 235.84/235.99 [12]P6(x121,x122)+~P4(x124,x123,x122)+~P6(x121,x123)
% 235.84/235.99 [13]P6(x131,x132)+~P4(x133,x134,x132)+~P6(x131,x133)
% 235.84/235.99 [14]P6(x141,x142)+~P1(x144,x142,x143)+~P6(x141,x143)
% 235.84/235.99 [15]P6(x151,x152)+~P1(x152,x154,x153)+~P6(x151,x153)
% 235.84/235.99 [16]P6(x161,x162)+~P2(x162,x164,x163)+~P6(x161,x163)
% 235.84/235.99 [17]~P6(x171,x172)+~P2(x174,x173,x172)+~P6(x171,x173)
% 235.84/235.99 [25]P4(x251,x252,x253)+P6(f10(x251,x252,x253),x253)+P6(f10(x251,x252,x253),x252)+P6(f10(x251,x252,x253),x251)
% 235.84/235.99 [28]P2(x281,x282,x283)+P6(f11(x281,x282,x283),x282)+~P6(f11(x281,x282,x283),x283)+~P6(f11(x281,x282,x283),x281)
% 235.84/235.99 [29]P1(x291,x292,x293)+~P6(f9(x291,x292,x293),x293)+~P6(f9(x291,x292,x293),x292)+~P6(f9(x291,x292,x293),x291)
% 235.84/235.99 [18]~P4(x183,x182,x184)+P6(x181,x182)+P6(x181,x183)+~P6(x181,x184)
% 235.84/235.99 [19]~P2(x194,x193,x192)+P6(x191,x192)+P6(x191,x193)+~P6(x191,x194)
% 235.84/235.99 [20]~P1(x204,x203,x202)+P6(x201,x202)+~P6(x201,x203)+~P6(x201,x204)
% 235.84/235.99 %EqnAxiom
% 235.84/235.99
% 235.84/235.99 %-------------------------------------------
% 235.84/236.01 cnf(30,plain,
% 235.84/236.01 (~P6(x301,x302)+~P3(x303,x302)+P6(x301,x303)),
% 235.84/236.01 inference(scs_inference,[],[6,9])).
% 235.84/236.01 cnf(32,plain,
% 235.84/236.01 (~P6(x321,x322)+P6(x321,x323)+P6(f8(x322,x323),x322)),
% 235.84/236.01 inference(scs_inference,[],[8,9])).
% 235.84/236.01 cnf(33,plain,
% 235.84/236.01 (~P5(x331,x332)+P3(x332,x331)+~P6(f8(x332,x331),x331)),
% 235.84/236.01 inference(scs_inference,[],[11,10])).
% 235.84/236.01 cnf(34,plain,
% 235.84/236.01 (~P6(x341,x342)+P6(x341,a2)+~P3(a3,x342)),
% 235.84/236.01 inference(scs_inference,[],[1,30,14])).
% 235.84/236.01 cnf(39,plain,
% 235.84/236.01 (~P6(x391,a5)+P6(x391,x392)+~P4(a4,x393,x392)),
% 235.84/236.01 inference(scs_inference,[],[2,13,16])).
% 235.84/236.01 cnf(48,plain,
% 235.84/236.01 (P2(x481,x481,x482)+P6(f11(x481,x481,x482),x482)),
% 235.84/236.01 inference(scs_inference,[],[23,24])).
% 235.84/236.01 cnf(58,plain,
% 235.84/236.01 (P5(x581,x581)),
% 235.84/236.01 inference(scs_inference,[],[8,11])).
% 235.84/236.01 cnf(59,plain,
% 235.84/236.01 (P3(x591,x591)),
% 235.84/236.01 inference(scs_inference,[],[58,10])).
% 235.84/236.01 cnf(64,plain,
% 235.84/236.01 (P5(x641,x642)+P6(f8(x641,x642),x643)+~P4(x644,x641,x643)),
% 235.84/236.01 inference(scs_inference,[],[8,12])).
% 235.84/236.01 cnf(76,plain,
% 235.84/236.01 (P5(a3,x761)+P6(f8(a3,x761),a2)),
% 235.84/236.01 inference(scs_inference,[],[1,8,14])).
% 235.84/236.01 cnf(78,plain,
% 235.84/236.01 (P5(a3,x781)+P6(f8(a3,x781),a1)),
% 235.84/236.01 inference(scs_inference,[],[1,8,15])).
% 235.84/236.01 cnf(80,plain,
% 235.84/236.01 (P5(a5,x801)+P6(f8(a5,x801),a4)),
% 235.84/236.01 inference(scs_inference,[],[2,8,16])).
% 235.84/236.01 cnf(82,plain,
% 235.84/236.01 (P5(a6,x821)+P6(f8(a6,x821),a4)),
% 235.84/236.01 inference(scs_inference,[],[4,8,16])).
% 235.84/236.01 cnf(84,plain,
% 235.84/236.01 (~P6(f8(a6,x841),a3)+P5(a6,x841)),
% 235.84/236.01 inference(scs_inference,[],[4,8,17])).
% 235.84/236.01 cnf(88,plain,
% 235.84/236.01 (~P6(f8(a5,x881),a1)+P5(a5,x881)),
% 235.84/236.01 inference(scs_inference,[],[2,8,17])).
% 235.84/236.01 cnf(90,plain,
% 235.84/236.01 (P5(a7,x901)+P6(f8(a7,x901),a4)),
% 235.84/236.01 inference(scs_inference,[],[3,8,16])).
% 235.84/236.01 cnf(97,plain,
% 235.84/236.01 (~P6(f8(a7,x971),a2)+P5(a7,x971)),
% 235.84/236.01 inference(scs_inference,[],[3,8,17])).
% 235.84/236.01 cnf(109,plain,
% 235.84/236.01 (P5(a3,a2)),
% 235.84/236.01 inference(scs_inference,[],[11,76])).
% 235.84/236.01 cnf(110,plain,
% 235.84/236.01 (P3(a2,a3)+~P5(a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[109,10])).
% 235.84/236.01 cnf(112,plain,
% 235.84/236.01 (P3(a2,a3)+~P3(a3,a2)),
% 235.84/236.01 inference(scs_inference,[],[109,10,6])).
% 235.84/236.01 cnf(126,plain,
% 235.84/236.01 (P3(a2,a3)+~P6(f8(a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[110,11])).
% 235.84/236.01 cnf(133,plain,
% 235.84/236.01 (P6(f8(a2,a3),x1331)+~P4(x1332,a2,x1331)+P3(a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[110,64])).
% 235.84/236.01 cnf(134,plain,
% 235.84/236.01 (P3(a2,a3)+~P4(x1341,a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[133,126])).
% 235.84/236.01 cnf(145,plain,
% 235.84/236.01 (P3(a2,a3)+~P6(f10(x1451,a2,a3),a3)+~P6(f10(x1451,a2,a3),a2)),
% 235.84/236.01 inference(scs_inference,[],[134,26])).
% 235.84/236.01 cnf(146,plain,
% 235.84/236.01 (P5(a2,a3)+~P6(f10(x1461,a2,a3),a2)+~P6(f10(x1461,a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[145,7])).
% 235.84/236.01 cnf(147,plain,
% 235.84/236.01 (~P6(f10(x1471,a2,a3),a3)+P5(a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[59,146,34])).
% 235.84/236.01 cnf(203,plain,
% 235.84/236.01 (P5(a5,a4)),
% 235.84/236.01 inference(scs_inference,[],[11,80])).
% 235.84/236.01 cnf(204,plain,
% 235.84/236.01 (P3(a4,a5)+~P5(a4,a5)),
% 235.84/236.01 inference(scs_inference,[],[203,10])).
% 235.84/236.01 cnf(214,plain,
% 235.84/236.01 (P3(a4,a5)+P6(f8(a4,a5),a4)),
% 235.84/236.01 inference(scs_inference,[],[204,8])).
% 235.84/236.01 cnf(292,plain,
% 235.84/236.01 (P5(a7,a4)),
% 235.84/236.01 inference(scs_inference,[],[11,90])).
% 235.84/236.01 cnf(293,plain,
% 235.84/236.01 (P3(a4,a7)+~P5(a4,a7)),
% 235.84/236.01 inference(scs_inference,[],[292,10])).
% 235.84/236.01 cnf(295,plain,
% 235.84/236.01 (P3(a4,a7)+~P3(a7,a4)),
% 235.84/236.01 inference(scs_inference,[],[292,10,6])).
% 235.84/236.01 cnf(308,plain,
% 235.84/236.01 (P3(a4,a7)+~P6(f8(a4,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[293,11])).
% 235.84/236.01 cnf(346,plain,
% 235.84/236.01 (P6(f8(x3461,a6),a3)+~P6(f8(x3461,a6),a4)+P5(x3461,a6)),
% 235.84/236.01 inference(scs_inference,[],[4,11,19])).
% 235.84/236.01 cnf(380,plain,
% 235.84/236.01 (~P2(x3801,a1,a1)+P5(a3,x3802)),
% 235.84/236.01 inference(scs_inference,[],[78,17])).
% 235.84/236.01 cnf(382,plain,
% 235.84/236.01 (P6(f11(a1,a1,a1),a1)+P5(a3,x3821)),
% 235.84/236.01 inference(scs_inference,[],[380,48])).
% 235.84/236.01 cnf(413,plain,
% 235.84/236.01 (P6(f8(a6,x4131),x4132)+~P4(x4133,a4,x4132)+P5(a6,x4131)),
% 235.84/236.01 inference(scs_inference,[],[82,12])).
% 235.84/236.01 cnf(416,plain,
% 235.84/236.01 (~P2(x4161,a4,a4)+P5(a6,x4162)),
% 235.84/236.01 inference(scs_inference,[],[82,17])).
% 235.84/236.01 cnf(418,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+P5(a6,x4181)),
% 235.84/236.01 inference(scs_inference,[],[416,48])).
% 235.84/236.01 cnf(425,plain,
% 235.84/236.01 (P6(f8(a6,x4251),a1)+P6(f8(a6,x4251),a5)+P5(a6,x4251)),
% 235.84/236.01 inference(scs_inference,[],[2,82,19])).
% 235.84/236.01 cnf(428,plain,
% 235.84/236.01 (~P1(a4,a4,x4281)+P6(f8(a6,x4282),x4281)+P5(a6,x4282)),
% 235.84/236.01 inference(scs_inference,[],[82,20])).
% 235.84/236.01 cnf(437,plain,
% 235.84/236.01 (P6(f8(x4371,a3),x4371)+~P6(f8(a6,x4372),x4371)+P5(a6,x4372)),
% 235.84/236.01 inference(scs_inference,[],[84,32])).
% 235.84/236.01 cnf(451,plain,
% 235.84/236.01 (~P6(f8(a6,x4511),x4512)+~P4(a3,a3,x4512)+P5(a6,x4511)),
% 235.84/236.01 inference(scs_inference,[],[84,18])).
% 235.84/236.01 cnf(453,plain,
% 235.84/236.01 (~P6(f8(a6,x4531),x4532)+~P2(x4532,a3,a3)+P5(a6,x4531)),
% 235.84/236.01 inference(scs_inference,[],[84,19])).
% 235.84/236.01 cnf(455,plain,
% 235.84/236.01 (~P6(f8(a6,x4551),a2)+~P6(f8(a6,x4551),a1)+P5(a6,x4551)),
% 235.84/236.01 inference(scs_inference,[],[1,84,20])).
% 235.84/236.01 cnf(488,plain,
% 235.84/236.01 (~P6(f8(a5,x4881),a3)+P5(a5,x4881)),
% 235.84/236.01 inference(scs_inference,[],[1,88,15])).
% 235.84/236.01 cnf(554,plain,
% 235.84/236.01 (~P6(f8(a7,x5541),a3)+P5(a7,x5541)),
% 235.84/236.01 inference(scs_inference,[],[1,97,14])).
% 235.84/236.01 cnf(722,plain,
% 235.84/236.01 (P3(a4,a5)+~P2(x7221,a4,a4)),
% 235.84/236.01 inference(scs_inference,[],[214,17])).
% 235.84/236.01 cnf(725,plain,
% 235.84/236.01 (P3(a4,a5)+P6(f11(a4,a4,a4),a4)),
% 235.84/236.01 inference(scs_inference,[],[722,48])).
% 235.84/236.01 cnf(726,plain,
% 235.84/236.01 (P5(a4,a5)+P6(f11(a4,a4,a4),a4)),
% 235.84/236.01 inference(scs_inference,[],[725,7])).
% 235.84/236.01 cnf(864,plain,
% 235.84/236.01 (P3(a4,a7)+~P6(f8(a4,a7),x8641)+~P2(x8641,a7,a7)),
% 235.84/236.01 inference(scs_inference,[],[308,19])).
% 235.84/236.01 cnf(1080,plain,
% 235.84/236.01 (P5(a5,a6)+~P6(f8(a5,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[488,346])).
% 235.84/236.01 cnf(1137,plain,
% 235.84/236.01 (P5(a7,a6)+~P6(f8(a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[554,346])).
% 235.84/236.01 cnf(1138,plain,
% 235.84/236.01 (P5(a7,a6)),
% 235.84/236.01 inference(scs_inference,[],[1137,90])).
% 235.84/236.01 cnf(1139,plain,
% 235.84/236.01 (P3(a6,a7)+~P5(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[1138,10])).
% 235.84/236.01 cnf(1159,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a6,a7),a6)),
% 235.84/236.01 inference(scs_inference,[],[1139,8])).
% 235.84/236.01 cnf(1171,plain,
% 235.84/236.01 (P3(a6,a7)+~P6(f8(a6,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[1139,11])).
% 235.84/236.01 cnf(1172,plain,
% 235.84/236.01 (P6(f8(x11721,a7),x11721)+~P6(f8(a6,a7),x11721)+P3(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[1171,32])).
% 235.84/236.01 cnf(1173,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a6,a7),a4)),
% 235.84/236.01 inference(scs_inference,[],[1139,82])).
% 235.84/236.01 cnf(1185,plain,
% 235.84/236.01 (P6(f8(a6,a7),x11851)+~P4(x11852,a6,x11851)+P3(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[1139,64])).
% 235.84/236.01 cnf(1191,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a6,a7),x11911)+~P4(x11912,a4,x11911)),
% 235.84/236.01 inference(scs_inference,[],[1139,413])).
% 235.84/236.01 cnf(1207,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a6,a7),x12071)+~P1(a4,a4,x12071)),
% 235.84/236.01 inference(scs_inference,[],[1139,428])).
% 235.84/236.01 cnf(1215,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(x12151,a3),x12151)+~P6(f8(a6,a7),x12151)),
% 235.84/236.01 inference(scs_inference,[],[1139,437])).
% 235.84/236.01 cnf(1227,plain,
% 235.84/236.01 (P3(a6,a7)+~P6(f8(a6,a7),x12271)+~P4(a3,a3,x12271)),
% 235.84/236.01 inference(scs_inference,[],[1139,451])).
% 235.84/236.01 cnf(1232,plain,
% 235.84/236.01 (P3(a6,a7)+~P6(f8(a6,a7),x12321)+~P2(x12321,a3,a3)),
% 235.84/236.01 inference(scs_inference,[],[1139,453])).
% 235.84/236.01 cnf(1237,plain,
% 235.84/236.01 (P3(a6,a7)+~P6(f8(a6,a7),a1)+~P6(f8(a6,a7),a2)),
% 235.84/236.01 inference(scs_inference,[],[1139,455])).
% 235.84/236.01 cnf(1345,plain,
% 235.84/236.01 (P5(a5,a6)),
% 235.84/236.01 inference(scs_inference,[],[1080,80])).
% 235.84/236.01 cnf(1346,plain,
% 235.84/236.01 (P3(a6,a5)+~P5(a6,a5)),
% 235.84/236.01 inference(scs_inference,[],[1345,10])).
% 235.84/236.01 cnf(1371,plain,
% 235.84/236.01 (P3(a6,a5)+~P6(f8(a6,a5),a5)),
% 235.84/236.01 inference(scs_inference,[],[1346,11])).
% 235.84/236.01 cnf(1376,plain,
% 235.84/236.01 (P6(x13761,a6)+~P6(x13761,a5)+~P5(a6,a5)),
% 235.84/236.01 inference(scs_inference,[],[1346,30])).
% 235.84/236.01 cnf(1415,plain,
% 235.84/236.01 (P3(a6,a5)+P6(f8(a6,a5),a5)+P6(f8(a6,a5),a1)),
% 235.84/236.01 inference(scs_inference,[],[1346,425])).
% 235.84/236.01 cnf(1416,plain,
% 235.84/236.01 (P3(a6,a5)+P6(f8(a6,a5),a1)),
% 235.84/236.01 inference(scs_inference,[],[1415,1371])).
% 235.84/236.01 cnf(1417,plain,
% 235.84/236.01 (P5(a6,a5)+P6(f8(a6,a5),a1)),
% 235.84/236.01 inference(scs_inference,[],[1416,7])).
% 235.84/236.01 cnf(1514,plain,
% 235.84/236.01 (P3(a6,a7)+~P2(x15141,a6,a6)),
% 235.84/236.01 inference(scs_inference,[],[1159,17])).
% 235.84/236.01 cnf(1519,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f11(a6,a6,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[1514,48])).
% 235.84/236.01 cnf(1520,plain,
% 235.84/236.01 (P5(a6,a7)+P6(f11(a6,a6,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[1519,7])).
% 235.84/236.01 cnf(1529,plain,
% 235.84/236.01 (P3(a6,a7)+~P1(a6,a6,x15291)+P6(f8(a6,a7),x15291)),
% 235.84/236.01 inference(scs_inference,[],[1159,20])).
% 235.84/236.01 cnf(1552,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a4,a7),a4)),
% 235.84/236.01 inference(scs_inference,[],[1173,1172])).
% 235.84/236.01 cnf(1555,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a6,a7),a2)+P6(f8(a6,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[3,1173,19])).
% 235.84/236.01 cnf(1556,plain,
% 235.84/236.01 (P5(a6,a7)+P6(f8(a6,a7),a2)+P6(f8(a6,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[1555,7])).
% 235.84/236.01 cnf(1557,plain,
% 235.84/236.01 (P5(a6,a7)+P6(f8(a6,a7),a2)),
% 235.84/236.01 inference(scs_inference,[],[1556,11])).
% 235.84/236.01 cnf(1742,plain,
% 235.84/236.01 (P3(a6,a7)+P6(f8(a4,a7),a2)+P6(f8(a4,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[3,1552,19])).
% 235.84/236.01 cnf(1780,plain,
% 235.84/236.01 (P5(a6,a7)+~P1(a2,a2,x17801)+P6(f8(a6,a7),x17801)),
% 235.84/236.01 inference(scs_inference,[],[1557,20])).
% 235.84/236.01 cnf(1781,plain,
% 235.84/236.01 (P6(f8(a6,a7),x17811)+P3(a6,a7)+~P1(a2,a2,x17811)),
% 235.84/236.01 inference(scs_inference,[],[1138,1780,10])).
% 235.84/236.01 cnf(1873,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+~P6(x18731,a5)+P6(x18731,a6)),
% 235.84/236.01 inference(scs_inference,[],[418,1376])).
% 235.84/236.01 cnf(1874,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+~P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[5,1873,27])).
% 235.84/236.01 cnf(2174,plain,
% 235.84/236.01 (P3(a3,a2)+~P5(a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[109,10])).
% 235.84/236.01 cnf(2181,plain,
% 235.84/236.01 (P3(a5,a4)+~P5(a4,a5)),
% 235.84/236.01 inference(scs_inference,[],[203,10])).
% 235.84/236.01 cnf(2187,plain,
% 235.84/236.01 (P3(a7,a4)+~P5(a4,a7)),
% 235.84/236.01 inference(scs_inference,[],[292,10])).
% 235.84/236.01 cnf(2190,plain,
% 235.84/236.01 (P3(a7,a6)+~P5(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[1138,10])).
% 235.84/236.01 cnf(2193,plain,
% 235.84/236.01 (P3(a5,a6)+~P5(a6,a5)),
% 235.84/236.01 inference(scs_inference,[],[1345,10])).
% 235.84/236.01 cnf(2199,plain,
% 235.84/236.01 (P3(a7,a4)+~P6(f8(a4,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[2187,11])).
% 235.84/236.01 cnf(2205,plain,
% 235.84/236.01 (~P6(f8(a4,a7),x22051)+~P4(x22052,x22051,a7)+P3(a7,a4)),
% 235.84/236.01 inference(scs_inference,[],[2199,12])).
% 235.84/236.01 cnf(2242,plain,
% 235.84/236.01 (~P6(x22421,a3)+P6(x22421,a2)),
% 235.84/236.01 inference(scs_inference,[],[59,34])).
% 235.84/236.01 cnf(2251,plain,
% 235.84/236.01 (~P6(x22511,a7)+~P6(x22511,a3)),
% 235.84/236.01 inference(scs_inference,[],[3,2242,17])).
% 235.84/236.01 cnf(2272,plain,
% 235.84/236.01 (~P3(a2,a3)+P3(a3,a2)),
% 235.84/236.01 inference(scs_inference,[],[2174,7])).
% 235.84/236.01 cnf(2273,plain,
% 235.84/236.01 (P6(x22731,a3)+~P6(x22731,a2)+~P3(a2,a3)),
% 235.84/236.01 inference(scs_inference,[],[2272,30])).
% 235.84/236.01 cnf(2289,plain,
% 235.84/236.01 (P3(a3,a2)+~P6(f10(x22891,a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[2174,147])).
% 235.84/236.01 cnf(2290,plain,
% 235.84/236.01 (P3(a2,a3)+~P6(f10(x22901,a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[2289,112])).
% 235.84/236.01 cnf(2291,plain,
% 235.84/236.01 (~P6(x22911,a2)+P6(x22911,a3)+~P6(f10(x22912,a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[2290,2273])).
% 235.84/236.01 cnf(2292,plain,
% 235.84/236.01 (~P6(x22921,a6)+~P6(x22921,a2)+~P6(f10(x22922,a2,a3),a3)),
% 235.84/236.01 inference(scs_inference,[],[4,2291,17])).
% 235.84/236.01 cnf(2488,plain,
% 235.84/236.01 (P3(a5,a4)+P6(f11(a4,a4,a4),a4)),
% 235.84/236.01 inference(scs_inference,[],[2181,726])).
% 235.84/236.01 cnf(2489,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+P6(x24891,a5)+~P6(x24891,a4)),
% 235.84/236.01 inference(scs_inference,[],[2488,30])).
% 235.84/236.01 cnf(2490,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[2489,1874])).
% 235.84/236.01 cnf(2491,plain,
% 235.84/236.01 (~P2(x24911,a4,a4)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[2490,17])).
% 235.84/236.01 cnf(2644,plain,
% 235.84/236.01 (P3(a7,a4)+~P3(a4,a7)),
% 235.84/236.01 inference(scs_inference,[],[2187,7])).
% 235.84/236.01 cnf(2645,plain,
% 235.84/236.01 (P6(x26451,a7)+~P6(x26451,a4)+~P3(a4,a7)),
% 235.84/236.01 inference(scs_inference,[],[2644,30])).
% 235.84/236.01 cnf(2693,plain,
% 235.84/236.01 (P3(a7,a6)+~P3(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[2190,7])).
% 235.84/236.01 cnf(2694,plain,
% 235.84/236.01 (P6(x26941,a7)+~P6(x26941,a6)+~P3(a6,a7)),
% 235.84/236.01 inference(scs_inference,[],[2693,30])).
% 235.84/236.01 cnf(2699,plain,
% 235.84/236.01 (P3(a7,a6)+~P6(f8(a6,a7),a7)),
% 235.84/236.01 inference(scs_inference,[],[2190,11])).
% 235.84/236.01 cnf(2700,plain,
% 235.84/236.01 (~P6(f8(a6,a7),a7)+P6(x27001,a7)+~P6(x27001,a6)),
% 235.84/236.01 inference(scs_inference,[],[2699,30])).
% 235.84/236.01 cnf(2702,plain,
% 235.84/236.01 (P3(a7,a6)+~P6(f8(a6,a7),a3)),
% 235.84/236.01 inference(scs_inference,[],[2190,84])).
% 235.84/236.01 cnf(2703,plain,
% 235.84/236.01 (P6(x27031,a7)+~P6(x27031,a6)+~P6(f8(a6,a7),a3)),
% 235.84/236.01 inference(scs_inference,[],[2702,30])).
% 235.84/236.01 cnf(2707,plain,
% 235.84/236.01 (P3(a7,a6)+P6(f11(a4,a4,a4),a4)),
% 235.84/236.01 inference(scs_inference,[],[2190,418])).
% 235.84/236.01 cnf(2708,plain,
% 235.84/236.01 (P6(f11(a4,a4,a4),a4)+P6(x27081,a7)+~P6(x27081,a6)),
% 235.84/236.01 inference(scs_inference,[],[2707,30])).
% 235.84/236.01 cnf(2750,plain,
% 235.84/236.01 (P3(a7,a6)+P6(f11(a6,a6,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[2190,1520])).
% 235.84/236.01 cnf(2751,plain,
% 235.84/236.01 (P6(x27511,a7)+~P6(x27511,a6)+P6(f11(a6,a6,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[2750,30])).
% 235.84/236.01 cnf(2768,plain,
% 235.84/236.01 (P3(a7,a6)+P6(f8(a6,a7),a2)),
% 235.84/236.01 inference(scs_inference,[],[2190,1557])).
% 235.84/236.01 cnf(2836,plain,
% 235.84/236.01 (P3(a5,a6)+P6(f8(a6,a5),a1)),
% 235.84/236.01 inference(scs_inference,[],[2193,1417])).
% 235.84/236.01 cnf(2837,plain,
% 235.84/236.01 (P6(x28371,a5)+~P6(x28371,a6)+P6(f8(a6,a5),a1)),
% 235.84/236.01 inference(scs_inference,[],[2836,30])).
% 235.84/236.01 cnf(2838,plain,
% 235.84/236.01 (~P2(x28381,a1,a1)+~P6(x28382,a6)+P6(x28382,a5)),
% 235.84/236.01 inference(scs_inference,[],[2837,17])).
% 235.84/236.01 cnf(2839,plain,
% 235.84/236.01 (~P6(f10(a5,a7,a6),a6)+~P2(x28391,a1,a1)),
% 235.84/236.01 inference(scs_inference,[],[5,2838,27])).
% 235.84/236.01 cnf(2969,plain,
% 235.84/236.01 (~P6(x29691,a4)+P6(x29691,a6)+~P6(x29691,a7)),
% 235.84/236.01 inference(scs_inference,[],[4,2251,19])).
% 235.84/236.01 cnf(2970,plain,
% 235.84/236.01 (~P6(f10(a5,a7,a6),a7)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[5,2969,26])).
% 235.84/236.01 cnf(3016,plain,
% 235.84/236.01 (P3(a7,a6)+~P6(f8(a6,a7),a2)+~P6(f8(a6,a7),a1)),
% 235.84/236.01 inference(scs_inference,[],[2693,1237])).
% 235.84/236.01 cnf(3017,plain,
% 235.84/236.01 (P3(a7,a6)+~P6(f8(a6,a7),a1)),
% 235.84/236.01 inference(scs_inference,[],[3016,2768])).
% 235.84/236.01 cnf(3018,plain,
% 235.84/236.01 (P5(a6,a7)+~P6(f8(a6,a7),a1)),
% 235.84/236.01 inference(scs_inference,[],[3017,6])).
% 235.84/236.01 cnf(3227,plain,
% 235.84/236.01 (~P6(x32271,a7)+P6(x32271,a4)),
% 235.84/236.01 inference(scs_inference,[],[292,9])).
% 235.84/236.01 cnf(3246,plain,
% 235.84/236.01 (P2(a1,a1,a1)+~P6(f11(a1,a1,a1),a5)),
% 235.84/236.01 inference(scs_inference,[],[2,17,382,48])).
% 235.84/236.01 cnf(3249,plain,
% 235.84/236.01 (~P6(x32491,a6)+P6(x32491,a4)),
% 235.84/236.01 inference(scs_inference,[],[4,16])).
% 235.84/236.01 cnf(3251,plain,
% 235.84/236.01 (P2(x32511,x32511,a6)+P6(f11(x32511,x32511,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[4,16,48])).
% 235.84/236.01 cnf(3254,plain,
% 235.84/236.01 (~P6(f10(a5,a7,a6),a7)),
% 235.84/236.01 inference(scs_inference,[],[3227,2970])).
% 235.84/236.01 cnf(3256,plain,
% 235.84/236.01 (~P3(a4,a7)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[3254,2645])).
% 235.84/236.01 cnf(3258,plain,
% 235.84/236.01 (~P6(f8(a4,a7),a7)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[3254,292,2645,33])).
% 235.84/236.01 cnf(3260,plain,
% 235.84/236.01 (~P5(a4,a7)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[3254,292,2645,33,10])).
% 235.84/236.01 cnf(3264,plain,
% 235.84/236.01 (~P3(a7,a4)+~P6(f10(a5,a7,a6),a4)),
% 235.84/236.01 inference(scs_inference,[],[3254,292,2645,33,10,8,295])).
% 235.84/236.01 cnf(3289,plain,
% 235.84/236.01 (P6(f10(a5,a7,a6),a6)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25])).
% 235.84/236.01 cnf(3291,plain,
% 235.84/236.01 (P6(f10(a5,a7,a6),a4)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25,3249])).
% 235.84/236.01 cnf(3293,plain,
% 235.84/236.01 (~P3(a4,a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25,3249,3256])).
% 235.84/236.01 cnf(3294,plain,
% 235.84/236.01 (~P5(a4,a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25,3249,3256,3260])).
% 235.84/236.01 cnf(3295,plain,
% 235.84/236.01 (~P3(a7,a4)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25,3249,3256,3260,3264])).
% 235.84/236.01 cnf(3299,plain,
% 235.84/236.01 (~P6(f8(a4,a7),a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.01 inference(scs_inference,[],[3254,5,25,3249,3256,3260,3264,2491,2839,3246,3258])).
% 235.84/236.01 cnf(3306,plain,
% 235.84/236.01 (~P6(f10(a5,a7,a6),a5)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[5,27])).
% 235.84/236.01 cnf(3308,plain,
% 235.84/236.01 (~P3(a4,a7)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[5,27,3293])).
% 235.84/236.01 cnf(3310,plain,
% 235.84/236.01 (~P3(a7,a4)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[5,27,3293,3294,3295])).
% 235.84/236.01 cnf(3311,plain,
% 235.84/236.01 (~P6(f8(a4,a7),a7)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[5,27,3293,3294,3295,3299])).
% 235.84/236.01 cnf(3347,plain,
% 235.84/236.01 (~P6(f8(a6,a7),a3)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[3254,2700,2703])).
% 235.84/236.01 cnf(3354,plain,
% 235.84/236.01 (P6(f11(a6,a6,a6),a6)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.01 inference(scs_inference,[],[3254,2708,2751])).
% 235.84/236.02 cnf(3357,plain,
% 235.84/236.02 (~P3(a6,a7)+~P6(f10(a5,a7,a6),a6)),
% 235.84/236.02 inference(scs_inference,[],[3254,2694])).
% 235.84/236.02 cnf(3363,plain,
% 235.84/236.02 (~P6(x33631,a5)+P6(x33631,a6)),
% 235.84/236.02 inference(scs_inference,[],[1345,3254,39,9])).
% 235.84/236.02 cnf(3365,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x33651)+~P4(x33651,x33652,a7)),
% 235.84/236.02 inference(scs_inference,[],[3254,13])).
% 235.84/236.02 cnf(3371,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x33711)+~P4(x33712,x33711,a7)),
% 235.84/236.02 inference(scs_inference,[],[3254,12])).
% 235.84/236.02 cnf(3373,plain,
% 235.84/236.02 (~P6(x33731,a3)+~P6(x33731,a6)),
% 235.84/236.02 inference(scs_inference,[],[3254,4,12,17])).
% 235.84/236.02 cnf(3375,plain,
% 235.84/236.02 (P6(x33751,a1)+~P6(x33751,a4)+P6(x33751,a5)),
% 235.84/236.02 inference(scs_inference,[],[2,19])).
% 235.84/236.02 cnf(3381,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x33811)+~P4(a7,a7,x33811)),
% 235.84/236.02 inference(scs_inference,[],[3254,18])).
% 235.84/236.02 cnf(3434,plain,
% 235.84/236.02 (~P3(a6,a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.02 inference(scs_inference,[],[3357,3289])).
% 235.84/236.02 cnf(3447,plain,
% 235.84/236.02 (~P5(a6,a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.02 inference(scs_inference,[],[3434,1139])).
% 235.84/236.02 cnf(3550,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x35501)+~P6(f10(a5,a7,a6),a4)+~P1(x35501,a2,a7)),
% 235.84/236.02 inference(scs_inference,[],[3,3254,20,19])).
% 235.84/236.02 cnf(3564,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),a1)+~P6(f10(a5,a7,a6),a4)+P6(f10(a5,a7,a6),a3)),
% 235.84/236.02 inference(scs_inference,[],[3,3254,1,20,19])).
% 235.84/236.02 cnf(3624,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a1)+~P6(f10(a5,a7,a6),a4)+~P1(a5,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[2,3254,19,20])).
% 235.84/236.02 cnf(3657,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),a6)+~P5(a6,a7)),
% 235.84/236.02 inference(scs_inference,[],[3306,3447])).
% 235.84/236.02 cnf(3932,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x39321)+~P6(f10(a5,a7,a6),a4)+P6(f10(a5,a7,a6),a1)+~P1(x39321,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[3254,2,20,19])).
% 235.84/236.02 cnf(3940,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x39401)+~P6(f10(a5,a7,a6),a4)+~P1(x39401,a1,a7)+P6(f10(a5,a7,a6),a5)),
% 235.84/236.02 inference(scs_inference,[],[2,3254,20,19])).
% 235.84/236.02 cnf(5552,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x55521)+~P1(x55522,a7,x55521)),
% 235.84/236.02 inference(scs_inference,[],[3254,14])).
% 235.84/236.02 cnf(5565,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x55651)+~P2(a7,x55652,x55651)),
% 235.84/236.02 inference(scs_inference,[],[3254,16])).
% 235.84/236.02 cnf(5601,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x56011)+~P1(a7,x56012,x56011)),
% 235.84/236.02 inference(scs_inference,[],[3254,15])).
% 235.84/236.02 cnf(5644,plain,
% 235.84/236.02 (P6(f8(x56441,a7),x56441)+~P6(f10(a5,a7,a6),x56441)),
% 235.84/236.02 inference(scs_inference,[],[3254,32])).
% 235.84/236.02 cnf(6994,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a1)+~P6(f10(a5,a7,a6),a6)+~P1(a4,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[3249,3932])).
% 235.84/236.02 cnf(7707,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a6)),
% 235.84/236.02 inference(scs_inference,[],[5,3254,3363,25])).
% 235.84/236.02 cnf(7713,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),a5)),
% 235.84/236.02 inference(scs_inference,[],[7707,3306])).
% 235.84/236.02 cnf(7714,plain,
% 235.84/236.02 (~P3(a4,a7)),
% 235.84/236.02 inference(scs_inference,[],[7707,3308])).
% 235.84/236.02 cnf(7716,plain,
% 235.84/236.02 (~P3(a7,a4)),
% 235.84/236.02 inference(scs_inference,[],[7707,3310])).
% 235.84/236.02 cnf(7717,plain,
% 235.84/236.02 (~P6(f8(a4,a7),a7)),
% 235.84/236.02 inference(scs_inference,[],[7707,3311])).
% 235.84/236.02 cnf(7728,plain,
% 235.84/236.02 (~P6(f8(a6,a7),a3)),
% 235.84/236.02 inference(scs_inference,[],[7707,3347])).
% 235.84/236.02 cnf(7730,plain,
% 235.84/236.02 (P6(f11(a6,a6,a6),a6)),
% 235.84/236.02 inference(scs_inference,[],[7707,3354])).
% 235.84/236.02 cnf(7731,plain,
% 235.84/236.02 (~P3(a6,a7)),
% 235.84/236.02 inference(scs_inference,[],[7707,3357])).
% 235.84/236.02 cnf(7733,plain,
% 235.84/236.02 (~P5(a6,a7)),
% 235.84/236.02 inference(scs_inference,[],[7707,3657])).
% 235.84/236.02 cnf(7748,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a1)+~P1(a4,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[7707,6994])).
% 235.84/236.02 cnf(7751,plain,
% 235.84/236.02 (P6(f8(a6,a7),a6)),
% 235.84/236.02 inference(scs_inference,[],[7707,5565,5644])).
% 235.84/236.02 cnf(7765,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),a3)),
% 235.84/236.02 inference(scs_inference,[],[7707,5565,5644,5552,5601,3371,3365,3381,3251,3373])).
% 235.84/236.02 cnf(7773,plain,
% 235.84/236.02 (~P2(a3,x77731,a6)),
% 235.84/236.02 inference(scs_inference,[],[7707,5565,5644,5552,5601,3371,3365,3381,3251,3373,9,15,17,16])).
% 235.84/236.02 cnf(7831,plain,
% 235.84/236.02 (~P6(f8(a4,a7),x78311)+~P2(x78311,a7,a7)),
% 235.84/236.02 inference(scs_inference,[],[7714,864])).
% 235.84/236.02 cnf(7847,plain,
% 235.84/236.02 (P6(f8(a6,a7),x78471)+~P4(x78472,a6,x78471)),
% 235.84/236.02 inference(scs_inference,[],[7731,1185])).
% 235.84/236.02 cnf(7848,plain,
% 235.84/236.02 (P6(f8(a6,a7),x78481)+~P4(x78482,a4,x78481)),
% 235.84/236.02 inference(scs_inference,[],[7731,1191])).
% 235.84/236.02 cnf(7856,plain,
% 235.84/236.02 (P6(f8(a6,a7),x78561)+~P1(a4,a4,x78561)),
% 235.84/236.02 inference(scs_inference,[],[7731,1207])).
% 235.84/236.02 cnf(7859,plain,
% 235.84/236.02 (~P6(f8(a6,a7),x78591)+P6(f8(x78591,a3),x78591)),
% 235.84/236.02 inference(scs_inference,[],[7731,1215])).
% 235.84/236.02 cnf(7867,plain,
% 235.84/236.02 (~P6(f8(a6,a7),x78671)+~P4(a3,a3,x78671)),
% 235.84/236.02 inference(scs_inference,[],[7731,1227])).
% 235.84/236.02 cnf(7871,plain,
% 235.84/236.02 (~P6(f8(a6,a7),x78711)+~P2(x78711,a3,a3)),
% 235.84/236.02 inference(scs_inference,[],[7731,1232])).
% 235.84/236.02 cnf(7902,plain,
% 235.84/236.02 (P6(f8(a6,a7),x79021)+~P1(a6,a6,x79021)),
% 235.84/236.02 inference(scs_inference,[],[7731,1529])).
% 235.84/236.02 cnf(7919,plain,
% 235.84/236.02 (P6(f8(a6,a7),a2)),
% 235.84/236.02 inference(scs_inference,[],[7733,1557])).
% 235.84/236.02 cnf(7939,plain,
% 235.84/236.02 (P6(f8(a4,a7),a2)),
% 235.84/236.02 inference(scs_inference,[],[7731,7717,1742])).
% 235.84/236.02 cnf(7957,plain,
% 235.84/236.02 (P6(f8(a6,a7),x79571)+~P1(a2,a2,x79571)),
% 235.84/236.02 inference(scs_inference,[],[7733,1780])).
% 235.84/236.02 cnf(7958,plain,
% 235.84/236.02 (P6(f8(a6,a7),x79581)+~P1(a2,a2,x79581)),
% 235.84/236.02 inference(scs_inference,[],[7731,1781])).
% 235.84/236.02 cnf(7986,plain,
% 235.84/236.02 (~P6(f8(a4,a7),x79861)+~P4(x79862,x79861,a7)),
% 235.84/236.02 inference(scs_inference,[],[7716,2205])).
% 235.84/236.02 cnf(8022,plain,
% 235.84/236.02 (~P6(f8(a6,a7),a1)),
% 235.84/236.02 inference(scs_inference,[],[7733,3018])).
% 235.84/236.02 cnf(8035,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a4)),
% 235.84/236.02 inference(scs_inference,[],[7713,3291])).
% 235.84/236.02 cnf(8056,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),a4)+~P6(f10(a5,a7,a6),a1)),
% 235.84/236.02 inference(scs_inference,[],[7765,3564])).
% 235.84/236.02 cnf(8063,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x80631)+~P6(f10(a5,a7,a6),a4)+~P1(x80631,a1,a7)),
% 235.84/236.02 inference(scs_inference,[],[7713,3940])).
% 235.84/236.02 cnf(8197,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x81971)+~P1(x81971,a2,a7)),
% 235.84/236.02 inference(scs_inference,[],[8035,3550])).
% 235.84/236.02 cnf(8198,plain,
% 235.84/236.02 (P6(f10(a5,a7,a6),a1)+~P1(a5,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[8035,3624])).
% 235.84/236.02 cnf(8200,plain,
% 235.84/236.02 (~P6(f10(a5,a7,a6),x82001)+P6(f10(a5,a7,a6),a1)+~P1(x82001,a5,a7)),
% 235.84/236.02 inference(scs_inference,[],[8035,3932])).
% 235.84/236.02 cnf(8251,plain,
% 235.84/236.02 ($false),
% 235.84/236.02 inference(scs_inference,[],[7707,8022,7728,7713,7919,8035,7939,7751,7730,7773,7831,7859,7867,7871,7986,8056,8197,7748,7847,7848,7856,7902,7957,7958,8198,3365,3251,5601,5565,3373,8063,8200,2292,3375]),
% 235.84/236.02 ['proof']).
% 235.84/236.02 % SZS output end Proof
% 235.84/236.02 % Total time :235.130000s
%------------------------------------------------------------------------------