%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : COL075-2 : TPTP v8.2.0. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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 04:45:03 EDT 2024
% Result : Unsatisfiable 281.53s 282.00s
% Output : CNFRefutation 281.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : COL075-2 : TPTP v8.2.0. Released v1.2.0.
% 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n027.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Tue Jun 18 16:11:54 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.57/0.62 start to proof:theBenchmark
% 281.44/281.97 %-------------------------------------------
% 281.44/281.97 % File :CSE---1.7
% 281.44/281.97 % Problem :theBenchmark
% 281.44/281.97 % Transform :cnf
% 281.44/281.97 % Format :tptp:raw
% 281.44/281.97 % Command :java -jar mcs_scs.jar %d %s
% 281.44/281.97
% 281.44/281.97 % Result :Theorem 280.780000s
% 281.44/281.97 % Output :CNFRefutation 280.780000s
% 281.44/281.97 %-------------------------------------------
% 281.53/282.00 %--------------------------------------------------------------------------
% 281.53/282.00 % File : COL075-2 : TPTP v8.2.0. Released v1.2.0.
% 281.53/282.00 % Domain : Combinatory Logic
% 281.53/282.00 % Problem : Lemma 1 for showing the unsatisfiable variant of TRC
% 281.53/282.00 % Version : [Jec95] (equality) axioms : Reduced > Incomplete.
% 281.53/282.00 % English : Searching for a diagonal combinator F with the property
% 281.53/282.00 % f X Y = X X.
% 281.53/282.00
% 281.53/282.00 % Refs : [Jec95] Jech (1995), Otter Experiments in a System of Combinat
% 281.53/282.00 % Source : [Jec95]
% 281.53/282.00 % Names : - [Jec95]
% 281.53/282.00
% 281.53/282.00 % Status : Unsatisfiable
% 281.53/282.00 % Rating : 0.14 v8.2.0, 0.21 v8.1.0, 0.25 v7.5.0, 0.21 v7.4.0, 0.26 v7.3.0, 0.21 v7.1.0, 0.11 v6.4.0, 0.16 v6.3.0, 0.18 v6.2.0, 0.14 v6.1.0, 0.00 v6.0.0, 0.14 v5.5.0, 0.05 v5.4.0, 0.00 v5.1.0, 0.13 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.12 v3.3.0, 0.00 v2.0.0
% 281.53/282.00 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR)
% 281.53/282.00 % Number of literals : 3 ( 3 equ; 1 neg)
% 281.53/282.00 % Maximal clause size : 1 ( 1 avg)
% 281.53/282.00 % Maximal term depth : 4 ( 2 avg)
% 281.53/282.00 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 281.53/282.00 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 281.53/282.00 % Number of variables : 6 ( 1 sgn)
% 281.53/282.00 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 281.53/282.00
% 281.53/282.00 % Comments :
% 281.53/282.00 %--------------------------------------------------------------------------
% 281.53/282.00 %----Don't include axioms of Type-respecting combinators
% 281.53/282.00 %include('Axioms/COL001-0.ax').
% 281.53/282.00 %--------------------------------------------------------------------------
% 281.53/282.00 %----Replace k function by k combinator
% 281.53/282.00 %input_clause(k_definition,axiom,
% 281.53/282.00 % [++equal(apply(k(X),Y),X)]).
% 281.53/282.00 cnf(k_definition,axiom,
% 281.53/282.00 apply(apply(k,X),Y) = X ).
% 281.53/282.00
% 281.53/282.00 %----Replace k function by k combinator
% 281.53/282.00 %input_clause(abstraction,axiom,
% 281.53/282.00 % [++equal(apply(apply(apply(abstraction,X),Y),Z),apply(apply(X,k(Z)),
% 281.53/282.00 %apply(Y,Z)))]).
% 281.53/282.00 cnf(abstraction,axiom,
% 281.53/282.00 apply(apply(apply(abstraction,X),Y),Z) = apply(apply(X,apply(k,Z)),apply(Y,Z)) ).
% 281.53/282.00
% 281.53/282.00 %----Subsitution axioms
% 281.53/282.00 cnf(prove_diagonal_combinator,negated_conjecture,
% 281.53/282.00 apply(apply(Y,b(Y)),c(Y)) != apply(b(Y),b(Y)) ).
% 281.53/282.00
% 281.53/282.00 %--------------------------------------------------------------------------
% 281.53/282.00 %-------------------------------------------
% 281.53/282.00 % Proof found
% 281.53/282.00 % SZS status Theorem for theBenchmark
% 281.53/282.00 % SZS output start Proof
% 281.56/282.02 %ClaNum:10(EqnAxiom:7)
% 281.56/282.02 %VarNum:15(SingletonVarNum:6)
% 281.56/282.02 %MaxLitNum:1
% 281.56/282.02 %MaxfuncDepth:3
% 281.56/282.02 %SharedTerms:2
% 281.56/282.02 %goalClause: 10
% 281.56/282.02 %singleGoalClaCount:1
% 281.56/282.02 [10]~E(f2(f2(x101,f4(x101)),f5(x101)),f2(f4(x101),f4(x101)))
% 281.56/282.02 [8]E(f2(f2(a1,x81),x82),x81)
% 281.56/282.02 [9]E(f2(f2(x91,f2(a1,x92)),f2(x93,x92)),f2(f2(f2(a3,x91),x93),x92))
% 281.56/282.02 %EqnAxiom
% 281.56/282.02 [1]E(x11,x11)
% 281.56/282.02 [2]E(x22,x21)+~E(x21,x22)
% 281.56/282.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 281.56/282.03 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 281.56/282.03 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 281.56/282.03 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 281.56/282.03 [7]~E(x71,x72)+E(f5(x71),f5(x72))
% 281.56/282.03
% 281.56/282.03 %-------------------------------------------
% 281.56/282.05 cnf(11,plain,
% 281.56/282.05 (E(x111,f2(f2(a1,x111),x112))),
% 281.56/282.05 inference(scs_inference,[],[8,2])).
% 281.56/282.05 cnf(12,plain,
% 281.56/282.05 (E(f2(f2(f2(a3,x121),x122),x123),f2(f2(x121,f2(a1,x123)),f2(x122,x123)))),
% 281.56/282.05 inference(scs_inference,[],[9,2])).
% 281.56/282.05 cnf(13,plain,
% 281.56/282.05 (E(f2(a1,x131),f2(f2(f2(a3,a1),x132),x131))),
% 281.56/282.05 inference(scs_inference,[],[11,9,2,3])).
% 281.56/282.05 cnf(16,plain,
% 281.56/282.05 (E(f2(f2(f2(a3,a1),x161),x162),f2(a1,x162))),
% 281.56/282.05 inference(scs_inference,[],[13,2])).
% 281.56/282.05 cnf(17,plain,
% 281.56/282.05 (E(f2(f2(a1,f2(a1,x171)),x172),f2(f2(f2(a3,a1),x173),x171))),
% 281.56/282.05 inference(scs_inference,[],[13,8,2,3])).
% 281.56/282.05 cnf(25,plain,
% 281.56/282.05 (E(f2(f2(a1,x251),x252),f2(f2(a1,x251),x253))),
% 281.56/282.05 inference(scs_inference,[],[8,11,3])).
% 281.56/282.05 cnf(27,plain,
% 281.56/282.05 (E(f2(f2(f2(a3,f2(a3,a1)),x271),x272),f2(a1,f2(x271,x272)))),
% 281.56/282.05 inference(scs_inference,[],[16,12,3])).
% 281.56/282.05 cnf(30,plain,
% 281.56/282.05 (E(f2(a1,f2(x301,x302)),f2(f2(f2(a3,f2(a3,a1)),x301),x302))),
% 281.56/282.05 inference(scs_inference,[],[16,12,3,2])).
% 281.56/282.05 cnf(31,plain,
% 281.56/282.05 (E(f2(f2(f2(a3,a1),x311),f2(x312,x313)),f2(f2(f2(a3,f2(a3,a1)),x312),x313))),
% 281.56/282.05 inference(scs_inference,[],[30,16,3])).
% 281.56/282.05 cnf(33,plain,
% 281.56/282.05 (E(f2(f2(f2(a3,f2(a3,a1)),x331),x332),f2(f2(f2(a3,a1),x333),f2(x331,x332)))),
% 281.56/282.05 inference(scs_inference,[],[31,2])).
% 281.56/282.05 cnf(36,plain,
% 281.56/282.05 (~E(f2(x361,f4(x361)),f2(a1,f2(f4(x361),f4(x361))))),
% 281.56/282.05 inference(scs_inference,[],[10,31,8,2,3,4])).
% 281.56/282.05 cnf(37,plain,
% 281.56/282.05 (~E(f4(a1),f2(f4(a1),f4(a1)))),
% 281.56/282.05 inference(scs_inference,[],[10,31,8,2,3,4,5])).
% 281.56/282.05 cnf(38,plain,
% 281.56/282.05 (~E(f2(x381,f4(x381)),f2(f2(f2(a3,a1),x382),f2(f4(x381),f4(x381))))),
% 281.56/282.05 inference(scs_inference,[],[16,36,3])).
% 281.56/282.05 cnf(40,plain,
% 281.56/282.05 (~E(f2(x401,f4(x401)),f2(f2(f2(a3,f2(a3,a1)),f4(x401)),f4(x401)))),
% 281.56/282.05 inference(scs_inference,[],[33,38,3])).
% 281.56/282.05 cnf(42,plain,
% 281.56/282.05 (~E(x421,f2(f2(a3,f2(a3,a1)),f4(x421)))),
% 281.56/282.05 inference(scs_inference,[],[33,38,3,4])).
% 281.56/282.05 cnf(43,plain,
% 281.56/282.05 (~E(x431,f4(f2(f2(a3,f2(a3,a1)),x431)))),
% 281.56/282.05 inference(scs_inference,[],[33,38,3,4,5])).
% 281.56/282.05 cnf(44,plain,
% 281.56/282.05 (~E(f4(a1),f2(f2(a1,f2(f4(a1),f4(a1))),x441))),
% 281.56/282.05 inference(scs_inference,[],[37,8,3])).
% 281.56/282.05 cnf(46,plain,
% 281.56/282.05 (~E(x461,f2(f2(a1,f2(f2(a3,f2(a3,a1)),f4(x461))),x462))),
% 281.56/282.05 inference(scs_inference,[],[42,8,3])).
% 281.56/282.05 cnf(48,plain,
% 281.56/282.05 (~E(x481,f2(a1,f2(f2(a3,f2(a3,a1)),f4(f2(x481,x482)))))),
% 281.56/282.05 inference(scs_inference,[],[42,8,3,4])).
% 281.56/282.05 cnf(49,plain,
% 281.56/282.05 (~E(x491,f2(f2(a3,f2(a3,a1)),f4(f2(f2(a1,x491),x492))))),
% 281.56/282.05 inference(scs_inference,[],[42,8,3,4,5])).
% 281.56/282.05 cnf(50,plain,
% 281.56/282.05 (~E(x501,f2(f2(f2(a3,a1),x502),f2(f2(a3,f2(a3,a1)),f4(f2(x501,x503)))))),
% 281.56/282.05 inference(scs_inference,[],[16,48,3])).
% 281.56/282.05 cnf(52,plain,
% 281.56/282.05 (~E(x521,f2(f2(f2(a3,f2(a3,a1)),f2(a3,f2(a3,a1))),f4(f2(x521,x522))))),
% 281.56/282.05 inference(scs_inference,[],[33,50,3])).
% 281.56/282.05 cnf(54,plain,
% 281.56/282.05 (E(f5(f2(f2(a1,x541),x542)),f5(x541))),
% 281.56/282.05 inference(scs_inference,[],[8,7])).
% 281.56/282.05 cnf(55,plain,
% 281.56/282.05 (E(f4(f2(f2(a1,x551),x552)),f4(x551))),
% 281.56/282.05 inference(scs_inference,[],[8,7,6])).
% 281.56/282.05 cnf(56,plain,
% 281.56/282.05 (E(f2(x561,f2(f2(a1,x562),x563)),f2(x561,x562))),
% 281.56/282.06 inference(scs_inference,[],[8,7,6,5])).
% 281.56/282.06 cnf(57,plain,
% 281.56/282.06 (E(f2(f2(f2(a1,x571),x572),x573),f2(x571,x573))),
% 281.56/282.06 inference(scs_inference,[],[8,7,6,5,4])).
% 281.56/282.06 cnf(58,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,f2(a3,a1)),f4(x581)),f4(x581)),f2(x581,f4(x581)))),
% 281.56/282.06 inference(scs_inference,[],[8,40,7,6,5,4,2])).
% 281.56/282.06 cnf(59,plain,
% 281.56/282.06 (~E(x591,f2(f2(f2(a3,f2(a3,a1)),f4(f2(a1,x591))),f4(f2(a1,x591))))),
% 281.56/282.06 inference(scs_inference,[],[8,40,7,6,5,4,2,3])).
% 281.56/282.06 cnf(66,plain,
% 281.56/282.06 (~E(f4(f2(f2(a3,f2(a3,a1)),x661)),x661)),
% 281.56/282.06 inference(scs_inference,[],[25,43,6,7,5,4,2])).
% 281.56/282.06 cnf(67,plain,
% 281.56/282.06 (~E(x671,f4(f2(f2(a3,f2(a3,a1)),f2(f2(a1,x671),x672))))),
% 281.56/282.06 inference(scs_inference,[],[8,25,43,6,7,5,4,2,3])).
% 281.56/282.06 cnf(70,plain,
% 281.56/282.06 (E(f4(f2(x701,f2(f2(a1,x702),x703))),f4(f2(x701,x702)))),
% 281.56/282.06 inference(scs_inference,[],[56,7,6])).
% 281.56/282.06 cnf(73,plain,
% 281.56/282.06 (~E(f2(f2(a1,f2(f4(a1),f4(a1))),x731),f4(a1))),
% 281.56/282.06 inference(scs_inference,[],[56,44,7,6,5,4,2])).
% 281.56/282.06 cnf(74,plain,
% 281.56/282.06 (~E(f2(a1,f2(f4(x741),f4(x741))),f2(x741,f4(x741)))),
% 281.56/282.06 inference(scs_inference,[],[56,58,44,27,7,6,5,4,2,3])).
% 281.56/282.06 cnf(78,plain,
% 281.56/282.06 (E(f2(x781,f2(f2(f2(a1,x782),x783),x784)),f2(x781,f2(x782,x784)))),
% 281.56/282.06 inference(scs_inference,[],[57,6,7,5])).
% 281.56/282.06 cnf(79,plain,
% 281.56/282.06 (E(f2(f2(f2(f2(a1,x791),x792),x793),x794),f2(f2(x791,x793),x794))),
% 281.56/282.06 inference(scs_inference,[],[57,6,7,5,4])).
% 281.56/282.06 cnf(81,plain,
% 281.56/282.06 (~E(f2(f4(a1),f4(a1)),f4(a1))),
% 281.56/282.06 inference(scs_inference,[],[8,57,73,52,6,7,5,4,2,3])).
% 281.56/282.06 cnf(87,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,f2(a3,a1)),f4(f2(a1,x871))),f4(f2(a1,x871))),x871)),
% 281.56/282.06 inference(scs_inference,[],[54,59,7,6,5,4,2])).
% 281.56/282.06 cnf(88,plain,
% 281.56/282.06 (~E(f4(f2(f2(a3,f2(a3,a1)),x881)),f2(f2(a1,x881),x882))),
% 281.56/282.06 inference(scs_inference,[],[54,66,70,59,7,6,5,4,2,3])).
% 281.56/282.06 cnf(93,plain,
% 281.56/282.06 (E(f2(x931,f4(f2(f2(a1,x932),x933))),f2(x931,f4(x932)))),
% 281.56/282.06 inference(scs_inference,[],[55,6,7,5])).
% 281.56/282.06 cnf(94,plain,
% 281.56/282.06 (E(f2(f4(f2(f2(a1,x941),x942)),x943),f2(f4(x941),x943))),
% 281.56/282.06 inference(scs_inference,[],[55,6,7,5,4])).
% 281.56/282.06 cnf(95,plain,
% 281.56/282.06 (~E(f2(f2(a1,x951),x952),f4(f2(f2(a3,f2(a3,a1)),x951)))),
% 281.56/282.06 inference(scs_inference,[],[55,88,6,7,5,4,2])).
% 281.56/282.06 cnf(98,plain,
% 281.56/282.06 (E(f5(x981),f5(f2(f2(a1,x981),x982)))),
% 281.56/282.06 inference(scs_inference,[],[11,7])).
% 281.56/282.06 cnf(99,plain,
% 281.56/282.06 (E(f4(x991),f4(f2(f2(a1,x991),x992)))),
% 281.56/282.06 inference(scs_inference,[],[11,7,6])).
% 281.56/282.06 cnf(100,plain,
% 281.56/282.06 (E(f2(x1001,x1002),f2(x1001,f2(f2(a1,x1002),x1003)))),
% 281.56/282.06 inference(scs_inference,[],[11,7,6,5])).
% 281.56/282.06 cnf(101,plain,
% 281.56/282.06 (E(f2(x1011,x1012),f2(f2(f2(a1,x1011),x1013),x1012))),
% 281.56/282.06 inference(scs_inference,[],[11,7,6,5,4])).
% 281.56/282.06 cnf(102,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(a3,a1)),f4(f2(f2(a1,x1021),x1022))),x1021)),
% 281.56/282.06 inference(scs_inference,[],[49,11,7,6,5,4,2])).
% 281.56/282.06 cnf(103,plain,
% 281.56/282.06 (~E(f2(f2(a1,f4(a1)),x1031),f2(f4(a1),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[49,37,11,7,6,5,4,2,3])).
% 281.56/282.06 cnf(108,plain,
% 281.56/282.06 (E(f2(f2(x1081,x1082),x1083),f2(f2(x1081,f2(f2(a1,x1082),x1084)),x1083))),
% 281.56/282.06 inference(scs_inference,[],[100,6,7,5,4])).
% 281.56/282.06 cnf(109,plain,
% 281.56/282.06 (~E(f2(f4(a1),f4(a1)),f2(f2(a1,f4(a1)),x1091))),
% 281.56/282.06 inference(scs_inference,[],[100,103,6,7,5,4,2])).
% 281.56/282.06 cnf(110,plain,
% 281.56/282.06 (~E(f2(f4(a1),f2(f2(a1,f4(a1)),x1101)),f4(a1))),
% 281.56/282.06 inference(scs_inference,[],[81,100,103,6,7,5,4,2,3])).
% 281.56/282.06 cnf(114,plain,
% 281.56/282.06 (E(f2(x1141,f2(x1142,x1143)),f2(x1141,f2(f2(f2(a1,x1142),x1144),x1143)))),
% 281.56/282.06 inference(scs_inference,[],[101,7,6,5])).
% 281.56/282.06 cnf(115,plain,
% 281.56/282.06 (E(f2(f2(x1151,x1152),x1153),f2(f2(f2(f2(a1,x1151),x1154),x1152),x1153))),
% 281.56/282.06 inference(scs_inference,[],[101,7,6,5,4])).
% 281.56/282.06 cnf(117,plain,
% 281.56/282.06 (~E(f2(f2(f2(a1,a1),x1171),f2(f4(x1172),f4(x1172))),f2(x1172,f4(x1172)))),
% 281.56/282.06 inference(scs_inference,[],[101,74,110,7,6,5,4,2,3])).
% 281.56/282.06 cnf(123,plain,
% 281.56/282.06 (~E(f2(x1231,f4(x1231)),f2(f2(f2(a1,a1),x1232),f2(f4(x1231),f4(x1231))))),
% 281.56/282.06 inference(scs_inference,[],[98,117,6,7,5,4,2])).
% 281.56/282.06 cnf(124,plain,
% 281.56/282.06 (~E(f2(f2(f2(a1,a1),x1241),f2(f2(f2(a1,f4(x1242)),x1243),f4(x1242))),f2(x1242,f4(x1242)))),
% 281.56/282.06 inference(scs_inference,[],[98,117,114,6,7,5,4,2,3])).
% 281.56/282.06 cnf(129,plain,
% 281.56/282.06 (E(f2(x1291,f4(x1292)),f2(x1291,f4(f2(f2(a1,x1292),x1293))))),
% 281.56/282.06 inference(scs_inference,[],[99,67,2,7,6,5])).
% 281.56/282.06 cnf(130,plain,
% 281.56/282.06 (E(f2(f4(x1301),x1302),f2(f4(f2(f2(a1,x1301),x1303)),x1302))),
% 281.56/282.06 inference(scs_inference,[],[99,67,2,7,6,5,4])).
% 281.56/282.06 cnf(131,plain,
% 281.56/282.06 (~E(x1311,f2(f2(f2(a1,a1),x1312),f2(f4(f2(a1,x1311)),f4(f2(a1,x1311)))))),
% 281.56/282.06 inference(scs_inference,[],[8,99,123,67,2,7,6,5,4,3])).
% 281.56/282.06 cnf(134,plain,
% 281.56/282.06 (~E(f2(f2(a1,f2(f2(a3,f2(a3,a1)),f4(x1341))),x1342),x1341)),
% 281.56/282.06 inference(scs_inference,[],[46,2])).
% 281.56/282.06 cnf(138,plain,
% 281.56/282.06 (E(f2(f2(a1,x1381),x1382),f2(f2(f2(f2(a3,a1),x1383),x1381),x1382))),
% 281.56/282.06 inference(scs_inference,[],[46,13,2,7,6,5,4])).
% 281.56/282.06 cnf(139,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(a3,a1)),f4(x1391)),x1391)),
% 281.56/282.06 inference(scs_inference,[],[93,102,46,13,2,7,6,5,4,3])).
% 281.56/282.06 cnf(146,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(f2(a1,f2(a3,a1)),x1461)),f4(x1462)),x1462)),
% 281.56/282.06 inference(scs_inference,[],[139,108,124,16,2,7,6,5,4,3])).
% 281.56/282.06 cnf(148,plain,
% 281.56/282.06 (~E(x1481,f2(f2(a3,f2(f2(a1,f2(a3,a1)),x1482)),f4(x1481)))),
% 281.56/282.06 inference(scs_inference,[],[146,2])).
% 281.56/282.06 cnf(149,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x1491),x1492),f4(f2(f2(a3,f2(a3,a1)),f2(a1,x1492))))),
% 281.56/282.06 inference(scs_inference,[],[9,146,95,2,3])).
% 281.56/282.06 cnf(153,plain,
% 281.56/282.06 (~E(f2(f4(a1),f4(f2(f2(a1,a1),x1531))),f4(a1))),
% 281.56/282.06 inference(scs_inference,[],[149,129,81,2,3])).
% 281.56/282.06 cnf(156,plain,
% 281.56/282.06 (~E(f2(f4(f2(f2(a1,a1),x1561)),f4(a1)),f2(f2(a1,f4(a1)),x1562))),
% 281.56/282.06 inference(scs_inference,[],[109,153,130,2,3])).
% 281.56/282.06 cnf(158,plain,
% 281.56/282.06 (~E(f2(f2(a1,f4(a1)),x1581),f2(f4(f2(f2(a1,a1),x1582)),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[156,2])).
% 281.56/282.06 cnf(159,plain,
% 281.56/282.06 (~E(f2(f2(f2(f2(a1,a3),x1591),f2(a3,a1)),f4(x1592)),x1592)),
% 281.56/282.06 inference(scs_inference,[],[156,115,139,2,3])).
% 281.56/282.06 cnf(161,plain,
% 281.56/282.06 (~E(x1611,f2(f2(f2(f2(a1,a3),x1612),f2(a3,a1)),f4(x1611)))),
% 281.56/282.06 inference(scs_inference,[],[159,2])).
% 281.56/282.06 cnf(162,plain,
% 281.56/282.06 (~E(f2(f2(f2(f2(a1,a3),x1621),f2(a3,a1)),f4(x1622)),f2(f2(a1,x1622),x1623))),
% 281.56/282.06 inference(scs_inference,[],[159,93,2,3])).
% 281.56/282.06 cnf(165,plain,
% 281.56/282.06 (~E(f2(f2(a1,x1651),x1652),f2(f2(f2(f2(a1,a3),x1653),f2(a3,a1)),f4(x1651)))),
% 281.56/282.06 inference(scs_inference,[],[162,2])).
% 281.56/282.06 cnf(166,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(a3,a1)),f4(x1661)),f2(f2(a1,x1661),x1662))),
% 281.56/282.06 inference(scs_inference,[],[162,79,2,3])).
% 281.56/282.06 cnf(169,plain,
% 281.56/282.06 (~E(f2(f2(a1,x1691),x1692),f2(f2(a3,f2(a3,a1)),f4(x1691)))),
% 281.56/282.06 inference(scs_inference,[],[166,2])).
% 281.56/282.06 cnf(170,plain,
% 281.56/282.06 (~E(f5(f2(f2(a1,x1701),x1702)),f2(f2(f2(f2(a1,a3),x1703),f2(a3,a1)),f4(f5(x1701))))),
% 281.56/282.06 inference(scs_inference,[],[161,166,98,2,3])).
% 281.56/282.06 cnf(172,plain,
% 281.56/282.06 (~E(f2(f2(f2(f2(a1,a3),x1721),f2(a3,a1)),f4(f5(x1722))),f5(f2(f2(a1,x1722),x1723)))),
% 281.56/282.06 inference(scs_inference,[],[170,2])).
% 281.56/282.06 cnf(173,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x1731),x1732),f2(f2(a3,f2(a3,a1)),f4(f2(a1,x1732))))),
% 281.56/282.06 inference(scs_inference,[],[9,169,170,2,3])).
% 281.56/282.06 cnf(177,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x1771),x1772),f2(f2(f2(f2(a1,a3),x1773),f2(a3,a1)),f4(f2(a1,x1772))))),
% 281.56/282.06 inference(scs_inference,[],[9,165,173,2,3])).
% 281.56/282.06 cnf(181,plain,
% 281.56/282.06 (~E(f2(f2(a1,x1811),x1812),f2(f2(a3,f2(f2(a1,f2(a3,a1)),x1813)),f4(x1811)))),
% 281.56/282.06 inference(scs_inference,[],[11,148,177,2,3])).
% 281.56/282.06 cnf(184,plain,
% 281.56/282.06 (~E(f2(f2(f2(f2(a3,a1),x1841),f4(a1)),x1842),f2(f4(f2(f2(a1,a1),x1843)),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[158,138,181,2,3])).
% 281.56/282.06 cnf(186,plain,
% 281.56/282.06 (~E(f2(f4(f2(f2(a1,a1),x1861)),f4(a1)),f2(f2(f2(f2(a3,a1),x1862),f4(a1)),x1863))),
% 281.56/282.06 inference(scs_inference,[],[184,2])).
% 281.56/282.06 cnf(187,plain,
% 281.56/282.06 (~E(f2(f2(a1,f2(f2(a3,f2(a3,a1)),f4(x1871))),x1872),f2(f2(a1,x1871),x1873))),
% 281.56/282.06 inference(scs_inference,[],[11,184,166,2,3])).
% 281.56/282.06 cnf(190,plain,
% 281.56/282.06 (~E(f2(f2(f2(f2(a3,a1),x1901),f2(f2(a3,f2(a3,a1)),f4(x1902))),x1903),x1902)),
% 281.56/282.06 inference(scs_inference,[],[134,187,138,2,3])).
% 281.56/282.06 cnf(193,plain,
% 281.56/282.06 (~E(f2(f2(a1,f2(f2(a1,x1931),x1932)),x1933),f2(f2(a3,f2(a3,a1)),f4(x1931)))),
% 281.56/282.06 inference(scs_inference,[],[11,190,169,2,3])).
% 281.56/282.06 cnf(196,plain,
% 281.56/282.06 (~E(f2(a1,f2(f4(f2(a1,x1961)),f4(f2(a1,x1961)))),x1961)),
% 281.56/282.06 inference(scs_inference,[],[87,193,27,2,3])).
% 281.56/282.06 cnf(198,plain,
% 281.56/282.06 (~E(x1981,f2(a1,f2(f4(f2(a1,x1981)),f4(f2(a1,x1981)))))),
% 281.56/282.06 inference(scs_inference,[],[196,2])).
% 281.56/282.06 cnf(205,plain,
% 281.56/282.06 (~E(f2(f2(a1,x2051),x2052),f2(a1,f2(f4(f2(a1,x2051)),f4(f2(a1,x2051)))))),
% 281.56/282.06 inference(scs_inference,[],[11,198,131,2,3])).
% 281.56/282.06 cnf(211,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x2111),f2(f4(x2112),f4(x2112))),f2(x2112,f4(x2112)))),
% 281.56/282.06 inference(scs_inference,[],[38,2])).
% 281.56/282.06 cnf(212,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(a3,a1)),f4(f5(x2121))),f5(f2(f2(a1,x2121),x2122)))),
% 281.56/282.06 inference(scs_inference,[],[172,38,79,2,3])).
% 281.56/282.06 cnf(216,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x2161),f2(f2(f2(a1,f4(x2162)),x2163),f4(x2162))),f2(x2162,f4(x2162)))),
% 281.56/282.06 inference(scs_inference,[],[211,212,114,2,3])).
% 281.56/282.06 cnf(219,plain,
% 281.56/282.06 (~E(f2(f4(a1),f4(a1)),f2(f2(f2(f2(a3,a1),x2191),f4(a1)),x2192))),
% 281.56/282.06 inference(scs_inference,[],[94,216,186,2,3])).
% 281.56/282.06 cnf(249,plain,
% 281.56/282.06 (~E(f2(a1,f2(f4(a1),f4(a1))),f2(f2(f2(a3,a1),x2491),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[13,36,3,2])).
% 281.56/282.06 cnf(250,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x2501),f2(f4(a1),f4(a1))),f2(f2(f2(a3,a1),x2502),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[13,249,3])).
% 281.56/282.06 cnf(256,plain,
% 281.56/282.06 (~E(f2(f2(f2(a1,a1),x2561),f2(f4(a1),f4(a1))),f2(f2(f2(a3,a1),x2562),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[13,123,3,2])).
% 281.56/282.06 cnf(257,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,f2(a3,a1)),f4(a1)),f4(a1)),f2(f2(f2(a3,a1),x2571),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[250,31,3])).
% 281.56/282.06 cnf(260,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x2601),f2(f4(f2(a1,x2602)),f4(f2(a1,x2602)))),x2602)),
% 281.56/282.06 inference(scs_inference,[],[13,196,3])).
% 281.56/282.06 cnf(263,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,f2(a1,a1)),f4(a1)),f4(a1)),f2(f2(f2(a3,a1),x2631),f4(a1)))),
% 281.56/282.06 inference(scs_inference,[],[256,260,9,2,3])).
% 281.56/282.06 cnf(297,plain,
% 281.56/282.06 (~E(f2(x2971,f2(f2(a1,x2972),x2973)),f2(f2(a3,f2(a3,a1)),f4(f2(x2971,x2972))))),
% 281.56/282.06 inference(scs_inference,[],[42,100,3])).
% 281.56/282.06 cnf(310,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,f2(a3,a1)),f2(a1,x3101)),x3102),f2(f2(a3,f2(a3,a1)),f4(f2(a1,x3101))))),
% 281.56/282.06 inference(scs_inference,[],[297,30,3])).
% 281.56/282.06 cnf(524,plain,
% 281.56/282.06 (E(f2(x5241,f2(x5242,f2(f2(f2(a1,x5243),x5244),x5245))),f2(x5241,f2(x5242,f2(x5243,x5245))))),
% 281.56/282.06 inference(scs_inference,[],[78,7,6,5])).
% 281.56/282.06 cnf(525,plain,
% 281.56/282.06 (E(f2(f2(x5251,f2(f2(f2(a1,x5252),x5253),x5254)),x5255),f2(f2(x5251,f2(x5252,x5254)),x5255))),
% 281.56/282.06 inference(scs_inference,[],[78,7,6,5,4])).
% 281.56/282.06 cnf(560,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(x5601,x5602)),x5603),f2(f2(f2(a1,x5601),x5604),x5602))),
% 281.56/282.06 inference(scs_inference,[],[8,101,123,162,524,2,4,5,3])).
% 281.56/282.06 cnf(567,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(x5671,x5672)),x5673),f2(x5671,f2(f2(a1,x5672),x5674)))),
% 281.56/282.06 inference(scs_inference,[],[8,100,161,103,525,4,5,2,3])).
% 281.56/282.06 cnf(646,plain,
% 281.56/282.06 (E(f2(f2(f2(a1,x6461),x6462),x6463),f2(f2(a1,f2(x6461,x6463)),x6464))),
% 281.56/282.06 inference(scs_inference,[],[560,2])).
% 281.56/282.06 cnf(647,plain,
% 281.56/282.06 (~E(f2(f2(a3,f2(a3,a1)),f4(a1)),f2(f2(a3,a1),x6471))),
% 281.56/282.06 inference(scs_inference,[],[257,560,2,4])).
% 281.56/282.06 cnf(648,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(f2(f2(a3,x6481),x6482),x6483)),x6484),f2(f2(x6481,f2(a1,x6483)),f2(x6482,x6483)))),
% 281.56/282.06 inference(scs_inference,[],[8,12,257,560,2,4,3])).
% 281.56/282.06 cnf(652,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(f2(a1,f2(a1,x6521)),x6522)),x6523),f2(f2(f2(a3,a1),x6524),x6521))),
% 281.56/282.06 inference(scs_inference,[],[8,17,263,648,4,2,3])).
% 281.56/282.06 cnf(657,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(f2(f2(a3,a1),x6571),f2(x6572,x6573))),x6574),f2(f2(f2(a3,f2(a3,a1)),x6572),x6573))),
% 281.56/282.06 inference(scs_inference,[],[8,31,310,652,2,4,3])).
% 281.56/282.06 cnf(662,plain,
% 281.56/282.06 (E(f2(f2(a1,f2(f2(x6621,x6622),x6623)),x6624),f2(f2(x6621,f2(f2(a1,x6622),x6625)),x6623))),
% 281.56/282.06 inference(scs_inference,[],[8,108,219,567,4,2,3])).
% 281.56/282.06 cnf(685,plain,
% 281.56/282.06 (~E(f2(a1,x6851),a1)),
% 281.56/282.06 inference(scs_inference,[],[205,657,2,4])).
% 281.56/282.06 cnf(715,plain,
% 281.56/282.06 (~E(f2(a3,f2(a3,a1)),f2(a3,a1))),
% 281.56/282.06 inference(scs_inference,[],[662,647,2,4])).
% 281.56/282.06 cnf(867,plain,
% 281.56/282.06 (E(f2(f2(x8671,f2(a1,f2(f2(a1,x8672),x8673))),f2(x8674,f2(f2(a1,x8672),x8673))),f2(f2(f2(a3,x8671),x8674),x8672))),
% 281.56/282.06 inference(scs_inference,[],[9,56,3])).
% 281.56/282.06 cnf(948,plain,
% 281.56/282.06 (E(f2(f2(f2(a1,f2(a1,x9481)),x9482),x9483),x9481)),
% 281.56/282.06 inference(scs_inference,[],[11,101,3,2])).
% 281.56/282.06 cnf(957,plain,
% 281.56/282.06 (E(f2(f2(f2(f2(a3,a1),x9571),x9572),x9573),x9572)),
% 281.56/282.06 inference(scs_inference,[],[11,138,3,2])).
% 281.56/282.06 cnf(961,plain,
% 281.56/282.06 (E(f2(a1,f2(f2(a1,x9611),x9612)),f2(f2(f2(a3,a1),x9613),x9611))),
% 281.56/282.06 inference(scs_inference,[],[11,867,3])).
% 281.56/282.06 cnf(1074,plain,
% 281.56/282.06 (E(f2(x10741,f2(x10742,x10743)),f2(f2(f2(a3,f2(a1,x10741)),x10742),x10743))),
% 281.56/282.06 inference(scs_inference,[],[12,57,3,2])).
% 281.56/282.06 cnf(1391,plain,
% 281.56/282.06 (~E(f2(a3,a1),f2(f2(a1,f2(a3,f2(a3,a1))),x13911))),
% 281.56/282.06 inference(scs_inference,[],[11,715,3,2])).
% 281.56/282.06 cnf(1399,plain,
% 281.56/282.06 (E(f2(f2(f2(x13991,f2(a1,x13992)),f2(x13993,x13992)),x13994),f2(f2(f2(f2(a3,x13991),x13993),x13992),x13994))),
% 281.56/282.06 inference(scs_inference,[],[9,7,6,5,4])).
% 281.56/282.06 cnf(1442,plain,
% 281.56/282.06 (E(f2(x14421,f2(f2(f2(f2(a3,a1),x14422),x14423),x14424)),f2(x14421,x14423))),
% 281.56/282.06 inference(scs_inference,[],[957,7,6,5])).
% 281.56/282.06 cnf(1449,plain,
% 281.56/282.06 (E(f4(f2(f2(f2(a1,f2(a1,x14491)),x14492),x14493)),f4(x14491))),
% 281.56/282.06 inference(scs_inference,[],[948,7,6])).
% 281.56/282.06 cnf(1562,plain,
% 281.56/282.06 (~E(f2(a3,a1),f2(f2(f2(a1,a3),x15621),f2(a3,a1)))),
% 281.56/282.06 inference(scs_inference,[],[646,1391,3])).
% 281.56/282.06 cnf(1581,plain,
% 281.56/282.06 (~E(f2(f2(x15811,f4(x15811)),f5(x15811)),f2(f4(x15811),f2(f2(f2(f2(a3,a1),x15812),f4(x15811)),x15813)))),
% 281.56/282.06 inference(scs_inference,[],[10,1442,3])).
% 281.56/282.06 cnf(1863,plain,
% 281.56/282.06 (~E(f2(f2(f2(a3,a1),x18631),x18632),a1)),
% 281.56/282.06 inference(scs_inference,[],[685,1562,961,2,3])).
% 281.56/282.06 cnf(1948,plain,
% 281.56/282.06 (E(f2(f4(f2(f2(f2(a1,f2(a1,x19481)),x19482),x19483)),x19484),f2(f4(x19481),x19484))),
% 281.56/282.06 inference(scs_inference,[],[1449,7,6,5,4])).
% 281.56/282.06 cnf(2150,plain,
% 281.56/282.06 (~E(f2(f4(x21501),f2(f2(f2(f2(a3,a1),x21502),f4(x21501)),x21503)),f2(f2(x21501,f4(x21501)),f5(x21501)))),
% 281.56/282.06 inference(scs_inference,[],[1948,1581,6,4,5,7,2])).
% 281.56/282.06 cnf(2595,plain,
% 281.56/282.06 ($false),
% 281.56/282.06 inference(scs_inference,[],[1074,2150,1863,1399,2,3]),
% 281.56/282.06 ['proof']).
% 281.56/282.06 % SZS output end Proof
% 281.56/282.06 % Total time :280.780000s
%------------------------------------------------------------------------------