%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : CSR063+1 : TPTP v9.2.1. Released v3.4.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 : n003.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:14:39 PM UTC 2026
% Result : Theorem 1.30s 1.72s
% Output : CNFRefutation 1.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 12
% Syntax : Number of formulae : 46 ( 9 unt; 0 def)
% Number of atoms : 83 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 73 ( 36 ~; 27 |; 1 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 47 ( 3 sgn 26 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just16,axiom,
! [X1] :
( inanimateobject_nonnatural(X1)
=> inanimateobject(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just16) ).
fof(just14,axiom,
! [X1] :
( artifact(X1)
=> inanimateobject_nonnatural(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just14) ).
fof(just9,axiom,
! [X1] :
( computerdataartifact(X1)
=> artifact(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just9) ).
fof(just18,axiom,
! [X1] :
( inanimateobject(X1)
=> partiallytangible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just18) ).
fof(just7,axiom,
! [X1] :
~ ( intangible(X1)
& partiallytangible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just7) ).
fof(just5,axiom,
! [X1] :
( mathematicalorcomputationalthing(X1)
=> intangible(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just5) ).
fof(just11,axiom,
! [X1] :
( mathematicalthing(X1)
=> mathematicalorcomputationalthing(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just11) ).
fof(just2,axiom,
! [X1] :
( setorcollection(X1)
=> mathematicalthing(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just2) ).
fof(just22,axiom,
! [X7,X8] :
( disjointwith(X7,X8)
=> no(X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just22) ).
fof(query63,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query63) ).
fof(just95,axiom,
! [X7] : computerdataartifact(f_urlreferentfn(X7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just95) ).
fof(just44,axiom,
! [X9,X8] :
( no(X9,X8)
=> setorcollection(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just44) ).
fof(c_0_12,plain,
! [X206] :
( ~ inanimateobject_nonnatural(X206)
| inanimateobject(X206) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just16])]) ).
fof(c_0_13,plain,
! [X205] :
( ~ artifact(X205)
| inanimateobject_nonnatural(X205) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just14])]) ).
cnf(c_0_14,plain,
( inanimateobject(X1)
| ~ inanimateobject_nonnatural(X1) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_15,plain,
( inanimateobject_nonnatural(X1)
| ~ artifact(X1) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_16,plain,
! [X203] :
( ~ computerdataartifact(X203)
| artifact(X203) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just9])]) ).
fof(c_0_17,plain,
! [X207] :
( ~ inanimateobject(X207)
| partiallytangible(X207) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just18])]) ).
cnf(c_0_18,plain,
( inanimateobject(X1)
| ~ artifact(X1) ),
inference(spm,[status(thm)],[c_0_14,c_0_15]) ).
cnf(c_0_19,plain,
( artifact(X1)
| ~ computerdataartifact(X1) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_20,plain,
! [X202] :
( ~ intangible(X202)
| ~ partiallytangible(X202) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just7])]) ).
cnf(c_0_21,plain,
( partiallytangible(X1)
| ~ inanimateobject(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_22,plain,
( inanimateobject(X1)
| ~ computerdataartifact(X1) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_23,plain,
( ~ intangible(X1)
| ~ partiallytangible(X1) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_24,plain,
( partiallytangible(X1)
| ~ computerdataartifact(X1) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
fof(c_0_25,plain,
! [X201] :
( ~ mathematicalorcomputationalthing(X201)
| intangible(X201) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just5])]) ).
cnf(c_0_26,plain,
( ~ intangible(X1)
| ~ computerdataartifact(X1) ),
inference(spm,[status(thm)],[c_0_23,c_0_24]) ).
cnf(c_0_27,plain,
( intangible(X1)
| ~ mathematicalorcomputationalthing(X1) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
fof(c_0_28,plain,
! [X204] :
( ~ mathematicalthing(X204)
| mathematicalorcomputationalthing(X204) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just11])]) ).
cnf(c_0_29,plain,
( ~ mathematicalorcomputationalthing(X1)
| ~ computerdataartifact(X1) ),
inference(spm,[status(thm)],[c_0_26,c_0_27]) ).
cnf(c_0_30,plain,
( mathematicalorcomputationalthing(X1)
| ~ mathematicalthing(X1) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
fof(c_0_31,plain,
! [X200] :
( ~ setorcollection(X200)
| mathematicalthing(X200) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just2])]) ).
fof(c_0_32,plain,
! [X214,X215] :
( ~ disjointwith(X214,X215)
| no(X214,X215) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just22])]) ).
fof(c_0_33,negated_conjecture,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[query63])]) ).
cnf(c_0_34,plain,
( ~ computerdataartifact(X1)
| ~ mathematicalthing(X1) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_35,plain,
( mathematicalthing(X1)
| ~ setorcollection(X1) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
fof(c_0_36,plain,
! [X348] : computerdataartifact(f_urlreferentfn(X348)),
inference(variable_rename,[status(thm)],[just95]) ).
fof(c_0_37,plain,
! [X257,X258] :
( ~ no(X257,X258)
| setorcollection(X257) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[just44])]) ).
cnf(c_0_38,plain,
( no(X1,X2)
| ~ disjointwith(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_39,negated_conjecture,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_40,plain,
( ~ computerdataartifact(X1)
| ~ setorcollection(X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_41,plain,
computerdataartifact(f_urlreferentfn(X1)),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_42,plain,
( setorcollection(X1)
| ~ no(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_43,negated_conjecture,
no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_44,plain,
~ setorcollection(f_urlreferentfn(X1)),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_45,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_44]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR063+1 : TPTP v9.2.1. Released v3.4.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 : n003.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 16:41:41 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.30/1.72 % Version : CSE_E---1.7
% 1.30/1.72 % Problem : theBenchmark.p
% 1.30/1.72 % SZS status Theorem for theBenchmark.p
% 1.30/1.72 % SZS output start CNFRefutation
% See solution above
% 1.30/1.72 % Total time : 1.373s
%------------------------------------------------------------------------------