%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN003-4 : 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 : n020.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 07:26:46 EDT 2024
% Result : Unsatisfiable 105.88s 105.94s
% Output : CNFRefutation 105.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : HEN003-4 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sat Jun 22 05:22:54 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.63/0.64 start to proof:theBenchmark
% 105.88/105.93 %-------------------------------------------
% 105.88/105.93 % File :CSE---1.7
% 105.88/105.93 % Problem :theBenchmark
% 105.88/105.93 % Transform :cnf
% 105.88/105.93 % Format :tptp:raw
% 105.88/105.93 % Command :java -jar mcs_scs.jar %d %s
% 105.88/105.93
% 105.88/105.93 % Result :Theorem 105.180000s
% 105.88/105.93 % Output :CNFRefutation 105.180000s
% 105.88/105.93 %-------------------------------------------
% 105.88/105.94 %--------------------------------------------------------------------------
% 105.88/105.94 % File : HEN003-4 : TPTP v8.2.0. Released v1.0.0.
% 105.88/105.94 % Domain : Henkin Models
% 105.88/105.94 % Problem : X/X = zero
% 105.88/105.94 % Version : [MOW76] axioms : Augmented.
% 105.88/105.94 % English :
% 105.88/105.94
% 105.88/105.94 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 105.88/105.94 % Source : [ANL]
% 105.88/105.94 % Names : hp3.ver2.in [ANL]
% 105.88/105.94
% 105.88/105.94 % Status : Unsatisfiable
% 105.88/105.94 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 105.88/105.94 % Syntax : Number of clauses : 10 ( 7 unt; 0 nHn; 4 RR)
% 105.88/105.94 % Number of literals : 14 ( 6 equ; 5 neg)
% 105.88/105.94 % Maximal clause size : 3 ( 1 avg)
% 105.88/105.94 % Maximal term depth : 3 ( 1 avg)
% 105.88/105.94 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 105.88/105.94 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 105.88/105.94 % Number of variables : 15 ( 5 sgn)
% 105.88/105.94 % SPC : CNF_UNS_RFO_SEQ_HRN
% 105.88/105.94
% 105.88/105.94 % Comments :
% 105.88/105.94 %--------------------------------------------------------------------------
% 105.88/105.94 %----Include Henkin model axioms for equality formulation
% 105.88/105.94 include('Axioms/HEN002-0.ax').
% 105.88/105.94 %--------------------------------------------------------------------------
% 105.88/105.94 cnf(everything_divide_id_is_zero,axiom,
% 105.88/105.94 divide(X,identity) = zero ).
% 105.88/105.94
% 105.88/105.94 cnf(zero_divide_anything_is_zero,axiom,
% 105.88/105.94 divide(zero,X) = zero ).
% 105.88/105.94
% 105.88/105.94 cnf(prove_x_divide_x_is_zero,negated_conjecture,
% 105.88/105.94 divide(a,a) != zero ).
% 105.88/105.94
% 105.88/105.94 %--------------------------------------------------------------------------
% 105.88/105.94 %-------------------------------------------
% 105.88/105.94 % Proof found
% 105.88/105.94 % SZS status Theorem for theBenchmark
% 105.88/105.94 % SZS output start Proof
% 105.88/105.95 %ClaNum:17(EqnAxiom:7)
% 105.88/105.95 %VarNum:28(SingletonVarNum:15)
% 105.88/105.95 %MaxLitNum:3
% 105.88/105.95 %MaxfuncDepth:2
% 105.88/105.95 %SharedTerms:5
% 105.88/105.95 %goalClause: 14
% 105.88/105.95 %singleGoalClaCount:1
% 105.88/105.95 [14]~E(f2(a3,a3),a4)
% 105.88/105.95 [10]P1(x101,a1)
% 105.88/105.95 [11]P1(a4,x111)
% 105.88/105.95 [8]E(f2(x81,a1),a4)
% 105.88/105.95 [9]E(f2(a4,x91),a4)
% 105.88/105.95 [12]P1(f2(x121,x122),x121)
% 105.88/105.95 [13]P1(f2(f2(x131,x132),f2(x133,x132)),f2(f2(x131,x133),x132))
% 105.88/105.95 [15]~P1(x151,x152)+E(f2(x151,x152),a4)
% 105.88/105.95 [16]P1(x161,x162)+~E(f2(x161,x162),a4)
% 105.88/105.95 [17]~P1(x172,x171)+~P1(x171,x172)+E(x171,x172)
% 105.88/105.95 %EqnAxiom
% 105.88/105.95 [1]E(x11,x11)
% 105.88/105.95 [2]E(x22,x21)+~E(x21,x22)
% 105.88/105.95 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 105.88/105.95 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 105.88/105.95 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 105.88/105.95 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 105.88/105.95 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 105.88/105.95
% 105.88/105.95 %-------------------------------------------
% 105.88/105.96 cnf(18,plain,
% 105.88/105.96 (~P1(a3,a3)),
% 105.88/105.96 inference(scs_inference,[],[14,15])).
% 105.88/105.96 cnf(20,plain,
% 105.88/105.96 (E(a4,f2(x201,a1))),
% 105.88/105.96 inference(scs_inference,[],[14,8,15,2])).
% 105.88/105.96 cnf(21,plain,
% 105.88/105.96 (~E(f2(a3,a3),f2(x211,a1))),
% 105.88/105.96 inference(scs_inference,[],[14,8,15,2,3])).
% 105.88/105.96 cnf(22,plain,
% 105.88/105.96 (~E(a4,a3)),
% 105.88/105.96 inference(scs_inference,[],[14,11,8,15,2,3,6])).
% 105.88/105.96 cnf(25,plain,
% 105.88/105.96 (P1(x251,a1)),
% 105.88/105.96 inference(rename_variables,[],[10])).
% 105.88/105.96 cnf(27,plain,
% 105.88/105.96 (~P1(a1,a3)),
% 105.88/105.96 inference(scs_inference,[],[14,10,25,11,8,15,2,3,6,7,5,17])).
% 105.88/105.96 cnf(30,plain,
% 105.88/105.96 (E(a4,f2(a4,x301))),
% 105.88/105.96 inference(scs_inference,[],[9,2])).
% 105.88/105.96 cnf(31,plain,
% 105.88/105.96 (~P1(a3,a4)),
% 105.88/105.96 inference(scs_inference,[],[22,9,11,2,17])).
% 105.88/105.96 cnf(35,plain,
% 105.88/105.96 (~E(f2(a3,x351),a3)),
% 105.88/105.96 inference(scs_inference,[],[14,18,12,22,9,11,2,17,3,6])).
% 105.88/105.96 cnf(36,plain,
% 105.88/105.96 (P1(f2(x361,x362),x361)),
% 105.88/105.96 inference(rename_variables,[],[12])).
% 105.88/105.96 cnf(37,plain,
% 105.88/105.96 (P1(f2(a4,x371),f2(x372,a1))),
% 105.88/105.96 inference(scs_inference,[],[14,18,20,12,36,22,9,11,2,17,3,6,7])).
% 105.88/105.96 cnf(40,plain,
% 105.88/105.96 (~P1(a3,f2(a3,x401))),
% 105.88/105.96 inference(scs_inference,[],[35,12,17])).
% 105.88/105.96 cnf(43,plain,
% 105.88/105.96 (~E(f2(a4,x431),a3)),
% 105.88/105.96 inference(scs_inference,[],[37,35,12,17,6])).
% 105.88/105.96 cnf(45,plain,
% 105.88/105.96 (P1(f2(f2(x451,a1),f2(x452,a1)),a4)),
% 105.88/105.96 inference(scs_inference,[],[37,35,13,12,8,17,6,7])).
% 105.88/105.96 cnf(48,plain,
% 105.88/105.96 (E(f2(f2(x481,a1),f2(x482,a1)),a4)),
% 105.88/105.96 inference(scs_inference,[],[45,11,17])).
% 105.88/105.96 cnf(53,plain,
% 105.88/105.96 (P1(f2(f2(x531,a1),f2(x532,a1)),f2(a4,x533))),
% 105.88/105.96 inference(scs_inference,[],[14,30,31,45,11,17,3,6,7])).
% 105.88/105.96 cnf(54,plain,
% 105.88/105.96 (P1(f2(x541,a1),f2(x542,a1))),
% 105.88/105.96 inference(scs_inference,[],[14,30,31,45,11,17,3,6,7,16])).
% 105.88/105.96 cnf(56,plain,
% 105.88/105.96 (E(a4,f2(f2(x561,a1),f2(x562,a1)))),
% 105.88/105.96 inference(scs_inference,[],[14,30,31,45,11,17,3,6,7,16,2])).
% 105.88/105.96 cnf(58,plain,
% 105.88/105.96 (P1(f2(x581,a1),f2(x582,a1))),
% 105.88/105.96 inference(rename_variables,[],[54])).
% 105.88/105.96 cnf(60,plain,
% 105.88/105.96 (P1(f2(x601,a1),a4)),
% 105.88/105.96 inference(scs_inference,[],[40,54,58,9,6,7])).
% 105.88/105.96 cnf(67,plain,
% 105.88/105.96 (P1(f2(x671,a1),f2(f2(x672,a1),f2(x673,a1)))),
% 105.88/105.96 inference(scs_inference,[],[56,60,7])).
% 105.88/105.96 cnf(71,plain,
% 105.88/105.96 (E(f2(a4,a1),f2(f2(x711,a1),f2(x712,a1)))),
% 105.88/105.96 inference(scs_inference,[],[56,60,53,7,17,2])).
% 105.88/105.96 cnf(73,plain,
% 105.88/105.96 (P1(f2(x731,a1),f2(f2(x732,a1),f2(x733,a1)))),
% 105.88/105.96 inference(rename_variables,[],[67])).
% 105.88/105.96 cnf(78,plain,
% 105.88/105.96 (P1(f2(a4,x781),f2(f2(x782,a1),f2(x783,a1)))),
% 105.88/105.96 inference(scs_inference,[],[71,67,73,37,13,17,6,7])).
% 105.88/105.96 cnf(84,plain,
% 105.88/105.96 (P1(f2(f2(f2(x841,a1),f2(x842,a1)),x843),a4)),
% 105.88/105.96 inference(scs_inference,[],[48,78,53,12,17,7])).
% 105.88/105.96 cnf(86,plain,
% 105.88/105.96 (E(f2(f2(x861,a1),f2(x862,a1)),f2(a4,x863))),
% 105.88/105.96 inference(scs_inference,[],[48,78,53,12,17,7,2])).
% 105.88/105.96 cnf(87,plain,
% 105.88/105.96 (~E(f2(f2(f2(x871,a1),f2(x872,a1)),x873),a3)),
% 105.88/105.96 inference(scs_inference,[],[48,31,78,53,12,17,7,2,6])).
% 105.88/105.96 cnf(91,plain,
% 105.88/105.96 (P1(f2(f2(x911,a1),f2(x912,a1)),x913)),
% 105.88/105.96 inference(scs_inference,[],[84,11,17,16])).
% 105.88/105.96 cnf(99,plain,
% 105.88/105.96 (E(f2(x991,a1),f2(f2(x992,a1),f2(x993,a1)))),
% 105.88/105.96 inference(scs_inference,[],[91,67,17])).
% 105.88/105.96 cnf(104,plain,
% 105.88/105.96 (E(a4,f2(f2(a4,x1041),f2(f2(x1042,a1),f2(x1043,a1))))),
% 105.88/105.96 inference(scs_inference,[],[78,2,15])).
% 105.88/105.96 cnf(106,plain,
% 105.88/105.97 (E(f2(x1061,a1),f2(f2(a4,x1062),f2(f2(x1063,a1),f2(x1064,a1))))),
% 105.88/105.97 inference(scs_inference,[],[8,104,2,3])).
% 105.88/105.97 cnf(107,plain,
% 105.88/105.97 (P1(f2(f2(x1071,a1),x1072),a4)),
% 105.88/105.97 inference(scs_inference,[],[8,104,12,2,3,7])).
% 105.88/105.97 cnf(109,plain,
% 105.88/105.97 (E(f2(f2(x1091,a1),x1092),a4)),
% 105.88/105.97 inference(scs_inference,[],[8,104,12,11,2,3,7,17])).
% 105.88/105.97 cnf(112,plain,
% 105.88/105.97 (~E(f2(f2(x1121,a1),x1122),a3)),
% 105.88/105.97 inference(scs_inference,[],[8,104,31,12,11,2,3,7,17,6])).
% 105.88/105.97 cnf(113,plain,
% 105.88/105.97 (P1(f2(x1131,a1),x1132)),
% 105.88/105.97 inference(scs_inference,[],[8,104,31,12,11,2,3,7,17,6,16])).
% 105.88/105.97 cnf(115,plain,
% 105.88/105.97 (E(f2(a4,x1151),f2(f2(x1152,a1),x1151))),
% 105.88/105.97 inference(scs_inference,[],[8,2,4])).
% 105.88/105.97 cnf(116,plain,
% 105.88/105.97 (E(f2(f2(a4,x1161),f2(f2(x1162,a1),f2(x1163,a1))),f2(x1164,a1))),
% 105.88/105.97 inference(scs_inference,[],[106,2])).
% 105.88/105.97 cnf(122,plain,
% 105.88/105.97 (P1(f2(f2(x1221,a1),x1222),f2(f2(x1223,a1),f2(x1224,a1)))),
% 105.88/105.97 inference(scs_inference,[],[14,56,106,109,113,87,107,2,3,17,7])).
% 105.88/105.97 cnf(132,plain,
% 105.88/105.97 (P1(f2(f2(x1321,a1),x1322),f2(a4,x1323))),
% 105.88/105.97 inference(scs_inference,[],[116,86,109,21,112,122,113,2,3,17,7])).
% 105.88/105.97 cnf(134,plain,
% 105.88/105.97 (E(f2(x1341,a4),f2(x1341,f2(x1342,a1)))),
% 105.88/105.97 inference(scs_inference,[],[8,2,5])).
% 105.88/105.97 cnf(136,plain,
% 105.88/105.97 (E(f2(f2(x1361,a1),x1362),f2(a4,a1))),
% 105.88/105.97 inference(scs_inference,[],[132,115,113,2,17])).
% 105.88/105.97 cnf(147,plain,
% 105.88/105.97 (P1(f2(f2(f2(x1471,a1),f2(x1472,a1)),x1473),f2(a4,x1474))),
% 105.88/105.97 inference(scs_inference,[],[30,136,43,84,113,2,17,7])).
% 105.88/105.97 cnf(148,plain,
% 105.88/105.97 (P1(f2(f2(x1481,a1),x1482),f2(x1483,a1))),
% 105.88/105.97 inference(scs_inference,[],[8,107,2,7])).
% 105.88/105.97 cnf(149,plain,
% 105.88/105.97 (E(f2(x1491,f2(x1492,a1)),f2(x1491,a4))),
% 105.88/105.97 inference(scs_inference,[],[134,2])).
% 105.88/105.97 cnf(168,plain,
% 105.88/105.97 (~E(f2(x1681,a1),f2(a3,a3))),
% 105.88/105.97 inference(scs_inference,[],[14,20,2,3])).
% 105.88/105.97 cnf(175,plain,
% 105.88/105.97 (~P1(f2(a3,a3),a4)),
% 105.88/105.97 inference(scs_inference,[],[14,11,2,17])).
% 105.88/105.97 cnf(176,plain,
% 105.88/105.97 (~P1(f2(a3,a3),f2(x1761,a1))),
% 105.88/105.97 inference(scs_inference,[],[168,113,17])).
% 105.88/105.97 cnf(185,plain,
% 105.88/105.97 (~E(f2(a4,x1851),f2(a3,a3))),
% 105.88/105.97 inference(scs_inference,[],[14,30,2,3])).
% 105.88/105.97 cnf(191,plain,
% 105.88/105.97 (P1(f2(f2(a4,x1911),x1912),a4)),
% 105.88/105.97 inference(scs_inference,[],[9,12,7])).
% 105.88/105.97 cnf(193,plain,
% 105.88/105.97 (E(f2(f2(a4,x1931),x1932),a4)),
% 105.88/105.97 inference(scs_inference,[],[9,12,11,7,17])).
% 105.88/105.97 cnf(197,plain,
% 105.88/105.97 (P1(f2(a4,x1971),x1972)),
% 105.88/105.97 inference(scs_inference,[],[9,175,12,11,7,17,6,16])).
% 105.88/105.97 cnf(200,plain,
% 105.88/105.97 (~E(f2(a3,a3),f2(f2(a4,x2001),x2002))),
% 105.88/105.97 inference(scs_inference,[],[9,14,175,12,11,7,17,6,16,2,3])).
% 105.88/105.97 cnf(201,plain,
% 105.88/105.97 (E(f2(x2011,f2(f2(a4,x2012),x2013)),f2(x2011,a4))),
% 105.88/105.97 inference(scs_inference,[],[197,15,5])).
% 105.88/105.97 cnf(204,plain,
% 105.88/105.97 (E(f2(x2041,a4),f2(x2041,f2(f2(a4,x2042),x2043)))),
% 105.88/105.97 inference(scs_inference,[],[201,200,4,2])).
% 105.88/105.97 cnf(205,plain,
% 105.88/105.97 (~P1(f2(a3,a3),f2(a4,x2051))),
% 105.88/105.97 inference(scs_inference,[],[201,200,185,197,4,2,17])).
% 105.88/105.97 cnf(208,plain,
% 105.88/105.97 (P1(f2(f2(a4,x2081),x2082),f2(x2083,a1))),
% 105.88/105.97 inference(scs_inference,[],[20,201,200,185,191,197,4,2,17,7])).
% 105.88/105.97 cnf(210,plain,
% 105.88/105.97 (E(a4,f2(f2(f2(a4,x2101),x2102),f2(x2103,a1)))),
% 105.88/105.97 inference(scs_inference,[],[208,15,2])).
% 105.88/105.97 cnf(213,plain,
% 105.88/105.97 (E(f2(f2(f2(x2131,a1),f2(x2132,a1)),x2133),f2(a4,x2134))),
% 105.88/105.97 inference(scs_inference,[],[14,210,197,147,2,3,17])).
% 105.88/105.97 cnf(217,plain,
% 105.88/105.97 (P1(f2(f2(a4,x2171),x2172),f2(a4,x2173))),
% 105.88/105.97 inference(scs_inference,[],[14,30,210,191,197,147,2,3,17,7])).
% 105.88/105.97 cnf(220,plain,
% 105.88/105.97 (E(f2(f2(a4,x2201),x2202),f2(a4,x2203))),
% 105.88/105.97 inference(scs_inference,[],[213,217,197,2,17])).
% 105.88/105.97 cnf(225,plain,
% 105.88/105.97 (E(f2(a4,x2251),f2(f2(a4,x2252),x2253))),
% 105.88/105.97 inference(scs_inference,[],[220,2])).
% 105.88/105.97 cnf(226,plain,
% 105.88/105.97 (E(f2(f2(x2261,a1),x2262),f2(a4,x2263))),
% 105.88/105.97 inference(scs_inference,[],[220,132,197,2,17])).
% 105.88/105.97 cnf(230,plain,
% 105.88/105.97 (E(f2(x2301,a1),f2(x2302,a1))),
% 105.88/105.97 inference(scs_inference,[],[10,20,15,3])).
% 105.88/105.97 cnf(231,plain,
% 105.88/105.97 (E(f2(a4,x2311),f2(f2(x2312,a1),x2313))),
% 105.88/105.97 inference(scs_inference,[],[226,2])).
% 105.88/105.97 cnf(236,plain,
% 105.88/105.97 (E(f2(x2361,a1),f2(a4,x2362))),
% 105.88/105.97 inference(scs_inference,[],[10,30,15,3])).
% 105.88/105.97 cnf(237,plain,
% 105.88/105.97 (E(f2(a4,x2371),f2(x2372,a1))),
% 105.88/105.97 inference(scs_inference,[],[236,2])).
% 105.88/105.97 cnf(250,plain,
% 105.88/105.97 (~E(f2(a4,x2501),a1)),
% 105.88/105.97 inference(scs_inference,[],[27,197,6])).
% 105.88/105.97 cnf(256,plain,
% 105.88/105.97 (~E(f2(x2561,a1),a1)),
% 105.88/105.97 inference(scs_inference,[],[27,250,113,197,17,6])).
% 105.88/105.97 cnf(265,plain,
% 105.88/105.97 (~E(f2(a3,x2651),a1)),
% 105.88/105.97 inference(scs_inference,[],[27,12,6])).
% 105.88/105.97 cnf(268,plain,
% 105.88/105.97 (E(f2(x2681,f2(a4,x2682)),f2(x2681,a4))),
% 105.88/105.97 inference(scs_inference,[],[30,5,2])).
% 105.88/105.97 cnf(269,plain,
% 105.88/105.97 (E(f2(x2691,a4),f2(x2691,f2(a4,x2692)))),
% 105.88/105.97 inference(scs_inference,[],[268,2])).
% 105.88/105.97 cnf(279,plain,
% 105.88/105.97 (P1(f2(f2(x2791,a1),x2792),f2(f2(a4,x2793),x2794))),
% 105.88/105.97 inference(scs_inference,[],[225,148,7])).
% 105.88/105.97 cnf(282,plain,
% 105.88/105.97 (E(f2(a4,x2821),f2(f2(f2(x2822,a1),x2823),x2821))),
% 105.88/105.97 inference(scs_inference,[],[20,231,3,4])).
% 105.88/105.97 cnf(283,plain,
% 105.88/105.97 (E(f2(f2(f2(x2831,a1),x2832),x2833),f2(a4,x2833))),
% 105.88/105.97 inference(scs_inference,[],[282,2])).
% 105.88/105.97 cnf(292,plain,
% 105.88/105.97 (P1(f2(f2(f2(x2921,a1),x2922),f2(x2923,x2922)),f2(a4,x2922))),
% 105.88/105.97 inference(scs_inference,[],[283,13,7])).
% 105.88/105.97 cnf(310,plain,
% 105.88/105.97 (~E(f2(f2(a3,x3101),x3102),a3)),
% 105.88/105.97 inference(scs_inference,[],[40,12,6])).
% 105.88/105.97 cnf(343,plain,
% 105.88/105.97 (P1(f2(f2(x3431,x3432),f2(a1,x3432)),a4)),
% 105.88/105.97 inference(scs_inference,[],[109,13,7])).
% 105.88/105.97 cnf(345,plain,
% 105.88/105.97 (E(f2(f2(x3451,x3452),f2(a1,x3452)),a4)),
% 105.88/105.97 inference(scs_inference,[],[109,13,11,7,17])).
% 105.88/105.97 cnf(349,plain,
% 105.88/105.97 (~E(f2(f2(x3491,x3492),f2(a1,x3492)),f2(a3,a3))),
% 105.88/105.97 inference(scs_inference,[],[109,14,175,13,11,7,17,3,6])).
% 105.88/105.97 cnf(350,plain,
% 105.88/105.97 (P1(f2(x3501,x3502),f2(a1,x3502))),
% 105.88/105.97 inference(scs_inference,[],[109,14,175,13,11,7,17,3,6,16])).
% 105.88/105.97 cnf(353,plain,
% 105.88/105.97 (E(f2(x3531,f2(f2(x3532,x3533),f2(a1,x3533))),f2(x3531,a4))),
% 105.88/105.97 inference(scs_inference,[],[350,15,5])).
% 105.88/105.97 cnf(359,plain,
% 105.88/105.97 (P1(f2(f2(x3591,x3592),f2(a1,x3592)),f2(a4,x3593))),
% 105.88/105.97 inference(scs_inference,[],[30,349,353,343,12,2,17,7])).
% 105.88/105.97 cnf(360,plain,
% 105.88/105.97 (E(a4,f2(f2(f2(x3601,x3602),f2(a1,x3602)),f2(a4,x3603)))),
% 105.88/105.97 inference(scs_inference,[],[359,15,2])).
% 105.88/105.97 cnf(362,plain,
% 105.88/105.97 (E(f2(f2(x3621,x3622),f2(a1,x3622)),f2(a4,a1))),
% 105.88/105.97 inference(scs_inference,[],[360,359,113,2,17])).
% 105.88/105.97 cnf(372,plain,
% 105.88/105.97 (P1(f2(f2(x3721,x3722),f2(a1,x3722)),f2(x3723,a1))),
% 105.88/105.97 inference(scs_inference,[],[20,362,343,2,7])).
% 105.88/105.97 cnf(383,plain,
% 105.88/105.97 (P1(f2(f2(f2(x3831,a1),x3832),x3833),a4)),
% 105.88/105.97 inference(scs_inference,[],[109,279,12,372,17,7])).
% 105.88/105.97 cnf(392,plain,
% 105.88/105.97 (P1(f2(f2(x3921,a1),x3922),x3923)),
% 105.88/105.97 inference(scs_inference,[],[14,20,11,383,17,3,7,16])).
% 105.88/105.97 cnf(412,plain,
% 105.88/105.97 (P1(f2(x4121,a4),f2(a1,f2(x4122,a1)))),
% 105.88/105.97 inference(scs_inference,[],[134,350,7])).
% 105.88/105.97 cnf(417,plain,
% 105.88/105.97 (E(a4,f2(a1,f2(x4171,a1)))+~P1(f2(a1,f2(x4171,a1)),f2(a4,a4))),
% 105.88/105.97 inference(scs_inference,[],[134,30,350,7,17,3])).
% 105.88/105.97 cnf(421,plain,
% 105.88/105.97 (E(a4,f2(a1,f2(x4211,a1)))+~E(f2(f2(a1,f2(x4211,a1)),f2(a4,a4)),a4)),
% 105.88/105.97 inference(scs_inference,[],[417,16])).
% 105.88/105.97 cnf(422,plain,
% 105.88/105.97 (P1(f2(x4221,f2(x4222,a1)),f2(a1,f2(x4223,a1)))),
% 105.88/105.97 inference(scs_inference,[],[134,412,6])).
% 105.88/105.97 cnf(424,plain,
% 105.88/105.97 (P1(f2(f2(f2(x4241,a1),a4),f2(x4242,a4)),f2(a4,f2(x4243,a1)))),
% 105.88/105.97 inference(scs_inference,[],[134,292,412,6,7])).
% 105.88/105.97 cnf(436,plain,
% 105.88/105.97 (P1(f2(f2(x4361,a4),x4362),f2(x4361,f2(x4363,a1)))),
% 105.88/105.97 inference(scs_inference,[],[134,197,12,424,17,7])).
% 105.88/105.97 cnf(446,plain,
% 105.88/105.97 (P1(f2(x4461,f2(x4462,a1)),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[149,422,7])).
% 105.88/105.97 cnf(457,plain,
% 105.88/105.97 (P1(f2(f2(x4571,x4572),f2(a1,x4572)),x4573)),
% 105.88/105.97 inference(scs_inference,[],[14,345,175,11,12,7,17,3,6,16])).
% 105.88/105.97 cnf(472,plain,
% 105.88/105.97 (~E(a4,f2(f2(a1,f2(x4721,a1)),f2(a4,a4)))+E(a4,f2(a1,f2(x4721,a1)))),
% 105.88/105.97 inference(scs_inference,[],[421,2])).
% 105.88/105.97 cnf(479,plain,
% 105.88/105.97 (~P1(f2(f2(a1,f2(x4791,a1)),f2(a4,a4)),a4)+E(a4,f2(a1,f2(x4791,a1)))),
% 105.88/105.97 inference(scs_inference,[],[11,472,17])).
% 105.88/105.97 cnf(499,plain,
% 105.88/105.97 (P1(f2(f2(f2(x4991,a1),a4),f2(x4992,a4)),f2(f2(a4,x4993),x4994))),
% 105.88/105.97 inference(scs_inference,[],[225,424,7])).
% 105.88/105.97 cnf(527,plain,
% 105.88/105.97 (P1(f2(f2(a4,x5271),x5272),x5273)),
% 105.88/105.97 inference(scs_inference,[],[193,175,11,12,7,17,6,16])).
% 105.88/105.97 cnf(539,plain,
% 105.88/105.97 (P1(f2(x5391,f2(f2(a4,x5392),x5393)),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[201,350,7])).
% 105.88/105.97 cnf(621,plain,
% 105.88/105.97 (E(f2(x6211,f2(x6212,a1)),f2(x6211,f2(x6213,a1)))),
% 105.88/105.97 inference(scs_inference,[],[230,5,2])).
% 105.88/105.97 cnf(623,plain,
% 105.88/105.97 (E(f2(x6231,f2(a4,x6232)),f2(x6231,f2(x6233,a1)))),
% 105.88/105.97 inference(scs_inference,[],[236,5,2])).
% 105.88/105.97 cnf(624,plain,
% 105.88/105.97 (E(f2(x6241,f2(x6242,a1)),f2(x6241,f2(a4,x6243)))),
% 105.88/105.97 inference(scs_inference,[],[623,2])).
% 105.88/105.97 cnf(634,plain,
% 105.88/105.97 (E(f2(a1,f2(x6341,a1)),a4)+~P1(f2(a1,f2(x6341,a1)),f2(a4,a4))),
% 105.88/105.97 inference(scs_inference,[],[417,2])).
% 105.88/105.97 cnf(635,plain,
% 105.88/105.97 (E(f2(a1,f2(x6351,a1)),a4)+~E(f2(f2(a1,f2(x6351,a1)),f2(a4,a4)),a4)),
% 105.88/105.97 inference(scs_inference,[],[634,16])).
% 105.88/105.97 cnf(639,plain,
% 105.88/105.97 (~E(a4,f2(f2(a1,f2(x6391,a1)),f2(a4,a4)))+E(f2(a1,f2(x6391,a1)),a4)),
% 105.88/105.97 inference(scs_inference,[],[635,2])).
% 105.88/105.97 cnf(640,plain,
% 105.88/105.97 (~E(a4,f2(f2(a1,f2(x6401,a1)),a4))+E(f2(a1,f2(x6401,a1)),a4)),
% 105.88/105.97 inference(scs_inference,[],[269,639,3])).
% 105.88/105.97 cnf(645,plain,
% 105.88/105.97 (~E(f2(x6451,a1),f2(a1,f2(x6452,a1)))+E(a4,f2(a1,f2(x6452,a1)))),
% 105.88/105.97 inference(scs_inference,[],[113,417,6])).
% 105.88/105.97 cnf(646,plain,
% 105.88/105.97 (~E(f2(a1,f2(x6461,a1)),f2(x6462,a1))+E(a4,f2(a1,f2(x6461,a1)))),
% 105.88/105.97 inference(scs_inference,[],[645,2])).
% 105.88/105.97 cnf(654,plain,
% 105.88/105.97 (~P1(a1,f2(x6541,a1))),
% 105.88/105.97 inference(scs_inference,[],[256,10,17])).
% 105.88/105.97 cnf(671,plain,
% 105.88/105.97 (~P1(a1,f2(a3,x6711))),
% 105.88/105.97 inference(scs_inference,[],[265,10,17])).
% 105.88/105.97 cnf(679,plain,
% 105.88/105.97 (P1(f2(x6791,f2(a4,x6792)),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[268,350,7])).
% 105.88/105.97 cnf(689,plain,
% 105.88/105.97 (E(f2(x6891,a4),f2(x6891,f2(a4,x6892)))),
% 105.88/105.97 inference(rename_variables,[],[269])).
% 105.88/105.97 cnf(690,plain,
% 105.88/105.97 (P1(f2(x6901,f2(a4,x6902)),f2(a1,f2(a4,x6903)))),
% 105.88/105.97 inference(scs_inference,[],[269,689,350,7,6])).
% 105.88/105.97 cnf(705,plain,
% 105.88/105.97 (~E(f2(f2(a1,f2(x7051,a1)),a4),a4)+E(f2(a1,f2(x7051,a1)),a4)),
% 105.88/105.97 inference(scs_inference,[],[640,2])).
% 105.88/105.97 cnf(707,plain,
% 105.88/105.97 (~E(f2(f2(a1,f2(a3,a1)),a4),a4)),
% 105.88/105.97 inference(scs_inference,[],[671,705,16])).
% 105.88/105.97 cnf(708,plain,
% 105.88/105.97 (~P1(f2(a1,f2(a3,a1)),a4)),
% 105.88/105.97 inference(scs_inference,[],[707,15])).
% 105.88/105.97 cnf(711,plain,
% 105.88/105.97 (~E(a4,f2(f2(a1,f2(x7111,a1)),a4))),
% 105.88/105.97 inference(scs_inference,[],[654,640,16])).
% 105.88/105.97 cnf(712,plain,
% 105.88/105.97 (~E(f2(a4,x7121),f2(a1,f2(a3,a1)))),
% 105.88/105.97 inference(scs_inference,[],[708,197,6])).
% 105.88/105.97 cnf(716,plain,
% 105.88/105.97 (~E(f2(x7161,a1),f2(a1,f2(a3,a1)))),
% 105.88/105.97 inference(scs_inference,[],[712,8,645,3])).
% 105.88/105.97 cnf(729,plain,
% 105.88/105.97 (~E(f2(a1,f2(a3,a1)),f2(x7291,a1))),
% 105.88/105.97 inference(scs_inference,[],[708,11,436,716,17,6,421,472,479,646])).
% 105.88/105.97 cnf(740,plain,
% 105.88/105.97 (E(a4,f2(a1,a4))+~E(f2(x7401,a1),f2(a1,f2(x7402,a1)))),
% 105.88/105.97 inference(scs_inference,[],[149,645,3])).
% 105.88/105.97 cnf(767,plain,
% 105.88/105.97 (~E(f2(a1,f2(x7671,a1)),f2(x7672,a1))+E(a4,f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[740,2])).
% 105.88/105.97 cnf(779,plain,
% 105.88/105.97 (~E(f2(x7791,a1),f2(a1,a4))+E(a4,f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[204,740,3])).
% 105.88/105.97 cnf(781,plain,
% 105.88/105.97 (E(f2(f2(x7811,a1),x7812),f2(a1,a4))+~E(f2(x7813,a1),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[109,779,3])).
% 105.88/105.97 cnf(783,plain,
% 105.88/105.97 (E(f2(a1,a4),f2(f2(x7831,a1),x7832))+~E(f2(x7833,a1),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[781,2])).
% 105.88/105.97 cnf(785,plain,
% 105.88/105.97 (~E(f2(x7851,a1),f2(a1,a4))),
% 105.88/105.97 inference(scs_inference,[],[729,149,783,3])).
% 105.88/105.97 cnf(811,plain,
% 105.88/105.97 (~E(f2(a1,f2(x8111,a1)),f2(x8112,a1))),
% 105.88/105.97 inference(scs_inference,[],[785,109,767,3])).
% 105.88/105.97 cnf(816,plain,
% 105.88/105.97 (~E(f2(a1,f2(x8161,a1)),a4)),
% 105.88/105.97 inference(scs_inference,[],[310,20,811,457,17,3])).
% 105.88/105.97 cnf(822,plain,
% 105.88/105.98 (~P1(f2(a1,f2(x8221,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[816,705,15])).
% 105.88/105.98 cnf(823,plain,
% 105.88/105.98 (~E(f2(a4,x8231),f2(a1,f2(x8232,a1)))),
% 105.88/105.98 inference(scs_inference,[],[822,197,6])).
% 105.88/105.98 cnf(834,plain,
% 105.88/105.98 (~E(a4,f2(a1,f2(x8341,a1)))),
% 105.88/105.98 inference(scs_inference,[],[822,11,690,823,17,6])).
% 105.88/105.98 cnf(869,plain,
% 105.88/105.98 (~P1(f2(a3,a3),f2(f2(x8691,x8692),f2(a1,x8692)))),
% 105.88/105.98 inference(scs_inference,[],[349,457,17])).
% 105.88/105.98 cnf(899,plain,
% 105.88/105.98 (E(f2(f2(x8991,a1),x8992),f2(f2(x8991,x8992),f2(a1,x8992)))),
% 105.88/105.98 inference(scs_inference,[],[392,13,17,2])).
% 105.88/105.98 cnf(983,plain,
% 105.88/105.98 (E(f2(f2(a4,x9831),x9832),f2(f2(f2(x9833,a1),a4),f2(x9834,a4)))),
% 105.88/105.98 inference(scs_inference,[],[527,499,17,2])).
% 105.88/105.98 cnf(1127,plain,
% 105.88/105.98 (~E(a4,f2(f2(a1,f2(x11271,a1)),f2(a4,x11272)))),
% 105.88/105.98 inference(scs_inference,[],[711,268,11,17,3])).
% 105.88/105.98 cnf(1286,plain,
% 105.88/105.98 (~P1(f2(a1,f2(x12861,a1)),f2(a4,x12862))),
% 105.88/105.98 inference(scs_inference,[],[823,197,17])).
% 105.88/105.98 cnf(1289,plain,
% 105.88/105.98 (~E(f2(a4,x12891),f2(a1,a4))),
% 105.88/105.98 inference(scs_inference,[],[823,204,197,17,3])).
% 105.88/105.98 cnf(1297,plain,
% 105.88/105.98 (~E(a4,f2(a1,a4))),
% 105.88/105.98 inference(scs_inference,[],[834,204,539,1289,17,3])).
% 105.88/105.98 cnf(1324,plain,
% 105.88/105.98 (~E(f2(a1,a3),f2(f2(x13241,x13242),f2(a1,x13242)))),
% 105.88/105.98 inference(scs_inference,[],[869,350,7])).
% 105.88/105.98 cnf(1507,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(x15071,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[1127,11,13,17,7])).
% 105.88/105.98 cnf(1641,plain,
% 105.88/105.98 (~P1(f2(a1,a4),f2(a4,x16411))),
% 105.88/105.98 inference(scs_inference,[],[1289,197,17])).
% 105.88/105.98 cnf(1653,plain,
% 105.88/105.98 (~P1(f2(a1,a4),a4)),
% 105.88/105.98 inference(scs_inference,[],[1297,11,17])).
% 105.88/105.98 cnf(1670,plain,
% 105.88/105.98 (~E(f2(a1,a3),f2(x16701,a1))),
% 105.88/105.98 inference(scs_inference,[],[1324,99,3])).
% 105.88/105.98 cnf(1674,plain,
% 105.88/105.98 (~E(f2(a1,a3),f2(a4,x16741))),
% 105.88/105.98 inference(scs_inference,[],[1324,225,3])).
% 105.88/105.98 cnf(1680,plain,
% 105.88/105.98 (~E(f2(a1,a3),f2(f2(x16801,a1),x16802))),
% 105.88/105.98 inference(scs_inference,[],[1324,899,3])).
% 105.88/105.98 cnf(1686,plain,
% 105.88/105.98 (~E(f2(a1,a3),f2(f2(a4,x16861),x16862))),
% 105.88/105.98 inference(scs_inference,[],[1324,983,3])).
% 105.88/105.98 cnf(1813,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(x18131,a1)),f2(f2(x18132,a1),x18133))),
% 105.88/105.98 inference(scs_inference,[],[1507,109,3])).
% 105.88/105.98 cnf(1815,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(x18151,a1)),f2(x18152,a1))),
% 105.88/105.98 inference(scs_inference,[],[1507,8,3])).
% 105.88/105.98 cnf(1817,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(x18171,a1)),f2(a4,x18172))),
% 105.88/105.98 inference(scs_inference,[],[1507,9,3])).
% 105.88/105.98 cnf(2216,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),a4),a4)),
% 105.88/105.98 inference(scs_inference,[],[1653,679,15,16])).
% 105.88/105.98 cnf(2218,plain,
% 105.88/105.98 (E(f2(f2(x22181,a1),x22182),f2(f2(x22183,a1),x22182))),
% 105.88/105.98 inference(scs_inference,[],[1653,230,679,15,16,4])).
% 105.88/105.98 cnf(2221,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(a4,x22211)),f2(x22212,a1))),
% 105.88/105.98 inference(scs_inference,[],[1653,1670,1815,230,679,624,15,16,4,2,7,3])).
% 105.88/105.98 cnf(2225,plain,
% 105.88/105.98 (~E(f2(f2(a1,a4),f2(a4,x22251)),a4)),
% 105.88/105.98 inference(scs_inference,[],[1641,446,15,16])).
% 105.88/105.98 cnf(2229,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),a4),a4)),
% 105.88/105.98 inference(scs_inference,[],[1641,1674,2216,236,446,11,15,16,4,2,17])).
% 105.88/105.98 cnf(2235,plain,
% 105.88/105.98 (E(f2(f2(x22351,x22352),x22351),a4)),
% 105.88/105.98 inference(scs_inference,[],[12,15])).
% 105.88/105.98 cnf(2241,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),a4),f2(x22411,a1))),
% 105.88/105.98 inference(scs_inference,[],[8,1817,1286,2229,237,12,15,16,4,2,7])).
% 105.88/105.98 cnf(2242,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),f2(a4,x22421)),a4)),
% 105.88/105.98 inference(scs_inference,[],[8,1817,1286,2229,2225,237,12,11,15,16,4,2,7,17])).
% 105.88/105.98 cnf(2248,plain,
% 105.88/105.98 (~E(f2(f2(f2(a1,a4),a4),f2(x22481,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[2241,16])).
% 105.88/105.98 cnf(2251,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),f2(a4,x22511)),f2(x22512,a1))),
% 105.88/105.98 inference(scs_inference,[],[2241,2221,268,16,2,6])).
% 105.88/105.98 cnf(2259,plain,
% 105.88/105.98 (~E(f2(f2(f2(a1,a4),f2(a4,x22591)),f2(x22592,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[2251,16])).
% 105.88/105.98 cnf(2262,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),f2(x22621,a1)),f2(x22622,a1))),
% 105.88/105.98 inference(scs_inference,[],[2251,1680,621,16,2,6])).
% 105.88/105.98 cnf(2265,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),f2(a4,x22651)),f2(f2(x22652,x22653),x22652))),
% 105.88/105.98 inference(scs_inference,[],[2251,1680,2235,2242,621,16,2,6,7])).
% 105.88/105.98 cnf(2266,plain,
% 105.88/105.98 (~P1(f2(f2(f2(a1,a4),a4),f2(x22661,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[2251,1680,2235,2242,2248,621,11,16,2,6,7,17])).
% 105.88/105.98 cnf(2275,plain,
% 105.88/105.98 (~P1(f2(f2(a1,a4),f2(a4,x22751)),f2(f2(x22752,x22753),x22752))),
% 105.88/105.98 inference(rename_variables,[],[2265])).
% 105.88/105.98 cnf(2280,plain,
% 105.88/105.98 (~P1(f2(f2(f2(a1,a4),f2(a4,x22801)),f2(x22802,a1)),a4)),
% 105.88/105.98 inference(scs_inference,[],[2262,1686,2265,2275,2218,2259,621,11,16,2,6,7,17])).
% 105.88/105.98 cnf(2304,plain,
% 105.88/105.98 (~E(f2(f2(a3,a3),f2(a4,x23041)),a4)),
% 105.88/105.98 inference(scs_inference,[],[205,16])).
% 105.88/105.98 cnf(2307,plain,
% 105.88/105.98 (~P1(f2(f2(f2(a1,a4),a4),f2(x23071,a1)),f2(x23072,a1))),
% 105.88/105.98 inference(scs_inference,[],[8,1813,2266,205,16,2,7])).
% 105.88/105.98 cnf(2316,plain,
% 105.88/105.98 (~P1(f2(f2(a3,a3),f2(a4,x23161)),a4)),
% 105.88/105.98 inference(scs_inference,[],[8,2304,2307,2280,176,623,11,16,2,6,7,17])).
% 105.88/105.98 cnf(3257,plain,
% 105.88/105.98 ($false),
% 105.88/105.98 inference(scs_inference,[],[2316,2235,13,7]),
% 105.88/105.98 ['proof']).
% 105.88/105.98 % SZS output end Proof
% 105.88/105.98 % Total time :105.180000s
%------------------------------------------------------------------------------