%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : CSR110+3 : TPTP v9.2.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n014.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 04:15:24 PM UTC 2026
% Result : Unsatisfiable 172.57s 234.13s
% Output : CNFRefutation 172.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 39 ( 12 unt; 0 def)
% Number of atoms : 162 ( 33 equ)
% Maximal formula atoms : 45 ( 4 avg)
% Number of connectives : 192 ( 69 ~; 78 |; 34 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-3 aty)
% Number of variables : 86 ( 22 sgn 33 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(kb_SUMO_32603,axiom,
! [X137,X12,X136] :
( X12 = s__UnionFn(X136,X137)
<=> ! [X1138,X34,X1139] :
( ( s__instance(X136,s__SetOrClass)
& s__instance(X12,s__SetOrClass)
& s__instance(X137,s__SetOrClass) )
=> ( ( s__instance(X1138,X136)
& s__instance(X34,X137)
& s__instance(X1139,X12) )
=> ( s__instance(X1138,X12)
& s__instance(X34,X12)
& ( s__instance(X1139,X136)
| s__instance(X1139,X137) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32603) ).
fof(kb_SUMO_32640,axiom,
! [X817] :
( s__instance(X817,s__SetOrClass)
=> ( s__instance(X817,s__NullSet)
=> ~ ? [X851] : s__instance(X851,X817) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32640) ).
fof(kb_SUMO_14330,axiom,
s__BigSix != s__GroupOf6,
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_14330) ).
fof(kb_SUMO_27141,axiom,
! [X981,X982] :
( s__disjoint(X981,X982)
<=> ! [X851] :
( ( s__instance(X982,s__SetOrClass)
& s__instance(X981,s__SetOrClass) )
=> ~ ( s__instance(X851,X981)
& s__instance(X851,X982) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_27141) ).
fof(kb_SUMO_32596,axiom,
! [X1136,X1137] :
( ! [X1063] :
( ( s__instance(X1137,s__Set)
& s__instance(X1136,s__Set) )
=> ( s__element(X1063,X1137)
<=> s__element(X1063,X1136) ) )
=> X1137 = X1136 ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32596) ).
fof(kb_SUMO_39907,axiom,
! [X638] :
( s__instance(X638,s__Agreement)
=> ? [X288,X286] :
( s__instance(X286,s__CognitiveAgent)
& s__instance(X288,s__CognitiveAgent)
& s__partyToAgreement(X288,X638)
& s__partyToAgreement(X286,X638)
& X288 != X286 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_39907) ).
fof(kb_SUMO_11754,axiom,
s__instance(s__AirPollutionConvention,s__Agreement),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_11754) ).
fof(c_0_7,plain,
! [X108820,X108821,X108822,X108823,X108824,X108825,X108826,X108827,X108828] :
( ( s__instance(X108823,X108821)
| ~ s__instance(X108823,X108822)
| ~ s__instance(X108824,X108820)
| ~ s__instance(X108825,X108821)
| ~ s__instance(X108822,s__SetOrClass)
| ~ s__instance(X108821,s__SetOrClass)
| ~ s__instance(X108820,s__SetOrClass)
| X108821 != s__UnionFn(X108822,X108820) )
& ( s__instance(X108824,X108821)
| ~ s__instance(X108823,X108822)
| ~ s__instance(X108824,X108820)
| ~ s__instance(X108825,X108821)
| ~ s__instance(X108822,s__SetOrClass)
| ~ s__instance(X108821,s__SetOrClass)
| ~ s__instance(X108820,s__SetOrClass)
| X108821 != s__UnionFn(X108822,X108820) )
& ( s__instance(X108825,X108822)
| s__instance(X108825,X108820)
| ~ s__instance(X108823,X108822)
| ~ s__instance(X108824,X108820)
| ~ s__instance(X108825,X108821)
| ~ s__instance(X108822,s__SetOrClass)
| ~ s__instance(X108821,s__SetOrClass)
| ~ s__instance(X108820,s__SetOrClass)
| X108821 != s__UnionFn(X108822,X108820) )
& ( s__instance(X108828,s__SetOrClass)
| X108827 = s__UnionFn(X108828,X108826) )
& ( s__instance(X108827,s__SetOrClass)
| X108827 = s__UnionFn(X108828,X108826) )
& ( s__instance(X108826,s__SetOrClass)
| X108827 = s__UnionFn(X108828,X108826) )
& ( s__instance(esk4527_3(X108826,X108827,X108828),X108828)
| X108827 = s__UnionFn(X108828,X108826) )
& ( s__instance(esk4528_3(X108826,X108827,X108828),X108826)
| X108827 = s__UnionFn(X108828,X108826) )
& ( s__instance(esk4529_3(X108826,X108827,X108828),X108827)
| X108827 = s__UnionFn(X108828,X108826) )
& ( ~ s__instance(esk4529_3(X108826,X108827,X108828),X108828)
| ~ s__instance(esk4527_3(X108826,X108827,X108828),X108827)
| ~ s__instance(esk4528_3(X108826,X108827,X108828),X108827)
| X108827 = s__UnionFn(X108828,X108826) )
& ( ~ s__instance(esk4529_3(X108826,X108827,X108828),X108826)
| ~ s__instance(esk4527_3(X108826,X108827,X108828),X108827)
| ~ s__instance(esk4528_3(X108826,X108827,X108828),X108827)
| X108827 = s__UnionFn(X108828,X108826) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_32603])])])])])]) ).
fof(c_0_8,plain,
! [X108832,X108833] :
( ~ s__instance(X108832,s__SetOrClass)
| ~ s__instance(X108832,s__NullSet)
| ~ s__instance(X108833,X108832) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_32640])])]) ).
cnf(c_0_9,plain,
s__BigSix != s__GroupOf6,
inference(split_conjunct,[status(thm)],[kb_SUMO_14330]) ).
cnf(c_0_10,plain,
( s__instance(X1,s__SetOrClass)
| X2 = s__UnionFn(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_11,plain,
( ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X1,s__NullSet)
| ~ s__instance(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
cnf(c_0_12,plain,
s__instance(X1,s__SetOrClass),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_9,c_0_10]),c_0_10]) ).
fof(c_0_13,plain,
! [X99241,X99242,X99243,X99244,X99245] :
( ( ~ s__disjoint(X99241,X99242)
| ~ s__instance(X99242,s__SetOrClass)
| ~ s__instance(X99241,s__SetOrClass)
| ~ s__instance(X99243,X99241)
| ~ s__instance(X99243,X99242) )
& ( s__instance(X99245,s__SetOrClass)
| s__disjoint(X99244,X99245) )
& ( s__instance(X99244,s__SetOrClass)
| s__disjoint(X99244,X99245) )
& ( s__instance(esk4310_2(X99244,X99245),X99244)
| s__disjoint(X99244,X99245) )
& ( s__instance(esk4310_2(X99244,X99245),X99245)
| s__disjoint(X99244,X99245) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_27141])])])])])]) ).
cnf(c_0_14,plain,
( ~ s__instance(X1,s__NullSet)
| ~ s__instance(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11,c_0_12])]) ).
cnf(c_0_15,plain,
( s__instance(esk4310_2(X1,X2),X1)
| s__disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_16,plain,
( s__disjoint(s__NullSet,X1)
| ~ s__instance(X2,esk4310_2(s__NullSet,X1)) ),
inference(spm,[status(thm)],[c_0_14,c_0_15]) ).
cnf(c_0_17,plain,
( s__instance(esk4527_3(X1,X2,X3),X3)
| X2 = s__UnionFn(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_18,plain,
( X1 = s__UnionFn(esk4310_2(s__NullSet,X2),X3)
| s__disjoint(s__NullSet,X2) ),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
cnf(c_0_19,plain,
( ~ s__disjoint(X1,X2)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X3,X1)
| ~ s__instance(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_20,plain,
( X1 = X2
| s__disjoint(s__NullSet,X3) ),
inference(spm,[status(thm)],[c_0_18,c_0_18]) ).
fof(c_0_21,plain,
! [X108817,X108818] :
( ( s__instance(X108818,s__Set)
| X108818 = X108817 )
& ( s__instance(X108817,s__Set)
| X108818 = X108817 )
& ( ~ s__element(esk4526_2(X108817,X108818),X108818)
| ~ s__element(esk4526_2(X108817,X108818),X108817)
| X108818 = X108817 )
& ( s__element(esk4526_2(X108817,X108818),X108818)
| s__element(esk4526_2(X108817,X108818),X108817)
| X108818 = X108817 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_32596])])])])]) ).
cnf(c_0_22,plain,
( ~ s__disjoint(X1,X2)
| ~ s__instance(X3,X2)
| ~ s__instance(X3,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19,c_0_12]),c_0_12])]) ).
cnf(c_0_23,plain,
s__disjoint(s__NullSet,X1),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_9,c_0_20])]) ).
cnf(c_0_24,plain,
( s__instance(X1,s__Set)
| X2 = X1 ),
inference(split_conjunct,[status(thm)],[c_0_21]) ).
cnf(c_0_25,plain,
( ~ s__instance(X1,s__NullSet)
| ~ s__instance(X1,X2) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_26,plain,
( s__instance(esk4529_3(X1,X2,X3),X2)
| X2 = s__UnionFn(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_27,plain,
s__instance(s__GroupOf6,s__Set),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_9,c_0_24])]) ).
cnf(c_0_28,plain,
( s__NullSet = s__UnionFn(X1,X2)
| ~ s__instance(esk4529_3(X2,s__NullSet,X1),X3) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_29,plain,
s__instance(X1,s__Set),
inference(spm,[status(thm)],[c_0_27,c_0_24]) ).
cnf(c_0_30,plain,
( s__instance(esk4528_3(X1,X2,X3),X1)
| X2 = s__UnionFn(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_31,plain,
s__NullSet = s__UnionFn(X1,X2),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
fof(c_0_32,plain,
! [X112032] :
( ( s__instance(esk5358_1(X112032),s__CognitiveAgent)
| ~ s__instance(X112032,s__Agreement) )
& ( s__instance(esk5357_1(X112032),s__CognitiveAgent)
| ~ s__instance(X112032,s__Agreement) )
& ( s__partyToAgreement(esk5357_1(X112032),X112032)
| ~ s__instance(X112032,s__Agreement) )
& ( s__partyToAgreement(esk5358_1(X112032),X112032)
| ~ s__instance(X112032,s__Agreement) )
& ( esk5357_1(X112032) != esk5358_1(X112032)
| ~ s__instance(X112032,s__Agreement) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_39907])])])]) ).
cnf(c_0_33,plain,
( X1 = s__NullSet
| ~ s__instance(esk4528_3(s__NullSet,X1,X2),X3) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_30]),c_0_31]) ).
cnf(c_0_34,plain,
( esk5357_1(X1) != esk5358_1(X1)
| ~ s__instance(X1,s__Agreement) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_35,plain,
X1 = s__NullSet,
inference(spm,[status(thm)],[c_0_33,c_0_29]) ).
cnf(c_0_36,plain,
s__instance(s__AirPollutionConvention,s__Agreement),
inference(split_conjunct,[status(thm)],[kb_SUMO_11754]) ).
cnf(c_0_37,plain,
~ s__instance(X1,s__Agreement),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_34,c_0_35]),c_0_35])]) ).
cnf(c_0_38,plain,
$false,
inference(sr,[status(thm)],[c_0_36,c_0_37]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR110+3 : TPTP v9.2.1. Bugfixed v7.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n014.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 : Mon May 4 17:02:21 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 43.65/57.70 % Warning 104: No lemmas were extracted from the log file '/export/starexec/sandbox2/solver/bin/output/initial_lemmas_CSE.log'. Continuing with baseline prover only.
% 172.57/234.13 % Version : CSE_E---1.7
% 172.57/234.13 % Problem : theBenchmark.p
% 172.57/234.13 % SZS status Unsatisfiable for theBenchmark.p
% 172.57/234.13 % SZS output start CNFRefutation
% See solution above
% 172.74/234.34 % Total time : 225.851s
%------------------------------------------------------------------------------