%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KLE004+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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 09:59:46 EDT 2024
% Result : Theorem 6.94s 6.99s
% Output : CNFRefutation 6.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KLE004+1 : TPTP v8.2.0. Released v4.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n018.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 : Thu Jun 20 22:04:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 6.84/6.99 %-------------------------------------------
% 6.84/6.99 % File :CSE---1.7
% 6.84/6.99 % Problem :theBenchmark
% 6.84/6.99 % Transform :cnf
% 6.84/6.99 % Format :tptp:raw
% 6.84/6.99 % Command :java -jar mcs_scs.jar %d %s
% 6.84/6.99
% 6.84/6.99 % Result :Theorem 6.380000s
% 6.84/6.99 % Output :CNFRefutation 6.380000s
% 6.84/6.99 %-------------------------------------------
% 6.94/6.99 %------------------------------------------------------------------------------
% 6.94/6.99 % File : KLE004+1 : TPTP v8.2.0. Released v4.0.0.
% 6.94/6.99 % Domain : Kleene Algebra (Idempotent Test Semirings)
% 6.94/6.99 % Problem : Complement - 1 is the complement of 0
% 6.94/6.99 % Version : [Hoe08] axioms.
% 6.94/6.99 % English :
% 6.94/6.99
% 6.94/6.99 % Refs : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% 6.94/6.99 % Source : [Hoe08]
% 6.94/6.99 % Names :
% 6.94/6.99
% 6.94/6.99 % Status : Theorem
% 6.94/6.99 % Rating : 0.25 v8.2.0, 0.22 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.17 v4.0.0
% 6.94/6.99 % Syntax : Number of formulae : 17 ( 12 unt; 0 def)
% 6.94/6.99 % Number of atoms : 25 ( 18 equ)
% 6.94/6.99 % Maximal formula atoms : 4 ( 1 avg)
% 6.94/6.99 % Number of connectives : 9 ( 1 ~; 0 |; 2 &)
% 6.94/6.99 % ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% 6.94/6.99 % Maximal formula depth : 6 ( 3 avg)
% 6.94/6.99 % Maximal term depth : 3 ( 1 avg)
% 6.94/6.99 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty)
% 6.94/6.99 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 6.94/6.99 % Number of variables : 29 ( 28 !; 1 ?)
% 6.94/6.99 % SPC : FOF_THM_RFO_SEQ
% 6.94/6.99
% 6.94/6.99 % Comments : Equational encoding
% 6.94/6.99 %------------------------------------------------------------------------------
% 6.94/6.99 %---Include axioms for idempotent test semiring
% 6.94/6.99 include('Axioms/KLE001+0.ax').
% 6.94/6.99 %---Include test axioms
% 6.94/6.99 include('Axioms/KLE001+1.ax').
% 6.94/6.99 %------------------------------------------------------------------------------
% 6.94/6.99 fof(goals,conjecture,
% 6.94/6.99 c(zero) = one ).
% 6.94/6.99
% 6.94/6.99 %------------------------------------------------------------------------------
% 6.94/6.99 %-------------------------------------------
% 6.94/6.99 % Proof found
% 6.94/6.99 % SZS status Theorem for theBenchmark
% 6.94/6.99 % SZS output start Proof
% 6.95/7.00 %ClaNum:37(EqnAxiom:14)
% 6.95/7.00 %VarNum:89(SingletonVarNum:40)
% 6.95/7.00 %MaxLitNum:4
% 6.95/7.00 %MaxfuncDepth:2
% 6.95/7.00 %SharedTerms:4
% 6.95/7.00 %goalClause: 26
% 6.95/7.00 %singleGoalClaCount:1
% 6.95/7.00 [26]~E(f4(a1),a6)
% 6.95/7.00 [15]E(f2(x151,a1),a1)
% 6.95/7.00 [16]E(f2(a1,x161),a1)
% 6.95/7.00 [17]E(f3(x171,a1),x171)
% 6.95/7.00 [18]E(f2(x181,a6),x181)
% 6.95/7.00 [19]E(f2(a6,x191),x191)
% 6.95/7.00 [20]E(f3(x201,x201),x201)
% 6.95/7.00 [21]E(f3(x211,x212),f3(x212,x211))
% 6.95/7.00 [22]E(f3(f3(x221,x222),x223),f3(x221,f3(x222,x223)))
% 6.95/7.00 [23]E(f2(f2(x231,x232),x233),f2(x231,f2(x232,x233)))
% 6.95/7.00 [24]E(f3(f2(x241,x242),f2(x241,x243)),f2(x241,f3(x242,x243)))
% 6.95/7.00 [25]E(f3(f2(x251,x252),f2(x253,x252)),f2(f3(x251,x253),x252))
% 6.95/7.00 [27]P1(x271)+E(f4(x271),a1)
% 6.95/7.00 [29]~P1(x291)+P2(f5(x291),x291)
% 6.95/7.00 [28]P1(x281)+~P2(x282,x281)
% 6.95/7.00 [32]~P2(x322,x321)+E(f3(x321,x322),a6)
% 6.95/7.00 [33]~P2(x332,x331)+E(f2(x331,x332),a1)
% 6.95/7.00 [34]~P2(x341,x342)+E(f2(x341,x342),a1)
% 6.95/7.00 [35]~P3(x351,x352)+E(f3(x351,x352),x352)
% 6.95/7.00 [36]P3(x361,x362)+~E(f3(x361,x362),x362)
% 6.95/7.00 [30]~P1(x301)+P2(x301,x302)+~E(f4(x301),x302)
% 6.95/7.00 [31]~P1(x311)+~P2(x311,x312)+E(f4(x311),x312)
% 6.95/7.00 [37]P2(x371,x372)+~E(f3(x372,x371),a6)+~E(f2(x371,x372),a1)+~E(f2(x372,x371),a1)
% 6.95/7.00 %EqnAxiom
% 6.95/7.00 [1]E(x11,x11)
% 6.95/7.00 [2]E(x22,x21)+~E(x21,x22)
% 6.95/7.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 6.95/7.00 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 6.95/7.00 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 6.95/7.00 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63))
% 6.95/7.00 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72))
% 6.95/7.00 [8]~E(x81,x82)+E(f4(x81),f4(x82))
% 6.95/7.00 [9]~E(x91,x92)+E(f5(x91),f5(x92))
% 6.95/7.00 [10]~P1(x101)+P1(x102)+~E(x101,x102)
% 6.95/7.00 [11]P2(x112,x113)+~E(x111,x112)+~P2(x111,x113)
% 6.95/7.00 [12]P2(x123,x122)+~E(x121,x122)+~P2(x123,x121)
% 6.95/7.00 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133)
% 6.95/7.00 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141)
% 6.95/7.00
% 6.95/7.00 %-------------------------------------------
% 6.96/7.00 cnf(39,plain,
% 6.96/7.00 (E(x391,f3(x391,x391))),
% 6.96/7.00 inference(scs_inference,[],[20,2])).
% 6.96/7.00 cnf(40,plain,
% 6.96/7.00 (P3(x401,x401)),
% 6.96/7.00 inference(scs_inference,[],[20,2,36])).
% 6.96/7.00 cnf(42,plain,
% 6.96/7.00 (~E(f4(a1),f3(a6,a6))),
% 6.96/7.00 inference(scs_inference,[],[26,20,2,36,3])).
% 6.96/7.00 cnf(43,plain,
% 6.96/7.00 (E(f3(x431,x431),x431)),
% 6.96/7.00 inference(rename_variables,[],[20])).
% 6.96/7.00 cnf(46,plain,
% 6.96/7.00 (P2(a1,a6)),
% 6.96/7.00 inference(scs_inference,[],[26,20,17,18,19,2,36,3,13,14,37])).
% 6.96/7.00 cnf(51,plain,
% 6.96/7.00 (~P1(a1)),
% 6.96/7.00 inference(scs_inference,[],[26,20,17,18,19,2,36,3,13,14,37,31])).
% 6.96/7.00 cnf(53,plain,
% 6.96/7.00 (~P1(f3(a1,a1))),
% 6.96/7.00 inference(scs_inference,[],[26,20,43,17,18,19,2,36,3,13,14,37,31,10])).
% 6.96/7.00 cnf(55,plain,
% 6.96/7.00 (P2(x551,a6)+~E(a1,x551)),
% 6.96/7.00 inference(scs_inference,[],[26,20,43,17,18,19,2,36,3,13,14,37,31,10,11])).
% 6.96/7.00 cnf(56,plain,
% 6.96/7.00 (P2(a1,f3(a6,a6))),
% 6.96/7.00 inference(scs_inference,[],[26,20,43,17,18,19,2,36,3,13,14,37,31,10,11,12])).
% 6.96/7.00 cnf(57,plain,
% 6.96/7.00 (~P2(x571,a1)),
% 6.96/7.00 inference(scs_inference,[],[26,20,43,17,18,19,2,36,3,13,14,37,31,10,11,12,28])).
% 6.96/7.00 cnf(60,plain,
% 6.96/7.00 (P2(f3(a1,a1),a6)),
% 6.96/7.00 inference(scs_inference,[],[39,55])).
% 6.96/7.00 cnf(61,plain,
% 6.96/7.00 (E(x611,f3(x611,x611))),
% 6.96/7.00 inference(rename_variables,[],[39])).
% 6.96/7.00 cnf(62,plain,
% 6.96/7.00 (E(f2(x621,f3(x622,x623)),f3(f2(x621,x622),f2(x621,x623)))),
% 6.96/7.00 inference(scs_inference,[],[39,24,55,2])).
% 6.96/7.00 cnf(63,plain,
% 6.96/7.00 (~P2(x631,f3(a1,a1))),
% 6.96/7.00 inference(scs_inference,[],[39,53,24,55,2,28])).
% 6.96/7.00 cnf(65,plain,
% 6.96/7.00 (P3(x651,f3(x651,x651))),
% 6.96/7.00 inference(scs_inference,[],[39,61,40,53,24,55,2,28,14])).
% 6.96/7.00 cnf(66,plain,
% 6.96/7.00 (P3(x661,x661)),
% 6.96/7.00 inference(rename_variables,[],[40])).
% 6.96/7.00 cnf(67,plain,
% 6.96/7.00 (~P1(f2(x671,a1))),
% 6.96/7.00 inference(scs_inference,[],[51,39,61,40,53,24,15,55,2,28,14,10])).
% 6.96/7.00 cnf(68,plain,
% 6.96/7.00 (P2(f3(a1,a1),f3(a6,a6))),
% 6.96/7.00 inference(scs_inference,[],[51,39,61,40,53,56,24,15,55,2,28,14,10,11])).
% 6.96/7.00 cnf(69,plain,
% 6.96/7.00 (E(x691,f3(x691,x691))),
% 6.96/7.00 inference(rename_variables,[],[39])).
% 6.96/7.00 cnf(70,plain,
% 6.96/7.00 (P3(f3(x701,x701),x701)),
% 6.96/7.00 inference(scs_inference,[],[51,39,61,69,40,66,53,56,24,15,55,2,28,14,10,11,13])).
% 6.96/7.00 cnf(72,plain,
% 6.96/7.00 (~E(a6,a1)),
% 6.96/7.00 inference(scs_inference,[],[51,39,61,69,40,66,46,57,53,56,24,15,55,2,28,14,10,11,13,12])).
% 6.96/7.00 cnf(74,plain,
% 6.96/7.00 (E(f2(x741,x742),f2(x741,f3(x742,x742)))),
% 6.96/7.00 inference(scs_inference,[],[51,39,61,69,40,66,46,57,53,56,24,15,55,2,28,14,10,11,13,12,3])).
% 6.96/7.00 cnf(83,plain,
% 6.96/7.00 (E(f2(x831,f3(x832,x832)),f2(x831,x832))),
% 6.96/7.00 inference(scs_inference,[],[74,2])).
% 6.96/7.00 cnf(84,plain,
% 6.96/7.00 (~P2(x841,f2(x842,a1))),
% 6.96/7.00 inference(scs_inference,[],[74,67,2,28])).
% 6.96/7.00 cnf(86,plain,
% 6.96/7.00 (P2(f3(f3(a1,a1),f3(a1,a1)),f3(a6,a6))),
% 6.96/7.00 inference(scs_inference,[],[74,39,68,67,2,28,11])).
% 6.96/7.00 cnf(87,plain,
% 6.96/7.00 (E(x871,f3(x871,x871))),
% 6.96/7.00 inference(rename_variables,[],[39])).
% 6.96/7.00 cnf(88,plain,
% 6.96/7.00 (~P1(f3(f2(x881,a1),f2(x882,a1)))),
% 6.96/7.00 inference(scs_inference,[],[74,39,68,67,25,2,28,11,10])).
% 6.96/7.00 cnf(91,plain,
% 6.96/7.01 (P3(x911,f3(f3(x911,x911),f3(x911,x911)))),
% 6.96/7.01 inference(scs_inference,[],[74,39,87,65,68,67,25,2,28,11,10,14])).
% 6.96/7.01 cnf(95,plain,
% 6.96/7.01 (~E(f3(a6,a6),f3(a1,a1))),
% 6.96/7.01 inference(scs_inference,[],[74,39,87,65,68,63,67,25,2,28,11,10,14,13,12])).
% 6.96/7.01 cnf(97,plain,
% 6.96/7.01 (E(f3(f2(x971,x972),a1),f2(x971,f3(x972,x972)))),
% 6.96/7.01 inference(scs_inference,[],[74,39,87,17,65,68,63,67,25,2,28,11,10,14,13,12,3])).
% 6.96/7.01 cnf(99,plain,
% 6.96/7.01 (~P2(x991,f3(f2(x992,a1),f2(x993,a1)))),
% 6.96/7.01 inference(scs_inference,[],[88,28])).
% 6.96/7.01 cnf(101,plain,
% 6.96/7.01 (E(f2(x1011,f3(x1012,x1012)),f3(f2(x1011,x1012),a1))),
% 6.96/7.01 inference(scs_inference,[],[97,88,28,2])).
% 6.96/7.01 cnf(102,plain,
% 6.96/7.01 (P3(f3(f3(x1021,x1021),f3(x1021,x1021)),x1021)),
% 6.96/7.01 inference(scs_inference,[],[97,39,70,88,28,2,13])).
% 6.96/7.01 cnf(103,plain,
% 6.96/7.01 (E(x1031,f3(x1031,x1031))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(104,plain,
% 6.96/7.01 (P3(f2(x1041,f3(x1042,x1042)),f2(x1041,x1042))),
% 6.96/7.01 inference(scs_inference,[],[83,97,39,70,88,40,28,2,13,14])).
% 6.96/7.01 cnf(106,plain,
% 6.96/7.01 (~P1(f2(x1061,f3(a1,a1)))),
% 6.96/7.01 inference(scs_inference,[],[83,97,39,70,88,40,67,28,2,13,14,10])).
% 6.96/7.01 cnf(107,plain,
% 6.96/7.01 (E(f2(x1071,f3(x1072,x1072)),f2(x1071,x1072))),
% 6.96/7.01 inference(rename_variables,[],[83])).
% 6.96/7.01 cnf(108,plain,
% 6.96/7.01 (P2(f3(f3(a1,a1),f3(a1,a1)),a6)),
% 6.96/7.01 inference(scs_inference,[],[83,97,39,103,70,60,88,40,67,28,2,13,14,10,11])).
% 6.96/7.01 cnf(112,plain,
% 6.96/7.01 (~E(f3(a6,a6),f2(x1121,f3(a1,a1)))),
% 6.96/7.01 inference(scs_inference,[],[83,107,97,39,103,70,86,60,84,88,40,67,28,2,13,14,10,11,12,3])).
% 6.96/7.01 cnf(116,plain,
% 6.96/7.01 (E(x1161,f3(x1161,a1))),
% 6.96/7.01 inference(scs_inference,[],[17,106,28,2])).
% 6.96/7.01 cnf(117,plain,
% 6.96/7.01 (~P1(f3(f2(x1171,a1),a1))),
% 6.96/7.01 inference(scs_inference,[],[97,17,106,28,2,10])).
% 6.96/7.01 cnf(119,plain,
% 6.96/7.01 (P3(f2(x1191,f3(x1192,x1193)),f3(f2(x1191,x1192),f2(x1191,x1193)))),
% 6.96/7.01 inference(scs_inference,[],[62,97,17,106,40,28,2,10,14])).
% 6.96/7.01 cnf(120,plain,
% 6.96/7.01 (P3(x1201,x1201)),
% 6.96/7.01 inference(rename_variables,[],[40])).
% 6.96/7.01 cnf(127,plain,
% 6.96/7.01 (~P1(x1271)+P2(x1271,f3(f4(x1271),a1))),
% 6.96/7.01 inference(scs_inference,[],[62,97,17,106,99,108,40,120,28,2,10,14,13,12,3,30])).
% 6.96/7.01 cnf(132,plain,
% 6.96/7.01 (E(f3(x1321,f3(x1322,x1323)),f3(f3(x1321,x1322),x1323))),
% 6.96/7.01 inference(scs_inference,[],[117,22,28,2])).
% 6.96/7.01 cnf(135,plain,
% 6.96/7.01 (~P1(f2(x1351,f3(f3(a1,a1),f3(a1,a1))))),
% 6.96/7.01 inference(scs_inference,[],[83,60,63,117,22,106,28,2,12,10])).
% 6.96/7.01 cnf(137,plain,
% 6.96/7.01 (~E(f3(a6,a6),a1)),
% 6.96/7.01 inference(scs_inference,[],[116,83,60,63,95,117,22,106,28,2,12,10,3])).
% 6.96/7.01 cnf(141,plain,
% 6.96/7.01 (E(f2(x1411,f2(x1412,x1413)),f2(f2(x1411,x1412),x1413))),
% 6.96/7.01 inference(scs_inference,[],[135,23,28,2])).
% 6.96/7.01 cnf(144,plain,
% 6.96/7.01 (E(f3(x1441,x1442),f3(f3(f3(x1441,x1442),x1441),x1442))),
% 6.96/7.01 inference(scs_inference,[],[39,132,46,84,135,23,28,2,12,3])).
% 6.96/7.01 cnf(147,plain,
% 6.96/7.01 (~P1(f3(f2(x1471,f3(a1,a1)),a1))),
% 6.96/7.01 inference(scs_inference,[],[39,132,97,46,84,135,23,28,2,12,3,10])).
% 6.96/7.01 cnf(151,plain,
% 6.96/7.01 (E(f3(f3(f3(x1511,x1512),x1511),x1512),f3(x1511,x1512))),
% 6.96/7.01 inference(scs_inference,[],[144,147,28,2])).
% 6.96/7.01 cnf(152,plain,
% 6.96/7.01 (~P1(f3(a1,f2(x1521,f3(a1,a1))))),
% 6.96/7.01 inference(scs_inference,[],[144,147,21,28,2,10])).
% 6.96/7.01 cnf(154,plain,
% 6.96/7.01 (~E(f3(a6,a6),f2(x1541,f2(x1542,f3(a1,a1))))),
% 6.96/7.01 inference(scs_inference,[],[141,144,112,147,21,28,2,10,3])).
% 6.96/7.01 cnf(159,plain,
% 6.96/7.01 (E(a1,f2(a1,x1591))),
% 6.96/7.01 inference(scs_inference,[],[152,16,28,2])).
% 6.96/7.01 cnf(160,plain,
% 6.96/7.01 (~P1(f2(a1,x1601))),
% 6.96/7.01 inference(scs_inference,[],[51,152,16,28,2,10])).
% 6.96/7.01 cnf(163,plain,
% 6.96/7.01 (P2(f2(a1,x1631),a6)),
% 6.96/7.01 inference(scs_inference,[],[51,151,42,152,16,28,2,10,3,55])).
% 6.96/7.01 cnf(164,plain,
% 6.96/7.01 (P2(f3(f2(a1,x1641),f2(a1,x1641)),a6)),
% 6.96/7.01 inference(scs_inference,[],[51,39,151,42,152,16,28,2,10,3,55,11])).
% 6.96/7.01 cnf(168,plain,
% 6.96/7.01 (E(x1681,f2(x1681,a6))),
% 6.96/7.01 inference(scs_inference,[],[160,18,28,2])).
% 6.96/7.01 cnf(169,plain,
% 6.96/7.01 (E(a1,f3(f2(a1,x1691),a1))),
% 6.96/7.01 inference(scs_inference,[],[101,159,160,18,28,2,3])).
% 6.96/7.01 cnf(172,plain,
% 6.96/7.01 (~P1(f3(f3(f3(f2(x1721,a1),f2(x1722,a1)),f2(x1721,a1)),f2(x1722,a1)))),
% 6.96/7.01 inference(scs_inference,[],[101,159,151,160,88,18,28,2,3,10])).
% 6.96/7.01 cnf(174,plain,
% 6.96/7.01 (P2(f3(f2(a1,x1741),a1),a6)),
% 6.96/7.01 inference(scs_inference,[],[101,159,151,160,88,18,28,2,3,10,55])).
% 6.96/7.01 cnf(175,plain,
% 6.96/7.01 (~P1(x1751)+P2(x1751,f2(f4(x1751),a6))),
% 6.96/7.01 inference(scs_inference,[],[101,159,151,160,88,18,28,2,3,10,55,30])).
% 6.96/7.01 cnf(180,plain,
% 6.96/7.01 (E(f3(f2(a1,x1801),a1),a1)),
% 6.96/7.01 inference(scs_inference,[],[169,172,28,2])).
% 6.96/7.01 cnf(181,plain,
% 6.96/7.01 (~P1(f3(f2(a1,x1811),a1))),
% 6.96/7.01 inference(scs_inference,[],[169,97,172,160,28,2,10])).
% 6.96/7.01 cnf(184,plain,
% 6.96/7.01 (E(x1841,f2(f3(x1841,x1841),a6))),
% 6.96/7.01 inference(scs_inference,[],[39,168,169,97,172,160,28,2,10,3])).
% 6.96/7.01 cnf(186,plain,
% 6.96/7.01 (P3(f2(a1,x1861),a1)),
% 6.96/7.01 inference(scs_inference,[],[39,168,169,97,172,160,28,2,10,3,36])).
% 6.96/7.01 cnf(188,plain,
% 6.96/7.01 (P2(f2(f3(a1,a1),a6),a6)),
% 6.96/7.01 inference(scs_inference,[],[39,168,169,97,172,160,28,2,10,3,36,55])).
% 6.96/7.01 cnf(189,plain,
% 6.96/7.01 (P2(f3(f3(a1,a1),a1),a6)),
% 6.96/7.01 inference(scs_inference,[],[39,116,168,169,97,60,172,160,28,2,10,3,36,55,11])).
% 6.96/7.01 cnf(197,plain,
% 6.96/7.01 (E(f2(f3(x1971,x1971),a6),x1971)),
% 6.96/7.01 inference(scs_inference,[],[184,181,28,2])).
% 6.96/7.01 cnf(199,plain,
% 6.96/7.01 (E(x1991,f3(x1991,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(200,plain,
% 6.96/7.01 (P3(f3(x2001,a1),x2001)),
% 6.96/7.01 inference(scs_inference,[],[116,199,184,68,40,181,28,2,11,13])).
% 6.96/7.01 cnf(202,plain,
% 6.96/7.01 (P3(f3(x2021,x2021),f3(x2021,a1))),
% 6.96/7.01 inference(scs_inference,[],[116,199,184,68,70,40,181,28,2,11,13,14])).
% 6.96/7.01 cnf(204,plain,
% 6.96/7.01 (E(x2041,f2(f3(f3(x2041,a1),f3(x2041,a1)),a6))),
% 6.96/7.01 inference(scs_inference,[],[116,199,184,68,70,40,181,28,2,11,13,14,3])).
% 6.96/7.01 cnf(206,plain,
% 6.96/7.01 (~P1(f3(a1,f2(a1,x2061)))),
% 6.96/7.01 inference(scs_inference,[],[116,199,184,68,70,40,181,21,28,2,11,13,14,3,10])).
% 6.96/7.01 cnf(215,plain,
% 6.96/7.01 (E(f2(f3(f3(x2151,a1),f3(x2151,a1)),a6),x2151)),
% 6.96/7.01 inference(scs_inference,[],[204,206,28,2])).
% 6.96/7.01 cnf(216,plain,
% 6.96/7.01 (P3(f3(f3(x2161,x2161),f3(x2161,x2161)),f3(x2161,a1))),
% 6.96/7.01 inference(scs_inference,[],[39,204,202,206,28,2,13])).
% 6.96/7.01 cnf(217,plain,
% 6.96/7.01 (E(x2171,f3(x2171,x2171))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(218,plain,
% 6.96/7.01 (P3(f3(x2181,x2181),f3(f3(x2181,a1),f3(x2181,a1)))),
% 6.96/7.01 inference(scs_inference,[],[39,217,204,202,206,28,2,13,14])).
% 6.96/7.01 cnf(221,plain,
% 6.96/7.01 (~P1(f2(f3(a1,a1),a6))),
% 6.96/7.01 inference(scs_inference,[],[51,39,217,180,197,204,72,202,206,28,2,13,14,3,10])).
% 6.96/7.01 cnf(225,plain,
% 6.96/7.01 (E(x2251,f2(a6,x2251))),
% 6.96/7.01 inference(scs_inference,[],[221,19,28,2])).
% 6.96/7.01 cnf(227,plain,
% 6.96/7.01 (E(x2271,f3(x2271,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(228,plain,
% 6.96/7.01 (P3(x2281,f3(x2281,a1))),
% 6.96/7.01 inference(scs_inference,[],[116,227,164,40,221,19,28,2,11,14])).
% 6.96/7.01 cnf(230,plain,
% 6.96/7.01 (P3(f3(x2301,a1),f3(x2301,x2301))),
% 6.96/7.01 inference(scs_inference,[],[116,227,164,65,40,221,19,28,2,11,14,13])).
% 6.96/7.01 cnf(232,plain,
% 6.96/7.01 (E(x2321,f2(f3(x2321,a1),a6))),
% 6.96/7.01 inference(scs_inference,[],[116,227,168,164,65,40,221,19,28,2,11,14,13,3])).
% 6.96/7.01 cnf(234,plain,
% 6.96/7.01 (~P1(f2(f3(f3(a1,a1),f3(a1,a1)),a6))),
% 6.96/7.01 inference(scs_inference,[],[51,116,227,168,215,164,65,40,221,19,28,2,11,14,13,3,10])).
% 6.96/7.01 cnf(236,plain,
% 6.96/7.01 (P2(f2(a6,a1),a6)),
% 6.96/7.01 inference(scs_inference,[],[51,116,227,168,215,164,65,40,221,19,28,2,11,14,13,3,10,55])).
% 6.96/7.01 cnf(242,plain,
% 6.96/7.01 (E(f2(f3(x2421,a1),a6),x2421)),
% 6.96/7.01 inference(scs_inference,[],[232,234,28,2])).
% 6.96/7.01 cnf(244,plain,
% 6.96/7.01 (E(x2441,f3(x2441,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(246,plain,
% 6.96/7.01 (E(x2461,f3(x2461,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(249,plain,
% 6.96/7.01 (~E(f3(a6,a6),f3(f2(a1,x2491),a1))),
% 6.96/7.01 inference(scs_inference,[],[116,244,246,180,232,86,104,137,234,28,2,11,13,14,3])).
% 6.96/7.01 cnf(250,plain,
% 6.96/7.01 (~P1(f3(f3(a1,a1),f3(a1,a1)))),
% 6.96/7.01 inference(scs_inference,[],[116,244,246,180,168,232,86,104,137,234,28,2,11,13,14,3,10])).
% 6.96/7.01 cnf(260,plain,
% 6.96/7.01 (E(x2601,f3(x2601,x2601))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(262,plain,
% 6.96/7.01 (E(x2621,f3(x2621,x2621))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(263,plain,
% 6.96/7.01 (P3(f3(f3(x2631,a1),f3(x2631,a1)),f3(x2631,x2631))),
% 6.96/7.01 inference(scs_inference,[],[39,260,262,236,250,216,230,25,28,2,11,14,13])).
% 6.96/7.01 cnf(267,plain,
% 6.96/7.01 (~P1(f3(a1,f3(a1,f3(a1,a1))))),
% 6.96/7.01 inference(scs_inference,[],[39,260,262,116,132,236,250,216,230,249,25,28,2,11,14,13,3,10])).
% 6.96/7.01 cnf(269,plain,
% 6.96/7.01 (E(f4(a1),a1)),
% 6.96/7.01 inference(scs_inference,[],[57,27,29])).
% 6.96/7.01 cnf(272,plain,
% 6.96/7.01 (E(a1,f4(a1))),
% 6.96/7.01 inference(scs_inference,[],[267,269,28,2])).
% 6.96/7.01 cnf(273,plain,
% 6.96/7.01 (P3(f3(f3(x2731,a1),f3(x2731,a1)),x2731)),
% 6.96/7.01 inference(scs_inference,[],[39,200,267,269,28,2,13])).
% 6.96/7.01 cnf(274,plain,
% 6.96/7.01 (E(x2741,f3(x2741,x2741))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(276,plain,
% 6.96/7.01 (E(x2761,f3(x2761,x2761))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(277,plain,
% 6.96/7.01 (E(x2771,f2(f3(f3(x2771,x2771),f3(x2771,x2771)),a6))),
% 6.96/7.01 inference(scs_inference,[],[39,274,276,184,263,200,267,269,28,2,13,14,3])).
% 6.96/7.01 cnf(279,plain,
% 6.96/7.01 (~P1(f2(f3(a1,a1),f3(a6,a6)))),
% 6.96/7.01 inference(scs_inference,[],[39,274,276,184,83,263,200,267,269,221,28,2,13,14,3,10])).
% 6.96/7.01 cnf(281,plain,
% 6.96/7.01 (P2(f4(a1),a6)),
% 6.96/7.01 inference(scs_inference,[],[39,274,276,184,83,263,200,267,269,221,28,2,13,14,3,10,55])).
% 6.96/7.01 cnf(282,plain,
% 6.96/7.01 (P2(f3(f4(a1),f4(a1)),a6)),
% 6.96/7.01 inference(scs_inference,[],[39,274,276,184,83,263,200,267,269,221,28,2,13,14,3,10,55,11])).
% 6.96/7.01 cnf(286,plain,
% 6.96/7.01 (E(f2(f3(f3(x2861,x2861),f3(x2861,x2861)),a6),x2861)),
% 6.96/7.01 inference(scs_inference,[],[277,279,28,2])).
% 6.96/7.01 cnf(288,plain,
% 6.96/7.01 (E(x2881,f3(x2881,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(290,plain,
% 6.96/7.01 (E(x2901,f3(x2901,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(293,plain,
% 6.96/7.01 (E(x2931,f2(f3(f3(x2931,a1),a1),a6))),
% 6.96/7.01 inference(scs_inference,[],[116,288,290,232,277,108,91,279,28,2,11,14,13,3])).
% 6.96/7.01 cnf(295,plain,
% 6.96/7.01 (~P1(f2(f3(a1,a1),f3(f3(a6,a6),f3(a6,a6))))),
% 6.96/7.01 inference(scs_inference,[],[116,288,290,232,277,83,108,91,279,28,2,11,14,13,3,10])).
% 6.96/7.01 cnf(300,plain,
% 6.96/7.01 (E(f2(f3(f3(x3001,a1),a1),a6),x3001)),
% 6.96/7.01 inference(scs_inference,[],[293,295,28,2])).
% 6.96/7.01 cnf(301,plain,
% 6.96/7.01 (P3(f3(f2(a1,x3011),f2(a1,x3011)),a1)),
% 6.96/7.01 inference(scs_inference,[],[39,293,295,186,28,2,13])).
% 6.96/7.01 cnf(302,plain,
% 6.96/7.01 (E(x3021,f3(x3021,x3021))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(303,plain,
% 6.96/7.01 (P3(x3031,f3(f3(x3031,a1),f3(x3031,a1)))),
% 6.96/7.01 inference(scs_inference,[],[39,302,293,295,228,186,28,2,13,14])).
% 6.96/7.01 cnf(304,plain,
% 6.96/7.01 (E(x3041,f3(x3041,x3041))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(305,plain,
% 6.96/7.01 (E(x3051,f2(f3(f3(x3051,x3051),a1),a6))),
% 6.96/7.01 inference(scs_inference,[],[39,302,304,232,293,295,228,186,28,2,13,14,3])).
% 6.96/7.01 cnf(307,plain,
% 6.96/7.01 (~P1(f3(f2(f3(a1,a1),f3(a6,a6)),a1))),
% 6.96/7.01 inference(scs_inference,[],[39,302,304,232,293,97,295,228,186,28,2,13,14,3,10])).
% 6.96/7.01 cnf(311,plain,
% 6.96/7.01 (E(f2(f3(f3(x3111,x3111),a1),a6),x3111)),
% 6.96/7.01 inference(scs_inference,[],[305,307,28,2])).
% 6.96/7.01 cnf(313,plain,
% 6.96/7.01 (E(x3131,f3(x3131,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(315,plain,
% 6.96/7.01 (E(x3151,f3(x3151,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(318,plain,
% 6.96/7.01 (~E(f4(a1),f2(f3(f3(a6,a6),f3(a6,a6)),a6))),
% 6.96/7.01 inference(scs_inference,[],[26,116,313,315,286,305,188,102,218,307,28,2,11,13,14,3])).
% 6.96/7.01 cnf(320,plain,
% 6.96/7.01 (~P1(f2(f3(f3(a1,a1),a1),a6))),
% 6.96/7.01 inference(scs_inference,[],[26,51,116,313,315,286,305,300,188,102,218,307,28,2,11,13,14,3,10])).
% 6.96/7.01 cnf(325,plain,
% 6.96/7.01 (P3(f3(f2(a1,x3251),f2(a1,x3251)),f3(a1,a1))),
% 6.96/7.01 inference(scs_inference,[],[39,320,301,15,28,2,14])).
% 6.96/7.01 cnf(329,plain,
% 6.96/7.01 (~P1(f3(f3(a1,a1),a1))),
% 6.96/7.01 inference(scs_inference,[],[26,39,168,242,320,301,15,28,2,14,3,10])).
% 6.96/7.01 cnf(337,plain,
% 6.96/7.01 (E(x3371,f3(x3371,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(339,plain,
% 6.96/7.01 (E(x3391,f3(x3391,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(344,plain,
% 6.96/7.01 (~P1(f3(a1,f3(a1,a1)))),
% 6.96/7.01 inference(scs_inference,[],[116,337,339,168,132,189,318,329,325,28,11,13,14,3,10])).
% 6.96/7.01 cnf(348,plain,
% 6.96/7.01 (P3(f2(a1,x3481),f3(a1,a1))),
% 6.96/7.01 inference(scs_inference,[],[39,344,186,28,14])).
% 6.96/7.01 cnf(350,plain,
% 6.96/7.01 (E(f3(f2(a1,x3501),a1),f4(a1))),
% 6.96/7.01 inference(scs_inference,[],[39,180,272,344,186,28,14,3])).
% 6.96/7.01 cnf(351,plain,
% 6.96/7.01 (~P1(f4(a1))),
% 6.96/7.01 inference(scs_inference,[],[51,39,180,272,344,269,186,28,14,3,10])).
% 6.96/7.01 cnf(356,plain,
% 6.96/7.01 (E(x3561,f2(f3(x3561,x3561),a6))),
% 6.96/7.01 inference(rename_variables,[],[184])).
% 6.96/7.01 cnf(358,plain,
% 6.96/7.01 (E(x3581,f2(f3(x3581,x3581),a6))),
% 6.96/7.01 inference(rename_variables,[],[184])).
% 6.96/7.01 cnf(359,plain,
% 6.96/7.01 (P3(f3(x3591,x3591),f2(f3(x3591,x3591),a6))),
% 6.96/7.01 inference(scs_inference,[],[184,356,358,56,70,351,28,11,13,14])).
% 6.96/7.01 cnf(363,plain,
% 6.96/7.01 (~P1(f2(f2(a1,x3631),x3632))),
% 6.96/7.01 inference(scs_inference,[],[26,184,356,358,311,56,70,351,23,160,28,11,13,14,3,10])).
% 6.96/7.01 cnf(369,plain,
% 6.96/7.01 (E(x3691,f3(x3691,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(371,plain,
% 6.96/7.01 (E(x3711,f3(x3711,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(373,plain,
% 6.96/7.01 (E(x3731,f3(x3731,a1))),
% 6.96/7.01 inference(rename_variables,[],[116])).
% 6.96/7.01 cnf(376,plain,
% 6.96/7.01 (~P1(f3(f2(f2(a1,x3761),x3762),a1))),
% 6.96/7.01 inference(scs_inference,[],[116,369,371,373,350,97,174,273,303,363,28,11,13,14,3,10])).
% 6.96/7.01 cnf(379,plain,
% 6.96/7.01 (E(f4(a1),f2(a1,x3791))),
% 6.96/7.01 inference(scs_inference,[],[116,369,371,373,350,97,174,273,303,363,28,11,13,14,3,10,2])).
% 6.96/7.01 cnf(383,plain,
% 6.96/7.01 (E(x3831,f3(x3831,x3831))),
% 6.96/7.01 inference(rename_variables,[],[39])).
% 6.96/7.01 cnf(389,plain,
% 6.96/7.01 (~P1(f3(a1,f2(f2(a1,x3891),x3892)))),
% 6.96/7.01 inference(scs_inference,[],[39,383,379,154,348,359,376,21,28,13,14,3,10])).
% 6.96/7.01 cnf(394,plain,
% 6.96/7.01 (E(x3941,f2(f3(x3941,x3941),a6))),
% 6.96/7.01 inference(rename_variables,[],[184])).
% 6.96/7.01 cnf(396,plain,
% 6.96/7.01 (P3(x3961,f3(x3961,x3961))),
% 6.96/7.01 inference(rename_variables,[],[65])).
% 6.96/7.01 cnf(399,plain,
% 6.96/7.01 (~P1(f2(f2(f2(a1,x3991),x3992),x3993))),
% 6.96/7.01 inference(scs_inference,[],[184,394,68,65,396,389,363,23,28,11,13,14,10])).
% 6.96/7.01 cnf(406,plain,
% 6.96/7.01 (P2(f2(a6,a1),f3(a6,a6))),
% 6.96/7.01 inference(scs_inference,[],[225,56,399,28,11])).
% 6.96/7.01 cnf(407,plain,
% 6.96/7.01 (E(x4071,f2(a6,x4071))),
% 6.96/7.01 inference(rename_variables,[],[225])).
% 6.96/7.01 cnf(409,plain,
% 6.96/7.01 (P3(x4091,x4091)),
% 6.96/7.01 inference(rename_variables,[],[40])).
% 6.96/7.01 cnf(410,plain,
% 6.96/7.01 (P3(x4101,f2(a6,x4101))),
% 6.96/7.01 inference(scs_inference,[],[225,407,56,40,409,399,28,11,13,14])).
% 6.96/7.01 cnf(432,plain,
% 6.96/7.01 (E(x4321,f2(f3(x4321,x4321),a6))),
% 6.96/7.01 inference(rename_variables,[],[184])).
% 6.96/7.01 cnf(434,plain,
% 6.96/7.01 (P3(x4341,x4341)),
% 6.96/7.01 inference(rename_variables,[],[40])).
% 6.96/7.02 cnf(435,plain,
% 6.96/7.02 (P3(x4351,f2(f3(x4351,x4351),a6))),
% 6.96/7.02 inference(scs_inference,[],[184,432,163,40,434,11,13,14])).
% 6.96/7.02 cnf(488,plain,
% 6.96/7.02 (P2(f2(a6,f3(a1,a1)),f3(a6,a6))),
% 6.96/7.02 inference(scs_inference,[],[225,68,11])).
% 6.96/7.02 cnf(617,plain,
% 6.96/7.02 (E(x6171,f3(x6171,a1))),
% 6.96/7.02 inference(rename_variables,[],[116])).
% 6.96/7.02 cnf(618,plain,
% 6.96/7.02 (P3(f3(x6181,a1),f2(f3(x6181,x6181),a6))),
% 6.96/7.02 inference(scs_inference,[],[116,617,282,435,11,13])).
% 6.96/7.02 cnf(704,plain,
% 6.96/7.02 (P3(x7041,f2(a6,x7041))),
% 6.96/7.02 inference(rename_variables,[],[410])).
% 6.96/7.02 cnf(705,plain,
% 6.96/7.02 (P3(x7051,f2(f3(f2(a6,x7051),a1),a6))),
% 6.96/7.02 inference(scs_inference,[],[232,410,704,13,14])).
% 6.96/7.02 cnf(711,plain,
% 6.96/7.02 (E(f3(a6,f2(a6,a1)),a6)),
% 6.96/7.02 inference(scs_inference,[],[225,32,55])).
% 6.96/7.02 cnf(712,plain,
% 6.96/7.02 (E(a6,f3(a6,f2(a6,a1)))),
% 6.96/7.02 inference(scs_inference,[],[711,2])).
% 6.96/7.02 cnf(727,plain,
% 6.96/7.02 (E(x7271,f3(x7271,a1))),
% 6.96/7.02 inference(rename_variables,[],[116])).
% 6.96/7.02 cnf(732,plain,
% 6.96/7.02 (~P1(a6)+P1(f3(a6,f2(a6,a1)))),
% 6.96/7.02 inference(scs_inference,[],[116,727,712,488,705,618,11,13,14,10])).
% 6.96/7.02 cnf(1083,plain,
% 6.96/7.02 (P3(f3(f2(x10831,a1),a1),a1)),
% 6.96/7.02 inference(scs_inference,[],[15,200,410,13,14])).
% 6.96/7.02 cnf(1142,plain,
% 6.96/7.02 (P2(f2(a6,f4(a1)),a6)),
% 6.96/7.02 inference(scs_inference,[],[225,281,11])).
% 6.96/7.02 cnf(1151,plain,
% 6.96/7.02 (E(x11511,f3(x11511,a1))),
% 6.96/7.02 inference(rename_variables,[],[116])).
% 6.96/7.02 cnf(1153,plain,
% 6.96/7.02 (E(x11531,f3(x11531,a1))),
% 6.96/7.02 inference(rename_variables,[],[116])).
% 6.96/7.02 cnf(1154,plain,
% 6.96/7.02 (P3(f3(f2(x11541,a1),a1),f3(a1,a1))),
% 6.96/7.02 inference(scs_inference,[],[116,1151,1153,1142,1083,11,13,14])).
% 6.96/7.02 cnf(1158,plain,
% 6.96/7.02 (P3(a1,f3(f2(a1,x11581),f2(a1,x11581)))),
% 6.96/7.02 inference(scs_inference,[],[16,65,13])).
% 6.96/7.02 cnf(1163,plain,
% 6.96/7.02 (P2(a6,f3(f4(a6),a1))),
% 6.96/7.02 inference(scs_inference,[],[46,127,28])).
% 6.96/7.02 cnf(1166,plain,
% 6.96/7.02 (P2(f2(f3(a6,a6),a6),f3(f4(a6),a1))),
% 6.96/7.02 inference(scs_inference,[],[184,84,1163,12,11])).
% 6.96/7.02 cnf(1172,plain,
% 6.96/7.02 (P2(a6,f2(f4(a6),a6))),
% 6.96/7.02 inference(scs_inference,[],[46,175,28])).
% 6.96/7.02 cnf(1173,plain,
% 6.96/7.02 (~E(f3(f4(a6),a1),a1)),
% 6.96/7.02 inference(scs_inference,[],[57,1166,12])).
% 6.96/7.02 cnf(1175,plain,
% 6.96/7.02 (P2(f2(a6,a6),f2(f4(a6),a6))),
% 6.96/7.02 inference(scs_inference,[],[168,57,1166,1172,12,11])).
% 6.96/7.02 cnf(1176,plain,
% 6.96/7.02 (E(x11761,f2(x11761,a6))),
% 6.96/7.02 inference(rename_variables,[],[168])).
% 6.96/7.02 cnf(1182,plain,
% 6.96/7.02 (~P3(f4(a6),a1)),
% 6.96/7.02 inference(scs_inference,[],[16,168,1176,57,119,1166,1158,1172,12,11,13,14,35])).
% 6.96/7.02 cnf(1188,plain,
% 6.96/7.02 (P2(f3(f2(a6,a6),f2(a6,a6)),f2(f4(a6),a6))),
% 6.96/7.02 inference(scs_inference,[],[16,39,63,1175,1173,3,12,11])).
% 6.96/7.02 cnf(1192,plain,
% 6.96/7.02 (~E(f3(f4(a6),f4(a6)),a1)),
% 6.96/7.02 inference(scs_inference,[],[16,39,63,65,70,1175,1182,1173,3,12,11,13,14])).
% 6.96/7.02 cnf(1198,plain,
% 6.96/7.02 (P2(f2(a6,f2(a6,a1)),f3(a6,a6))),
% 6.96/7.02 inference(scs_inference,[],[16,225,84,406,1188,1192,3,12,11])).
% 6.96/7.02 cnf(1199,plain,
% 6.96/7.02 (E(x11991,f2(a6,x11991))),
% 6.96/7.02 inference(rename_variables,[],[225])).
% 6.96/7.02 cnf(1201,plain,
% 6.96/7.02 (P3(x12011,x12011)),
% 6.96/7.02 inference(rename_variables,[],[40])).
% 6.96/7.02 cnf(1202,plain,
% 6.96/7.02 (~E(f4(a6),a1)),
% 6.96/7.02 inference(scs_inference,[],[16,225,84,40,1201,406,1188,1192,1182,3,12,11,13,14])).
% 6.96/7.02 cnf(1207,plain,
% 6.96/7.02 (P1(f2(a6,a6))),
% 6.96/7.02 inference(scs_inference,[],[16,225,1199,84,40,1201,406,1188,1192,1182,3,12,11,13,14,27,732,10])).
% 6.96/7.02 cnf(1209,plain,
% 6.96/7.02 (P2(a6,f2(f3(f4(a6),a1),a6))),
% 6.96/7.02 inference(scs_inference,[],[16,225,1199,232,84,40,1201,406,1188,1192,1182,3,12,11,13,14,27,732,10,30])).
% 6.96/7.02 cnf(1214,plain,
% 6.96/7.02 (E(x12141,f2(a6,x12141))),
% 6.96/7.02 inference(rename_variables,[],[225])).
% 6.96/7.02 cnf(1216,plain,
% 6.96/7.02 (E(x12161,f2(a6,x12161))),
% 6.96/7.02 inference(rename_variables,[],[225])).
% 6.96/7.02 cnf(1222,plain,
% 6.96/7.02 (E(x12221,f2(a6,x12221))),
% 6.96/7.02 inference(rename_variables,[],[225])).
% 6.96/7.02 cnf(1227,plain,
% 6.96/7.02 ($false),
% 6.96/7.02 inference(scs_inference,[],[16,225,1214,1216,1222,57,102,1207,1198,1154,1209,1202,1163,1182,10,30,3,12,11,13,14,33]),
% 6.96/7.02 ['proof']).
% 6.96/7.02 % SZS output end Proof
% 6.96/7.02 % Total time :6.380000s
%------------------------------------------------------------------------------