%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET014-2 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:55:53 AM UTC 2026
% Result : Unsatisfiable 0.46s 0.73s
% Output : Proof 0.52s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(empty_set,axiom,
~ member(X,empty_set),
file('SET002-0.ax',empty_set) ).
cnf(membership_in_subsets,axiom,
( member(Element,Superset)
| ~ subset(Subset,Superset)
| ~ member(Element,Subset) ),
file('SET002-0.ax',membership_in_subsets) ).
cnf(subsets_axiom1,axiom,
( member(member_of_1_not_of_2(Subset,Superset),Subset)
| subset(Subset,Superset) ),
file('SET002-0.ax',subsets_axiom1) ).
cnf(subsets_axiom2,axiom,
( subset(Subset,Superset)
| ~ member(member_of_1_not_of_2(Subset,Superset),Superset) ),
file('SET002-0.ax',subsets_axiom2) ).
cnf(member_of_set_or_complement,axiom,
( member(X,complement(Xs))
| member(X,Xs) ),
file('SET002-0.ax',member_of_set_or_complement) ).
cnf(not_member_of_set_and_complement,axiom,
( ~ member(X,complement(Xs))
| ~ member(X,Xs) ),
file('SET002-0.ax',not_member_of_set_and_complement) ).
cnf(member_of_set1_is_member_of_union,axiom,
( member(X,union(Xs,Ys))
| ~ member(X,Xs) ),
file('SET002-0.ax',member_of_set1_is_member_of_union) ).
cnf(member_of_set2_is_member_of_union,axiom,
( member(X,union(Xs,Ys))
| ~ member(X,Ys) ),
file('SET002-0.ax',member_of_set2_is_member_of_union) ).
cnf(member_of_union_is_member_of_one_set,axiom,
( member(X,Ys)
| member(X,Xs)
| ~ member(X,union(Xs,Ys)) ),
file('SET002-0.ax',member_of_union_is_member_of_one_set) ).
cnf(member_of_both_is_member_of_intersection,axiom,
( member(X,intersection(Xs,Ys))
| ~ member(X,Ys)
| ~ member(X,Xs) ),
file('SET002-0.ax',member_of_both_is_member_of_intersection) ).
cnf(member_of_intersection_is_member_of_set1,axiom,
( member(X,Xs)
| ~ member(X,intersection(Xs,Ys)) ),
file('SET002-0.ax',member_of_intersection_is_member_of_set1) ).
cnf(member_of_intersection_is_member_of_set2,axiom,
( member(X,Ys)
| ~ member(X,intersection(Xs,Ys)) ),
file('SET002-0.ax',member_of_intersection_is_member_of_set2) ).
cnf(set_equal_sets_are_subsets1,axiom,
( subset(Subset,Superset)
| ~ equal_sets(Subset,Superset) ),
file('SET002-0.ax',set_equal_sets_are_subsets1) ).
cnf(set_equal_sets_are_subsets2,axiom,
( subset(Subset,Superset)
| ~ equal_sets(Superset,Subset) ),
file('SET002-0.ax',set_equal_sets_are_subsets2) ).
cnf(subsets_are_set_equal_sets,axiom,
( equal_sets(Set2,Set1)
| ~ subset(Set2,Set1)
| ~ subset(Set1,Set2) ),
file('SET002-0.ax',subsets_are_set_equal_sets) ).
cnf(reflexivity_for_set_equal,axiom,
equal_sets(Xs,Xs),
file('SET002-0.ax',reflexivity_for_set_equal) ).
cnf(symmetry_for_set_equal,axiom,
( equal_sets(Ys,Xs)
| ~ equal_sets(Xs,Ys) ),
file('SET002-0.ax',symmetry_for_set_equal) ).
cnf(transitivity_for_set_equal,axiom,
( equal_sets(Xs,Zs)
| ~ equal_sets(Ys,Zs)
| ~ equal_sets(Xs,Ys) ),
file('SET002-0.ax',transitivity_for_set_equal) ).
cnf(reflexivity_for_equal_elements,axiom,
equal_elements(X,X),
file('SET002-0.ax',reflexivity_for_equal_elements) ).
cnf(symmetry_for_equal_elements,axiom,
( equal_elements(Y,X)
| ~ equal_elements(X,Y) ),
file('SET002-0.ax',symmetry_for_equal_elements) ).
cnf(transitivity_for_equal_elements,axiom,
( equal_elements(X,Z)
| ~ equal_elements(Y,Z)
| ~ equal_elements(X,Y) ),
file('SET002-0.ax',transitivity_for_equal_elements) ).
cnf(a_subset_of_c,hypothesis,
subset(as,cs),
file('theBenchmark.p',a_subset_of_c) ).
cnf(b_subset_of_c,hypothesis,
subset(bs,cs),
file('theBenchmark.p',b_subset_of_c) ).
cnf(prove_a_union_b_subset_of_c,negated_conjecture,
~ subset(union(as,bs),cs),
file('theBenchmark.p',prove_a_union_b_subset_of_c) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET014-2 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 21:29:05 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.46/0.73 % SZS status Unsatisfiable for theBenchmark
% 0.46/0.73 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------