%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET005-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 : n025.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:19:57 EDT 2024
% Result : Unsatisfiable 70.26s 70.37s
% Output : CNFRefutation 70.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET005-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.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 : Sun Jun 23 14:32:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 70.26/70.36 %-------------------------------------------
% 70.26/70.36 % File :CSE---1.7
% 70.26/70.36 % Problem :theBenchmark
% 70.26/70.36 % Transform :cnf
% 70.26/70.36 % Format :tptp:raw
% 70.26/70.36 % Command :java -jar mcs_scs.jar %d %s
% 70.26/70.36
% 70.26/70.36 % Result :Theorem 69.700000s
% 70.26/70.36 % Output :CNFRefutation 69.700000s
% 70.26/70.36 %-------------------------------------------
% 70.26/70.37 %--------------------------------------------------------------------------
% 70.26/70.37 % File : SET005-1 : TPTP v8.2.0. Released v1.0.0.
% 70.26/70.37 % Domain : Set Theory
% 70.26/70.37 % Problem : Associativity of set intersection
% 70.26/70.37 % Version : [LS74] axioms.
% 70.26/70.37 % English :
% 70.26/70.37
% 70.26/70.37 % Refs : [LS74] Lawrence & Starkey (1974), Experimental Tests of Resol
% 70.26/70.37 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 70.26/70.37 % Source : [SPRFN]
% 70.26/70.37 % Names : ls108 [LS74]
% 70.26/70.37 % : ls108 [WM76]
% 70.26/70.37
% 70.26/70.37 % Status : Unsatisfiable
% 70.26/70.37 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.00 v3.1.0, 0.17 v2.7.0, 0.00 v2.1.0, 0.12 v2.0.0
% 70.26/70.37 % Syntax : Number of clauses : 16 ( 4 unt; 3 nHn; 13 RR)
% 70.26/70.37 % Number of literals : 38 ( 0 equ; 18 neg)
% 70.26/70.37 % Maximal clause size : 4 ( 2 avg)
% 70.26/70.37 % Maximal term depth : 2 ( 1 avg)
% 70.26/70.37 % Number of predicates : 4 ( 4 usr; 0 prp; 2-3 aty)
% 70.26/70.37 % Number of functors : 8 ( 8 usr; 6 con; 0-3 aty)
% 70.26/70.37 % Number of variables : 34 ( 2 sgn)
% 70.26/70.37 % SPC : CNF_UNS_RFO_NEQ_NHN
% 70.26/70.37
% 70.26/70.37 % Comments :
% 70.26/70.37 %--------------------------------------------------------------------------
% 70.26/70.37 %----Include the member and subset axioms
% 70.26/70.37 include('Axioms/SET001-0.ax').
% 70.26/70.37 %----Include the member and intersection axioms
% 70.26/70.37 include('Axioms/SET001-2.ax').
% 70.26/70.37 %--------------------------------------------------------------------------
% 70.26/70.37 cnf(a_intersection_b,axiom,
% 70.26/70.37 intersection(a,b,aIb) ).
% 70.26/70.37
% 70.26/70.37 cnf(b_intersection_c,axiom,
% 70.26/70.37 intersection(b,c,bIc) ).
% 70.26/70.37
% 70.26/70.37 cnf(a_intersection_bIc,axiom,
% 70.26/70.37 intersection(a,bIc,aIbIc) ).
% 70.26/70.37
% 70.26/70.37 cnf(prove_aIb_intersection_c_is_aIbIc,negated_conjecture,
% 70.26/70.37 ~ intersection(aIb,c,aIbIc) ).
% 70.26/70.37
% 70.26/70.37 %--------------------------------------------------------------------------
% 70.26/70.37 %-------------------------------------------
% 70.26/70.37 % Proof found
% 70.26/70.37 % SZS status Theorem for theBenchmark
% 70.26/70.37 % SZS output start Proof
% 70.26/70.37 %ClaNum:16(EqnAxiom:0)
% 70.26/70.37 %VarNum:90(SingletonVarNum:34)
% 70.26/70.37 %MaxLitNum:4
% 70.26/70.37 %MaxfuncDepth:1
% 70.26/70.37 %SharedTerms:10
% 70.26/70.37 %goalClause: 4
% 70.26/70.37 %singleGoalClaCount:1
% 70.26/70.37 [1]P1(a1,a2,a3)
% 70.26/70.37 [2]P1(a1,a5,a4)
% 70.26/70.37 [3]P1(a2,a6,a5)
% 70.26/70.37 [4]~P1(a3,a6,a4)
% 70.26/70.37 [5]~P2(x52,x51)+P3(x51,x52)
% 70.26/70.37 [6]~P2(x61,x62)+P3(x61,x62)
% 70.26/70.37 [7]P3(x71,x72)+P4(f7(x71,x72),x71)
% 70.26/70.37 [10]P3(x101,x102)+~P4(f7(x101,x102),x102)
% 70.26/70.37 [9]~P3(x91,x92)+~P3(x92,x91)+P2(x91,x92)
% 70.26/70.37 [8]~P3(x83,x82)+P4(x81,x82)+~P4(x81,x83)
% 70.26/70.37 [14]P1(x141,x142,x143)+P4(f8(x141,x142,x143),x143)+P4(f8(x141,x142,x143),x142)
% 70.26/70.37 [15]P1(x151,x152,x153)+P4(f8(x151,x152,x153),x153)+P4(f8(x151,x152,x153),x151)
% 70.26/70.37 [11]P4(x111,x112)+~P1(x114,x112,x113)+~P4(x111,x113)
% 70.26/70.37 [12]P4(x121,x122)+~P1(x122,x124,x123)+~P4(x121,x123)
% 70.26/70.37 [16]P1(x161,x162,x163)+~P4(f8(x161,x162,x163),x163)+~P4(f8(x161,x162,x163),x162)+~P4(f8(x161,x162,x163),x161)
% 70.26/70.37 [13]~P1(x134,x133,x132)+P4(x131,x132)+~P4(x131,x133)+~P4(x131,x134)
% 70.26/70.37 %EqnAxiom
% 70.26/70.37
% 70.26/70.37 %-------------------------------------------
% 70.26/70.38 cnf(47,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a5)+P4(f8(a3,a6,a4),a6)),
% 70.26/70.38 inference(scs_inference,[],[4,2,14,11])).
% 70.26/70.38 cnf(88,plain,
% 70.26/70.38 (P3(a5,x881)+P4(f7(a5,x881),a2)),
% 70.26/70.38 inference(scs_inference,[],[3,7,12])).
% 70.26/70.38 cnf(109,plain,
% 70.26/70.38 (P3(a4,x1091)+P4(f7(a4,x1091),a5)),
% 70.26/70.38 inference(scs_inference,[],[2,7,11])).
% 70.26/70.38 cnf(117,plain,
% 70.26/70.38 (P3(a4,x1171)+P4(f7(a4,x1171),a1)),
% 70.26/70.38 inference(scs_inference,[],[2,7,12])).
% 70.26/70.38 cnf(222,plain,
% 70.26/70.38 (P3(a5,a2)),
% 70.26/70.38 inference(scs_inference,[],[10,88])).
% 70.26/70.38 cnf(340,plain,
% 70.26/70.38 (~P4(f7(x3401,a6),a5)+P3(x3401,a6)),
% 70.26/70.38 inference(scs_inference,[],[3,10,11])).
% 70.26/70.38 cnf(366,plain,
% 70.26/70.38 (~P4(f7(x3661,a3),a2)+~P4(f7(x3661,a3),a1)+P3(x3661,a3)),
% 70.26/70.38 inference(scs_inference,[],[1,10,13])).
% 70.26/70.38 cnf(518,plain,
% 70.26/70.38 (P3(a4,a6)),
% 70.26/70.38 inference(scs_inference,[],[109,340])).
% 70.26/70.38 cnf(584,plain,
% 70.26/70.38 (P4(f7(a4,x5841),a2)+P3(a4,x5841)),
% 70.26/70.38 inference(scs_inference,[],[222,109,8])).
% 70.26/70.38 cnf(656,plain,
% 70.26/70.38 (P3(a4,a3)+~P4(f7(a4,a3),a2)),
% 70.26/70.38 inference(scs_inference,[],[117,366])).
% 70.26/70.38 cnf(1607,plain,
% 70.26/70.38 (P3(a4,a3)),
% 70.26/70.38 inference(scs_inference,[],[584,656])).
% 70.26/70.38 cnf(3180,plain,
% 70.26/70.38 (~P4(x31801,a3)+P4(x31801,a2)),
% 70.26/70.38 inference(scs_inference,[],[1,11])).
% 70.26/70.38 cnf(3184,plain,
% 70.26/70.38 (~P4(x31841,a3)+P4(x31841,a1)),
% 70.26/70.38 inference(scs_inference,[],[1,12])).
% 70.26/70.38 cnf(3187,plain,
% 70.26/70.38 (~P4(x31871,a5)+P4(x31871,a6)),
% 70.26/70.38 inference(scs_inference,[],[3,11])).
% 70.26/70.38 cnf(3190,plain,
% 70.26/70.38 (~P4(x31901,a4)+P4(x31901,a6)),
% 70.26/70.38 inference(scs_inference,[],[518,8])).
% 70.26/70.38 cnf(3208,plain,
% 70.26/70.38 (~P4(f8(a3,a6,a4),a3)+~P4(f8(a3,a6,a4),a4)),
% 70.26/70.38 inference(scs_inference,[],[4,3190,16])).
% 70.26/70.38 cnf(3211,plain,
% 70.26/70.38 (~P4(x32111,a4)+P4(x32111,a3)),
% 70.26/70.38 inference(scs_inference,[],[1607,8])).
% 70.26/70.38 cnf(3325,plain,
% 70.26/70.38 (~P4(x33251,a6)+P4(x33251,a5)+~P4(x33251,a3)),
% 70.26/70.38 inference(scs_inference,[],[3,3180,13])).
% 70.26/70.38 cnf(3326,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a5)+P4(f8(a3,a6,a4),a4)+~P4(f8(a3,a6,a4),a6)),
% 70.26/70.38 inference(scs_inference,[],[4,3325,15])).
% 70.26/70.38 cnf(3327,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a4)+P4(f8(a3,a6,a4),a5)),
% 70.26/70.38 inference(scs_inference,[],[3326,47])).
% 70.26/70.38 cnf(3361,plain,
% 70.26/70.38 (~P4(x33611,a5)+P4(x33611,a4)+~P4(x33611,a3)),
% 70.26/70.38 inference(scs_inference,[],[2,3184,13])).
% 70.26/70.38 cnf(3362,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a4)+~P4(f8(a3,a6,a4),a5)),
% 70.26/70.38 inference(scs_inference,[],[4,3361,15])).
% 70.26/70.38 cnf(3418,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a6)),
% 70.26/70.38 inference(scs_inference,[],[3187,47])).
% 70.26/70.38 cnf(3444,plain,
% 70.26/70.38 (~P4(f8(a3,a6,a4),a3)+P4(f8(a3,a6,a4),a5)),
% 70.26/70.38 inference(scs_inference,[],[3418,3325])).
% 70.26/70.38 cnf(3456,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),x34561)+~P1(x34562,x34561,a6)),
% 70.26/70.38 inference(scs_inference,[],[3418,11])).
% 70.26/70.38 cnf(3481,plain,
% 70.26/70.38 (P4(f8(a3,a6,a4),a4)+~P4(f8(a3,a6,a4),a3)),
% 70.26/70.38 inference(scs_inference,[],[3444,3362])).
% 70.26/70.38 cnf(3486,plain,
% 70.26/70.38 (~P4(f8(a3,a6,a4),a3)),
% 70.26/70.38 inference(scs_inference,[],[3481,3208])).
% 70.26/70.38 cnf(3541,plain,
% 70.26/70.38 ($false),
% 70.26/70.38 inference(scs_inference,[],[3486,3211,3456,3362,3327]),
% 70.26/70.38 ['proof']).
% 70.26/70.38 % SZS output end Proof
% 70.26/70.38 % Total time :69.700000s
%------------------------------------------------------------------------------