%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET014-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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 14:20:01 EDT 2024
% Result : Unsatisfiable 117.22s 117.39s
% Output : CNFRefutation 117.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET014-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jun 23 18:06:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.61 start to proof:theBenchmark
% 117.22/117.38 %-------------------------------------------
% 117.22/117.38 % File :CSE---1.7
% 117.22/117.38 % Problem :theBenchmark
% 117.22/117.38 % Transform :cnf
% 117.22/117.38 % Format :tptp:raw
% 117.22/117.38 % Command :java -jar mcs_scs.jar %d %s
% 117.22/117.38
% 117.22/117.38 % Result :Theorem 116.610000s
% 117.22/117.38 % Output :CNFRefutation 116.610000s
% 117.22/117.38 %-------------------------------------------
% 117.22/117.39 %------------------------------------------------------------------------------
% 117.22/117.39 % File : SET014-2 : TPTP v8.2.0. Bugfixed v2.1.0.
% 117.22/117.39 % Domain : Set Theory
% 117.22/117.39 % Problem : Union of subsets is a subset
% 117.22/117.39 % Version : [MOW76] axioms : Especial.
% 117.22/117.39 % English : If A and B are contained in C then the union of A and B is also.
% 117.22/117.39
% 117.22/117.39 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 117.22/117.39 % : [WB87] Wang & Bledsoe (1987), Hierarchical Deduction
% 117.22/117.39 % Source : [ANL]
% 117.22/117.39 % Names : S4 [MOW76]
% 117.22/117.39 % : subset.ver1.in [ANL]
% 117.22/117.39 % : EST-S4 [WB87]
% 117.22/117.39
% 117.22/117.39 % Status : Unsatisfiable
% 117.22/117.39 % Rating : 0.08 v8.2.0, 0.14 v7.5.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0, 0.00 v2.4.0, 0.20 v2.3.0, 0.33 v2.2.1, 0.00 v2.1.0
% 117.22/117.39 % Syntax : Number of clauses : 24 ( 6 unt; 3 nHn; 18 RR)
% 117.22/117.39 % Number of literals : 48 ( 0 equ; 24 neg)
% 117.22/117.39 % Maximal clause size : 3 ( 2 avg)
% 117.22/117.39 % Maximal term depth : 2 ( 1 avg)
% 117.22/117.39 % Number of predicates : 4 ( 4 usr; 0 prp; 2-2 aty)
% 117.22/117.39 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 117.22/117.39 % Number of variables : 48 ( 5 sgn)
% 117.22/117.39 % SPC : CNF_UNS_RFO_NEQ_NHN
% 117.22/117.39
% 117.22/117.39 % Comments :
% 117.22/117.39 % Bugfixes : v2.1.0 - Bugfix in SET002-0.eq
% 117.22/117.39 %------------------------------------------------------------------------------
% 117.22/117.39 %----Include set axioms
% 117.22/117.39 include('Axioms/SET002-0.ax').
% 117.22/117.39 %------------------------------------------------------------------------------
% 117.22/117.39 cnf(a_subset_of_c,hypothesis,
% 117.22/117.39 subset(as,cs) ).
% 117.22/117.39
% 117.22/117.39 cnf(b_subset_of_c,hypothesis,
% 117.22/117.39 subset(bs,cs) ).
% 117.22/117.39
% 117.22/117.39 cnf(prove_a_union_b_subset_of_c,negated_conjecture,
% 117.22/117.39 ~ subset(union(as,bs),cs) ).
% 117.22/117.39
% 117.22/117.39 %------------------------------------------------------------------------------
% 117.22/117.39 %-------------------------------------------
% 117.22/117.39 % Proof found
% 117.22/117.39 % SZS status Theorem for theBenchmark
% 117.22/117.39 % SZS output start Proof
% 117.22/117.40 %ClaNum:24(EqnAxiom:0)
% 117.22/117.40 %VarNum:97(SingletonVarNum:48)
% 117.22/117.40 %MaxLitNum:3
% 117.22/117.40 %MaxfuncDepth:1
% 117.22/117.40 %SharedTerms:8
% 117.22/117.40 %goalClause: 6
% 117.22/117.40 %singleGoalClaCount:1
% 117.22/117.40 [1]P1(a1,a2)
% 117.22/117.40 [2]P1(a3,a2)
% 117.22/117.40 [6]~P1(f6(a1,a3),a2)
% 117.22/117.40 [3]P2(x31,x31)
% 117.22/117.40 [4]P3(x41,x41)
% 117.22/117.40 [5]~P4(x51,a5)
% 117.22/117.40 [8]~P2(x82,x81)+P1(x81,x82)
% 117.22/117.40 [9]~P2(x91,x92)+P1(x91,x92)
% 117.22/117.40 [10]~P2(x102,x101)+P2(x101,x102)
% 117.22/117.40 [11]~P3(x112,x111)+P3(x111,x112)
% 117.22/117.40 [7]P4(x71,x72)+P4(x71,f4(x72))
% 117.22/117.40 [12]P1(x121,x122)+P4(f7(x121,x122),x121)
% 117.22/117.40 [13]~P4(x131,x132)+~P4(x131,f4(x132))
% 117.22/117.40 [22]P1(x221,x222)+~P4(f7(x221,x222),x222)
% 117.22/117.40 [18]~P4(x181,x183)+P4(x181,f6(x182,x183))
% 117.22/117.40 [19]~P4(x191,x192)+P4(x191,f6(x192,x193))
% 117.22/117.40 [20]P4(x201,x202)+~P4(x201,f8(x203,x202))
% 117.22/117.40 [21]P4(x211,x212)+~P4(x211,f8(x212,x213))
% 117.22/117.40 [15]~P1(x151,x152)+~P1(x152,x151)+P2(x151,x152)
% 117.22/117.40 [14]~P1(x143,x142)+P4(x141,x142)+~P4(x141,x143)
% 117.22/117.40 [16]~P2(x161,x163)+P2(x161,x162)+~P2(x163,x162)
% 117.22/117.40 [17]~P3(x171,x173)+P3(x171,x172)+~P3(x173,x172)
% 117.22/117.40 [23]~P4(x231,x233)+~P4(x231,x232)+P4(x231,f8(x232,x233))
% 117.22/117.40 [24]P4(x241,x242)+P4(x241,x243)+~P4(x241,f6(x243,x242))
% 117.22/117.40 %EqnAxiom
% 117.22/117.40
% 117.22/117.40 %-------------------------------------------
% 117.22/117.41 cnf(29,plain,
% 117.22/117.41 (P1(a5,x291)),
% 117.22/117.41 inference(scs_inference,[],[6,5,8,9,12])).
% 117.22/117.41 cnf(39,plain,
% 117.22/117.41 (P4(x391,f4(f8(x392,a5)))),
% 117.22/117.41 inference(scs_inference,[],[5,7,20])).
% 117.22/117.41 cnf(40,plain,
% 117.22/117.41 (~P4(x401,f8(x402,a5))),
% 117.22/117.41 inference(scs_inference,[],[39,13])).
% 117.22/117.41 cnf(45,plain,
% 117.22/117.41 (P4(x451,f6(f4(a5),x452))),
% 117.22/117.41 inference(scs_inference,[],[5,19,7])).
% 117.22/117.41 cnf(46,plain,
% 117.22/117.41 (P4(x461,f4(a5))),
% 117.22/117.41 inference(scs_inference,[],[5,45,24])).
% 117.22/117.41 cnf(55,plain,
% 117.22/117.41 (~P4(x551,f8(a5,x552))),
% 117.22/117.41 inference(scs_inference,[],[46,21,13])).
% 117.22/117.41 cnf(56,plain,
% 117.22/117.41 (P1(f8(a5,x561),x562)),
% 117.22/117.41 inference(scs_inference,[],[55,12])).
% 117.22/117.41 cnf(62,plain,
% 117.22/117.41 (~P4(x621,f6(a5,a5))),
% 117.22/117.41 inference(scs_inference,[],[29,5,14,24])).
% 117.22/117.41 cnf(63,plain,
% 117.22/117.41 (P1(f6(a5,a5),x631)),
% 117.22/117.41 inference(scs_inference,[],[62,12])).
% 117.22/117.41 cnf(66,plain,
% 117.22/117.41 (P2(a5,f6(a5,a5))),
% 117.22/117.41 inference(scs_inference,[],[29,62,12,15])).
% 117.22/117.41 cnf(106,plain,
% 117.22/117.41 (P2(f6(a5,a5),f8(a5,x1061))),
% 117.22/117.41 inference(scs_inference,[],[63,56,15])).
% 117.22/117.41 cnf(116,plain,
% 117.22/117.41 (P2(f6(a5,a5),a5)),
% 117.22/117.41 inference(scs_inference,[],[63,29,15])).
% 117.22/117.41 cnf(152,plain,
% 117.22/117.41 (~P4(x1521,f4(f4(a5)))),
% 117.22/117.41 inference(scs_inference,[],[5,7,13])).
% 117.22/117.41 cnf(153,plain,
% 117.22/117.41 (P4(x1531,f6(x1532,f4(a5)))),
% 117.22/117.41 inference(scs_inference,[],[152,7,18])).
% 117.22/117.41 cnf(154,plain,
% 117.22/117.41 (P4(x1541,f4(f8(a5,x1542)))),
% 117.22/117.41 inference(scs_inference,[],[5,7,21])).
% 117.22/117.41 cnf(155,plain,
% 117.22/117.41 (P4(x1551,f4(f6(a5,a5)))),
% 117.22/117.41 inference(scs_inference,[],[5,7,24])).
% 117.22/117.41 cnf(160,plain,
% 117.22/117.41 (~P4(x1601,f8(f8(a5,x1602),x1603))),
% 117.22/117.41 inference(scs_inference,[],[154,13,21])).
% 117.22/117.41 cnf(161,plain,
% 117.22/117.41 (P1(f4(f6(x1611,f4(a5))),x1612)),
% 117.22/117.41 inference(scs_inference,[],[153,13,12])).
% 117.22/117.41 cnf(204,plain,
% 117.22/117.41 (~P1(f4(f8(a5,x2041)),f4(f4(f8(a5,x2041))))),
% 117.22/117.41 inference(scs_inference,[],[154,13,14])).
% 117.22/117.41 cnf(216,plain,
% 117.22/117.41 (~P4(f7(f6(a1,a3),a2),f4(f6(a1,a3)))),
% 117.22/117.41 inference(scs_inference,[],[6,12,13])).
% 117.22/117.41 cnf(246,plain,
% 117.22/117.41 (~P1(f6(a1,a3),a5)),
% 117.22/117.41 inference(scs_inference,[],[6,5,12,14])).
% 117.22/117.41 cnf(247,plain,
% 117.22/117.41 (~P2(a5,f6(a1,a3))),
% 117.22/117.41 inference(scs_inference,[],[246,8])).
% 117.22/117.41 cnf(251,plain,
% 117.22/117.41 (~P4(x2511,f4(f6(x2512,f4(f6(a5,a5)))))),
% 117.22/117.41 inference(scs_inference,[],[155,18,13])).
% 117.22/117.41 cnf(331,plain,
% 117.22/117.41 (~P1(f6(f6(x3311,f4(a5)),x3312),f8(x3313,a5))),
% 117.22/117.41 inference(scs_inference,[],[153,40,19,14])).
% 117.22/117.41 cnf(342,plain,
% 117.22/117.41 (~P4(f7(f6(a1,a3),a2),f8(x3421,a2))),
% 117.22/117.41 inference(scs_inference,[],[6,20,22])).
% 117.22/117.41 cnf(343,plain,
% 117.22/117.41 (~P4(f7(f6(a1,a3),a2),a2)),
% 117.22/117.41 inference(scs_inference,[],[342,154,23])).
% 117.22/117.41 cnf(447,plain,
% 117.22/117.41 (~P4(x4471,f8(f6(f6(a5,a5),f6(a5,a5)),x4472))),
% 117.32/117.41 inference(scs_inference,[],[62,21,24])).
% 117.32/117.41 cnf(448,plain,
% 117.32/117.41 (P4(f7(f6(a1,a3),a2),f4(a2))),
% 117.32/117.41 inference(scs_inference,[],[6,22,7])).
% 117.32/117.41 cnf(456,plain,
% 117.32/117.41 (~P1(f4(a2),a2)),
% 117.32/117.41 inference(scs_inference,[],[6,448,22,14])).
% 117.32/117.41 cnf(562,plain,
% 117.32/117.41 (~P1(f4(f6(a5,a5)),f8(x5621,a2))),
% 117.32/117.41 inference(scs_inference,[],[342,155,14])).
% 117.32/117.41 cnf(569,plain,
% 117.32/117.41 (~P1(f4(f8(x5691,a5)),f8(x5692,a2))),
% 117.32/117.41 inference(scs_inference,[],[342,562,39,8,9,14])).
% 117.32/117.41 cnf(577,plain,
% 117.32/117.41 (~P1(f4(f8(a5,x5771)),f8(x5772,a2))),
% 117.32/117.41 inference(scs_inference,[],[342,569,154,8,9,14])).
% 117.32/117.41 cnf(585,plain,
% 117.32/117.41 (~P1(f4(a5),f8(x5851,a2))),
% 117.32/117.41 inference(scs_inference,[],[342,577,46,8,9,14])).
% 117.32/117.41 cnf(611,plain,
% 117.32/117.41 (~P1(f4(f6(a5,a5)),a2)),
% 117.32/117.41 inference(scs_inference,[],[343,155,14])).
% 117.32/117.41 cnf(619,plain,
% 117.32/117.41 (~P1(f4(f8(x6191,a5)),a2)),
% 117.32/117.41 inference(scs_inference,[],[343,611,39,8,9,14])).
% 117.32/117.41 cnf(627,plain,
% 117.32/117.41 (~P1(f4(f8(a5,x6271)),a2)),
% 117.32/117.41 inference(scs_inference,[],[343,619,154,8,9,14])).
% 117.32/117.41 cnf(635,plain,
% 117.32/117.41 (~P1(f4(a5),a2)),
% 117.32/117.41 inference(scs_inference,[],[343,627,46,8,9,14])).
% 117.32/117.41 cnf(907,plain,
% 117.32/117.41 (~P1(f4(a2),f6(a5,a5))),
% 117.32/117.41 inference(scs_inference,[],[62,448,14])).
% 117.32/117.41 cnf(1667,plain,
% 117.32/117.41 (~P4(x16671,a1)+P4(x16671,a2)),
% 117.32/117.41 inference(scs_inference,[],[1,66,247,16,14])).
% 117.32/117.41 cnf(1673,plain,
% 117.32/117.41 (~P4(x16731,a1)+~P4(x16731,f4(a2))),
% 117.32/117.41 inference(scs_inference,[],[1,66,247,16,14,18,19,13])).
% 117.32/117.41 cnf(1677,plain,
% 117.32/117.41 (~P4(x16771,a3)+P4(x16771,a2)),
% 117.32/117.41 inference(scs_inference,[],[2,14])).
% 117.32/117.41 cnf(1709,plain,
% 117.32/117.41 (P4(x17091,a2)+P4(x17091,f4(a1))),
% 117.32/117.41 inference(scs_inference,[],[1667,7])).
% 117.32/117.41 cnf(1719,plain,
% 117.32/117.41 (P4(x17191,a2)+~P4(x17191,f8(x17192,a1))),
% 117.32/117.41 inference(scs_inference,[],[1667,20])).
% 117.32/117.41 cnf(1792,plain,
% 117.32/117.41 (P4(x17921,a2)+P4(x17921,f4(a3))),
% 117.32/117.41 inference(scs_inference,[],[1677,7])).
% 117.32/117.41 cnf(1867,plain,
% 117.32/117.41 (~P4(x18671,f4(a2))+P4(x18671,f4(a1))),
% 117.32/117.41 inference(scs_inference,[],[1673,7])).
% 117.32/117.41 cnf(1948,plain,
% 117.32/117.41 (~P1(f4(a1),f6(a5,a5))+P4(x19481,a2)),
% 117.32/117.41 inference(scs_inference,[],[62,1709,14])).
% 117.32/117.41 cnf(1949,plain,
% 117.32/117.41 (~P2(f4(a1),f6(a5,a5))+P4(x19491,a2)),
% 117.32/117.41 inference(scs_inference,[],[1948,9])).
% 117.32/117.41 cnf(1950,plain,
% 117.32/117.41 (~P2(f6(a5,a5),f4(a1))+P4(x19501,a2)),
% 117.32/117.41 inference(scs_inference,[],[1949,10])).
% 117.32/117.41 cnf(1951,plain,
% 117.32/117.41 (~P2(a5,f4(a1))+P4(x19511,a2)),
% 117.32/117.41 inference(scs_inference,[],[116,1950,16])).
% 117.32/117.41 cnf(1952,plain,
% 117.32/117.41 (~P2(f4(a1),a5)+P4(x19521,a2)),
% 117.32/117.41 inference(scs_inference,[],[1951,10])).
% 117.32/117.41 cnf(1953,plain,
% 117.32/117.41 (~P1(f4(a1),a5)+P4(x19531,a2)),
% 117.32/117.41 inference(scs_inference,[],[29,1952,15])).
% 117.32/117.41 cnf(1954,plain,
% 117.32/117.41 (P4(f7(f4(a1),a5),f4(a1))+P4(x19541,a2)),
% 117.32/117.41 inference(scs_inference,[],[1953,12])).
% 117.32/117.41 cnf(2010,plain,
% 117.32/117.41 (~P1(f4(a3),a5)+P4(x20101,a2)),
% 117.32/117.41 inference(scs_inference,[],[5,1792,14])).
% 117.32/117.41 cnf(2011,plain,
% 117.32/117.41 (~P2(a5,f4(a3))+P4(x20111,a2)),
% 117.32/117.41 inference(scs_inference,[],[2010,8])).
% 117.32/117.41 cnf(2012,plain,
% 117.32/117.41 (~P2(f4(a3),a5)+P4(x20121,a2)),
% 117.32/117.41 inference(scs_inference,[],[2011,10])).
% 117.32/117.41 cnf(2013,plain,
% 117.32/117.42 (~P2(f4(a3),a5)),
% 117.32/117.42 inference(scs_inference,[],[635,2012,22])).
% 117.32/117.42 cnf(2014,plain,
% 117.32/117.42 (~P1(f4(a3),a5)),
% 117.32/117.42 inference(scs_inference,[],[29,2013,15])).
% 117.32/117.42 cnf(2017,plain,
% 117.32/117.42 (~P1(f4(a3),f6(a5,a5))+P4(x20171,a2)),
% 117.32/117.42 inference(scs_inference,[],[62,1792,14])).
% 117.32/117.42 cnf(2018,plain,
% 117.32/117.42 (~P2(f4(a3),f6(a5,a5))+P4(x20181,a2)),
% 117.32/117.42 inference(scs_inference,[],[2017,9])).
% 117.32/117.42 cnf(2019,plain,
% 117.32/117.42 (~P2(f6(a5,a5),f4(a3))+P4(x20191,a2)),
% 117.32/117.42 inference(scs_inference,[],[2018,10])).
% 117.32/117.42 cnf(2020,plain,
% 117.32/117.42 (~P2(f6(a5,a5),f4(a3))),
% 117.32/117.42 inference(scs_inference,[],[456,2019,22])).
% 117.32/117.42 cnf(2047,plain,
% 117.32/117.42 (~P2(f8(a5,x20471),f4(a3))),
% 117.32/117.42 inference(scs_inference,[],[106,2020,16])).
% 117.32/117.42 cnf(2259,plain,
% 117.32/117.42 (~P4(f7(f4(a5),a2),f8(x22591,a1))),
% 117.32/117.42 inference(scs_inference,[],[635,1719,22])).
% 117.32/117.42 cnf(2475,plain,
% 117.32/117.42 (P4(f7(f4(a2),f6(a5,a5)),f4(a1))),
% 117.32/117.42 inference(scs_inference,[],[907,1867,12])).
% 117.32/117.42 cnf(2667,plain,
% 117.32/117.42 (P4(f7(f4(a1),a5),f4(a1))),
% 117.32/117.42 inference(scs_inference,[],[343,1954])).
% 117.32/117.42 cnf(2669,plain,
% 117.32/117.42 (~P4(f7(f6(a1,a3),a2),a1)),
% 117.32/117.42 inference(scs_inference,[],[343,1667])).
% 117.32/117.42 cnf(2671,plain,
% 117.32/117.42 (~P4(f7(f6(a1,a3),a2),a3)),
% 117.32/117.42 inference(scs_inference,[],[343,1667,1677])).
% 117.32/117.42 cnf(2823,plain,
% 117.32/117.42 (P4(f7(f4(a3),a5),f4(a3))),
% 117.32/117.42 inference(scs_inference,[],[2014,2667,2259,585,7,21,20,19,18,13,22,12])).
% 117.32/117.42 cnf(2914,plain,
% 117.32/117.42 (P4(f7(f6(a1,a3),a2),f6(a1,a3))),
% 117.32/117.42 inference(scs_inference,[],[39,160,204,2823,216,9,8,12,22,13,7])).
% 117.32/117.42 cnf(3058,plain,
% 117.32/117.42 ($false),
% 117.32/117.42 inference(scs_inference,[],[46,29,153,152,2047,2914,2475,2669,447,251,331,161,2671,9,8,12,22,13,10,7,15,23,24]),
% 117.32/117.42 ['proof']).
% 117.32/117.42 % SZS output end Proof
% 117.32/117.42 % Total time :116.610000s
%------------------------------------------------------------------------------