%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : CSR236+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 12:17:47 PM UTC 2026
% Result : Theorem 126.58s 26.93s
% Output : CNFRefutation 126.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 47 ( 18 unt; 0 def)
% Number of atoms : 114 ( 0 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 115 ( 48 ~; 40 |; 22 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-1 aty)
% Number of variables : 56 ( 4 sgn 22 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(instrumentRelation0042,conjecture,
? [X1,X2] :
( p__instrument(X1,X2)
& p__d__instance(X2,c__EngineeringComponent)
& p__d__instance(X1,c__Process)
& p__d__instance(X2,c__Physical)
& p__d__instance(X1,c__Process) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',instrumentRelation0042) ).
fof(typeA435,axiom,
! [X1038,X1039] :
( p__instrument(X1038,X1039)
=> ( p__d__instance(X1038,c__Process)
& p__d__instance(X1039,c__Physical) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',typeA435) ).
fof(predefinitionsA12,axiom,
! [X1,X2,X3] :
( ( p__d__subclass(X2,X3)
& p__d__instance(X1,X2) )
=> p__d__instance(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA12) ).
fof(miloA287,axiom,
! [X289] :
( p__d__instance(X289,c__SwitchDevice)
=> ? [X87,X88,X545] :
( p__d__instance(X545,c__ElectricDevice)
& p__instrument(X88,X545)
& p__causes(X87,X88)
& p__instrument(X87,X289)
& p__d__instance(X88,c__Process)
& p__d__instance(X87,c__Process) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',miloA287) ).
fof(miloA286,axiom,
p__d__subclass(c__SwitchDevice,c__EngineeringComponent),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',miloA286) ).
fof(predefinitionsA8,axiom,
! [X1,X2,X3] :
( ( p__d__subclass(X2,X3)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',predefinitionsA8) ).
fof(mergeA176,axiom,
! [X7] :
( p__d__subclass(X7,c__Entity)
=> ? [X35] : p__d__instance(X35,X7) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA176) ).
fof(mergeA3134,axiom,
p__d__subclass(c__Artifact,c__Object),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA3134) ).
fof(mergeA3181,axiom,
p__d__subclass(c__Device,c__Artifact),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA3181) ).
fof(mergeA3200,axiom,
p__d__subclass(c__EngineeringComponent,c__Device),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA3200) ).
fof(mergeA178,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA178) ).
fof(mergeA181,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox/benchmark/Axioms/CSR006+0.ax',mergeA181) ).
fof(c_0_12,negated_conjecture,
~ ? [X1,X2] :
( p__instrument(X1,X2)
& p__d__instance(X2,c__EngineeringComponent)
& p__d__instance(X1,c__Process)
& p__d__instance(X2,c__Physical)
& p__d__instance(X1,c__Process) ),
inference(assume_negation,[status(cth)],[instrumentRelation0042]) ).
fof(c_0_13,negated_conjecture,
! [X7881,X7882] :
( ~ p__instrument(X7881,X7882)
| ~ p__d__instance(X7882,c__EngineeringComponent)
| ~ p__d__instance(X7881,c__Process)
| ~ p__d__instance(X7882,c__Physical)
| ~ p__d__instance(X7881,c__Process) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_12])])]) ).
cnf(c_0_14,negated_conjecture,
( ~ p__instrument(X1,X2)
| ~ p__d__instance(X2,c__EngineeringComponent)
| ~ p__d__instance(X1,c__Process)
| ~ p__d__instance(X2,c__Physical)
| ~ p__d__instance(X1,c__Process) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
fof(c_0_15,plain,
! [X7477,X7478] :
( ( ~ p__instrument(X7477,X7478)
| p__d__instance(X7477,c__Process) )
& ( ~ p__instrument(X7477,X7478)
| p__d__instance(X7478,c__Physical) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[typeA435])])])]) ).
fof(c_0_16,plain,
! [X1050,X1051,X1052] :
( p__d__instance(X1050,X1052)
| ~ p__d__subclass(X1051,X1052)
| ~ p__d__instance(X1050,X1051) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[predefinitionsA12])])]) ).
cnf(c_0_17,negated_conjecture,
( ~ p__d__instance(X1,c__Process)
| ~ p__d__instance(X2,c__EngineeringComponent)
| ~ p__d__instance(X2,c__Physical)
| ~ p__instrument(X1,X2) ),
inference(cn,[status(thm)],[c_0_14]) ).
cnf(c_0_18,plain,
( ~ p__instrument(X1,X2)
| p__d__instance(X1,c__Process) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_19,plain,
( ~ p__instrument(X2,X1)
| p__d__instance(X1,c__Physical) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
fof(c_0_20,plain,
! [X3096] :
( ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__d__instance(esk415_1(X3096),c__ElectricDevice) )
& ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__instrument(esk414_1(X3096),esk415_1(X3096)) )
& ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__causes(esk413_1(X3096),esk414_1(X3096)) )
& ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__instrument(esk413_1(X3096),X3096) )
& ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__d__instance(esk414_1(X3096),c__Process) )
& ( ~ p__d__instance(X3096,c__SwitchDevice)
| p__d__instance(esk413_1(X3096),c__Process) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[miloA287])])])])]) ).
cnf(c_0_21,plain,
( ~ p__d__subclass(X2,X3)
| ~ p__d__instance(X1,X2)
| p__d__instance(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_22,plain,
p__d__subclass(c__SwitchDevice,c__EngineeringComponent),
inference(split_conjunct,[status(thm)],[miloA286]) ).
fof(c_0_23,plain,
! [X1045,X1046,X1047] :
( p__d__subclass(X1045,X1047)
| ~ p__d__subclass(X1046,X1047)
| ~ p__d__subclass(X1045,X1046) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[predefinitionsA8])])]) ).
cnf(c_0_24,negated_conjecture,
( ~ p__d__instance(X2,c__EngineeringComponent)
| ~ p__instrument(X1,X2) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_17,c_0_18]),c_0_19]) ).
cnf(c_0_25,plain,
( ~ p__d__instance(X1,c__SwitchDevice)
| p__instrument(esk413_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_26,plain,
( ~ p__d__instance(X1,c__SwitchDevice)
| p__d__instance(X1,c__EngineeringComponent) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
fof(c_0_27,plain,
! [X1279] :
( p__d__instance(esk13_1(X1279),X1279)
| ~ p__d__subclass(X1279,c__Entity) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mergeA176])])])]) ).
cnf(c_0_28,plain,
( ~ p__d__subclass(X2,X3)
| ~ p__d__subclass(X1,X2)
| p__d__subclass(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_29,plain,
p__d__subclass(c__Artifact,c__Object),
inference(split_conjunct,[status(thm)],[mergeA3134]) ).
cnf(c_0_30,plain,
p__d__subclass(c__Device,c__Artifact),
inference(split_conjunct,[status(thm)],[mergeA3181]) ).
cnf(c_0_31,plain,
p__d__subclass(c__EngineeringComponent,c__Device),
inference(split_conjunct,[status(thm)],[mergeA3200]) ).
cnf(c_0_32,negated_conjecture,
~ p__d__instance(X1,c__SwitchDevice),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_24,c_0_25]),c_0_26]) ).
cnf(c_0_33,plain,
( ~ p__d__subclass(X1,c__Entity)
| p__d__instance(esk13_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_34,plain,
p__d__subclass(c__Physical,c__Entity),
inference(split_conjunct,[status(thm)],[mergeA178]) ).
cnf(c_0_35,plain,
( ~ p__d__subclass(X1,c__Artifact)
| p__d__subclass(X1,c__Object) ),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
cnf(c_0_36,plain,
( ~ p__d__subclass(X1,c__Device)
| p__d__subclass(X1,c__Artifact) ),
inference(spm,[status(thm)],[c_0_28,c_0_30]) ).
cnf(c_0_37,plain,
( ~ p__d__subclass(X1,c__EngineeringComponent)
| p__d__subclass(X1,c__Device) ),
inference(spm,[status(thm)],[c_0_28,c_0_31]) ).
cnf(c_0_38,negated_conjecture,
~ p__d__subclass(c__SwitchDevice,c__Entity),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_39,plain,
( ~ p__d__subclass(X1,c__Physical)
| p__d__subclass(X1,c__Entity) ),
inference(spm,[status(thm)],[c_0_28,c_0_34]) ).
cnf(c_0_40,plain,
p__d__subclass(c__Object,c__Physical),
inference(split_conjunct,[status(thm)],[mergeA181]) ).
cnf(c_0_41,plain,
( ~ p__d__subclass(X1,c__Device)
| p__d__subclass(X1,c__Object) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_42,plain,
p__d__subclass(c__SwitchDevice,c__Device),
inference(spm,[status(thm)],[c_0_37,c_0_22]) ).
cnf(c_0_43,negated_conjecture,
~ p__d__subclass(c__SwitchDevice,c__Physical),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_44,plain,
( ~ p__d__subclass(X1,c__Object)
| p__d__subclass(X1,c__Physical) ),
inference(spm,[status(thm)],[c_0_28,c_0_40]) ).
cnf(c_0_45,plain,
p__d__subclass(c__SwitchDevice,c__Object),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_46,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_44]),c_0_45])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR236+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.47 % Computer : n009.cluster.edu
% 0.21/0.47 % Model : x86_64 x86_64
% 0.21/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.47 % Memory : 8046.5625MB
% 0.21/0.47 % OS : Linux 6.8.0-71-generic
% 0.21/0.47 % CPULimit : 300
% 0.21/0.47 % WCLimit : 300
% 0.21/0.47 % DateTime : Mon Sep 21 15:19:43 UTC 2026
% 0.21/0.47 % CPUTime :
% 0.21/0.47 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.24/0.56 Running first-order theorem proving
% 0.24/0.56 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 126.58/26.93 % Version: 3.5.1
% 126.58/26.93 % Preprocessing class: FMLLSMSLSSSNFFN.
% 126.58/26.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 126.58/26.93 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 126.58/26.93 % Starting new_bool_3 with 300s (1) cores
% 126.58/26.93 % Starting new_bool_1 with 300s (1) cores
% 126.58/26.93 % Starting sh5l with 300s (1) cores
% 126.58/26.93 % new_bool_1 with pid 2074026 completed with status 9
% 126.58/26.93 % new_bool_3 with pid 2074025 completed with status 9
% 126.58/26.93 % G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with pid 2074024 completed with status 0
% 126.58/26.93 % Result found by G-E--_208_B07_F1_AE_CS_SP_PS_S0Y
% 126.58/26.93 % Preprocessing class: FMLLSMSLSSSNFFN.
% 126.58/26.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 126.58/26.93 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 126.58/26.93 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 126.58/26.93 % No SInE strategy applied
% 126.58/26.93 % Search class: FGHSS-SMLM31-MFFFFFNN
% 126.58/26.93 % Scheduled 13 strats onto 5 cores with 1499 seconds (1499 total)
% 126.58/26.93 % Starting SubtermCWHack with 135s (1) cores
% 126.58/26.93 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 150s (1) cores
% 126.58/26.93 % Starting G-E--_042_C45_F1_PI_AE_Q4_CS_SP_PS_S4S with 113s (1) cores
% 126.58/26.93 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S04BN with 113s (1) cores
% 126.58/26.93 % Starting G----_0021_C18_F1_SE_CS_SP_S4S with 113s (1) cores
% 126.58/26.93 % SubtermCWHack with pid 2074055 completed with status 0
% 126.58/26.93 % Result found by SubtermCWHack
% 126.58/26.93 % Preprocessing class: FMLLSMSLSSSNFFN.
% 126.58/26.93 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 126.58/26.93 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 126.58/26.93 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 126.58/26.93 % No SInE strategy applied
% 126.58/26.93 % Search class: FGHSS-SMLM31-MFFFFFNN
% 126.58/26.93 % Scheduled 13 strats onto 5 cores with 1499 seconds (1499 total)
% 126.58/26.93 % Starting SubtermCWHack with 135s (1) cores
% 126.58/26.93 % Preprocessing time : 0.112 s
% 126.58/26.93
% 126.58/26.93 % Proof found!
% 126.58/26.93 % SZS status Theorem
% 126.58/26.93 % SZS output start CNFRefutation
% See solution above
% 126.58/26.93 % Parsed axioms : 7433
% 126.58/26.93 % Removed by relevancy pruning/SinE : 0
% 126.58/26.93 % Initial clauses : 10860
% 126.58/26.93 % Removed in clause preprocessing : 20
% 126.58/26.93 % Initial clauses in saturation : 10840
% 126.58/26.93 % Processed clauses : 30867
% 126.58/26.93 % ...of these trivial : 314
% 126.58/26.93 % ...subsumed : 575
% 126.58/26.93 % ...remaining for further processing : 29978
% 126.58/26.93 % Other redundant clauses eliminated : 88
% 126.58/26.93 % Clauses deleted for lack of memory : 0
% 126.58/26.93 % Backward-subsumed : 128
% 126.58/26.93 % Backward-rewritten : 453
% 126.58/26.93 % Generated clauses : 333836
% 126.58/26.93 % ...of the previous two non-redundant : 326591
% 126.58/26.93 % ...aggressively subsumed : 0
% 126.58/26.93 % Contextual simplify-reflections : 1837
% 126.58/26.93 % Paramodulations : 333744
% 126.58/26.93 % Factorizations : 1
% 126.58/26.93 % NegExts : 0
% 126.58/26.93 % Equation resolutions : 91
% 126.58/26.93 % Disequality decompositions : 0
% 126.58/26.93 % Total rewrite steps : 7870
% 126.58/26.93 % ...of those cached : 3103
% 126.58/26.93 % Propositional unsat checks : 0
% 126.58/26.93 % Propositional check models : 0
% 126.58/26.93 % Propositional check unsatisfiable : 0
% 126.58/26.93 % Propositional clauses : 0
% 126.58/26.93 % Propositional clauses after purity: 0
% 126.58/26.93 % Propositional unsat core size : 0
% 126.58/26.93 % Propositional preprocessing time : 0.000
% 126.58/26.93 % Propositional encoding time : 0.000
% 126.58/26.93 % Propositional solver time : 0.000
% 126.58/26.93 % Success case prop preproc time : 0.000
% 126.58/26.93 % Success case prop encoding time : 0.000
% 126.58/26.93 % Success case prop solver time : 0.000
% 126.58/26.93 % Current number of processed clauses : 29313
% 126.58/26.93 % Positive orientable unit clauses : 10987
% 126.58/26.93 % Positive unorientable unit clauses: 0
% 126.58/26.93 % Negative unit clauses : 87
% 126.58/26.93 % Non-unit-clauses : 18239
% 126.58/26.93 % Current number of unprocessed clauses: 306412
% 126.58/26.93 % ...number of literals in the above : 646157
% 126.58/26.93 % Current number of archived formulas : 0
% 126.58/26.93 % Current number of archived clauses : 581
% 126.58/26.93 % Clause-clause subsumption calls (NU) : 39208342
% 126.58/26.93 % Rec. Clause-clause subsumption calls : 31471305
% 126.58/26.93 % Non-unit clause-clause subsumptions : 2365
% 126.58/26.93 % Unit Clause-clause subsumption calls : 23891522
% 126.58/26.93 % Rewrite failures with RHS unbound : 0
% 126.58/26.93 % BW rewrite match attempts : 2590
% 126.58/26.93 % BW rewrite match successes : 104
% 126.58/26.93 % Condensation attempts : 0
% 126.58/26.93 % Condensation successes : 0
% 126.58/26.93 % Termbank termtop insertions : 3109103
% 126.58/26.93 % Search garbage collected termcells : 89360
% 126.58/26.93
% 126.58/26.93 % -------------------------------------------------
% 126.58/26.93 % User time : 25.371 s
% 126.58/26.93 % System time : 0.350 s
% 126.58/26.93 % Total time : 25.721 s
% 126.58/26.93 % Maximum resident set size: 32472 pages
% 126.58/26.93
% 126.58/26.93 % -------------------------------------------------
% 126.58/26.93 % User time : 124.050 s
% 126.58/26.93 % System time : 1.898 s
% 126.58/26.93 % Total time : 125.948 s
% 126.58/26.93 % Maximum resident set size: 12544 pages
% 126.58/26.93 % E exiting
%------------------------------------------------------------------------------