%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM533+2 : TPTP v9.2.1. Released v4.0.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 : n023.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:57:43 PM UTC 2026
% Result : Theorem 0.27s 1.61s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 41)
% Comments :
%------------------------------------------------------------------------------
fof(m__,conjecture,
( ( ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,xB) )
& aSubsetOf0(xA,xB)
& ! [X1] :
( aElementOf0(X1,xB)
=> aElementOf0(X1,xC) )
& aSubsetOf0(xB,xC) )
=> ( ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,xC) )
| aSubsetOf0(xA,xC) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(mCountNFin,axiom,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> ~ isFinite0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin) ).
fof(mDefSub,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aSubsetOf0(X2,X1)
<=> ( aSet0(X2)
& ! [X3] :
( aElementOf0(X3,X2)
=> aElementOf0(X3,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefSub) ).
fof(mSubASymm,axiom,
! [X1,X2] :
( ( aSet0(X1)
& aSet0(X2) )
=> ( ( aSubsetOf0(X1,X2)
& aSubsetOf0(X2,X1) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubASymm) ).
fof(mSubFSet,axiom,
! [X1] :
( ( aSet0(X1)
& isFinite0(X1) )
=> ! [X2] :
( aSubsetOf0(X2,X1)
=> isFinite0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubFSet) ).
fof(mEOfElem,axiom,
! [X1] :
( aSet0(X1)
=> ! [X2] :
( aElementOf0(X2,X1)
=> aElement0(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEOfElem) ).
fof(mDefEmp,axiom,
! [X1] :
( X1 = slcrc0
<=> ( aSet0(X1)
& ~ ? [X2] : aElementOf0(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefEmp) ).
fof(mSubRefl,axiom,
! [X1] :
( aSet0(X1)
=> aSubsetOf0(X1,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSubRefl) ).
fof(mCountNFin_01,axiom,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> X1 != slcrc0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mCountNFin_01) ).
fof(mEmpFin,axiom,
isFinite0(slcrc0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mEmpFin) ).
fof(m__522,hypothesis,
( aSet0(xA)
& aSet0(xB)
& aSet0(xC) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__522) ).
fof(i_0_11,negated_conjecture,
~ ( ( ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,xB) )
& aSubsetOf0(xA,xB)
& ! [X1] :
( aElementOf0(X1,xB)
=> aElementOf0(X1,xC) )
& aSubsetOf0(xB,xC) )
=> ( ! [X1] :
( aElementOf0(X1,xA)
=> aElementOf0(X1,xC) )
| aSubsetOf0(xA,xC) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(i_0_12,plain,
! [X1] :
( ( aSet0(X1)
& isCountable0(X1) )
=> ~ isFinite0(X1) ),
inference(fof_simplification,[status(thm)],[mCountNFin]) ).
fof(i_0_13,plain,
! [X33,X34,X35,X36] :
( ( aSet0(X34)
| ~ aSubsetOf0(X34,X33)
| ~ aSet0(X33) )
& ( ~ aElementOf0(X35,X34)
| aElementOf0(X35,X33)
| ~ aSubsetOf0(X34,X33)
| ~ aSet0(X33) )
& ( aElementOf0(esk2_2(X33,X36),X36)
| ~ aSet0(X36)
| aSubsetOf0(X36,X33)
| ~ aSet0(X33) )
& ( ~ aElementOf0(esk2_2(X33,X36),X33)
| ~ aSet0(X36)
| aSubsetOf0(X36,X33)
| ~ aSet0(X33) ) ),
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)],[mDefSub])])])])])]) ).
fof(i_0_14,plain,
! [X41,X42] :
( ~ aSet0(X41)
| ~ aSet0(X42)
| ~ aSubsetOf0(X41,X42)
| ~ aSubsetOf0(X42,X41)
| X41 = X42 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubASymm])]) ).
fof(i_0_15,plain,
! [X38,X39] :
( ~ aSet0(X38)
| ~ isFinite0(X38)
| ~ aSubsetOf0(X39,X38)
| isFinite0(X39) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubFSet])])]) ).
fof(i_0_16,plain,
! [X25,X26] :
( ~ aSet0(X25)
| ~ aElementOf0(X26,X25)
| aElement0(X26) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mEOfElem])])]) ).
fof(i_0_17,negated_conjecture,
! [X43,X44] :
( ( ~ aElementOf0(X43,xA)
| aElementOf0(X43,xB) )
& aSubsetOf0(xA,xB)
& ( ~ aElementOf0(X44,xB)
| aElementOf0(X44,xC) )
& aSubsetOf0(xB,xC)
& aElementOf0(esk3_0,xA)
& ~ aElementOf0(esk3_0,xC)
& ~ aSubsetOf0(xA,xC) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_11])])])]) ).
fof(i_0_18,plain,
! [X27,X28,X29] :
( ( aSet0(X27)
| X27 != slcrc0 )
& ( ~ aElementOf0(X28,X27)
| X27 != slcrc0 )
& ( ~ aSet0(X29)
| aElementOf0(esk1_1(X29),X29)
| X29 = slcrc0 ) ),
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)],[mDefEmp])])])])])]) ).
fof(i_0_19,plain,
! [X40] :
( ~ aSet0(X40)
| aSubsetOf0(X40,X40) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mSubRefl])]) ).
fof(i_0_20,plain,
! [X31] :
( ~ aSet0(X31)
| ~ isCountable0(X31)
| ~ isFinite0(X31) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_12])]) ).
fof(i_0_21,plain,
! [X32] :
( ~ aSet0(X32)
| ~ isCountable0(X32)
| X32 != slcrc0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mCountNFin_01])]) ).
cnf(i_0_22,plain,
( aSubsetOf0(X2,X1)
| ~ aElementOf0(esk2_2(X1,X2),X1)
| ~ aSet0(X2)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_13]),
[final] ).
cnf(i_0_23,plain,
( aElementOf0(esk2_2(X1,X2),X2)
| aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_13]),
[final] ).
cnf(i_0_24,plain,
( aElementOf0(X1,X3)
| ~ aElementOf0(X1,X2)
| ~ aSubsetOf0(X2,X3)
| ~ aSet0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_13]),
[final] ).
cnf(i_0_25,plain,
( X1 = X2
| ~ aSet0(X1)
| ~ aSet0(X2)
| ~ aSubsetOf0(X1,X2)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_26,plain,
( isFinite0(X2)
| ~ aSet0(X1)
| ~ isFinite0(X1)
| ~ aSubsetOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_27,plain,
( aElement0(X2)
| ~ aSet0(X1)
| ~ aElementOf0(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_16]),
[final] ).
cnf(i_0_28,plain,
( aSet0(X1)
| ~ aSubsetOf0(X1,X2)
| ~ aSet0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_13]),
[final] ).
cnf(i_0_29,negated_conjecture,
( aElementOf0(X1,xC)
| ~ aElementOf0(X1,xB) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_30,negated_conjecture,
( aElementOf0(X1,xB)
| ~ aElementOf0(X1,xA) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_31,plain,
( aElementOf0(esk1_1(X1),X1)
| X1 = slcrc0
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_32,plain,
( ~ aElementOf0(X1,X2)
| X2 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_33,plain,
( aSubsetOf0(X1,X1)
| ~ aSet0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_19]),
[final] ).
cnf(i_0_34,plain,
( ~ aSet0(X1)
| ~ isCountable0(X1)
| ~ isFinite0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_35,negated_conjecture,
~ aSubsetOf0(xA,xC),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_36,negated_conjecture,
~ aElementOf0(esk3_0,xC),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_37,plain,
( ~ aSet0(X1)
| ~ isCountable0(X1)
| X1 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_38,negated_conjecture,
aSubsetOf0(xB,xC),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_39,negated_conjecture,
aSubsetOf0(xA,xB),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_40,negated_conjecture,
aElementOf0(esk3_0,xA),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_41,plain,
( aSet0(X1)
| X1 != slcrc0 ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_42,plain,
isFinite0(slcrc0),
inference(split_conjunct,[status(thm)],[mEmpFin]),
[final] ).
cnf(i_0_43,hypothesis,
aSet0(xC),
inference(split_conjunct,[status(thm)],[m__522]),
[final] ).
cnf(i_0_44,hypothesis,
aSet0(xB),
inference(split_conjunct,[status(thm)],[m__522]),
[final] ).
cnf(i_0_45,hypothesis,
aSet0(xA),
inference(split_conjunct,[status(thm)],[m__522]),
[final] ).
cnf(i_0_46,axiom,
X1 = X1 ).
cnf(i_0_47,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_48,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_49,axiom,
( X1 != X2
| ~ aSubsetOf0(X1,X3)
| aSubsetOf0(X2,X3) ) ).
cnf(i_0_50,axiom,
( X1 != X2
| ~ aSubsetOf0(X3,X1)
| aSubsetOf0(X3,X2) ) ).
cnf(i_0_51,axiom,
( X1 != X2
| ~ aElementOf0(X1,X3)
| aElementOf0(X2,X3) ) ).
cnf(i_0_52,axiom,
( X1 != X2
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X2) ) ).
cnf(i_0_53,axiom,
( X1 != X2
| ~ aSet0(X1)
| aSet0(X2) ) ).
cnf(i_0_54,axiom,
( X1 != X2
| ~ isFinite0(X1)
| isFinite0(X2) ) ).
cnf(i_0_55,axiom,
( X1 != X2
| ~ aElement0(X1)
| aElement0(X2) ) ).
cnf(i_0_56,axiom,
( X1 != X2
| ~ isCountable0(X1)
| isCountable0(X2) ) ).
cnf(i_0_46_001,axiom,
X1 = X1 ).
cnf(i_0_47_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_48_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_49_004,axiom,
( X1 != X2
| ~ aSubsetOf0(X1,X3)
| aSubsetOf0(X2,X3) ) ).
cnf(i_0_50_005,axiom,
( X1 != X2
| ~ aSubsetOf0(X3,X1)
| aSubsetOf0(X3,X2) ) ).
cnf(i_0_51_006,axiom,
( X1 != X2
| ~ aElementOf0(X1,X3)
| aElementOf0(X2,X3) ) ).
cnf(i_0_52_007,axiom,
( X1 != X2
| ~ aElementOf0(X3,X1)
| aElementOf0(X3,X2) ) ).
cnf(i_0_53_008,axiom,
( X1 != X2
| ~ aSet0(X1)
| aSet0(X2) ) ).
cnf(i_0_54_009,axiom,
( X1 != X2
| ~ isFinite0(X1)
| isFinite0(X2) ) ).
cnf(i_0_55_010,axiom,
( X1 != X2
| ~ aElement0(X1)
| aElement0(X2) ) ).
cnf(i_0_56_011,axiom,
( X1 != X2
| ~ isCountable0(X1)
| isCountable0(X2) ) ).
cnf(i_0_57,plain,
~ aElementOf0(X1,slcrc0),
inference(equality_inference,[],[32]) ).
cnf(i_0_58,plain,
( ~ isCountable0(slcrc0)
| ~ aSet0(slcrc0) ),
inference(equality_inference,[],[37]) ).
cnf(i_0_59,plain,
aSet0(slcrc0),
inference(equality_inference,[],[41]) ).
cnf(i_0_60,plain,
~ isCountable0(slcrc0),
inference(scs_inference,[],[i_0_59,i_0_58]) ).
cnf(i_0_61,plain,
aElementOf0(esk3_0,xB),
inference(scs_inference,[],[i_0_40,i_0_30]) ).
cnf(i_0_62,plain,
( ~ aElementOf0(X1,xA)
| aElementOf0(X1,xB) ),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_63,plain,
aSubsetOf0(xC,xC),
inference(scs_inference,[],[i_0_40,i_0_43,i_0_30,i_0_33]) ).
cnf(i_0_64,plain,
( ~ aSet0(X1)
| aSubsetOf0(X1,X1) ),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_65,plain,
aElement0(esk3_0),
inference(scs_inference,[],[i_0_40,i_0_43,i_0_45,i_0_30,i_0_33,i_0_27]) ).
cnf(i_0_66,plain,
( ~ aElementOf0(X1,X2)
| aElement0(X1)
| ~ aSet0(X2) ),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_67,plain,
xB != xA,
inference(scs_inference,[],[i_0_35,i_0_38,i_0_40,i_0_43,i_0_45,i_0_30,i_0_33,i_0_27,i_0_49]) ).
cnf(i_0_68,plain,
xB != xC,
inference(scs_inference,[],[i_0_35,i_0_38,i_0_39,i_0_40,i_0_43,i_0_45,i_0_30,i_0_33,i_0_27,i_0_49,i_0_50]) ).
cnf(i_0_69,plain,
xA != xC,
inference(scs_inference,[],[i_0_35,i_0_36,i_0_38,i_0_39,i_0_40,i_0_43,i_0_45,i_0_30,i_0_33,i_0_27,i_0_49,i_0_50,i_0_52]) ).
cnf(i_0_70,plain,
aSubsetOf0(slcrc0,xC),
inference(scs_inference,[],[i_0_35,i_0_36,i_0_38,i_0_39,i_0_40,i_0_57,i_0_43,i_0_45,i_0_59,i_0_30,i_0_33,i_0_27,i_0_49,i_0_50,i_0_52,i_0_23]) ).
cnf(i_0_71,plain,
~ aElementOf0(X1,slcrc0),
inference(rename_variables,[],[i_0_57]) ).
cnf(i_0_72,plain,
( aElementOf0(esk2_2(X1,X2),X2)
| aSubsetOf0(X2,X1)
| ~ aSet0(X2)
| ~ aSet0(X1) ),
inference(rename_variables,[],[i_0_23]) ).
cnf(i_0_73,plain,
$false,
inference(scs_inference,[],[i_0_35,i_0_36,i_0_38,i_0_39,i_0_40,i_0_57,i_0_43,i_0_45,i_0_59,i_0_30,i_0_33,i_0_27,i_0_49,i_0_50,i_0_52,i_0_23,i_0_24]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM533+2 : TPTP v9.2.1. Released v4.0.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 : n023.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 00:43:23 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.27/1.61 % Version : CSE_E---1.7
% 0.27/1.61 % Problem : theBenchmark.p
% 0.27/1.61 % SZS status Theorem for theBenchmark.p
% 0.27/1.61 % SZS output start CNFRefutation
% See solution above
% 0.27/1.67 % Total time : 1.272s
%------------------------------------------------------------------------------