%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN012-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 07:26:54 EDT 2024
% Result : Unsatisfiable 3.98s 4.09s
% Output : CNFRefutation 3.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : HEN012-1 : TPTP v8.2.0. Released v1.0.0.
% 0.10/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n018.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sat Jun 22 05:20:54 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 3.98/4.08 %-------------------------------------------
% 3.98/4.08 % File :CSE---1.7
% 3.98/4.08 % Problem :theBenchmark
% 3.98/4.08 % Transform :cnf
% 3.98/4.08 % Format :tptp:raw
% 3.98/4.08 % Command :java -jar mcs_scs.jar %d %s
% 3.98/4.08
% 3.98/4.08 % Result :Theorem 3.500000s
% 3.98/4.08 % Output :CNFRefutation 3.500000s
% 3.98/4.08 %-------------------------------------------
% 3.98/4.09 %--------------------------------------------------------------------------
% 3.98/4.09 % File : HEN012-1 : TPTP v8.2.0. Released v1.0.0.
% 3.98/4.09 % Domain : Henkin Models
% 3.98/4.09 % Problem : X <= X
% 3.98/4.09 % Version : [MOW76] axioms.
% 3.98/4.09 % English :
% 3.98/4.09
% 3.98/4.09 % Refs :
% 3.98/4.09 % Source : [TPTP]
% 3.98/4.09 % Names :
% 3.98/4.09
% 3.98/4.09 % Status : Unsatisfiable
% 3.98/4.09 % Rating : 0.06 v8.2.0, 0.00 v6.0.0, 0.33 v5.5.0, 0.38 v5.4.0, 0.33 v5.2.0, 0.38 v5.1.0, 0.29 v5.0.0, 0.14 v4.1.0, 0.00 v4.0.0, 0.17 v3.5.0, 0.00 v3.1.0, 0.22 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.17 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 3.98/4.09 % Syntax : Number of clauses : 10 ( 4 unt; 0 nHn; 7 RR)
% 3.98/4.09 % Number of literals : 22 ( 2 equ; 13 neg)
% 3.98/4.09 % Maximal clause size : 6 ( 2 avg)
% 3.98/4.09 % Maximal term depth : 2 ( 1 avg)
% 3.98/4.09 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 3.98/4.09 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 3.98/4.09 % Number of variables : 25 ( 3 sgn)
% 3.98/4.09 % SPC : CNF_UNS_RFO_SEQ_HRN
% 3.98/4.09
% 3.98/4.09 % Comments :
% 3.98/4.09 %--------------------------------------------------------------------------
% 3.98/4.09 %----Include Henkin model axioms
% 3.98/4.09 include('Axioms/HEN001-0.ax').
% 3.98/4.09 %--------------------------------------------------------------------------
% 3.98/4.09 cnf(prove_X_less_than_or_equal_to_X,negated_conjecture,
% 3.98/4.09 ~ less_equal(x,x) ).
% 3.98/4.09
% 3.98/4.09 %--------------------------------------------------------------------------
% 3.98/4.09 %-------------------------------------------
% 3.98/4.09 % Proof found
% 3.98/4.09 % SZS status Theorem for theBenchmark
% 3.98/4.09 % SZS output start Proof
% 3.98/4.09 %ClaNum:20(EqnAxiom:10)
% 3.98/4.09 %VarNum:50(SingletonVarNum:25)
% 3.98/4.09 %MaxLitNum:6
% 3.98/4.09 %MaxfuncDepth:1
% 3.98/4.09 %SharedTerms:4
% 3.98/4.09 %goalClause: 14
% 3.98/4.09 %singleGoalClaCount:1
% 3.98/4.09 [14]~P1(a4,a4)
% 3.98/4.09 [11]P1(x111,a1)
% 3.98/4.09 [12]P1(a3,x121)
% 3.98/4.09 [13]P2(x131,x132,f2(x131,x132))
% 3.98/4.09 [16]~P1(x161,x162)+P2(x161,x162,a3)
% 3.98/4.09 [17]P1(x171,x172)+~P2(x171,x172,a3)
% 3.98/4.09 [18]P1(x181,x182)+~P2(x182,x183,x181)
% 3.98/4.09 [15]~P1(x152,x151)+~P1(x151,x152)+E(x151,x152)
% 3.98/4.09 [19]~P2(x193,x194,x191)+E(x191,x192)+~P2(x193,x194,x192)
% 3.98/4.09 [20]~P2(x208,x207,x205)+P1(x201,x202)+~P2(x203,x204,x201)+~P2(x205,x206,x202)+~P2(x207,x206,x204)+~P2(x208,x206,x203)
% 3.98/4.09 %EqnAxiom
% 3.98/4.09 [1]E(x11,x11)
% 3.98/4.09 [2]E(x22,x21)+~E(x21,x22)
% 3.98/4.09 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 3.98/4.09 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 3.98/4.09 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 3.98/4.09 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 3.98/4.09 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 3.98/4.09 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 3.98/4.09 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 3.98/4.09 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 3.98/4.09
% 3.98/4.09 %-------------------------------------------
% 3.98/4.10 cnf(24,plain,
% 3.98/4.10 (P1(a3,x241)),
% 3.98/4.10 inference(rename_variables,[],[12])).
% 3.98/4.10 cnf(27,plain,
% 3.98/4.10 (~P1(a4,a3)),
% 3.98/4.10 inference(scs_inference,[],[14,11,12,24,18,6,7,15])).
% 3.98/4.10 cnf(30,plain,
% 3.98/4.10 (~E(f2(a4,x301),a4)),
% 3.98/4.10 inference(scs_inference,[],[14,13,11,12,24,18,6,7,15,10])).
% 3.98/4.10 cnf(31,plain,
% 3.98/4.10 (P2(x311,x312,f2(x311,x312))),
% 3.98/4.10 inference(rename_variables,[],[13])).
% 3.98/4.10 cnf(32,plain,
% 3.98/4.10 (P2(x321,x322,f2(x323,x322))+~E(x323,x321)),
% 3.98/4.10 inference(scs_inference,[],[14,13,31,11,12,24,18,6,7,15,10,8])).
% 3.98/4.10 cnf(33,plain,
% 3.98/4.10 (P2(x331,x332,f2(x331,x333))+~E(x333,x332)),
% 3.98/4.10 inference(scs_inference,[],[14,13,31,11,12,24,18,6,7,15,10,8,9])).
% 3.98/4.10 cnf(41,plain,
% 3.98/4.10 (~P2(a3,x411,a4)),
% 3.98/4.10 inference(scs_inference,[],[27,18])).
% 3.98/4.10 cnf(44,plain,
% 3.98/4.10 (P2(f2(x441,x442),x441,a3)),
% 3.98/4.10 inference(scs_inference,[],[13,16,18])).
% 3.98/4.10 cnf(45,plain,
% 3.98/4.10 (P1(f2(x451,x452),x451)),
% 3.98/4.10 inference(scs_inference,[],[44,17])).
% 3.98/4.10 cnf(47,plain,
% 3.98/4.10 (E(f2(f2(x471,x472),x471),a3)),
% 3.98/4.10 inference(scs_inference,[],[13,44,17,19])).
% 3.98/4.10 cnf(48,plain,
% 3.98/4.10 (P2(f2(x481,x482),x481,a3)),
% 3.98/4.10 inference(rename_variables,[],[44])).
% 3.98/4.10 cnf(51,plain,
% 3.98/4.10 (~P1(a4,f2(a4,x511))),
% 3.98/4.10 inference(scs_inference,[],[13,44,30,17,19,15])).
% 3.98/4.10 cnf(53,plain,
% 3.98/4.10 (P2(a3,f2(a4,x531),a3)),
% 3.98/4.10 inference(scs_inference,[],[13,44,48,30,17,19,15,8])).
% 3.98/4.10 cnf(55,plain,
% 3.98/4.10 (E(a3,f2(f2(a4,x551),a4))),
% 3.98/4.10 inference(scs_inference,[],[13,44,48,30,17,19,15,8,2])).
% 3.98/4.10 cnf(56,plain,
% 3.98/4.10 (~P2(f2(a4,x561),x562,a4)),
% 3.98/4.10 inference(scs_inference,[],[13,44,48,30,17,19,15,8,2,18])).
% 3.98/4.10 cnf(61,plain,
% 3.98/4.10 (P2(f2(f2(a4,x611),a4),x612,x613)+~E(f2(a3,x612),x613)),
% 3.98/4.10 inference(scs_inference,[],[13,44,48,30,17,19,15,8,2,18,7,32,33,10])).
% 3.98/4.10 cnf(71,plain,
% 3.98/4.10 (E(a3,f2(f2(x711,x712),x711))),
% 3.98/4.10 inference(scs_inference,[],[47,2])).
% 3.98/4.10 cnf(72,plain,
% 3.98/4.10 (P2(f2(f2(x721,x722),x721),x723,f2(a3,x723))),
% 3.98/4.10 inference(scs_inference,[],[47,2,32])).
% 3.98/4.10 cnf(73,plain,
% 3.98/4.10 (P2(x731,f2(f2(x732,x733),x732),f2(x731,a3))),
% 3.98/4.10 inference(scs_inference,[],[47,2,32,33])).
% 3.98/4.10 cnf(76,plain,
% 3.98/4.10 (P2(f2(f2(a4,x761),a4),f2(a4,x762),a3)),
% 3.98/4.10 inference(scs_inference,[],[56,13,47,55,53,2,32,33,10,8])).
% 3.98/4.10 cnf(79,plain,
% 3.98/4.10 (E(f2(f2(a4,x791),a4),f2(a4,x792))+~P1(f2(a4,x792),f2(f2(a4,x791),a4))),
% 3.98/4.10 inference(scs_inference,[],[56,13,47,55,53,2,32,33,10,8,17,15])).
% 3.98/4.10 cnf(88,plain,
% 3.98/4.10 (P2(a3,f2(x881,x882),a3)),
% 3.98/4.10 inference(scs_inference,[],[44,47,8])).
% 3.98/4.10 cnf(96,plain,
% 3.98/4.10 (E(f2(a3,a3),f2(f2(a3,a3),a3))),
% 3.98/4.10 inference(scs_inference,[],[45,13,44,73,47,8,20,6,15])).
% 3.98/4.10 cnf(106,plain,
% 3.98/4.10 (E(a3,f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[71,96,2,3])).
% 3.98/4.10 cnf(107,plain,
% 3.98/4.10 (E(a3,f2(f2(x1071,x1072),x1071))),
% 3.98/4.10 inference(rename_variables,[],[71])).
% 3.98/4.10 cnf(109,plain,
% 3.98/4.10 (P2(f2(x1091,x1092),x1091,a3)),
% 3.98/4.10 inference(rename_variables,[],[44])).
% 3.98/4.10 cnf(110,plain,
% 3.98/4.10 (P1(f2(a3,x1101),f2(f2(x1102,x1103),x1102))),
% 3.98/4.10 inference(scs_inference,[],[45,71,107,44,96,2,3,8,7])).
% 3.98/4.10 cnf(111,plain,
% 3.98/4.10 (P1(f2(x1111,x1112),x1111)),
% 3.98/4.10 inference(rename_variables,[],[45])).
% 3.98/4.10 cnf(116,plain,
% 3.98/4.10 (P2(f2(a3,a3),x1161,f2(a3,x1161))),
% 3.98/4.10 inference(scs_inference,[],[45,71,107,44,109,96,2,3,8,7,9,17,32])).
% 3.98/4.10 cnf(117,plain,
% 3.98/4.10 (P2(x1171,f2(a3,a3),f2(x1171,a3))),
% 3.98/4.10 inference(scs_inference,[],[45,71,107,44,109,96,2,3,8,7,9,17,32,33])).
% 3.98/4.10 cnf(118,plain,
% 3.98/4.10 (E(f2(f2(a3,a3),x1181),f2(a3,x1181))),
% 3.98/4.10 inference(scs_inference,[],[45,13,71,107,44,109,96,2,3,8,7,9,17,32,33,19])).
% 3.98/4.10 cnf(121,plain,
% 3.98/4.10 (E(f2(a3,x1211),f2(f2(a3,x1211),a3))),
% 3.98/4.10 inference(scs_inference,[],[45,111,13,71,107,44,109,96,2,3,8,7,9,17,32,33,19,15])).
% 3.98/4.10 cnf(125,plain,
% 3.98/4.10 (E(f2(a3,x1251),f2(f2(a3,a3),x1251))),
% 3.98/4.10 inference(scs_inference,[],[118,2])).
% 3.98/4.10 cnf(126,plain,
% 3.98/4.10 (E(f2(x1261,f2(a3,a3)),f2(x1261,a3))),
% 3.98/4.10 inference(scs_inference,[],[13,117,118,2,19])).
% 3.98/4.10 cnf(128,plain,
% 3.98/4.10 (P2(x1281,x1282,f2(x1281,x1282))),
% 3.98/4.10 inference(rename_variables,[],[13])).
% 3.98/4.10 cnf(131,plain,
% 3.98/4.10 (P2(f2(a3,a3),x1311,f2(a3,x1311))),
% 3.98/4.10 inference(rename_variables,[],[116])).
% 3.98/4.10 cnf(132,plain,
% 3.98/4.10 (E(f2(f2(x1321,x1322),x1321),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[13,116,117,118,106,121,47,2,19,10,3])).
% 3.98/4.10 cnf(133,plain,
% 3.98/4.10 (P2(f2(a3,x1331),f2(a3,a3),a3)),
% 3.98/4.10 inference(scs_inference,[],[13,44,116,117,118,106,121,47,2,19,10,3,8])).
% 3.98/4.10 cnf(135,plain,
% 3.98/4.10 (P1(f2(a3,x1351),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[110,13,44,116,117,118,106,121,47,2,19,10,3,8,7])).
% 3.98/4.10 cnf(138,plain,
% 3.98/4.10 (P2(f2(a3,a3),f2(f2(x1381,x1382),x1381),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[110,13,71,44,116,131,117,118,106,121,47,2,19,10,3,8,7,9])).
% 3.98/4.10 cnf(139,plain,
% 3.98/4.10 (P2(f2(a3,a3),x1391,f2(a3,x1391))),
% 3.98/4.10 inference(rename_variables,[],[116])).
% 3.98/4.10 cnf(140,plain,
% 3.98/4.10 (P1(f2(a3,a3),f2(a3,f2(x1401,x1402)))),
% 3.98/4.10 inference(scs_inference,[],[110,13,128,71,44,116,131,139,117,118,106,121,88,47,2,19,10,3,8,7,9,20])).
% 3.98/4.10 cnf(146,plain,
% 3.98/4.10 (E(f2(a3,a3),f2(a3,f2(x1461,x1462)))),
% 3.98/4.10 inference(scs_inference,[],[110,13,128,71,44,116,131,139,117,118,106,121,88,47,2,19,10,3,8,7,9,20,61,15])).
% 3.98/4.10 cnf(148,plain,
% 3.98/4.10 (E(f2(a3,a3),f2(f2(x1481,x1482),x1481))),
% 3.98/4.10 inference(scs_inference,[],[132,2])).
% 3.98/4.10 cnf(152,plain,
% 3.98/4.10 (P2(f2(a3,a3),f2(a4,x1521),a3)),
% 3.98/4.10 inference(scs_inference,[],[76,132,72,126,2,10,8])).
% 3.98/4.10 cnf(154,plain,
% 3.98/4.10 (E(f2(f2(x1541,x1542),x1541),f2(a3,a3))),
% 3.98/4.10 inference(rename_variables,[],[132])).
% 3.98/4.10 cnf(155,plain,
% 3.98/4.10 (P2(f2(a3,a3),f2(a3,a3),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[76,138,132,154,72,126,2,10,8,9])).
% 3.98/4.10 cnf(162,plain,
% 3.98/4.10 (E(f2(f2(x1621,x1622),x1621),f2(a4,x1623))+~P1(f2(a4,x1623),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[51,76,138,132,154,72,126,2,10,8,9,17,15,6,3])).
% 3.98/4.10 cnf(163,plain,
% 3.98/4.10 (~P1(f2(a4,x1631),f2(a3,a3))+P2(f2(f2(a4,x1632),a4),a3,f2(a4,x1631))),
% 3.98/4.10 inference(scs_inference,[],[51,76,138,132,154,72,126,2,10,8,9,17,15,6,3,61])).
% 3.98/4.10 cnf(164,plain,
% 3.98/4.10 (P2(x1641,f2(a4,x1642),f2(x1641,f2(a3,a3)))+~P1(f2(a4,x1642),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[51,76,138,132,154,72,126,2,10,8,9,17,15,6,3,61,33])).
% 3.98/4.10 cnf(169,plain,
% 3.98/4.10 (E(f2(a3,a3),a3)),
% 3.98/4.10 inference(scs_inference,[],[106,2])).
% 3.98/4.10 cnf(170,plain,
% 3.98/4.10 (P2(f2(a3,x1701),f2(a3,a3),f2(f2(x1702,x1703),x1702))),
% 3.98/4.10 inference(scs_inference,[],[71,106,133,2,10])).
% 3.98/4.10 cnf(173,plain,
% 3.98/4.10 (E(a3,f2(a3,f2(x1731,x1732)))),
% 3.98/4.10 inference(scs_inference,[],[135,71,106,133,148,146,2,10,6,3])).
% 3.98/4.10 cnf(174,plain,
% 3.98/4.10 (P1(f2(a3,a3),f2(f2(a3,a3),f2(x1741,x1742)))),
% 3.98/4.10 inference(scs_inference,[],[135,140,71,106,133,148,125,146,2,10,6,3,7])).
% 3.98/4.10 cnf(182,plain,
% 3.98/4.10 (P2(a3,x1821,f2(f2(a3,a3),x1821))),
% 3.98/4.10 inference(scs_inference,[],[135,140,71,106,133,148,125,146,2,10,6,3,7,8,61,17,33,32])).
% 3.98/4.10 cnf(183,plain,
% 3.98/4.10 (E(f2(x1831,a3),f2(x1831,f2(a3,a3)))),
% 3.98/4.10 inference(scs_inference,[],[135,140,13,71,106,133,148,125,146,2,10,6,3,7,8,61,17,33,32,19])).
% 3.98/4.10 cnf(195,plain,
% 3.98/4.10 (E(f2(a3,f2(x1951,x1952)),a3)),
% 3.98/4.10 inference(scs_inference,[],[173,33,32,2])).
% 3.98/4.10 cnf(196,plain,
% 3.98/4.10 (E(f2(a3,a3),f2(f2(a3,a3),f2(x1961,x1962)))),
% 3.98/4.10 inference(scs_inference,[],[45,174,173,33,32,2,15])).
% 3.98/4.10 cnf(201,plain,
% 3.98/4.10 (E(f2(x2011,a3),f2(x2011,f2(a3,a3)))),
% 3.98/4.10 inference(rename_variables,[],[183])).
% 3.98/4.10 cnf(202,plain,
% 3.98/4.10 (E(a3,f2(f2(a3,x2021),f2(a3,a3)))),
% 3.98/4.10 inference(scs_inference,[],[45,174,71,116,183,201,173,33,32,2,15,10,3])).
% 3.98/4.10 cnf(203,plain,
% 3.98/4.10 (E(f2(x2031,a3),f2(x2031,f2(a3,a3)))),
% 3.98/4.10 inference(rename_variables,[],[183])).
% 3.98/4.10 cnf(204,plain,
% 3.98/4.10 (E(a3,f2(f2(x2041,x2042),x2041))),
% 3.98/4.10 inference(rename_variables,[],[71])).
% 3.98/4.10 cnf(206,plain,
% 3.98/4.10 (E(f2(x2061,a3),f2(x2061,f2(a3,a3)))),
% 3.98/4.10 inference(rename_variables,[],[183])).
% 3.98/4.10 cnf(207,plain,
% 3.98/4.10 (P2(f2(f2(x2071,x2072),x2071),f2(x2073,x2074),a3)),
% 3.98/4.10 inference(scs_inference,[],[45,135,174,71,204,116,88,183,201,203,173,33,32,2,15,10,3,7,8])).
% 3.98/4.10 cnf(212,plain,
% 3.98/4.10 (~E(f2(f2(x2121,x2122),x2121),a4)),
% 3.98/4.10 inference(scs_inference,[],[45,135,174,71,204,51,116,88,155,183,201,203,206,173,33,32,2,15,10,3,7,8,9,17,6])).
% 3.98/4.10 cnf(214,plain,
% 3.98/4.10 (P2(f2(f2(a3,x2141),f2(a3,a3)),x2142,f2(a3,x2142))),
% 3.98/4.10 inference(scs_inference,[],[202,33,32])).
% 3.98/4.10 cnf(215,plain,
% 3.98/4.10 (E(f2(f2(a3,a3),f2(x2151,x2152)),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[196,202,33,32,2])).
% 3.98/4.10 cnf(216,plain,
% 3.98/4.10 (P2(f2(a3,a3),f2(a4,x2161),f2(f2(x2162,x2163),x2162))),
% 3.98/4.10 inference(scs_inference,[],[71,152,196,202,33,32,2,10])).
% 3.98/4.10 cnf(217,plain,
% 3.98/4.10 (E(a3,f2(f2(a3,a3),f2(x2171,x2172)))),
% 3.98/4.10 inference(scs_inference,[],[71,106,152,196,202,33,32,2,10,3])).
% 3.98/4.10 cnf(218,plain,
% 3.98/4.10 (P1(f2(a3,x2181),f2(f2(a3,a3),f2(x2182,x2183)))),
% 3.98/4.10 inference(scs_inference,[],[135,71,106,152,196,202,33,32,2,10,3,7])).
% 3.98/4.10 cnf(226,plain,
% 3.98/4.10 (P2(f2(f2(a3,a3),f2(x2261,x2262)),x2263,f2(a3,x2263))),
% 3.98/4.10 inference(scs_inference,[],[217,32])).
% 3.98/4.10 cnf(230,plain,
% 3.98/4.10 (E(f2(a3,a3),f2(f2(a3,x2301),f2(a3,a3)))),
% 3.98/4.10 inference(scs_inference,[],[41,169,182,217,202,32,2,10,3])).
% 3.98/4.10 cnf(238,plain,
% 3.98/4.10 (P2(f2(a3,a3),f2(x2381,x2382),a3)),
% 3.98/4.10 inference(scs_inference,[],[116,195,230,2,10])).
% 3.98/4.10 cnf(241,plain,
% 3.98/4.10 (P2(a3,f2(a3,a3),f2(f2(x2411,x2412),x2411))),
% 3.98/4.10 inference(scs_inference,[],[116,106,195,230,170,2,10,3,8])).
% 3.98/4.10 cnf(247,plain,
% 3.98/4.10 (E(f2(f2(a3,x2471),a3),f2(a3,x2471))),
% 3.98/4.10 inference(scs_inference,[],[121,2])).
% 3.98/4.10 cnf(248,plain,
% 3.98/4.10 (P2(f2(f2(a3,a3),f2(x2481,x2482)),f2(a3,a3),f2(a3,a3))),
% 3.98/4.10 inference(scs_inference,[],[126,226,121,2,10])).
% 3.98/4.10 cnf(251,plain,
% 3.98/4.10 (E(a3,f2(a3,x2511))),
% 3.98/4.10 inference(scs_inference,[],[71,126,226,121,2,10,3])).
% 3.98/4.10 cnf(255,plain,
% 3.98/4.10 (P2(x2551,f2(a3,x2552),f2(x2551,a3))),
% 3.98/4.10 inference(scs_inference,[],[71,126,169,226,216,241,121,2,10,3,8,9,33])).
% 3.98/4.10 cnf(256,plain,
% 3.98/4.10 (P2(f2(a3,x2561),x2562,f2(a3,x2562))),
% 3.98/4.10 inference(scs_inference,[],[71,126,169,226,216,241,121,2,10,3,8,9,33,32])).
% 3.98/4.10 cnf(257,plain,
% 3.98/4.10 (E(f2(x2571,f2(a3,x2572)),f2(x2571,a3))),
% 3.98/4.10 inference(scs_inference,[],[13,71,126,169,226,216,241,121,2,10,3,8,9,33,32,19])).
% 3.98/4.10 cnf(260,plain,
% 3.98/4.10 (E(f2(x2601,a3),f2(x2601,f2(a3,x2602)))),
% 3.98/4.10 inference(scs_inference,[],[257,2])).
% 3.98/4.10 cnf(261,plain,
% 3.98/4.10 (E(f2(f2(a3,x2611),x2612),f2(a3,x2612))),
% 3.98/4.10 inference(scs_inference,[],[13,257,256,2,19])).
% 3.98/4.10 cnf(262,plain,
% 3.98/4.10 (P2(f2(a3,x2621),x2622,f2(a3,x2622))),
% 3.98/4.10 inference(rename_variables,[],[256])).
% 3.98/4.10 cnf(267,plain,
% 3.98/4.10 (E(f2(a3,f2(x2671,x2672)),f2(a3,x2673))),
% 3.98/4.10 inference(scs_inference,[],[13,195,214,257,256,251,2,19,10,3])).
% 3.98/4.10 cnf(269,plain,
% 3.98/4.10 (E(f2(f2(a3,a3),x2691),f2(a3,x2691))),
% 3.98/4.10 inference(rename_variables,[],[118])).
% 3.98/4.10 cnf(274,plain,
% 3.98/4.10 (P2(f2(f2(a4,x2741),a4),f2(x2742,x2743),f2(a3,x2744))),
% 3.98/4.11 inference(scs_inference,[],[218,13,71,118,269,195,248,214,257,256,262,251,2,19,10,3,7,8,9,61])).
% 3.98/4.11 cnf(280,plain,
% 3.98/4.11 (E(f2(a3,x2801),f2(f2(a3,x2802),x2801))),
% 3.98/4.11 inference(scs_inference,[],[261,2])).
% 3.98/4.11 cnf(281,plain,
% 3.98/4.11 (P2(f2(a3,a3),f2(x2811,x2812),f2(f2(x2813,x2814),x2813))),
% 3.98/4.11 inference(scs_inference,[],[71,238,261,2,10])).
% 3.98/4.11 cnf(282,plain,
% 3.98/4.11 (E(f2(f2(a3,x2821),f2(x2822,x2823)),a3)),
% 3.98/4.11 inference(scs_inference,[],[71,238,195,261,2,10,3])).
% 3.98/4.11 cnf(291,plain,
% 3.98/4.11 (E(f2(a3,x2911),f2(a3,f2(x2912,x2913)))),
% 3.98/4.11 inference(scs_inference,[],[267,2])).
% 3.98/4.11 cnf(292,plain,
% 3.98/4.11 (P2(f2(a3,a3),f2(x2921,x2922),f2(f2(a3,x2923),f2(a3,x2924)))),
% 3.98/4.11 inference(scs_inference,[],[281,260,267,2,10])).
% 3.98/4.11 cnf(294,plain,
% 3.98/4.11 (E(f2(x2941,a3),f2(x2941,f2(a3,x2942)))),
% 3.98/4.11 inference(rename_variables,[],[260])).
% 3.98/4.11 cnf(295,plain,
% 3.98/4.11 (P1(f2(a3,x2951),f2(f2(a3,x2952),f2(a3,x2953)))),
% 3.98/4.11 inference(scs_inference,[],[110,281,260,294,267,2,10,7])).
% 3.98/4.11 cnf(297,plain,
% 3.98/4.11 (E(f2(x2971,a3),f2(x2971,f2(a3,x2972)))),
% 3.98/4.11 inference(rename_variables,[],[260])).
% 3.98/4.11 cnf(298,plain,
% 3.98/4.11 (E(a3,f2(f2(a3,x2981),f2(a3,x2982)))),
% 3.98/4.11 inference(scs_inference,[],[110,71,281,260,294,297,267,2,10,7,3])).
% 3.98/4.11 cnf(299,plain,
% 3.98/4.11 (E(f2(x2991,a3),f2(x2991,f2(a3,x2992)))),
% 3.98/4.11 inference(rename_variables,[],[260])).
% 3.98/4.11 cnf(301,plain,
% 3.98/4.11 (P2(f2(f2(a3,x3011),f2(a3,x3012)),f2(x3013,x3014),a3)),
% 3.98/4.11 inference(scs_inference,[],[110,71,207,281,260,294,297,299,267,2,10,7,3,8])).
% 3.98/4.11 cnf(308,plain,
% 3.98/4.11 (P1(f2(f2(a3,x3081),f2(a3,x3082)),f2(x3083,x3084))),
% 3.98/4.11 inference(scs_inference,[],[301,17])).
% 3.98/4.11 cnf(310,plain,
% 3.98/4.11 (E(a3,f2(f2(a3,x3101),f2(x3102,x3103)))),
% 3.98/4.11 inference(scs_inference,[],[301,282,17,2])).
% 3.98/4.11 cnf(311,plain,
% 3.98/4.11 (E(f2(a3,x3111),f2(f2(a3,x3111),f2(a3,x3112)))),
% 3.98/4.11 inference(scs_inference,[],[45,295,301,282,17,2,15])).
% 3.98/4.11 cnf(316,plain,
% 3.98/4.11 (P2(f2(a3,a3),f2(x3161,x3162),f2(a3,a3))),
% 3.98/4.11 inference(scs_inference,[],[45,295,51,215,292,301,282,17,2,15,6,10])).
% 3.98/4.11 cnf(317,plain,
% 3.98/4.11 (P2(f2(a3,a3),f2(x3171,x3172),f2(f2(a3,x3173),f2(a3,x3174)))),
% 3.98/4.11 inference(rename_variables,[],[292])).
% 3.98/4.11 cnf(319,plain,
% 3.98/4.11 (E(f2(a3,a3),f2(f2(a3,x3191),f2(a3,x3192)))),
% 3.98/4.11 inference(scs_inference,[],[45,295,51,169,215,292,301,282,298,17,2,15,6,10,3])).
% 3.98/4.11 cnf(322,plain,
% 3.98/4.11 (P2(f2(a3,x3221),f2(x3222,x3223),a3)),
% 3.98/4.11 inference(scs_inference,[],[45,110,295,51,207,169,215,292,247,301,282,298,17,2,15,6,10,3,7,8])).
% 3.98/4.11 cnf(327,plain,
% 3.98/4.11 (P2(f2(f2(a3,x3271),f2(x3272,x3273)),x3274,f2(a3,x3274))),
% 3.98/4.11 inference(scs_inference,[],[45,110,295,51,207,169,215,292,317,247,301,282,298,17,2,15,6,10,3,7,8,9,33,32])).
% 3.98/4.11 cnf(332,plain,
% 3.98/4.11 (P2(f2(f2(a3,x3321),f2(x3322,x3323)),f2(x3324,x3325),a3)),
% 3.98/4.11 inference(scs_inference,[],[51,195,319,327,322,17,2,6,10])).
% 3.98/4.11 cnf(334,plain,
% 3.98/4.11 (E(f2(a3,x3341),a3)),
% 3.98/4.11 inference(scs_inference,[],[51,195,319,327,291,322,17,2,6,10,3])).
% 3.98/4.11 cnf(335,plain,
% 3.98/4.11 (E(f2(a3,f2(x3351,x3352)),a3)),
% 3.98/4.11 inference(rename_variables,[],[195])).
% 3.98/4.11 cnf(341,plain,
% 3.98/4.11 (P2(f2(f2(a4,x3411),a4),x3412,a3)),
% 3.98/4.11 inference(scs_inference,[],[308,51,195,335,169,316,319,327,274,291,322,17,2,6,10,3,7,8,9,61])).
% 3.98/4.11 cnf(342,plain,
% 3.98/4.11 (P2(x3421,a3,f2(x3421,f2(a3,x3422)))),
% 3.98/4.11 inference(scs_inference,[],[308,51,195,335,169,316,319,327,274,291,322,17,2,6,10,3,7,8,9,61,33])).
% 3.98/4.11 cnf(343,plain,
% 3.98/4.11 (P2(a3,x3431,f2(f2(a3,x3432),x3431))),
% 3.98/4.11 inference(scs_inference,[],[308,51,195,335,169,316,319,327,274,291,322,17,2,6,10,3,7,8,9,61,33,32])).
% 3.98/4.11 cnf(352,plain,
% 3.98/4.11 (E(f2(a3,x3521),f2(f2(x3522,x3523),x3522))),
% 3.98/4.11 inference(scs_inference,[],[51,71,256,280,311,332,334,17,2,6,10,3])).
% 3.98/4.11 cnf(361,plain,
% 3.98/4.11 (E(f2(f2(x3611,x3612),x3611),f2(a3,x3613))),
% 3.98/4.11 inference(scs_inference,[],[352,341,17,2])).
% 3.98/4.11 cnf(365,plain,
% 3.98/4.11 (P2(f2(a3,x3651),f2(x3652,x3653),f2(f2(x3654,x3655),x3654))),
% 3.98/4.11 inference(scs_inference,[],[212,71,322,352,341,17,2,15,10])).
% 3.98/4.11 cnf(366,plain,
% 3.98/4.11 (E(f2(a3,x3661),f2(f2(a3,x3662),f2(x3663,x3664)))),
% 3.98/4.11 inference(scs_inference,[],[212,71,334,310,322,352,341,17,2,15,10,3])).
% 3.98/4.11 cnf(383,plain,
% 3.98/4.11 (P2(f2(f2(a4,x3831),a4),x3832,f2(a3,x3833))),
% 3.98/4.11 inference(scs_inference,[],[41,334,251,343,365,366,332,2,10,3,8,9,61])).
% 3.98/4.11 cnf(384,plain,
% 3.98/4.11 (P2(x3841,f2(a3,x3842),f2(x3841,f2(a3,x3843)))),
% 3.98/4.11 inference(scs_inference,[],[41,334,251,343,365,366,332,2,10,3,8,9,61,33])).
% 3.98/4.11 cnf(385,plain,
% 3.98/4.11 (P2(f2(a3,x3851),x3852,a3)),
% 3.98/4.11 inference(scs_inference,[],[334,256,10])).
% 3.98/4.11 cnf(389,plain,
% 3.98/4.11 (P2(f2(a3,x3891),x3892,f2(a3,x3893))),
% 3.98/4.11 inference(scs_inference,[],[334,251,256,361,383,280,10,3,8])).
% 3.98/4.11 cnf(457,plain,
% 3.98/4.11 (~P2(f2(a4,x4571),f2(a3,a3),a3)+P2(f2(f2(a4,x4572),a4),a3,f2(a4,x4571))),
% 3.98/4.11 inference(scs_inference,[],[163,17])).
% 3.98/4.11 cnf(512,plain,
% 3.98/4.11 (~E(f2(a4,a4),a3)),
% 3.98/4.11 inference(scs_inference,[],[14,13,17,10])).
% 3.98/4.11 cnf(534,plain,
% 3.98/4.11 (~P2(f2(x5341,x5342),x5341,f2(a4,a4))),
% 3.98/4.11 inference(scs_inference,[],[44,512,19])).
% 3.98/4.11 cnf(622,plain,
% 3.98/4.11 (~P2(f2(a4,a4),f2(a3,a3),a3)),
% 3.98/4.11 inference(scs_inference,[],[534,13,10,79,162,18,457])).
% 3.98/4.11 cnf(674,plain,
% 3.98/4.11 (~E(f2(f2(a4,a4),f2(a3,x6741)),a3)),
% 3.98/4.11 inference(scs_inference,[],[622,384,10])).
% 3.98/4.11 cnf(677,plain,
% 3.98/4.11 (~E(f2(f2(a4,a4),f2(a3,x6771)),f2(a3,x6772))),
% 3.98/4.11 inference(scs_inference,[],[334,674,3])).
% 3.98/4.11 cnf(705,plain,
% 3.98/4.11 (~P2(f2(a3,x7051),x7052,f2(f2(a4,a4),f2(a3,x7053)))),
% 3.98/4.11 inference(scs_inference,[],[677,389,19])).
% 3.98/4.11 cnf(737,plain,
% 3.98/4.11 (~E(a3,f2(f2(a4,a4),f2(a3,x7371)))),
% 3.98/4.11 inference(scs_inference,[],[705,44,10])).
% 3.98/4.11 cnf(780,plain,
% 3.98/4.11 (~P1(f2(f2(a4,a4),f2(a3,x7801)),a3)),
% 3.98/4.11 inference(scs_inference,[],[737,12,15])).
% 3.98/4.11 cnf(820,plain,
% 3.98/4.11 (~P2(a4,f2(a4,x8201),f2(a4,x8201))),
% 3.98/4.11 inference(scs_inference,[],[780,44,13,342,20])).
% 3.98/4.11 cnf(828,plain,
% 3.98/4.11 (~P2(f2(a3,a3),x8281,f2(a4,f2(a3,a3)))),
% 3.98/4.11 inference(scs_inference,[],[780,44,13,342,20,164,18])).
% 3.98/4.11 cnf(832,plain,
% 3.98/4.11 (P2(x8321,x8322,f2(x8321,x8322))),
% 3.98/4.11 inference(rename_variables,[],[13])).
% 3.98/4.11 cnf(834,plain,
% 3.98/4.11 (P2(f2(a3,x8341),x8342,a3)),
% 3.98/4.11 inference(rename_variables,[],[385])).
% 3.98/4.11 cnf(835,plain,
% 3.98/4.11 ($false),
% 3.98/4.11 inference(scs_inference,[],[780,828,820,44,13,832,385,834,342,255,9,10,20]),
% 3.98/4.11 ['proof']).
% 3.98/4.11 % SZS output end Proof
% 3.98/4.11 % Total time :3.500000s
%------------------------------------------------------------------------------