%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : TOP001-2 : 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 : 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 21:15:02 EDT 2024
% Result : Unsatisfiable 145.25s 146.50s
% Output : CNFRefutation 145.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : TOP001-2 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n017.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 : Tue Jun 18 11:50:38 EDT 2024
% 0.11/0.34 % CPUTime :
% 0.54/0.60 start to proof:theBenchmark
% 145.25/146.48 %-------------------------------------------
% 145.25/146.48 % File :CSE---1.7
% 145.25/146.48 % Problem :theBenchmark
% 145.25/146.48 % Transform :cnf
% 145.25/146.48 % Format :tptp:raw
% 145.25/146.48 % Command :java -jar mcs_scs.jar %d %s
% 145.25/146.48
% 145.25/146.48 % Result :Theorem 144.590000s
% 145.25/146.48 % Output :CNFRefutation 144.590000s
% 145.25/146.48 %-------------------------------------------
% 145.25/146.50 %--------------------------------------------------------------------------
% 145.25/146.50 % File : TOP001-2 : TPTP v8.2.0. Released v1.0.0.
% 145.25/146.50 % Domain : Topology
% 145.25/146.50 % Problem : Topology generated by a basis forms a topological space, part 1
% 145.25/146.50 % Version : [WM89] axioms : Incomplete > Reduced & Augmented > Incomplete.
% 145.25/146.50 % English :
% 145.25/146.50
% 145.25/146.50 % Refs : [WM89] Wick & McCune (1989), Automated Reasoning about Elemen
% 145.25/146.50 % Source : [WM89]
% 145.25/146.50 % Names : Lemma 1a [WM89]
% 145.25/146.50
% 145.25/146.50 % Status : Unsatisfiable
% 145.25/146.50 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v5.4.0, 0.10 v5.1.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.00 v2.4.0, 0.00 v2.1.0, 0.00 v2.0.0
% 145.25/146.50 % Syntax : Number of clauses : 13 ( 3 unt; 1 nHn; 11 RR)
% 145.25/146.50 % Number of literals : 27 ( 0 equ; 14 neg)
% 145.25/146.50 % Maximal clause size : 3 ( 2 avg)
% 145.25/146.50 % Maximal term depth : 3 ( 1 avg)
% 145.25/146.50 % Number of predicates : 5 ( 5 usr; 0 prp; 2-2 aty)
% 145.25/146.50 % Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% 145.25/146.50 % Number of variables : 25 ( 0 sgn)
% 145.25/146.50 % SPC : CNF_UNS_RFO_NEQ_NHN
% 145.25/146.50
% 145.25/146.50 % Comments : The axioms in this version are known to be incomplete. To
% 145.25/146.50 % make them complete it is be necessary to add appropriate set
% 145.25/146.50 % theory axioms.
% 145.25/146.50 %--------------------------------------------------------------------------
% 145.25/146.50 %----Include Point-set topology axioms
% 145.25/146.50 % include('Axioms/TOP001-0.ax').
% 145.25/146.50 %--------------------------------------------------------------------------
% 145.25/146.50 %----Sigma (union of members).
% 145.25/146.50 cnf(union_of_members_1,axiom,
% 145.25/146.50 ( ~ element_of_set(U,union_of_members(Vf))
% 145.25/146.50 | element_of_set(U,f1(Vf,U)) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(union_of_members_2,axiom,
% 145.25/146.50 ( ~ element_of_set(U,union_of_members(Vf))
% 145.25/146.50 | element_of_collection(f1(Vf,U),Vf) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(union_of_members_3,axiom,
% 145.25/146.50 ( element_of_set(U,union_of_members(Vf))
% 145.25/146.50 | ~ element_of_set(U,Uu1)
% 145.25/146.50 | ~ element_of_collection(Uu1,Vf) ) ).
% 145.25/146.50
% 145.25/146.50 %----Basis for a topology
% 145.25/146.50 cnf(basis_for_topology_28,axiom,
% 145.25/146.50 ( ~ basis(X,Vf)
% 145.25/146.50 | equal_sets(union_of_members(Vf),X) ) ).
% 145.25/146.50
% 145.25/146.50 %----Topology generated by a basis
% 145.25/146.50 cnf(topology_generated_37,axiom,
% 145.25/146.50 ( ~ element_of_collection(U,top_of_basis(Vf))
% 145.25/146.50 | ~ element_of_set(X,U)
% 145.25/146.50 | element_of_set(X,f10(Vf,U,X)) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(topology_generated_38,axiom,
% 145.25/146.50 ( ~ element_of_collection(U,top_of_basis(Vf))
% 145.25/146.50 | ~ element_of_set(X,U)
% 145.25/146.50 | element_of_collection(f10(Vf,U,X),Vf) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(set_theory_1,axiom,
% 145.25/146.50 subset_sets(X,X) ).
% 145.25/146.50
% 145.25/146.50 cnf(set_theory_2,axiom,
% 145.25/146.50 ( ~ subset_sets(X,Y)
% 145.25/146.50 | ~ element_of_set(U,X)
% 145.25/146.50 | element_of_set(U,Y) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(set_theory_3,axiom,
% 145.25/146.50 ( ~ equal_sets(X,Y)
% 145.25/146.50 | subset_sets(X,Y) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(set_theory_4,axiom,
% 145.25/146.50 ( subset_sets(X,Y)
% 145.25/146.50 | element_of_set(in_1st_set(X,Y),X) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(set_theory_5,axiom,
% 145.25/146.50 ( subset_sets(X,Y)
% 145.25/146.50 | ~ element_of_set(in_1st_set(X,Y),Y) ) ).
% 145.25/146.50
% 145.25/146.50 cnf(lemma_1a_1,negated_conjecture,
% 145.25/146.50 basis(cx,f) ).
% 145.25/146.50
% 145.25/146.50 cnf(lemma_1a_2,negated_conjecture,
% 145.25/146.50 ~ subset_sets(union_of_members(top_of_basis(f)),cx) ).
% 145.25/146.50
% 145.25/146.50 %--------------------------------------------------------------------------
% 145.25/146.50 %-------------------------------------------
% 145.25/146.50 % Proof found
% 145.25/146.50 % SZS status Theorem for theBenchmark
% 145.25/146.50 % SZS output start Proof
% 145.25/146.52 %ClaNum:13(EqnAxiom:0)
% 145.25/146.52 %VarNum:58(SingletonVarNum:25)
% 145.25/146.52 %MaxLitNum:3
% 145.25/146.52 %MaxfuncDepth:2
% 145.25/146.52 %SharedTerms:6
% 145.25/146.52 %goalClause: 1 3
% 145.25/146.52 %singleGoalClaCount:2
% 145.25/146.52 [1]P1(a1,a2)
% 145.25/146.52 [3]~P2(f7(f3(a2)),a1)
% 145.25/146.52 [2]P2(x21,x21)
% 145.25/146.52 [4]~P3(x41,x42)+P2(x41,x42)
% 145.25/146.52 [5]~P1(x52,x51)+P3(f7(x51),x52)
% 145.25/146.52 [6]P2(x61,x62)+P4(f4(x61,x62),x61)
% 145.25/146.52 [9]~P4(x91,f7(x92))+P4(x91,f5(x92,x91))
% 145.25/146.52 [10]~P4(x102,f7(x101))+P5(f5(x101,x102),x101)
% 145.25/146.52 [11]P2(x111,x112)+~P4(f4(x111,x112),x112)
% 145.25/146.52 [7]~P2(x73,x72)+P4(x71,x72)+~P4(x71,x73)
% 145.25/146.52 [8]~P5(x83,x82)+~P4(x81,x83)+P4(x81,f7(x82))
% 145.25/146.52 [12]~P4(x121,x123)+~P5(x123,f3(x122))+P4(x121,f6(x122,x123,x121))
% 145.25/146.53 [13]~P4(x133,x132)+~P5(x132,f3(x131))+P5(f6(x131,x132,x133),x131)
% 145.25/146.53 %EqnAxiom
% 145.25/146.53
% 145.25/146.53 %-------------------------------------------
% 145.54/146.78 cnf(14,plain,
% 145.54/146.78 (~P3(f7(f3(a2)),a1)),
% 145.54/146.78 inference(scs_inference,[],[3,4])).
% 145.54/146.78 cnf(48,plain,
% 145.54/146.78 (~P4(x481,x482)+P4(x481,x483)+P4(f4(x482,x483),x482)),
% 145.54/146.78 inference(scs_inference,[],[6,7])).
% 145.54/146.78 cnf(79,plain,
% 145.54/146.78 (~P4(x791,x792)+P4(x791,x793)+~P4(f4(x792,x793),x793)),
% 145.54/146.78 inference(scs_inference,[],[11,7])).
% 145.54/146.78 cnf(110,plain,
% 145.54/146.78 (~P5(f5(x1101,x1102),x1103)+P4(x1102,f7(x1103))+~P4(x1102,f7(x1101))),
% 145.54/146.78 inference(scs_inference,[],[9,8])).
% 145.54/146.78 cnf(141,plain,
% 145.54/146.78 (~P4(x1411,f5(f3(x1412),x1413))+P4(x1411,f6(x1412,f5(f3(x1412),x1413),x1411))+~P4(x1413,f7(f3(x1412)))),
% 145.54/146.78 inference(scs_inference,[],[10,12])).
% 145.54/146.78 cnf(172,plain,
% 145.54/146.78 (~P4(x1721,f7(x1722))+P4(x1721,x1723)+P4(f4(f7(x1722),x1723),f5(x1722,f4(f7(x1722),x1723)))),
% 145.54/146.78 inference(scs_inference,[],[48,9])).
% 145.54/146.78 cnf(203,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),x2031),x2031)+P4(f4(f7(f3(a2)),a1),x2031)),
% 145.54/146.78 inference(scs_inference,[],[3,79,6])).
% 145.54/146.78 cnf(447,plain,
% 145.54/146.78 (~P4(x4471,x4472)+~P3(x4472,x4473)+P4(x4471,x4473)),
% 145.54/146.78 inference(scs_inference,[],[4,7])).
% 145.54/146.78 cnf(478,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),a1),x4781)+~P3(x4781,a1)),
% 145.54/146.78 inference(scs_inference,[],[3,447,11])).
% 145.54/146.78 cnf(166600,plain,
% 145.54/146.78 (P3(f7(a2),a1)),
% 145.54/146.78 inference(scs_inference,[],[1,5])).
% 145.54/146.78 cnf(210226,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),a1),f7(a2))),
% 145.54/146.78 inference(scs_inference,[],[166600,478])).
% 145.54/146.78 cnf(210228,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),f7(a2)),f7(a2))),
% 145.54/146.78 inference(scs_inference,[],[166600,478,203])).
% 145.54/146.78 cnf(210230,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),a1),f7(x2102301))+~P5(f5(x2102301,f4(f7(f3(a2)),a1)),a2)),
% 145.54/146.78 inference(scs_inference,[],[166600,478,203,110])).
% 145.54/146.78 cnf(210234,plain,
% 145.54/146.78 (~P4(f4(f7(f3(a2)),f7(a2)),f7(x2102341))+~P5(f5(x2102341,f4(f7(f3(a2)),f7(a2))),a2)),
% 145.54/146.78 inference(scs_inference,[],[210228,110])).
% 145.54/146.78 cnf(210239,plain,
% 145.54/146.78 (~P5(x2102391,a2)+~P4(f4(f7(f3(a2)),a1),x2102391)),
% 145.54/146.78 inference(scs_inference,[],[210226,8])).
% 145.54/146.78 cnf(210484,plain,
% 145.54/146.78 (P4(f4(f7(f3(a2)),a1),f7(f3(a2)))),
% 145.54/146.78 inference(scs_inference,[],[3,14,5,6])).
% 145.54/146.78 cnf(210486,plain,
% 145.54/146.78 (P4(f4(f7(f3(a2)),a1),f5(f3(a2),f4(f7(f3(a2)),a1)))),
% 145.54/146.78 inference(scs_inference,[],[3,14,5,6,9])).
% 145.54/146.78 cnf(210496,plain,
% 145.54/146.78 (P4(f4(f7(f3(a2)),f7(a2)),f7(f3(a2)))),
% 145.54/146.78 inference(scs_inference,[],[3,14,210226,5,6,9,478,10,11,447,48])).
% 145.54/146.78 cnf(210498,plain,
% 145.54/146.78 (P4(f4(f7(f3(a2)),f7(a2)),f5(f3(a2),f4(f7(f3(a2)),f7(a2))))),
% 145.54/146.78 inference(scs_inference,[],[3,14,210226,5,6,9,478,10,11,447,48,172])).
% 145.54/146.78 cnf(210500,plain,
% 145.54/146.78 (P4(f4(f7(f3(a2)),f7(a2)),f6(a2,f5(f3(a2),f4(f7(f3(a2)),f7(a2))),f4(f7(f3(a2)),f7(a2))))),
% 145.54/146.78 inference(scs_inference,[],[3,14,210226,5,6,9,478,10,11,447,48,172,141])).
% 145.54/146.78 cnf(210515,plain,
% 145.54/146.78 (P5(f5(f3(a2),f4(f7(f3(a2)),f7(a2))),f3(a2))),
% 145.54/146.78 inference(scs_inference,[],[14,210496,5,10])).
% 145.54/146.78 cnf(210525,plain,
% 145.54/146.78 (~P2(f5(f3(a2),f4(f7(f3(a2)),f7(a2))),f7(a2))),
% 145.54/146.78 inference(scs_inference,[],[14,210226,210228,210484,210496,210498,210486,5,10,478,8,79,48,7])).
% 145.54/146.78 cnf(252422,plain,
% 145.54/146.78 ($false),
% 145.54/146.78 inference(scs_inference,[],[210496,210525,210486,210228,210484,14,210226,210498,210500,210515,478,4,5,210230,210234,210239,447,8,13]),
% 145.54/146.78 ['proof']).
% 145.73/146.97 % SZS output end Proof
% 145.73/146.97 % Total time :144.590000s
%------------------------------------------------------------------------------