%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET015-2 : TPTP v9.2.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n004.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 : Tue May 5 05:06:50 PM UTC 2026
% Result : Unsatisfiable 141.60s 87.34s
% Output : CNFRefutation 141.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 24
% Syntax : Number of clauses : 104 ( 34 unt; 12 nHn; 84 RR)
% Number of literals : 195 ( 0 equ; 88 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 149 ( 15 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(member_of_union_is_member_of_one_set,axiom,
( member(X1,X2)
| member(X1,X3)
| ~ member(X1,union(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_union_is_member_of_one_set) ).
cnf(member_of_both_is_member_of_intersection,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_both_is_member_of_intersection) ).
cnf(subsets_axiom2,axiom,
( subset(X1,X2)
| ~ member(member_of_1_not_of_2(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',subsets_axiom2) ).
cnf(member_of_intersection_is_member_of_set1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_intersection_is_member_of_set1) ).
cnf(member_of_intersection_is_member_of_set2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_intersection_is_member_of_set2) ).
cnf(member_of_set1_is_member_of_union,axiom,
( member(X1,union(X2,X3))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_set1_is_member_of_union) ).
cnf(member_of_set2_is_member_of_union,axiom,
( member(X1,union(X3,X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_set2_is_member_of_union) ).
cnf(transitivity_for_equal_elements,axiom,
( equal_elements(X1,X3)
| ~ equal_elements(X1,X2)
| ~ equal_elements(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',transitivity_for_equal_elements) ).
cnf(transitivity_for_set_equal,axiom,
( equal_sets(X1,X3)
| ~ equal_sets(X1,X2)
| ~ equal_sets(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',transitivity_for_set_equal) ).
cnf(subsets_are_set_equal_sets,axiom,
( equal_sets(X2,X1)
| ~ subset(X1,X2)
| ~ subset(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',subsets_are_set_equal_sets) ).
cnf(membership_in_subsets,axiom,
( member(X1,X3)
| ~ member(X1,X2)
| ~ subset(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',membership_in_subsets) ).
cnf(not_member_of_set_and_complement,axiom,
( ~ member(X1,X2)
| ~ member(X1,complement(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',not_member_of_set_and_complement) ).
cnf(subsets_axiom1,axiom,
( subset(X1,X2)
| member(member_of_1_not_of_2(X1,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',subsets_axiom1) ).
cnf(symmetry_for_equal_elements,axiom,
( equal_elements(X2,X1)
| ~ equal_elements(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',symmetry_for_equal_elements) ).
cnf(symmetry_for_set_equal,axiom,
( equal_sets(X2,X1)
| ~ equal_sets(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',symmetry_for_set_equal) ).
cnf(set_equal_sets_are_subsets1,axiom,
( subset(X1,X2)
| ~ equal_sets(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',set_equal_sets_are_subsets1) ).
cnf(set_equal_sets_are_subsets2,axiom,
( subset(X2,X1)
| ~ equal_sets(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',set_equal_sets_are_subsets2) ).
cnf(member_of_set_or_complement,axiom,
( member(X1,X2)
| member(X1,complement(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',member_of_set_or_complement) ).
cnf(b_union_a_is_d,hypothesis,
equal_sets(union(bs,as),ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_union_a_is_d) ).
cnf(a_union_b_is_c,hypothesis,
equal_sets(union(as,bs),cs),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_union_b_is_c) ).
cnf(empty_set,axiom,
~ member(X1,empty_set),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',empty_set) ).
cnf(prove_c_equals_d,negated_conjecture,
~ equal_sets(cs,ds),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_c_equals_d) ).
cnf(reflexivity_for_equal_elements,axiom,
equal_elements(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',reflexivity_for_equal_elements) ).
cnf(reflexivity_for_set_equal,axiom,
equal_sets(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET002-0.ax',reflexivity_for_set_equal) ).
cnf(i_0_24,axiom,
( member(X1,X2)
| member(X1,X3)
| ~ member(X1,union(X2,X3)) ),
member_of_union_is_member_of_one_set,
[final] ).
cnf(i_0_25,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
member_of_both_is_member_of_intersection,
[final] ).
cnf(i_0_26,axiom,
( subset(X1,X2)
| ~ member(member_of_1_not_of_2(X1,X2),X2) ),
subsets_axiom2,
[final] ).
cnf(i_0_27,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
member_of_intersection_is_member_of_set1,
[final] ).
cnf(i_0_28,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
member_of_intersection_is_member_of_set2,
[final] ).
cnf(i_0_29,axiom,
( member(X1,union(X2,X3))
| ~ member(X1,X2) ),
member_of_set1_is_member_of_union,
[final] ).
cnf(i_0_30,axiom,
( member(X1,union(X3,X2))
| ~ member(X1,X2) ),
member_of_set2_is_member_of_union,
[final] ).
cnf(i_0_31,axiom,
( equal_elements(X1,X3)
| ~ equal_elements(X1,X2)
| ~ equal_elements(X2,X3) ),
transitivity_for_equal_elements,
[final] ).
cnf(i_0_32,axiom,
( equal_sets(X1,X3)
| ~ equal_sets(X1,X2)
| ~ equal_sets(X2,X3) ),
transitivity_for_set_equal,
[final] ).
cnf(i_0_33,axiom,
( equal_sets(X2,X1)
| ~ subset(X1,X2)
| ~ subset(X2,X1) ),
subsets_are_set_equal_sets,
[final] ).
cnf(i_0_34,axiom,
( member(X1,X3)
| ~ member(X1,X2)
| ~ subset(X2,X3) ),
membership_in_subsets,
[final] ).
cnf(i_0_35,axiom,
( ~ member(X1,X2)
| ~ member(X1,complement(X2)) ),
not_member_of_set_and_complement,
[final] ).
cnf(i_0_36,axiom,
( subset(X1,X2)
| member(member_of_1_not_of_2(X1,X2),X1) ),
subsets_axiom1,
[final] ).
cnf(i_0_37,axiom,
( equal_elements(X2,X1)
| ~ equal_elements(X1,X2) ),
symmetry_for_equal_elements,
[final] ).
cnf(i_0_38,axiom,
( equal_sets(X2,X1)
| ~ equal_sets(X1,X2) ),
symmetry_for_set_equal,
[final] ).
cnf(i_0_39,axiom,
( subset(X1,X2)
| ~ equal_sets(X1,X2) ),
set_equal_sets_are_subsets1,
[final] ).
cnf(i_0_40,axiom,
( subset(X2,X1)
| ~ equal_sets(X1,X2) ),
set_equal_sets_are_subsets2,
[final] ).
cnf(i_0_41,axiom,
( member(X1,X2)
| member(X1,complement(X2)) ),
member_of_set_or_complement,
[final] ).
cnf(i_0_42,hypothesis,
equal_sets(union(bs,as),ds),
b_union_a_is_d,
[final] ).
cnf(i_0_43,hypothesis,
equal_sets(union(as,bs),cs),
a_union_b_is_c,
[final] ).
cnf(i_0_44,axiom,
~ member(X1,empty_set),
empty_set,
[final] ).
cnf(i_0_45,negated_conjecture,
~ equal_sets(cs,ds),
prove_c_equals_d,
[final] ).
cnf(i_0_46,axiom,
equal_elements(X1,X1),
reflexivity_for_equal_elements,
[final] ).
cnf(i_0_47,axiom,
equal_sets(X1,X1),
reflexivity_for_set_equal,
[final] ).
cnf(i_0_48,plain,
equal_sets(ds,union(bs,as)),
inference(scs_inference,[],[i_0_42,i_0_38]) ).
cnf(i_0_50,plain,
subset(X1,X1),
inference(scs_inference,[],[i_0_47,i_0_42,i_0_38,i_0_39]) ).
cnf(i_0_52,plain,
subset(empty_set,X1),
inference(scs_inference,[],[i_0_47,i_0_42,i_0_44,i_0_38,i_0_39,i_0_36]) ).
cnf(i_0_53,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_55,plain,
subset(ds,union(bs,as)),
inference(scs_inference,[],[i_0_47,i_0_42,i_0_44,i_0_38,i_0_39,i_0_36,i_0_40]) ).
cnf(i_0_57,plain,
~ equal_sets(cs,union(bs,as)),
inference(scs_inference,[],[i_0_45,i_0_47,i_0_42,i_0_44,i_0_38,i_0_39,i_0_36,i_0_40,i_0_32]) ).
cnf(i_0_64,plain,
equal_sets(cs,union(as,bs)),
inference(scs_inference,[],[i_0_43,i_0_38]) ).
cnf(i_0_66,plain,
subset(union(as,bs),cs),
inference(scs_inference,[],[i_0_43,i_0_38,i_0_39]) ).
cnf(i_0_76,plain,
subset(cs,union(as,bs)),
inference(scs_inference,[],[i_0_43,i_0_40]) ).
cnf(i_0_90,plain,
member(X1,complement(empty_set)),
inference(scs_inference,[],[i_0_44,i_0_41]) ).
cnf(c_0_94,axiom,
( member(X1,X2)
| ~ member(X1,X3)
| ~ subset(X3,X2) ),
i_0_34 ).
cnf(c_0_95,axiom,
( subset(X1,X2)
| ~ equal_sets(X2,X1) ),
i_0_40 ).
cnf(c_0_96,axiom,
( equal_sets(X1,X2)
| ~ equal_sets(X1,X3)
| ~ equal_sets(X3,X2) ),
i_0_32 ).
cnf(c_0_97,plain,
equal_sets(ds,union(bs,as)),
i_0_48 ).
cnf(c_0_98,plain,
( member(X1,X2)
| ~ equal_sets(X2,X3)
| ~ member(X1,X3) ),
inference(spm,[status(thm)],[c_0_94,c_0_95]) ).
cnf(c_0_99,plain,
subset(cs,union(as,bs)),
i_0_76 ).
cnf(c_0_100,hypothesis,
equal_sets(union(as,bs),cs),
i_0_43 ).
cnf(c_0_101,axiom,
( equal_sets(X1,X2)
| ~ equal_sets(X2,X1) ),
i_0_38 ).
cnf(c_0_102,plain,
( equal_sets(X1,union(bs,as))
| ~ equal_sets(X1,ds) ),
inference(spm,[status(thm)],[c_0_96,c_0_97]) ).
cnf(c_0_103,plain,
equal_sets(cs,union(as,bs)),
i_0_64 ).
cnf(c_0_104,plain,
( member(X1,ds)
| ~ member(X1,union(bs,as)) ),
inference(spm,[status(thm)],[c_0_98,c_0_97]) ).
cnf(c_0_105,axiom,
( member(X1,union(X2,X3))
| ~ member(X1,X3) ),
i_0_30 ).
cnf(c_0_106,axiom,
( member(X1,X2)
| member(X1,X3)
| ~ member(X1,union(X2,X3)) ),
i_0_24 ).
cnf(c_0_107,plain,
( member(X1,union(as,bs))
| ~ member(X1,cs) ),
inference(spm,[status(thm)],[c_0_94,c_0_99]) ).
cnf(c_0_108,axiom,
( member(X1,union(X2,X3))
| ~ member(X1,X2) ),
i_0_29 ).
cnf(c_0_109,hypothesis,
( equal_sets(X1,cs)
| ~ equal_sets(X1,union(as,bs)) ),
inference(spm,[status(thm)],[c_0_96,c_0_100]) ).
cnf(c_0_110,plain,
( equal_sets(union(bs,as),X1)
| ~ equal_sets(X1,ds) ),
inference(spm,[status(thm)],[c_0_101,c_0_102]) ).
cnf(c_0_111,plain,
( equal_sets(X1,union(as,bs))
| ~ equal_sets(X1,cs) ),
inference(spm,[status(thm)],[c_0_96,c_0_103]) ).
cnf(c_0_112,plain,
subset(union(as,bs),cs),
i_0_66 ).
cnf(c_0_113,plain,
subset(ds,union(bs,as)),
i_0_55 ).
cnf(c_0_114,axiom,
( subset(X1,X2)
| ~ member(member_of_1_not_of_2(X1,X2),X2) ),
i_0_26 ).
cnf(c_0_115,plain,
( member(X1,ds)
| ~ member(X1,as) ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_116,plain,
( member(X1,as)
| member(X1,bs)
| ~ member(X1,cs) ),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
cnf(c_0_117,axiom,
( subset(X1,X2)
| member(member_of_1_not_of_2(X1,X2),X1) ),
i_0_36 ).
cnf(c_0_118,plain,
( member(X1,ds)
| ~ member(X1,bs) ),
inference(spm,[status(thm)],[c_0_104,c_0_108]) ).
cnf(c_0_119,hypothesis,
( equal_sets(union(bs,as),cs)
| ~ equal_sets(union(as,bs),ds) ),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
cnf(c_0_120,plain,
( equal_sets(union(as,bs),X1)
| ~ equal_sets(X1,cs) ),
inference(spm,[status(thm)],[c_0_101,c_0_111]) ).
cnf(c_0_121,plain,
( member(X1,cs)
| ~ member(X1,union(as,bs)) ),
inference(spm,[status(thm)],[c_0_94,c_0_112]) ).
cnf(c_0_122,plain,
( member(X1,union(bs,as))
| ~ member(X1,ds) ),
inference(spm,[status(thm)],[c_0_94,c_0_113]) ).
cnf(c_0_123,plain,
( subset(X1,ds)
| ~ member(member_of_1_not_of_2(X1,ds),as) ),
inference(spm,[status(thm)],[c_0_114,c_0_115]) ).
cnf(c_0_124,plain,
( subset(cs,X1)
| member(member_of_1_not_of_2(cs,X1),bs)
| member(member_of_1_not_of_2(cs,X1),as) ),
inference(spm,[status(thm)],[c_0_116,c_0_117]) ).
cnf(c_0_125,plain,
( subset(X1,ds)
| ~ member(member_of_1_not_of_2(X1,ds),bs) ),
inference(spm,[status(thm)],[c_0_114,c_0_118]) ).
cnf(c_0_126,plain,
( equal_sets(union(bs,as),cs)
| ~ equal_sets(ds,cs) ),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_127,plain,
~ equal_sets(cs,union(bs,as)),
i_0_57 ).
cnf(c_0_128,plain,
( member(X1,cs)
| ~ member(X1,as) ),
inference(spm,[status(thm)],[c_0_121,c_0_108]) ).
cnf(c_0_129,plain,
( member(X1,bs)
| member(X1,as)
| ~ member(X1,ds) ),
inference(spm,[status(thm)],[c_0_106,c_0_122]) ).
cnf(c_0_130,axiom,
( equal_sets(X1,X2)
| ~ subset(X2,X1)
| ~ subset(X1,X2) ),
i_0_33 ).
cnf(c_0_131,plain,
subset(cs,ds),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_124]),c_0_125]) ).
cnf(c_0_132,plain,
~ equal_sets(ds,cs),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_101,c_0_126]),c_0_127]) ).
cnf(c_0_133,plain,
( member(X1,cs)
| ~ member(X1,bs) ),
inference(spm,[status(thm)],[c_0_121,c_0_105]) ).
cnf(c_0_134,plain,
( subset(X1,cs)
| ~ member(member_of_1_not_of_2(X1,cs),as) ),
inference(spm,[status(thm)],[c_0_114,c_0_128]) ).
cnf(c_0_135,plain,
( subset(ds,X1)
| member(member_of_1_not_of_2(ds,X1),as)
| member(member_of_1_not_of_2(ds,X1),bs) ),
inference(spm,[status(thm)],[c_0_129,c_0_117]) ).
cnf(c_0_136,plain,
~ subset(ds,cs),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_131]),c_0_132]) ).
cnf(c_0_137,plain,
( subset(X1,cs)
| ~ member(member_of_1_not_of_2(X1,cs),bs) ),
inference(spm,[status(thm)],[c_0_114,c_0_133]) ).
cnf(c_0_138,plain,
member(member_of_1_not_of_2(ds,cs),bs),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_136]) ).
cnf(c_0_139,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_136]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET015-2 : TPTP v9.2.1. Bugfixed v2.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:08:32 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 141.60/87.34 % Version : CSE_E---1.7
% 141.60/87.34 % Problem : theBenchmark.p
% 141.60/87.34 % SZS status Unsatisfiable for theBenchmark.p
% 141.60/87.34 % SZS output start CNFRefutation
% See solution above
% 141.70/87.45 % Total time : 86.386s
%------------------------------------------------------------------------------