%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : CSR081+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:16:37 PM UTC 2026
% Result : Theorem 17.81s 10.88s
% Output : CNFRefutation 17.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 15
% Syntax : Number of formulae : 59 ( 23 unt; 0 def)
% Number of atoms : 204 ( 14 equ)
% Maximal formula atoms : 45 ( 3 avg)
% Number of connectives : 244 ( 99 ~; 102 |; 28 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-3 aty)
% Number of variables : 72 ( 8 sgn 43 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_from_ALL,conjecture,
( s__mother(s__Bob7_1,s__Jane7_1)
& s__mother(s__Bill7_1,s__Jane7_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(kb_SUMO_32603,axiom,
! [X137,X12,X136] :
( X12 = s__UnionFn(X136,X137)
<=> ! [X1138,X34,X1139] :
( ( s__instance(X137,s__SetOrClass)
& s__instance(X12,s__SetOrClass)
& s__instance(X136,s__SetOrClass) )
=> ( ( s__instance(X1139,X12)
& s__instance(X34,X137)
& s__instance(X1138,X136) )
=> ( ( s__instance(X1139,X137)
| s__instance(X1139,X136) )
& s__instance(X34,X12)
& s__instance(X1138,X12) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_32603) ).
fof(local_4,axiom,
s__mother(s__Bill7_1,s__Jane7_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_4) ).
fof(kb_SUMO_26636,axiom,
! [X1,X15,X13] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X15,s__SetOrClass) )
=> ( ( s__instance(X13,X1)
& s__subclass(X1,X15) )
=> s__instance(X13,X15) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_26636) ).
fof(kb_SUMO_35758,axiom,
! [X926,X928] :
( ( s__instance(X926,s__Organism)
& s__instance(X928,s__Organism) )
=> ( ( s__attribute(X928,s__Female)
& s__parent(X926,X928) )
=> s__mother(X926,X928) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_35758) ).
fof(kb_SUMO_35731,axiom,
! [X1224,X926] :
( ( s__instance(X1224,s__Organism)
& s__instance(X926,s__Organism) )
=> ( s__mother(X926,X1224)
=> s__attribute(X1224,s__Female) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_35731) ).
fof(kb_SUMO_28164,axiom,
! [X1034,X1035] :
( ( s__instance(X1034,s__Organism)
& s__instance(X1035,s__Organism) )
=> ( s__sibling(X1034,X1035)
=> s__sibling(X1035,X1034) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_28164) ).
fof(kb_SUMO_72666,axiom,
s__subclass(s__Man,s__Organism),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+5.ax',kb_SUMO_72666) ).
fof(kb_SUMO_36736,axiom,
s__subclass(s__Woman,s__Organism),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+5.ax',kb_SUMO_36736) ).
fof(local_5,axiom,
s__sibling(s__Bob7_1,s__Bill7_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_5) ).
fof(local_3,axiom,
s__instance(s__Bob7_1,s__Man),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_3) ).
fof(local_1,axiom,
s__instance(s__Bill7_1,s__Man),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_1) ).
fof(kb_SUMO_26692,axiom,
! [X548,X550] :
( ( s__instance(X548,s__Organism)
& s__instance(X550,s__Organism) )
=> ( s__mother(X548,X550)
=> s__parent(X548,X550) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_26692) ).
fof(local_2,axiom,
s__instance(s__Jane7_1,s__Woman),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',local_2) ).
fof(kb_SUMO_35756,axiom,
! [X858,X859,X928] :
( ( s__instance(X858,s__Organism)
& s__instance(X859,s__Organism)
& s__instance(X928,s__Organism) )
=> ( ( s__parent(X858,X928)
& s__sibling(X858,X859) )
=> s__parent(X859,X928) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+2.ax',kb_SUMO_35756) ).
fof(c_0_15,negated_conjecture,
~ ( s__mother(s__Bob7_1,s__Jane7_1)
& s__mother(s__Bill7_1,s__Jane7_1) ),
inference(assume_negation,[status(cth)],[prove_from_ALL]) ).
fof(c_0_16,negated_conjecture,
( ~ s__mother(s__Bob7_1,s__Jane7_1)
| ~ s__mother(s__Bill7_1,s__Jane7_1) ),
inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_15])]) ).
fof(c_0_17,plain,
! [X2415,X2416,X2417,X2418,X2419,X2420,X2421,X2422,X2423] :
( ( X2422 = s__UnionFn(X2423,X2421)
| ~ s__instance(esk7_3(X2421,X2422,X2423),X2422)
| ~ s__instance(esk6_3(X2421,X2422,X2423),X2422)
| ~ s__instance(esk8_3(X2421,X2422,X2423),X2421) )
& ( X2422 = s__UnionFn(X2423,X2421)
| ~ s__instance(esk7_3(X2421,X2422,X2423),X2422)
| ~ s__instance(esk6_3(X2421,X2422,X2423),X2422)
| ~ s__instance(esk8_3(X2421,X2422,X2423),X2423) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(esk8_3(X2421,X2422,X2423),X2422) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(esk7_3(X2421,X2422,X2423),X2421) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(esk6_3(X2421,X2422,X2423),X2423) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(X2421,s__SetOrClass) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(X2422,s__SetOrClass) )
& ( X2422 = s__UnionFn(X2423,X2421)
| s__instance(X2423,s__SetOrClass) )
& ( X2416 != s__UnionFn(X2417,X2415)
| ~ s__instance(X2415,s__SetOrClass)
| ~ s__instance(X2416,s__SetOrClass)
| ~ s__instance(X2417,s__SetOrClass)
| ~ s__instance(X2420,X2416)
| ~ s__instance(X2419,X2415)
| ~ s__instance(X2418,X2417)
| s__instance(X2420,X2415)
| s__instance(X2420,X2417) )
& ( X2416 != s__UnionFn(X2417,X2415)
| ~ s__instance(X2415,s__SetOrClass)
| ~ s__instance(X2416,s__SetOrClass)
| ~ s__instance(X2417,s__SetOrClass)
| ~ s__instance(X2420,X2416)
| ~ s__instance(X2419,X2415)
| ~ s__instance(X2418,X2417)
| s__instance(X2419,X2416) )
& ( X2416 != s__UnionFn(X2417,X2415)
| ~ s__instance(X2415,s__SetOrClass)
| ~ s__instance(X2416,s__SetOrClass)
| ~ s__instance(X2417,s__SetOrClass)
| ~ s__instance(X2420,X2416)
| ~ s__instance(X2419,X2415)
| ~ s__instance(X2418,X2417)
| s__instance(X2418,X2416) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[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])])])])])])]) ).
cnf(c_0_18,negated_conjecture,
( ~ s__mother(s__Bob7_1,s__Jane7_1)
| ~ s__mother(s__Bill7_1,s__Jane7_1) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_19,plain,
s__mother(s__Bill7_1,s__Jane7_1),
inference(split_conjunct,[status(thm)],[local_4]) ).
cnf(c_0_20,plain,
( X2 = s__UnionFn(X3,X1)
| s__instance(X1,s__SetOrClass) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_21,negated_conjecture,
~ s__mother(s__Bob7_1,s__Jane7_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_18,c_0_19])]) ).
cnf(c_0_22,plain,
( s__instance(X3,s__SetOrClass)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_20,c_0_20]) ).
fof(c_0_23,plain,
! [X2400,X2401,X2402] :
( s__instance(X2402,X2401)
| ~ s__instance(X2402,X2400)
| ~ s__subclass(X2400,X2401)
| ~ s__instance(X2400,s__SetOrClass)
| ~ s__instance(X2401,s__SetOrClass) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_26636])])]) ).
cnf(c_0_24,negated_conjecture,
( ~ s__mother(X2,s__Jane7_1)
| s__instance(X1,s__SetOrClass) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
cnf(c_0_25,plain,
( ~ s__instance(X3,X2)
| ~ s__subclass(X2,X1)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| s__instance(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_26,negated_conjecture,
s__instance(X1,s__SetOrClass),
inference(spm,[status(thm)],[c_0_24,c_0_19]) ).
fof(c_0_27,plain,
! [X2389,X2390] :
( s__mother(X2389,X2390)
| ~ s__attribute(X2390,s__Female)
| ~ s__parent(X2389,X2390)
| ~ s__instance(X2389,s__Organism)
| ~ s__instance(X2390,s__Organism) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_35758])])]) ).
fof(c_0_28,plain,
! [X2387,X2388] :
( s__attribute(X2387,s__Female)
| ~ s__mother(X2388,X2387)
| ~ s__instance(X2387,s__Organism)
| ~ s__instance(X2388,s__Organism) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_35731])])]) ).
fof(c_0_29,plain,
! [X2620,X2621] :
( s__sibling(X2621,X2620)
| ~ s__sibling(X2620,X2621)
| ~ s__instance(X2620,s__Organism)
| ~ s__instance(X2621,s__Organism) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_28164])])]) ).
cnf(c_0_30,plain,
( ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3)
| s__instance(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_25,c_0_26]),c_0_26])]) ).
cnf(c_0_31,plain,
s__subclass(s__Man,s__Organism),
inference(split_conjunct,[status(thm)],[kb_SUMO_72666]) ).
cnf(c_0_32,plain,
( ~ s__attribute(X1,s__Female)
| ~ s__parent(X2,X1)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__mother(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_33,plain,
( ~ s__mother(X1,X2)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__attribute(X2,s__Female) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_34,plain,
s__subclass(s__Woman,s__Organism),
inference(split_conjunct,[status(thm)],[kb_SUMO_36736]) ).
cnf(c_0_35,plain,
( ~ s__sibling(X2,X1)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__sibling(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_36,plain,
s__sibling(s__Bob7_1,s__Bill7_1),
inference(split_conjunct,[status(thm)],[local_5]) ).
cnf(c_0_37,plain,
( ~ s__instance(X1,s__Man)
| s__instance(X1,s__Organism) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_38,plain,
s__instance(s__Bob7_1,s__Man),
inference(split_conjunct,[status(thm)],[local_3]) ).
cnf(c_0_39,plain,
s__instance(s__Bill7_1,s__Man),
inference(split_conjunct,[status(thm)],[local_1]) ).
fof(c_0_40,plain,
! [X2369,X2370] :
( s__parent(X2369,X2370)
| ~ s__mother(X2369,X2370)
| ~ s__instance(X2369,s__Organism)
| ~ s__instance(X2370,s__Organism) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_26692])])]) ).
cnf(c_0_41,negated_conjecture,
( ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ s__attribute(s__Jane7_1,s__Female)
| ~ s__parent(s__Bob7_1,s__Jane7_1) ),
inference(spm,[status(thm)],[c_0_21,c_0_32]) ).
cnf(c_0_42,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__instance(s__Jane7_1,s__Organism)
| s__attribute(s__Jane7_1,s__Female) ),
inference(spm,[status(thm)],[c_0_33,c_0_19]) ).
cnf(c_0_43,plain,
( ~ s__instance(X1,s__Woman)
| s__instance(X1,s__Organism) ),
inference(spm,[status(thm)],[c_0_30,c_0_34]) ).
cnf(c_0_44,plain,
s__instance(s__Jane7_1,s__Woman),
inference(split_conjunct,[status(thm)],[local_2]) ).
fof(c_0_45,plain,
! [X2632,X2633,X2634] :
( s__parent(X2633,X2634)
| ~ s__parent(X2632,X2634)
| ~ s__sibling(X2632,X2633)
| ~ s__instance(X2632,s__Organism)
| ~ s__instance(X2633,s__Organism)
| ~ s__instance(X2634,s__Organism) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_35756])])]) ).
cnf(c_0_46,plain,
( ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism)
| s__sibling(s__Bill7_1,s__Bob7_1) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_47,plain,
s__instance(s__Bob7_1,s__Organism),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_48,plain,
s__instance(s__Bill7_1,s__Organism),
inference(spm,[status(thm)],[c_0_37,c_0_39]) ).
cnf(c_0_49,plain,
( ~ s__mother(X2,X1)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__parent(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_50,negated_conjecture,
( ~ s__instance(s__Bill7_1,s__Organism)
| ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bob7_1,s__Organism)
| ~ s__parent(s__Bob7_1,s__Jane7_1) ),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_51,plain,
s__instance(s__Jane7_1,s__Organism),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_52,plain,
( ~ s__parent(X3,X1)
| ~ s__sibling(X3,X2)
| ~ s__instance(X3,s__Organism)
| ~ s__instance(X2,s__Organism)
| ~ s__instance(X1,s__Organism)
| s__parent(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_53,plain,
s__sibling(s__Bill7_1,s__Bob7_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46,c_0_47])]),c_0_48])]) ).
cnf(c_0_54,plain,
( ~ s__instance(s__Jane7_1,s__Organism)
| ~ s__instance(s__Bill7_1,s__Organism)
| s__parent(s__Bill7_1,s__Jane7_1) ),
inference(spm,[status(thm)],[c_0_49,c_0_19]) ).
cnf(c_0_55,negated_conjecture,
~ s__parent(s__Bob7_1,s__Jane7_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50,c_0_51])]),c_0_47]),c_0_48])]) ).
cnf(c_0_56,plain,
( ~ s__instance(X1,s__Organism)
| ~ s__parent(s__Bill7_1,X1)
| s__parent(s__Bob7_1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_48]),c_0_47])]) ).
cnf(c_0_57,plain,
s__parent(s__Bill7_1,s__Jane7_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54,c_0_51])]),c_0_48])]) ).
cnf(c_0_58,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_56]),c_0_57]),c_0_51])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR081+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.45 % Computer : n026.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 14:53:07 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.46 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.51 Running first-order theorem proving
% 0.24/0.51 Running: /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p
% 17.81/10.88 % Version: 3.5.1
% 17.81/10.88 % Preprocessing class: FLLLSMSLSSSNFFN.
% 17.81/10.88 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 17.81/10.88 % Starting G-E--_300_C01_S5PRR_S00 with 1480s (5) cores
% 17.81/10.88 % Starting new_bool_3 with 296s (1) cores
% 17.81/10.88 % Starting new_bool_1 with 296s (1) cores
% 17.81/10.88 % Starting sh5l with 296s (1) cores
% 17.81/10.88 % new_bool_1 with pid 2543025 completed with status 0
% 17.81/10.88 % Result found by new_bool_1
% 17.81/10.88 % Preprocessing class: FLLLSMSLSSSNFFN.
% 17.81/10.88 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 17.81/10.88 % Starting G-E--_300_C01_S5PRR_S00 with 1480s (5) cores
% 17.81/10.88 % Starting new_bool_3 with 296s (1) cores
% 17.81/10.88 % Starting new_bool_1 with 296s (1) cores
% 17.81/10.88 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 17.81/10.88 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 17.81/10.88 % Search class: FGHSM-FSLM33-MFFFFFNN
% 17.81/10.88 % Scheduled 7 strats onto 1 cores with 296 seconds (296 total)
% 17.81/10.88 % Starting SubtermCWHack with 27s (1) cores
% 17.81/10.88 % SubtermCWHack with pid 2543027 completed with status 0
% 17.81/10.88 % Result found by SubtermCWHack
% 17.81/10.88 % Preprocessing class: FLLLSMSLSSSNFFN.
% 17.81/10.88 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 17.81/10.88 % Starting G-E--_300_C01_S5PRR_S00 with 1480s (5) cores
% 17.81/10.88 % Starting new_bool_3 with 296s (1) cores
% 17.81/10.88 % Starting new_bool_1 with 296s (1) cores
% 17.81/10.88 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 17.81/10.88 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 17.81/10.88 % Search class: FGHSM-FSLM33-MFFFFFNN
% 17.81/10.88 % Scheduled 7 strats onto 1 cores with 296 seconds (296 total)
% 17.81/10.88 % Starting SubtermCWHack with 27s (1) cores
% 17.81/10.88 % Preprocessing time : 0.033 s
% 17.81/10.88
% 17.81/10.88 % Proof found!
% 17.81/10.88 % SZS status Theorem
% 17.81/10.88 % SZS output start CNFRefutation
% See solution above
% 17.81/10.88 % Parsed axioms : 145107
% 17.81/10.88 % Removed by relevancy pruning/SinE : 144372
% 17.81/10.88 % Initial clauses : 882
% 17.81/10.88 % Removed in clause preprocessing : 26
% 17.81/10.88 % Initial clauses in saturation : 856
% 17.81/10.88 % Processed clauses : 15278
% 17.81/10.88 % ...of these trivial : 609
% 17.81/10.88 % ...subsumed : 9342
% 17.81/10.88 % ...remaining for further processing : 5327
% 17.81/10.88 % Other redundant clauses eliminated : 62
% 17.81/10.88 % Clauses deleted for lack of memory : 0
% 17.81/10.88 % Backward-subsumed : 35
% 17.81/10.88 % Backward-rewritten : 132
% 17.81/10.88 % Generated clauses : 99019
% 17.81/10.88 % ...of the previous two non-redundant : 97840
% 17.81/10.88 % ...aggressively subsumed : 0
% 17.81/10.88 % Contextual simplify-reflections : 225
% 17.81/10.88 % Paramodulations : 98957
% 17.81/10.88 % Factorizations : 0
% 17.81/10.88 % NegExts : 0
% 17.81/10.88 % Equation resolutions : 63
% 17.81/10.88 % Disequality decompositions : 0
% 17.81/10.88 % Total rewrite steps : 7282
% 17.81/10.88 % ...of those cached : 6686
% 17.81/10.88 % Propositional unsat checks : 0
% 17.81/10.88 % Propositional check models : 0
% 17.81/10.88 % Propositional check unsatisfiable : 0
% 17.81/10.88 % Propositional clauses : 0
% 17.81/10.88 % Propositional clauses after purity: 0
% 17.81/10.88 % Propositional unsat core size : 0
% 17.81/10.88 % Propositional preprocessing time : 0.000
% 17.81/10.88 % Propositional encoding time : 0.000
% 17.81/10.88 % Propositional solver time : 0.000
% 17.81/10.88 % Success case prop preproc time : 0.000
% 17.81/10.88 % Success case prop encoding time : 0.000
% 17.81/10.88 % Success case prop solver time : 0.000
% 17.81/10.88 % Current number of processed clauses : 5099
% 17.81/10.88 % Positive orientable unit clauses : 561
% 17.81/10.88 % Positive unorientable unit clauses: 0
% 17.81/10.88 % Negative unit clauses : 2
% 17.81/10.88 % Non-unit-clauses : 4536
% 17.81/10.88 % Current number of unprocessed clauses: 80589
% 17.81/10.88 % ...number of literals in the above : 245764
% 17.81/10.88 % Current number of archived formulas : 0
% 17.81/10.88 % Current number of archived clauses : 167
% 17.81/10.88 % Clause-clause subsumption calls (NU) : 4809266
% 17.81/10.88 % Rec. Clause-clause subsumption calls : 2894483
% 17.81/10.88 % Non-unit clause-clause subsumptions : 9597
% 17.81/10.88 % Unit Clause-clause subsumption calls : 24710
% 17.81/10.88 % Rewrite failures with RHS unbound : 0
% 17.81/10.88 % BW rewrite match attempts : 498
% 17.81/10.88 % BW rewrite match successes : 119
% 17.81/10.88 % Condensation attempts : 0
% 17.81/10.88 % Condensation successes : 0
% 17.81/10.88 % Termbank termtop insertions : 1988708
% 17.81/10.88 % Search garbage collected termcells : 465041
% 17.81/10.88
% 17.81/10.88 % -------------------------------------------------
% 17.81/10.88 % User time : 3.639 s
% 17.81/10.88 % System time : 0.482 s
% 17.81/10.88 % Total time : 4.121 s
% 17.81/10.88 % Maximum resident set size: 178160 pages
% 17.81/10.88
% 17.81/10.88 % -------------------------------------------------
% 17.81/10.88 % User time : 8.392 s
% 17.81/10.88 % System time : 0.679 s
% 17.81/10.88 % Total time : 9.071 s
% 17.81/10.88 % Maximum resident set size: 104448 pages
% 17.81/10.88 % E exiting
%------------------------------------------------------------------------------