%------------------------------------------------------------------------------
% File : ET---2.0
% Problem : SWW333+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_ET %s %d
% Computer : n020.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 : 600s
% DateTime : Thu Jul 21 00:10:35 EDT 2022
% Result : Theorem 1.77s 122.94s
% Output : CNFRefutation 1.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 17 ( 17 unt; 0 def)
% Number of atoms : 17 ( 16 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-3 aty)
% Number of variables : 85 ( 36 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(help_c__COMBS__1,axiom,
! [X154,X4,X6,X8,X169,X22] : hAPP(hAPP(hAPP(c_COMBS(X22,X169,X8),X6),X4),X154) = hAPP(hAPP(X6,X154),hAPP(X4,X154)),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',help_c__COMBS__1) ).
fof(help_c__COMBB__1,axiom,
! [X154,X4,X6,X169,X8,X22] : hAPP(hAPP(hAPP(c_COMBB(X22,X8,X169),X6),X4),X154) = hAPP(X6,hAPP(X4,X154)),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',help_c__COMBB__1) ).
fof(fact_n__not__Suc__n,axiom,
! [X16] : X16 != hAPP(c_Nat_OSuc,X16),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',fact_n__not__Suc__n) ).
fof(fact_the_Osimps,axiom,
! [X35,X17] : hAPP(c_Option_Othe(X17),hAPP(c_Option_Ooption_OSome(X17),X35)) = X35,
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',fact_the_Osimps) ).
fof(c_0_4,plain,
! [X170,X171,X172,X173,X174,X175] : hAPP(hAPP(hAPP(c_COMBS(X175,X174,X173),X172),X171),X170) = hAPP(hAPP(X172,X170),hAPP(X171,X170)),
inference(variable_rename,[status(thm)],[help_c__COMBS__1]) ).
fof(c_0_5,plain,
! [X170,X171,X172,X173,X174,X175] : hAPP(hAPP(hAPP(c_COMBB(X175,X174,X173),X172),X171),X170) = hAPP(X172,hAPP(X171,X170)),
inference(variable_rename,[status(thm)],[help_c__COMBB__1]) ).
fof(c_0_6,plain,
! [X17] : X17 != hAPP(c_Nat_OSuc,X17),
inference(variable_rename,[status(thm)],[fact_n__not__Suc__n]) ).
cnf(c_0_7,plain,
hAPP(hAPP(hAPP(c_COMBS(X1,X2,X3),X4),X5),X6) = hAPP(hAPP(X4,X6),hAPP(X5,X6)),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_8,plain,
hAPP(hAPP(hAPP(c_COMBB(X1,X2,X3),X4),X5),X6) = hAPP(X4,hAPP(X5,X6)),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_9,plain,
X1 != hAPP(c_Nat_OSuc,X1),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_10,plain,
hAPP(hAPP(hAPP(c_COMBS(X1,X2,X3),hAPP(c_COMBB(X4,X5,X6),X7)),X8),X9) = hAPP(X7,hAPP(X9,hAPP(X8,X9))),
inference(spm,[status(thm)],[c_0_7,c_0_8]) ).
cnf(c_0_11,plain,
hAPP(hAPP(hAPP(c_COMBS(X1,X2,X3),hAPP(c_COMBB(X4,X5,X6),c_Nat_OSuc)),X7),X8) != hAPP(X8,hAPP(X7,X8)),
inference(pm,[status(thm)],[c_0_9,c_0_10]) ).
fof(c_0_12,plain,
! [X36,X37] : hAPP(c_Option_Othe(X37),hAPP(c_Option_Ooption_OSome(X37),X36)) = X36,
inference(variable_rename,[status(thm)],[fact_the_Osimps]) ).
cnf(c_0_13,plain,
hAPP(hAPP(hAPP(c_COMBS(X1,X2,X3),hAPP(c_COMBB(X4,X5,X6),c_Nat_OSuc)),hAPP(hAPP(c_COMBB(X7,X8,X9),X10),X11)),X12) != hAPP(X12,hAPP(X10,hAPP(X11,X12))),
inference(spm,[status(thm)],[c_0_11,c_0_8]) ).
cnf(c_0_14,plain,
hAPP(c_Option_Othe(X1),hAPP(c_Option_Ooption_OSome(X1),X2)) = X2,
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_15,plain,
hAPP(hAPP(hAPP(c_COMBS(X1,X2,X3),hAPP(c_COMBB(X4,X5,X6),c_Nat_OSuc)),hAPP(hAPP(c_COMBB(X7,X8,X9),c_Option_Othe(X10)),c_Option_Ooption_OSome(X10))),X11) != hAPP(X11,X11),
inference(spm,[status(thm)],[c_0_13,c_0_14]) ).
cnf(c_0_16,plain,
$false,
inference(er,[status(thm)],[c_0_15]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWW333+1 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.13 % Command : run_ET %s %d
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 6 08:42:37 EDT 2022
% 0.13/0.35 % CPUTime :
% 1.10/24.12 eprover: CPU time limit exceeded, terminating
% 1.10/24.13 eprover: CPU time limit exceeded, terminating
% 1.10/24.13 eprover: CPU time limit exceeded, terminating
% 1.10/24.14 eprover: CPU time limit exceeded, terminating
% 1.25/47.14 eprover: CPU time limit exceeded, terminating
% 1.25/47.15 eprover: CPU time limit exceeded, terminating
% 1.25/47.17 eprover: CPU time limit exceeded, terminating
% 1.25/47.17 eprover: CPU time limit exceeded, terminating
% 1.42/70.16 eprover: CPU time limit exceeded, terminating
% 1.42/70.17 eprover: CPU time limit exceeded, terminating
% 1.42/70.18 eprover: CPU time limit exceeded, terminating
% 1.42/70.19 eprover: CPU time limit exceeded, terminating
% 1.57/93.18 eprover: eprover: CPU time limit exceeded, terminatingCPU time limit exceeded, terminating
% 1.57/93.18
% 1.57/93.20 eprover: CPU time limit exceeded, terminating
% 1.57/93.21 eprover: CPU time limit exceeded, terminating
% 1.72/116.20 eprover: CPU time limit exceeded, terminating
% 1.72/116.21 eprover: CPU time limit exceeded, terminating
% 1.72/116.22 eprover: CPU time limit exceeded, terminating
% 1.72/116.23 eprover: CPU time limit exceeded, terminating
% 1.77/122.94 # Running protocol protocol_eprover_29fa5c60d0ee03ec4f64b055553dc135fbe4ee3a for 23 seconds:
% 1.77/122.94
% 1.77/122.94 # Failure: Resource limit exceeded (time)
% 1.77/122.94 # OLD status Res
% 1.77/122.94 # Preprocessing time : 0.906 s
% 1.77/122.94 # Running protocol protocol_eprover_773c90a94152ea2e8c9d3df9c4b1eb6152c40c03 for 23 seconds:
% 1.77/122.94
% 1.77/122.94 # Failure: Resource limit exceeded (time)
% 1.77/122.94 # OLD status Res
% 1.77/122.94 # SinE strategy is GSinE(CountFormulas,hypos,1.5,,,100,1.0)
% 1.77/122.94 # Preprocessing time : 0.169 s
% 1.77/122.94 # Running protocol protocol_eprover_75515770aeb32f68e33e9fbd9dff93f5a2e34f2e for 23 seconds:
% 1.77/122.94
% 1.77/122.94 # Failure: Resource limit exceeded (time)
% 1.77/122.94 # OLD status Res
% 1.77/122.94 # Preprocessing time : 0.937 s
% 1.77/122.94 # Running protocol protocol_eprover_6c565d2524e660970ec2a72c26d577f665a55420 for 23 seconds:
% 1.77/122.94
% 1.77/122.94 # Failure: Resource limit exceeded (time)
% 1.77/122.94 # OLD status Res
% 1.77/122.94 # Preprocessing time : 1.038 s
% 1.77/122.94 # Running protocol protocol_eprover_750456fc664a9e0b97096ad0f5110b1ead7d782b for 23 seconds:
% 1.77/122.94
% 1.77/122.94 # Failure: Resource limit exceeded (time)
% 1.77/122.94 # OLD status Res
% 1.77/122.94 # Preprocessing time : 0.742 s
% 1.77/122.94 # Running protocol protocol_eprover_a9abcacdf80c460fdc9fe242616d68da2308faf5 for 23 seconds:
% 1.77/122.94 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,02,500,1.0)
% 1.77/122.94 # Preprocessing time : 0.177 s
% 1.77/122.94
% 1.77/122.94 # Proof found!
% 1.77/122.94 # SZS status Theorem
% 1.77/122.94 # SZS output start CNFRefutation
% See solution above
% 1.77/122.94 # Proof object total steps : 17
% 1.77/122.94 # Proof object clause steps : 9
% 1.77/122.94 # Proof object formula steps : 8
% 1.77/122.94 # Proof object conjectures : 0
% 1.77/122.94 # Proof object clause conjectures : 0
% 1.77/122.94 # Proof object formula conjectures : 0
% 1.77/122.94 # Proof object initial clauses used : 4
% 1.77/122.94 # Proof object initial formulas used : 4
% 1.77/122.94 # Proof object generating inferences : 5
% 1.77/122.94 # Proof object simplifying inferences : 0
% 1.77/122.94 # Training examples: 0 positive, 0 negative
% 1.77/122.94 # Parsed axioms : 5209
% 1.77/122.94 # Removed by relevancy pruning/SinE : 4708
% 1.77/122.94 # Initial clauses : 771
% 1.77/122.94 # Removed in clause preprocessing : 42
% 1.77/122.94 # Initial clauses in saturation : 729
% 1.77/122.94 # Processed clauses : 4185
% 1.77/122.94 # ...of these trivial : 42
% 1.77/122.94 # ...subsumed : 2854
% 1.77/122.94 # ...remaining for further processing : 1289
% 1.77/122.94 # Other redundant clauses eliminated : 75
% 1.77/122.94 # Clauses deleted for lack of memory : 145168
% 1.77/122.94 # Backward-subsumed : 37
% 1.77/122.94 # Backward-rewritten : 16
% 1.77/122.94 # Generated clauses : 253295
% 1.77/122.94 # ...of the previous two non-trivial : 251769
% 1.77/122.94 # Contextual simplify-reflections : 0
% 1.77/122.94 # Paramodulations : 253070
% 1.77/122.94 # Factorizations : 4
% 1.77/122.94 # Equation resolutions : 210
% 1.77/122.94 # Current number of processed clauses : 1214
% 1.77/122.94 # Positive orientable unit clauses : 118
% 1.77/122.94 # Positive unorientable unit clauses: 230
% 1.77/122.94 # Negative unit clauses : 99
% 1.77/122.94 # Non-unit-clauses : 767
% 1.77/122.94 # Current number of unprocessed clauses: 98997
% 1.77/122.94 # ...number of literals in the above : 165549
% 1.77/122.94 # Current number of archived formulas : 0
% 1.77/122.94 # Current number of archived clauses : 53
% 1.77/122.94 # Clause-clause subsumption calls (NU) : 66220
% 1.77/122.94 # Rec. Clause-clause subsumption calls : 53636
% 1.77/122.94 # Non-unit clause-clause subsumptions : 1884
% 1.77/122.94 # Unit Clause-clause subsumption calls : 7726
% 1.77/122.94 # Rewrite failures with RHS unbound : 4219
% 1.77/122.94 # BW rewrite match attempts : 24485
% 1.77/122.94 # BW rewrite match successes : 794
% 1.77/122.94 # Condensation attempts : 0
% 1.77/122.94 # Condensation successes : 0
% 1.77/122.94 # Termbank termtop insertions : 8136091
% 1.77/122.94
% 1.77/122.94 # -------------------------------------------------
% 1.77/122.94 # User time : 5.915 s
% 1.77/122.94 # System time : 0.099 s
% 1.77/122.94 # Total time : 6.014 s
% 1.77/122.94 # Maximum resident set size: 143016 pages
% 1.77/139.21 eprover: CPU time limit exceeded, terminating
% 1.77/139.23 eprover: CPU time limit exceeded, terminating
% 1.77/139.23 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.23 eprover: No such file or directory
% 1.77/139.24 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.24 eprover: No such file or directory
% 1.77/139.24 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.24 eprover: No such file or directory
% 1.77/139.25 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.25 eprover: No such file or directory
% 1.77/139.25 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.25 eprover: No such file or directory
% 1.77/139.25 eprover: CPU time limit exceeded, terminating
% 1.77/139.25 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.25 eprover: No such file or directory
% 1.77/139.25 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.25 eprover: No such file or directory
% 1.77/139.25 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 1.77/139.25 eprover: No such file or directory
% 1.77/139.26 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.26 eprover: No such file or directory
% 1.77/139.26 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.26 eprover: No such file or directory
% 1.77/139.26 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.26 eprover: No such file or directory
% 1.77/139.27 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.27 eprover: No such file or directory
% 1.77/139.27 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.27 eprover: No such file or directory
% 1.77/139.27 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.27 eprover: No such file or directory
% 1.77/139.27 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.27 eprover: No such file or directory
% 1.77/139.28 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.28 eprover: No such file or directory
% 1.77/139.28 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.28 eprover: No such file or directory
% 1.77/139.29 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 1.77/139.29 eprover: No such file or directory
%------------------------------------------------------------------------------