%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KLE076+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 : n023.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:59 EDT 2024
% Result : Theorem 10.18s 10.26s
% Output : CNFRefutation 10.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : KLE076+1 : TPTP v8.2.0. Released v4.0.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.31 % Computer : n023.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Thu Jun 20 22:14:54 EDT 2024
% 0.17/0.32 % CPUTime :
% 0.51/0.56 start to proof:theBenchmark
% 10.18/10.25 %-------------------------------------------
% 10.18/10.25 % File :CSE---1.7
% 10.18/10.25 % Problem :theBenchmark
% 10.18/10.25 % Transform :cnf
% 10.18/10.25 % Format :tptp:raw
% 10.18/10.25 % Command :java -jar mcs_scs.jar %d %s
% 10.18/10.25
% 10.18/10.25 % Result :Theorem 9.660000s
% 10.18/10.25 % Output :CNFRefutation 9.660000s
% 10.18/10.25 %-------------------------------------------
% 10.18/10.26 %------------------------------------------------------------------------------
% 10.18/10.26 % File : KLE076+1 : TPTP v8.2.0. Released v4.0.0.
% 10.18/10.26 % Domain : Kleene Algebra (Domain Semirings)
% 10.18/10.26 % Problem : Domain elements satisfy the fifth Kleene module axiom
% 10.18/10.26 % Version : [Hoe08] axioms.
% 10.18/10.26 % English :
% 10.18/10.26
% 10.18/10.26 % Refs : [DMS06] Desharnais et al. (2006), Kleene Algebra with Domain
% 10.18/10.26 % : [Lei06] Leiss (2006), Kleene Modules and Linear Languages
% 10.18/10.26 % : [DS08] Desharnais & Struth (2008), Modal Semirings Revisited
% 10.18/10.26 % : [Hoe08] Hoefner (2008), Email to G. Sutcliffe
% 10.18/10.26 % Source : [Hoe08]
% 10.18/10.26 % Names :
% 10.18/10.26
% 10.18/10.26 % Status : Theorem
% 10.18/10.26 % Rating : 0.03 v8.1.0, 0.00 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.04 v6.2.0, 0.08 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.04 v5.4.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.05 v5.0.0, 0.04 v4.0.0
% 10.18/10.26 % Syntax : Number of formulae : 18 ( 17 unt; 0 def)
% 10.18/10.26 % Number of atoms : 19 ( 18 equ)
% 10.18/10.26 % Maximal formula atoms : 2 ( 1 avg)
% 10.18/10.26 % Number of connectives : 1 ( 0 ~; 0 |; 0 &)
% 10.18/10.26 % ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% 10.18/10.26 % Maximal formula depth : 4 ( 3 avg)
% 10.18/10.26 % Maximal term depth : 4 ( 2 avg)
% 10.18/10.26 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 10.18/10.26 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 10.18/10.26 % Number of variables : 29 ( 29 !; 0 ?)
% 10.18/10.26 % SPC : FOF_THM_RFO_SEQ
% 10.18/10.26
% 10.18/10.26 % Comments : Equational encoding
% 10.18/10.26 %------------------------------------------------------------------------------
% 10.18/10.26 %---Include axioms for domain semiring
% 10.18/10.26 include('Axioms/KLE001+0.ax').
% 10.18/10.26 %---Include axioms for domain
% 10.18/10.26 include('Axioms/KLE001+5.ax').
% 10.18/10.26 %------------------------------------------------------------------------------
% 10.18/10.26 fof(goals,conjecture,
% 10.18/10.26 ! [X0] : domain(multiplication(X0,domain(zero))) = zero ).
% 10.18/10.26
% 10.18/10.26 %------------------------------------------------------------------------------
% 10.18/10.26 %-------------------------------------------
% 10.18/10.26 % Proof found
% 10.18/10.26 % SZS status Theorem for theBenchmark
% 10.18/10.26 % SZS output start Proof
% 10.18/10.26 %ClaNum:29(EqnAxiom:10)
% 10.18/10.26 %VarNum:65(SingletonVarNum:30)
% 10.18/10.26 %MaxLitNum:2
% 10.18/10.26 %MaxfuncDepth:3
% 10.18/10.26 %SharedTerms:8
% 10.18/10.26 %goalClause: 27
% 10.18/10.26 %singleGoalClaCount:1
% 10.18/10.26 [11]E(f2(a1),a1)
% 10.18/10.26 [27]~E(f2(f4(a5,f2(a1))),a1)
% 10.18/10.26 [12]E(f4(x121,a1),a1)
% 10.18/10.26 [13]E(f4(a1,x131),a1)
% 10.18/10.26 [14]E(f3(x141,a1),x141)
% 10.18/10.26 [15]E(f4(x151,a6),x151)
% 10.18/10.26 [16]E(f4(a6,x161),x161)
% 10.18/10.26 [17]E(f3(x171,x171),x171)
% 10.18/10.26 [18]E(f3(f2(x181),a6),a6)
% 10.18/10.26 [22]E(f3(x221,f4(f2(x221),x221)),f4(f2(x221),x221))
% 10.18/10.26 [19]E(f3(x191,x192),f3(x192,x191))
% 10.18/10.26 [20]E(f2(f3(x201,x202)),f3(f2(x201),f2(x202)))
% 10.18/10.26 [21]E(f2(f4(x211,f2(x212))),f2(f4(x211,x212)))
% 10.18/10.26 [23]E(f3(f3(x231,x232),x233),f3(x231,f3(x232,x233)))
% 10.18/10.26 [24]E(f4(f4(x241,x242),x243),f4(x241,f4(x242,x243)))
% 10.18/10.26 [25]E(f3(f4(x251,x252),f4(x251,x253)),f4(x251,f3(x252,x253)))
% 10.18/10.26 [26]E(f3(f4(x261,x262),f4(x263,x262)),f4(f3(x261,x263),x262))
% 10.18/10.26 [28]~P1(x281,x282)+E(f3(x281,x282),x282)
% 10.18/10.26 [29]P1(x291,x292)+~E(f3(x291,x292),x292)
% 10.18/10.26 %EqnAxiom
% 10.18/10.26 [1]E(x11,x11)
% 10.18/10.26 [2]E(x22,x21)+~E(x21,x22)
% 10.18/10.26 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 10.18/10.26 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 10.18/10.26 [5]~E(x51,x52)+E(f4(x51,x53),f4(x52,x53))
% 10.18/10.26 [6]~E(x61,x62)+E(f4(x63,x61),f4(x63,x62))
% 10.18/10.26 [7]~E(x71,x72)+E(f3(x71,x73),f3(x72,x73))
% 10.18/10.26 [8]~E(x81,x82)+E(f3(x83,x81),f3(x83,x82))
% 10.18/10.26 [9]P1(x92,x93)+~E(x91,x92)+~P1(x91,x93)
% 10.18/10.26 [10]P1(x103,x102)+~E(x101,x102)+~P1(x103,x101)
% 10.18/10.26
% 10.18/10.26 %-------------------------------------------
% 10.18/10.27 cnf(30,plain,
% 10.18/10.27 (E(x301,f3(x301,x301))),
% 10.18/10.27 inference(scs_inference,[],[17,2])).
% 10.18/10.27 cnf(31,plain,
% 10.18/10.27 (P1(x311,x311)),
% 10.18/10.27 inference(scs_inference,[],[17,2,29])).
% 10.18/10.27 cnf(33,plain,
% 10.18/10.27 (~E(f2(f4(a5,f2(a1))),f3(a1,a1))),
% 10.18/10.27 inference(scs_inference,[],[27,17,2,29,3])).
% 10.18/10.27 cnf(37,plain,
% 10.18/10.27 (P1(x371,f4(f2(x371),x371))),
% 10.18/10.27 inference(scs_inference,[],[22,29])).
% 10.18/10.27 cnf(39,plain,
% 10.18/10.27 (E(x391,f3(x391,a1))),
% 10.18/10.27 inference(scs_inference,[],[14,22,29,2])).
% 10.18/10.27 cnf(40,plain,
% 10.18/10.27 (P1(x401,f3(x401,x401))),
% 10.18/10.27 inference(scs_inference,[],[30,31,14,22,29,2,10])).
% 10.18/10.27 cnf(41,plain,
% 10.18/10.27 (P1(x411,x411)),
% 10.18/10.27 inference(rename_variables,[],[31])).
% 10.18/10.27 cnf(44,plain,
% 10.18/10.27 (P1(f3(x441,x441),x441)),
% 10.18/10.27 inference(scs_inference,[],[27,30,31,41,14,15,22,29,2,10,3,9])).
% 10.18/10.27 cnf(46,plain,
% 10.18/10.27 (P1(f2(x461),a6)),
% 10.18/10.27 inference(scs_inference,[],[18,29])).
% 10.18/10.27 cnf(48,plain,
% 10.18/10.27 (E(x481,f4(a6,x481))),
% 10.18/10.27 inference(scs_inference,[],[16,18,29,2])).
% 10.18/10.27 cnf(49,plain,
% 10.18/10.27 (P1(x491,f3(f3(x491,x491),a1))),
% 10.18/10.27 inference(scs_inference,[],[39,40,16,18,29,2,10])).
% 10.18/10.27 cnf(50,plain,
% 10.18/10.27 (E(x501,f3(x501,a1))),
% 10.18/10.27 inference(rename_variables,[],[39])).
% 10.18/10.27 cnf(51,plain,
% 10.18/10.27 (P1(f3(x511,a1),f3(x511,x511))),
% 10.18/10.27 inference(scs_inference,[],[39,50,40,16,18,29,2,10,9])).
% 10.18/10.27 cnf(53,plain,
% 10.18/10.27 (~E(f2(f4(a5,f2(a1))),f4(a6,a1))),
% 10.18/10.27 inference(scs_inference,[],[27,39,50,40,16,18,29,2,10,9,3])).
% 10.18/10.27 cnf(55,plain,
% 10.18/10.27 (E(f4(x551,f3(x552,x553)),f3(f4(x551,x552),f4(x551,x553)))),
% 10.18/10.27 inference(scs_inference,[],[25,2])).
% 10.18/10.27 cnf(56,plain,
% 10.18/10.27 (P1(f3(x561,x561),f4(a6,x561))),
% 10.18/10.27 inference(scs_inference,[],[48,44,25,2,10])).
% 10.18/10.27 cnf(57,plain,
% 10.18/10.27 (P1(f3(x571,x571),x571)),
% 10.18/10.27 inference(rename_variables,[],[44])).
% 10.18/10.27 cnf(58,plain,
% 10.18/10.27 (E(f4(x581,x582),f4(x581,f3(x582,x582)))),
% 10.18/10.27 inference(scs_inference,[],[48,30,44,25,2,10,3])).
% 10.18/10.27 cnf(61,plain,
% 10.18/10.27 (P1(f4(a6,f3(x611,x611)),x611)),
% 10.18/10.27 inference(scs_inference,[],[48,30,44,57,25,2,10,3,9])).
% 10.18/10.27 cnf(63,plain,
% 10.18/10.27 (E(f4(x631,f3(x632,x632)),f4(x631,x632))),
% 10.18/10.27 inference(scs_inference,[],[58,2])).
% 10.18/10.27 cnf(64,plain,
% 10.18/10.27 (P1(f3(x641,a1),f3(f3(x641,x641),a1))),
% 10.18/10.27 inference(scs_inference,[],[39,58,51,2,10])).
% 10.18/10.27 cnf(65,plain,
% 10.18/10.27 (E(x651,f3(x651,a1))),
% 10.18/10.27 inference(rename_variables,[],[39])).
% 10.18/10.27 cnf(66,plain,
% 10.18/10.27 (E(f3(x661,x662),f3(f4(a6,x661),f4(a6,x662)))),
% 10.18/10.27 inference(scs_inference,[],[55,39,48,58,51,2,10,3])).
% 10.18/10.27 cnf(69,plain,
% 10.18/10.27 (P1(f3(f3(x691,a1),a1),f3(x691,x691))),
% 10.18/10.27 inference(scs_inference,[],[55,39,65,48,58,51,2,10,3,9])).
% 10.18/10.27 cnf(71,plain,
% 10.18/10.27 (E(f3(f4(a6,x711),f4(a6,x712)),f3(x711,x712))),
% 10.18/10.27 inference(scs_inference,[],[66,2])).
% 10.18/10.27 cnf(74,plain,
% 10.18/10.27 (E(f4(x741,f3(x742,x742)),f4(x741,x742))),
% 10.18/10.27 inference(rename_variables,[],[63])).
% 10.18/10.27 cnf(75,plain,
% 10.18/10.27 (~E(f2(f4(a5,f2(a1))),f4(a6,f3(a1,a1)))),
% 10.18/10.27 inference(scs_inference,[],[63,74,66,37,53,2,10,3])).
% 10.18/10.27 cnf(77,plain,
% 10.18/10.27 (P1(f3(f3(x771,x771),a1),f4(a6,x771))),
% 10.18/10.27 inference(scs_inference,[],[63,74,39,66,37,56,53,2,10,3,9])).
% 10.18/10.27 cnf(79,plain,
% 10.18/10.27 (E(f4(f3(x791,x792),x793),f3(f4(x791,x793),f4(x792,x793)))),
% 10.18/10.27 inference(scs_inference,[],[26,2])).
% 10.18/10.27 cnf(80,plain,
% 10.18/10.27 (P1(x801,f3(f3(f3(x801,x801),a1),f3(f3(x801,x801),a1)))),
% 10.18/10.27 inference(scs_inference,[],[30,49,26,2,10])).
% 10.18/10.27 cnf(82,plain,
% 10.18/10.27 (~E(f2(f4(a5,f2(a1))),f3(f4(a6,a1),f4(a6,a1)))),
% 10.18/10.27 inference(scs_inference,[],[71,30,33,49,26,2,10,3])).
% 10.18/10.27 cnf(87,plain,
% 10.18/10.27 (E(f3(f2(x871),f2(x872)),f2(f3(x871,x872)))),
% 10.18/10.27 inference(scs_inference,[],[20,2])).
% 10.18/10.27 cnf(91,plain,
% 10.18/10.27 (~E(f2(f4(a5,f2(a1))),f4(f3(a6,a6),a1))),
% 10.18/10.27 inference(scs_inference,[],[79,71,82,69,20,2,10,3])).
% 10.18/10.27 cnf(93,plain,
% 10.18/10.27 (P1(f4(a6,x931),x931)),
% 10.18/10.27 inference(scs_inference,[],[79,63,71,82,61,69,20,2,10,3,9])).
% 10.18/10.27 cnf(96,plain,
% 10.18/10.27 (E(f3(x961,f3(x962,x963)),f3(f3(x961,x962),x963))),
% 10.18/10.27 inference(scs_inference,[],[23,2])).
% 10.18/10.27 cnf(97,plain,
% 10.18/10.27 (P1(f4(a6,f3(f2(x971),f2(x972))),f2(f3(x971,x972)))),
% 10.18/10.27 inference(scs_inference,[],[87,93,23,2,10])).
% 10.18/10.27 cnf(98,plain,
% 10.18/10.27 (P1(f4(a6,x981),x981)),
% 10.18/10.27 inference(rename_variables,[],[93])).
% 10.18/10.27 cnf(99,plain,
% 10.18/10.27 (E(f3(f4(a6,f2(x991)),f4(a6,f2(x992))),f2(f3(x991,x992)))),
% 10.18/10.27 inference(scs_inference,[],[87,71,93,23,2,10,3])).
% 10.18/10.27 cnf(101,plain,
% 10.18/10.27 (P1(f3(f4(a6,x1011),f4(a6,x1012)),f3(x1011,x1012))),
% 10.18/10.27 inference(scs_inference,[],[87,55,71,93,98,23,2,10,3,9])).
% 10.18/10.27 cnf(104,plain,
% 10.18/10.27 (E(f2(f3(x1041,x1042)),f3(f4(a6,f2(x1041)),f4(a6,f2(x1042))))),
% 10.18/10.27 inference(scs_inference,[],[99,2])).
% 10.18/10.27 cnf(106,plain,
% 10.18/10.27 (E(f3(x1061,f3(x1062,x1063)),f3(f3(x1061,x1062),x1063))),
% 10.18/10.27 inference(rename_variables,[],[96])).
% 10.18/10.27 cnf(107,plain,
% 10.18/10.27 (E(f3(f4(a6,x1071),f4(a6,f3(x1072,x1073))),f3(f3(x1071,x1072),x1073))),
% 10.18/10.27 inference(scs_inference,[],[96,106,71,99,80,2,10,3])).
% 10.18/10.27 cnf(110,plain,
% 10.18/10.27 (P1(f4(a6,f2(x1101)),f2(f3(x1101,x1101)))),
% 10.18/10.27 inference(scs_inference,[],[96,106,63,71,99,80,97,2,10,3,9])).
% 10.18/10.27 cnf(113,plain,
% 10.18/10.27 (E(f3(f3(x1131,x1132),x1133),f3(f4(a6,x1131),f4(a6,f3(x1132,x1133))))),
% 10.18/10.27 inference(scs_inference,[],[107,2])).
% 10.18/10.27 cnf(114,plain,
% 10.18/10.27 (P1(f3(f4(a6,x1141),f4(a6,f3(x1142,x1143))),f3(f3(x1141,x1142),x1143))),
% 10.18/10.27 inference(scs_inference,[],[96,107,101,2,10])).
% 10.18/10.27 cnf(116,plain,
% 10.18/10.27 (E(f3(x1161,x1162),f3(f3(f3(x1161,x1162),x1161),x1162))),
% 10.18/10.27 inference(scs_inference,[],[96,30,107,101,2,10,3])).
% 10.18/10.27 cnf(121,plain,
% 10.18/10.27 (E(f3(f3(f3(x1211,x1212),x1211),x1212),f3(x1211,x1212))),
% 10.18/10.27 inference(scs_inference,[],[116,2])).
% 10.18/10.27 cnf(127,plain,
% 10.18/10.27 (P1(f4(a6,f4(a6,f2(x1271))),f2(f3(x1271,x1271)))),
% 10.18/10.27 inference(scs_inference,[],[55,63,48,116,110,91,77,2,10,3,9])).
% 10.18/10.27 cnf(129,plain,
% 10.18/10.27 (E(f4(x1291,f4(x1292,x1293)),f4(f4(x1291,x1292),x1293))),
% 10.18/10.27 inference(scs_inference,[],[24,2])).
% 10.18/10.27 cnf(131,plain,
% 10.18/10.27 (P1(f3(f4(a6,x1311),f4(a6,f3(x1312,x1313))),f3(f3(x1311,x1312),x1313))),
% 10.18/10.27 inference(rename_variables,[],[114])).
% 10.18/10.27 cnf(132,plain,
% 10.18/10.27 (E(f3(f3(f3(f2(x1321),f2(x1322)),f2(x1321)),f2(x1322)),f2(f3(x1321,x1322)))),
% 10.18/10.27 inference(scs_inference,[],[121,87,114,24,2,10,3])).
% 10.18/10.27 cnf(134,plain,
% 10.18/10.27 (P1(f3(x1341,f3(x1342,x1343)),f3(f3(x1341,x1342),x1343))),
% 10.18/10.27 inference(scs_inference,[],[121,87,71,114,131,24,2,10,3,9])).
% 10.18/10.27 cnf(137,plain,
% 10.18/10.27 (E(f2(f3(x1371,x1372)),f3(f3(f3(f2(x1371),f2(x1372)),f2(x1371)),f2(x1372)))),
% 10.18/10.27 inference(scs_inference,[],[132,2])).
% 10.18/10.27 cnf(140,plain,
% 10.18/10.27 (E(f4(x1401,f3(f4(x1402,x1403),f4(x1402,x1403))),f4(f4(x1401,x1402),x1403))),
% 10.18/10.27 inference(scs_inference,[],[129,113,63,132,134,2,10,3])).
% 10.18/10.27 cnf(141,plain,
% 10.18/10.27 (E(f4(x1411,f4(x1412,x1413)),f4(f4(x1411,x1412),x1413))),
% 10.18/10.27 inference(rename_variables,[],[129])).
% 10.18/10.27 cnf(143,plain,
% 10.18/10.27 (P1(f4(f4(a6,a6),f2(x1431)),f2(f3(x1431,x1431)))),
% 10.18/10.27 inference(scs_inference,[],[129,141,113,63,132,134,127,2,10,3,9])).
% 10.18/10.27 cnf(145,plain,
% 10.18/10.27 (E(f4(f4(x1451,x1452),x1453),f4(x1451,f3(f4(x1452,x1453),f4(x1452,x1453))))),
% 10.18/10.28 inference(scs_inference,[],[140,2])).
% 10.18/10.28 cnf(147,plain,
% 10.18/10.28 (P1(f4(f4(a6,a6),f2(x1471)),f2(f3(x1471,x1471)))),
% 10.18/10.28 inference(rename_variables,[],[143])).
% 10.18/10.28 cnf(149,plain,
% 10.18/10.28 (E(f4(x1491,x1492),f4(f4(a6,x1491),x1492))),
% 10.18/10.28 inference(scs_inference,[],[137,129,48,140,143,2,10,3])).
% 10.18/10.28 cnf(152,plain,
% 10.18/10.28 (P1(f3(f4(f4(a6,a6),f2(x1521)),a1),f2(f3(x1521,x1521)))),
% 10.18/10.28 inference(scs_inference,[],[137,129,39,48,140,143,147,2,10,3,9])).
% 10.18/10.28 cnf(154,plain,
% 10.18/10.28 (E(f4(f4(a6,x1541),x1542),f4(x1541,x1542))),
% 10.18/10.28 inference(scs_inference,[],[149,2])).
% 10.18/10.28 cnf(158,plain,
% 10.18/10.28 (E(f3(f3(f3(x1581,f3(x1582,x1583)),x1581),f3(x1582,x1583)),f3(f3(x1581,x1582),x1583))),
% 10.18/10.28 inference(scs_inference,[],[113,121,96,149,64,2,10,3])).
% 10.18/10.28 cnf(164,plain,
% 10.18/10.28 (E(f3(f3(x1641,x1642),x1643),f3(f3(f3(x1641,f3(x1642,x1643)),x1641),f3(x1642,x1643)))),
% 10.18/10.28 inference(scs_inference,[],[158,2])).
% 10.18/10.28 cnf(165,plain,
% 10.18/10.28 (P1(f2(x1651),f3(a6,a6))),
% 10.18/10.28 inference(scs_inference,[],[30,158,46,2,10])).
% 10.18/10.28 cnf(167,plain,
% 10.18/10.28 (~E(f2(f4(a5,f2(a1))),f4(f4(a6,a6),f3(a1,a1)))),
% 10.18/10.28 inference(scs_inference,[],[154,30,158,75,46,2,10,3])).
% 10.18/10.28 cnf(171,plain,
% 10.18/10.28 (E(a1,f4(x1711,a1))),
% 10.18/10.28 inference(scs_inference,[],[12,2])).
% 10.18/10.28 cnf(172,plain,
% 10.18/10.28 (P1(f2(x1721),f3(f3(a6,a6),a1))),
% 10.18/10.28 inference(scs_inference,[],[39,165,12,2,10])).
% 10.18/10.28 cnf(176,plain,
% 10.18/10.28 (P1(f3(f4(a6,f2(x1761)),f4(a6,f2(x1762))),f3(a6,a6))),
% 10.18/10.28 inference(scs_inference,[],[104,154,39,165,167,12,2,10,3,9])).
% 10.18/10.28 cnf(178,plain,
% 10.18/10.28 (E(a1,f4(a1,x1781))),
% 10.18/10.28 inference(scs_inference,[],[13,2])).
% 10.18/10.28 cnf(179,plain,
% 10.18/10.28 (P1(f3(f4(a6,f2(x1791)),f4(a6,f2(x1792))),f4(a6,f3(a6,a6)))),
% 10.18/10.28 inference(scs_inference,[],[48,176,13,2,10])).
% 10.18/10.28 cnf(181,plain,
% 10.18/10.28 (E(a1,f4(x1811,f3(f4(x1812,a1),f4(x1812,a1))))),
% 10.18/10.28 inference(scs_inference,[],[171,145,48,176,13,2,10,3])).
% 10.18/10.28 cnf(186,plain,
% 10.18/10.28 (E(f4(x1861,f3(f4(x1862,a1),f4(x1862,a1))),a1)),
% 10.18/10.28 inference(scs_inference,[],[181,2])).
% 10.18/10.28 cnf(187,plain,
% 10.18/10.28 (P1(f2(x1871),f3(f3(f3(a6,f3(a6,a1)),a6),f3(a6,a1)))),
% 10.18/10.28 inference(scs_inference,[],[164,181,172,2,10])).
% 10.18/10.28 cnf(193,plain,
% 10.18/10.28 (E(a1,f2(a1))),
% 10.18/10.28 inference(scs_inference,[],[11,2])).
% 10.18/10.28 cnf(194,plain,
% 10.18/10.28 (P1(f3(f4(a6,f2(x1941)),f4(a6,f2(x1942))),f3(f4(a6,a6),f4(a6,a6)))),
% 10.18/10.28 inference(scs_inference,[],[55,179,11,2,10])).
% 10.18/10.28 cnf(196,plain,
% 10.18/10.28 (E(f4(f3(a6,a6),f2(x1961)),f2(f3(x1961,x1961)))),
% 10.18/10.28 inference(scs_inference,[],[79,55,99,179,11,2,10,3])).
% 10.18/10.28 cnf(201,plain,
% 10.18/10.28 (E(f2(f3(x2011,x2011)),f4(f3(a6,a6),f2(x2011)))),
% 10.18/10.28 inference(scs_inference,[],[196,2])).
% 10.18/10.28 cnf(202,plain,
% 10.18/10.28 (P1(f3(a1,a1),f4(a1,x2021))),
% 10.18/10.28 inference(scs_inference,[],[178,196,44,2,10])).
% 10.18/10.28 cnf(204,plain,
% 10.18/10.28 (E(f4(x2041,f3(f4(x2042,a1),f4(x2042,a1))),f2(a1))),
% 10.18/10.28 inference(scs_inference,[],[178,193,186,196,44,2,10,3])).
% 10.18/10.28 cnf(207,plain,
% 10.18/10.28 (E(f2(a1),f4(x2071,f3(f4(x2072,a1),f4(x2072,a1))))),
% 10.18/10.28 inference(scs_inference,[],[204,2])).
% 10.18/10.28 cnf(208,plain,
% 10.18/10.28 (P1(f3(a1,a1),f4(f4(a1,x2081),x2082))),
% 10.18/10.28 inference(scs_inference,[],[129,204,202,2,10])).
% 10.18/10.28 cnf(211,plain,
% 10.18/10.28 (E(f3(f2(x2111),f2(x2111)),f4(f3(a6,a6),f2(x2111)))),
% 10.18/10.28 inference(scs_inference,[],[201,129,87,204,202,2,10,3])).
% 10.18/10.28 cnf(212,plain,
% 10.18/10.28 (E(f2(f3(x2121,x2121)),f4(f3(a6,a6),f2(x2121)))),
% 10.18/10.28 inference(rename_variables,[],[201])).
% 10.18/10.28 cnf(214,plain,
% 10.18/10.28 (P1(f4(f3(a6,a6),f2(x2141)),f3(f3(f3(a6,f3(a6,a1)),a6),f3(a6,a1)))),
% 10.18/10.28 inference(scs_inference,[],[201,212,129,87,204,187,202,2,10,3,9])).
% 10.18/10.28 cnf(216,plain,
% 10.18/10.28 (E(f4(f3(a6,a6),f2(x2161)),f3(f2(x2161),f2(x2161)))),
% 10.18/10.28 inference(scs_inference,[],[211,2])).
% 10.18/10.28 cnf(219,plain,
% 10.18/10.28 (E(f3(f3(f3(f2(x2191),f2(x2191)),f2(x2191)),f2(x2191)),f4(f3(a6,a6),f2(x2191)))),
% 10.18/10.28 inference(scs_inference,[],[201,121,211,152,2,10,3])).
% 10.18/10.28 cnf(221,plain,
% 10.18/10.28 (P1(f3(f3(a1,a1),f3(a1,a1)),f4(f4(a1,x2211),x2212))),
% 10.18/10.28 inference(scs_inference,[],[201,121,30,211,208,152,2,10,3,9])).
% 10.18/10.28 cnf(224,plain,
% 10.18/10.28 (P1(f3(f3(a1,a1),f3(a1,a1)),f4(a1,f3(f4(x2241,x2242),f4(x2241,x2242))))),
% 10.18/10.28 inference(scs_inference,[],[145,219,221,2,10])).
% 10.18/10.28 cnf(227,plain,
% 10.18/10.28 (E(f4(f3(a6,a6),f3(x2271,x2272)),f3(f3(f3(x2271,x2272),x2271),x2272))),
% 10.18/10.28 inference(scs_inference,[],[79,145,219,107,221,2,10,3])).
% 10.18/10.28 cnf(230,plain,
% 10.18/10.28 (P1(f3(f2(x2301),f2(x2301)),f3(f3(f3(a6,f3(a6,a1)),a6),f3(a6,a1)))),
% 10.18/10.28 inference(scs_inference,[],[216,79,145,219,107,214,221,2,10,3,9])).
% 10.18/10.28 cnf(232,plain,
% 10.18/10.28 (E(f3(f3(f3(x2321,x2322),x2321),x2322),f4(f3(a6,a6),f3(x2321,x2322)))),
% 10.18/10.28 inference(scs_inference,[],[227,2])).
% 10.18/10.28 cnf(236,plain,
% 10.18/10.28 (E(f2(a1),f3(f3(f3(f4(x2361,a1),f4(x2361,a1)),f4(x2361,a1)),f4(x2361,a1)))),
% 10.18/10.28 inference(scs_inference,[],[207,186,227,224,2,10,3])).
% 10.18/10.28 cnf(239,plain,
% 10.18/10.28 (P1(f3(f2(x2391),f2(x2392)),f3(f4(a6,a6),f4(a6,a6)))),
% 10.18/10.28 inference(scs_inference,[],[207,186,71,227,194,224,2,10,3,9])).
% 10.18/10.28 cnf(244,plain,
% 10.18/10.28 (E(a1,f3(f3(f3(f4(x2441,a1),f4(x2441,a1)),f4(x2441,a1)),f4(x2441,a1)))),
% 10.18/10.28 inference(scs_inference,[],[232,193,236,230,2,10,3])).
% 10.18/10.28 cnf(245,plain,
% 10.18/10.28 (P1(f2(f3(x2451,x2452)),f3(f4(a6,a6),f4(a6,a6)))),
% 10.18/10.28 inference(scs_inference,[],[232,193,87,236,230,239,2,10,3,9])).
% 10.18/10.28 cnf(250,plain,
% 10.18/10.28 (~E(f2(f4(a5,f2(a1))),f2(a1))),
% 10.18/10.28 inference(scs_inference,[],[27,39,244,245,11,2,10,3])).
% 10.18/10.28 cnf(255,plain,
% 10.18/10.28 (E(f2(f4(x2551,x2552)),f2(f4(x2551,f2(x2552))))),
% 10.18/10.28 inference(scs_inference,[],[21,2])).
% 10.18/10.28 cnf(1468,plain,
% 10.18/10.28 (E(f2(a1),f2(f4(x14681,a1)))),
% 10.18/10.28 inference(scs_inference,[],[12,2,4])).
% 10.18/10.28 cnf(1470,plain,
% 10.18/10.28 (E(f2(a1),f2(f4(x14701,f2(a1))))),
% 10.18/10.28 inference(scs_inference,[],[255,1468,2,3])).
% 10.18/10.28 cnf(1475,plain,
% 10.18/10.28 ($false),
% 10.18/10.28 inference(scs_inference,[],[1470,250,2]),
% 10.18/10.28 ['proof']).
% 10.18/10.28 % SZS output end Proof
% 10.18/10.28 % Total time :9.660000s
%------------------------------------------------------------------------------