%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN012-3 : 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 : n026.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 0.81s 0.87s
% Output : CNFRefutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HEN012-3 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 05:22:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 0.81/0.86 %-------------------------------------------
% 0.81/0.86 % File :CSE---1.7
% 0.81/0.86 % Problem :theBenchmark
% 0.81/0.86 % Transform :cnf
% 0.81/0.86 % Format :tptp:raw
% 0.81/0.86 % Command :java -jar mcs_scs.jar %d %s
% 0.81/0.86
% 0.81/0.86 % Result :Theorem 0.270000s
% 0.81/0.86 % Output :CNFRefutation 0.270000s
% 0.81/0.86 %-------------------------------------------
% 0.81/0.87 %--------------------------------------------------------------------------
% 0.81/0.87 % File : HEN012-3 : TPTP v8.2.0. Released v1.0.0.
% 0.81/0.87 % Domain : Henkin Models
% 0.81/0.87 % Problem : X <= X
% 0.81/0.87 % Version : [MOW76] axioms.
% 0.81/0.87 % English :
% 0.81/0.87
% 0.81/0.87 % Refs :
% 0.81/0.87 % Source : [ANL]
% 0.81/0.87 % Names : new.ver2.in [ANL]
% 0.81/0.87
% 0.81/0.87 % Status : Unsatisfiable
% 0.81/0.87 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.22 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
% 0.81/0.87 % Syntax : Number of clauses : 8 ( 5 unt; 0 nHn; 4 RR)
% 0.81/0.87 % Number of literals : 12 ( 3 equ; 5 neg)
% 0.81/0.87 % Maximal clause size : 3 ( 1 avg)
% 0.81/0.87 % Maximal term depth : 3 ( 1 avg)
% 0.81/0.87 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 0.81/0.87 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 0.81/0.87 % Number of variables : 13 ( 3 sgn)
% 0.81/0.87 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.81/0.87
% 0.81/0.87 % Comments :
% 0.81/0.87 %--------------------------------------------------------------------------
% 0.81/0.87 %----Include Henkin model axioms for equality formulation
% 0.81/0.87 include('Axioms/HEN002-0.ax').
% 0.81/0.87 %--------------------------------------------------------------------------
% 0.81/0.87 cnf(prove_a_LE_a,negated_conjecture,
% 0.81/0.87 ~ less_equal(a,a) ).
% 0.81/0.87
% 0.81/0.87 %--------------------------------------------------------------------------
% 0.81/0.87 %-------------------------------------------
% 0.81/0.87 % Proof found
% 0.81/0.87 % SZS status Theorem for theBenchmark
% 0.81/0.87 % SZS output start Proof
% 0.81/0.87 %ClaNum:15(EqnAxiom:7)
% 0.81/0.87 %VarNum:26(SingletonVarNum:13)
% 0.81/0.87 %MaxLitNum:3
% 0.81/0.87 %MaxfuncDepth:2
% 0.81/0.87 %SharedTerms:4
% 0.81/0.87 %goalClause: 12
% 0.81/0.87 %singleGoalClaCount:1
% 0.81/0.87 [12]~P1(a3,a3)
% 0.81/0.87 [8]P1(x81,a1)
% 0.81/0.87 [9]P1(a4,x91)
% 0.81/0.87 [10]P1(f2(x101,x102),x101)
% 0.81/0.87 [11]P1(f2(f2(x111,x112),f2(x113,x112)),f2(f2(x111,x113),x112))
% 0.81/0.87 [13]~P1(x131,x132)+E(f2(x131,x132),a4)
% 0.81/0.87 [14]P1(x141,x142)+~E(f2(x141,x142),a4)
% 0.81/0.87 [15]~P1(x152,x151)+~P1(x151,x152)+E(x151,x152)
% 0.81/0.87 %EqnAxiom
% 0.81/0.87 [1]E(x11,x11)
% 0.81/0.87 [2]E(x22,x21)+~E(x21,x22)
% 0.81/0.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.81/0.87 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 0.81/0.87 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 0.81/0.87 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 0.81/0.87 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 0.81/0.87
% 0.81/0.87 %-------------------------------------------
% 0.81/0.87 cnf(17,plain,
% 0.81/0.87 (P1(a4,x171)),
% 0.81/0.87 inference(rename_variables,[],[9])).
% 0.81/0.87 cnf(20,plain,
% 0.81/0.87 (~P1(a3,a4)),
% 0.81/0.87 inference(scs_inference,[],[12,8,9,17,6,7,15])).
% 0.81/0.87 cnf(23,plain,
% 0.81/0.87 (E(f2(a4,x231),a4)),
% 0.81/0.87 inference(scs_inference,[],[10,9,15])).
% 0.81/0.87 cnf(24,plain,
% 0.81/0.87 (P1(f2(x241,x242),x241)),
% 0.81/0.88 inference(rename_variables,[],[10])).
% 0.81/0.88 cnf(27,plain,
% 0.81/0.88 (P1(f2(f2(a4,x271),x272),a4)),
% 0.81/0.88 inference(scs_inference,[],[10,24,9,15,7])).
% 0.81/0.88 cnf(28,plain,
% 0.81/0.88 (P1(f2(x281,x282),x281)),
% 0.81/0.88 inference(rename_variables,[],[10])).
% 0.81/0.88 cnf(31,plain,
% 0.81/0.88 (E(a4,f2(a4,x311))),
% 0.81/0.88 inference(scs_inference,[],[12,10,24,28,9,15,7,6,2])).
% 0.81/0.88 cnf(32,plain,
% 0.81/0.88 (E(f2(a4,x321),f2(a4,x322))),
% 0.81/0.88 inference(scs_inference,[],[23,31,3])).
% 0.81/0.88 cnf(33,plain,
% 0.81/0.88 (E(f2(f2(a4,x331),x332),a4)),
% 0.81/0.88 inference(scs_inference,[],[27,23,31,9,3,15])).
% 0.81/0.88 cnf(36,plain,
% 0.81/0.88 (P1(f2(f2(a4,x361),x362),f2(a4,x363))),
% 0.81/0.88 inference(scs_inference,[],[27,23,31,9,3,15,7])).
% 0.81/0.88 cnf(38,plain,
% 0.81/0.88 (P1(f2(a4,x381),x382)),
% 0.81/0.88 inference(scs_inference,[],[27,20,23,31,9,3,15,7,6,14])).
% 0.81/0.88 cnf(40,plain,
% 0.81/0.88 (E(a4,f2(f2(a4,x401),x402))),
% 0.81/0.88 inference(scs_inference,[],[27,20,23,31,9,3,15,7,6,14,2])).
% 0.81/0.88 cnf(41,plain,
% 0.81/0.88 (E(f2(f2(a4,x411),x412),f2(f2(a4,x413),x414))),
% 0.81/0.88 inference(scs_inference,[],[33,40,3])).
% 0.81/0.88 cnf(42,plain,
% 0.81/0.88 (E(f2(f2(a4,x421),x422),f2(a4,x423))),
% 0.81/0.88 inference(scs_inference,[],[38,36,33,40,3,15])).
% 0.81/0.88 cnf(44,plain,
% 0.81/0.88 (P1(f2(a4,x441),x442)),
% 0.81/0.88 inference(rename_variables,[],[38])).
% 0.81/0.88 cnf(47,plain,
% 0.81/0.88 (~E(f2(a4,x471),a3)),
% 0.81/0.88 inference(scs_inference,[],[12,38,44,36,27,33,40,3,15,7,6])).
% 0.81/0.88 cnf(50,plain,
% 0.81/0.88 (~P1(a3,f2(a4,x501))),
% 0.81/0.88 inference(scs_inference,[],[38,47,15])).
% 0.81/0.88 cnf(56,plain,
% 0.81/0.88 (E(f2(f2(f2(a4,x561),x562),a1),a4)),
% 0.81/0.88 inference(scs_inference,[],[8,41,13,6])).
% 0.81/0.88 cnf(64,plain,
% 0.81/0.88 (~E(f2(f2(f2(a4,x641),x642),x643),a3)),
% 0.81/0.88 inference(scs_inference,[],[38,42,50,56,10,31,2,3,7,15,6])).
% 0.81/0.88 cnf(69,plain,
% 0.81/0.88 (E(f2(x691,f2(a4,x692)),f2(x691,f2(a4,x693)))),
% 0.81/0.88 inference(scs_inference,[],[32,2,5])).
% 0.81/0.88 cnf(70,plain,
% 0.81/0.88 (P1(f2(f2(x701,x702),f2(a4,x703)),f2(f2(x701,a4),x702))),
% 0.81/0.88 inference(scs_inference,[],[69,11,6])).
% 0.81/0.88 cnf(72,plain,
% 0.81/0.88 (E(f2(x721,f2(a4,x722)),f2(x721,f2(a4,x723)))),
% 0.81/0.88 inference(rename_variables,[],[69])).
% 0.81/0.88 cnf(73,plain,
% 0.81/0.88 (P1(f2(f2(x731,f2(a4,x732)),f2(a4,x733)),f2(f2(x731,a4),f2(a4,x734)))),
% 0.81/0.88 inference(scs_inference,[],[69,72,11,6,7])).
% 0.81/0.88 cnf(75,plain,
% 0.81/0.88 (E(a4,f2(f2(x751,x752),x751))),
% 0.81/0.88 inference(scs_inference,[],[10,2,13])).
% 0.81/0.88 cnf(76,plain,
% 0.81/0.88 (E(f2(f2(x761,x762),x761),a4)),
% 0.81/0.88 inference(scs_inference,[],[75,2])).
% 0.81/0.88 cnf(77,plain,
% 0.81/0.88 (E(f2(f2(a4,x771),x772),f2(f2(x773,x774),x773))),
% 0.81/0.88 inference(scs_inference,[],[75,33,2,3])).
% 0.81/0.88 cnf(80,plain,
% 0.81/0.88 (E(f2(f2(x801,x802),x801),f2(f2(a4,x803),x804))),
% 0.81/0.88 inference(scs_inference,[],[77,2])).
% 0.81/0.88 cnf(84,plain,
% 0.81/0.88 (E(f2(f2(f2(x841,x842),x841),x843),a4)),
% 0.81/0.88 inference(scs_inference,[],[10,76,77,9,75,2,3,7,15])).
% 0.81/0.88 cnf(87,plain,
% 0.81/0.88 (~E(f2(f2(f2(x871,x872),x871),x873),a3)),
% 0.81/0.88 inference(scs_inference,[],[10,76,20,77,9,75,2,3,7,15,6])).
% 0.81/0.88 cnf(88,plain,
% 0.81/0.88 (P1(f2(f2(x881,x882),x881),x883)),
% 0.81/0.88 inference(scs_inference,[],[10,76,20,77,9,75,2,3,7,15,6,14])).
% 0.81/0.88 cnf(91,plain,
% 0.81/0.88 (E(a4,f2(f2(f2(x911,x912),x911),x913))),
% 0.81/0.88 inference(scs_inference,[],[84,2])).
% 0.81/0.88 cnf(93,plain,
% 0.81/0.88 (P1(f2(f2(x931,x932),x931),x933)),
% 0.81/0.88 inference(rename_variables,[],[88])).
% 0.81/0.88 cnf(96,plain,
% 0.81/0.88 (E(f2(f2(x961,x962),x961),f2(a4,x963))),
% 0.81/0.88 inference(scs_inference,[],[88,87,80,84,42,2,15,3])).
% 0.81/0.88 cnf(98,plain,
% 0.81/0.88 (~E(f2(f2(x981,x982),x981),a3)),
% 0.81/0.88 inference(scs_inference,[],[88,93,12,87,80,84,42,2,15,3,6])).
% 0.81/0.88 cnf(100,plain,
% 0.81/0.88 (P1(f2(f2(x1001,x1001),f2(a4,x1002)),f2(f2(a4,x1003),x1004))),
% 0.81/0.88 inference(scs_inference,[],[88,93,12,70,87,80,84,42,2,15,3,6,7])).
% 0.81/0.88 cnf(104,plain,
% 0.81/0.88 (E(f2(a4,x1041),f2(f2(x1042,x1043),x1042))),
% 0.81/0.88 inference(scs_inference,[],[96,2])).
% 0.81/0.88 cnf(105,plain,
% 0.81/0.88 (~P1(a3,f2(f2(x1051,x1052),x1051))),
% 0.81/0.88 inference(scs_inference,[],[88,98,96,2,15])).
% 0.81/0.88 cnf(108,plain,
% 0.81/0.88 (E(f2(f2(f2(x1081,x1082),x1081),x1083),f2(a4,x1084))),
% 0.81/0.88 inference(scs_inference,[],[88,98,96,84,31,2,15,3])).
% 0.81/0.88 cnf(109,plain,
% 0.81/0.88 (~E(f2(f2(x1091,x1091),f2(a4,x1092)),a3)),
% 0.81/0.88 inference(scs_inference,[],[88,100,98,96,84,31,2,15,3,6])).
% 0.81/0.88 cnf(116,plain,
% 0.81/0.88 (E(f2(f2(x1161,x1161),f2(a4,x1162)),f2(f2(x1161,a4),x1161))),
% 0.81/0.88 inference(scs_inference,[],[88,70,108,2,15])).
% 0.81/0.88 cnf(120,plain,
% 0.81/0.88 (~E(f2(f2(x1201,x1201),f2(x1202,x1201)),a3)),
% 0.81/0.88 inference(scs_inference,[],[88,70,105,108,11,2,15,6])).
% 0.81/0.88 cnf(126,plain,
% 0.81/0.88 (E(f2(f2(x1261,a4),x1261),f2(f2(x1261,x1261),f2(a4,x1262)))),
% 0.81/0.88 inference(scs_inference,[],[116,2])).
% 0.81/0.88 cnf(127,plain,
% 0.81/0.88 (E(f2(f2(x1271,x1271),f2(x1272,x1271)),f2(f2(x1271,x1272),x1271))),
% 0.81/0.88 inference(scs_inference,[],[88,116,11,2,15])).
% 0.81/0.88 cnf(131,plain,
% 0.81/0.88 (E(f2(a4,x1311),f2(f2(x1312,x1312),f2(a4,x1313)))),
% 0.81/0.88 inference(scs_inference,[],[88,104,116,11,2,15,3])).
% 0.81/0.88 cnf(134,plain,
% 0.81/0.88 (E(f2(f2(x1341,x1341),f2(a4,x1342)),f2(a4,x1343))),
% 0.81/0.88 inference(scs_inference,[],[131,2])).
% 0.81/0.88 cnf(139,plain,
% 0.81/0.88 (E(a4,f2(f2(f2(a4,x1391),f2(a4,x1391)),f2(a4,x1392)))),
% 0.81/0.88 inference(scs_inference,[],[91,127,126,2,3])).
% 0.81/0.88 cnf(144,plain,
% 0.81/0.88 (E(f2(f2(f2(x1441,x1441),f2(a4,x1442)),x1443),f2(a4,x1444))),
% 0.81/0.88 inference(scs_inference,[],[10,38,134,91,127,126,2,3,7,15])).
% 0.81/0.88 cnf(149,plain,
% 0.81/0.88 (E(f2(a4,x1491),f2(f2(f2(x1492,x1492),f2(a4,x1493)),x1494))),
% 0.81/0.88 inference(scs_inference,[],[144,2])).
% 0.81/0.88 cnf(150,plain,
% 0.81/0.88 (E(f2(f2(f2(x1501,x1501),f2(a4,x1502)),x1503),a4)),
% 0.81/0.88 inference(scs_inference,[],[144,23,2,3])).
% 0.81/0.88 cnf(156,plain,
% 0.81/0.88 (P1(f2(f2(x1561,x1561),f2(a4,x1562)),x1563)),
% 0.81/0.88 inference(scs_inference,[],[150,14])).
% 0.81/0.88 cnf(162,plain,
% 0.81/0.88 (E(f2(f2(x1621,x1621),f2(a4,x1622)),f2(f2(x1623,x1624),x1623))),
% 0.81/0.88 inference(scs_inference,[],[120,150,104,134,14,2,15,3])).
% 0.81/0.88 cnf(167,plain,
% 0.81/0.88 (E(f2(f2(f2(a4,x1671),f2(a4,x1671)),f2(a4,x1672)),a4)),
% 0.81/0.88 inference(scs_inference,[],[139,2])).
% 0.81/0.88 cnf(174,plain,
% 0.81/0.88 (E(f2(f2(x1741,x1742),x1741),f2(f2(x1743,x1743),f2(a4,x1744)))),
% 0.81/0.88 inference(scs_inference,[],[162,2])).
% 0.81/0.88 cnf(179,plain,
% 0.81/0.88 (E(f2(f2(x1791,x1791),f2(a4,x1792)),f2(f2(x1793,x1793),f2(a4,x1794)))),
% 0.81/0.88 inference(scs_inference,[],[156,64,162,126,2,15,3])).
% 0.81/0.88 cnf(189,plain,
% 0.81/0.88 (P1(f2(x1891,x1891),f2(a4,x1892))),
% 0.81/0.88 inference(scs_inference,[],[156,109,179,167,15,3,14])).
% 0.81/0.88 cnf(191,plain,
% 0.81/0.88 (E(a4,f2(f2(x1911,x1911),f2(a4,x1912)))),
% 0.81/0.88 inference(scs_inference,[],[156,109,179,167,15,3,14,2])).
% 0.81/0.88 cnf(200,plain,
% 0.81/0.88 (P1(f2(x2001,x2001),f2(f2(f2(x2002,x2002),f2(a4,x2003)),x2004))),
% 0.81/0.88 inference(scs_inference,[],[189,149,7])).
% 0.81/0.88 cnf(205,plain,
% 0.81/0.88 (E(f2(x2051,f2(f2(x2052,x2052),f2(a4,x2053))),f2(x2051,a4))),
% 0.81/0.88 inference(scs_inference,[],[191,2,5])).
% 0.81/0.88 cnf(207,plain,
% 0.81/0.88 (P1(f2(f2(f2(a4,x2071),f2(a4,x2072)),f2(a4,x2073)),f2(f2(x2074,x2074),f2(a4,x2075)))),
% 0.81/0.88 inference(scs_inference,[],[73,205,174,2,7])).
% 0.81/0.88 cnf(211,plain,
% 0.81/0.88 (P1(f2(x2111,x2111),f2(f2(x2112,x2112),f2(a4,x2113)))),
% 0.81/0.88 inference(scs_inference,[],[200,179,7])).
% 0.81/0.88 cnf(221,plain,
% 0.81/0.88 (E(f2(f2(a4,x2211),x2212),f2(f2(a4,x2213),x2214))),
% 0.81/0.88 inference(rename_variables,[],[41])).
% 0.81/0.88 cnf(222,plain,
% 0.81/0.88 (E(f2(f2(f2(a4,x2221),f2(a4,x2222)),f2(a4,x2223)),f2(f2(a4,a4),f2(a4,x2224)))),
% 0.81/0.88 inference(scs_inference,[],[156,207,41,7,15])).
% 0.81/0.88 cnf(226,plain,
% 0.81/0.88 (E(f2(f2(a4,x2261),x2262),f2(f2(f2(a4,x2263),f2(a4,x2264)),f2(a4,x2265)))),
% 0.81/0.88 inference(scs_inference,[],[156,207,41,221,7,15,2,3])).
% 0.81/0.88 cnf(230,plain,
% 0.81/0.88 (E(f2(f2(f2(a4,x2301),f2(a4,x2302)),f2(a4,x2303)),a4)),
% 0.81/0.88 inference(scs_inference,[],[226,222,33,2,3])).
% 0.81/0.88 cnf(244,plain,
% 0.81/0.88 ($false),
% 0.81/0.88 inference(scs_inference,[],[12,211,230,191,9,2,3,7,15,14]),
% 0.81/0.88 ['proof']).
% 0.81/0.88 % SZS output end Proof
% 0.81/0.88 % Total time :0.270000s
%------------------------------------------------------------------------------