%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP206_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:54:30 PM UTC 2026
% Result : Theorem 0.41s 0.79s
% Output : CNFRefutation 0.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 8
% Syntax : Number of formulae : 35 ( 15 unt; 0 typ; 0 def)
% Number of atoms : 66 ( 38 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 59 ( 28 ~; 22 |; 1 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 13 ( 12 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-2 aty)
% Number of variables : 74 ( 0 sgn 73 !; 1 ?; 74 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
bool: $tType ).
tff(decl_sort2,type,
ref_a: $tType ).
tff(decl_sort3,type,
heap_e7401611519738050253t_unit: $tType ).
tff(decl_sort4,type,
fun_Pr7082408943852936193t_unit: $tType ).
tff(decl_sort5,type,
fun_Pr1332931745038653183_ref_a: $tType ).
tff(decl_sort6,type,
produc7812382424243267045t_unit: $tType ).
tff(decl_sort7,type,
heap_Heap_ref_a: $tType ).
tff(decl_sort8,type,
fun_he1716177789110362441a_bool: $tType ).
tff(decl_sort9,type,
a: $tType ).
tff(decl_sort10,type,
fun_he3288789352778960325t_unit: $tType ).
tff(decl_sort11,type,
fun_a_7797985579152759073_ref_a: $tType ).
tff(decl_sort12,type,
fun_ref_a_bool: $tType ).
tff(decl_1796,type,
heap_effect_ref_a: ( heap_e7401611519738050253t_unit * heap_Heap_ref_a ) > fun_he1716177789110362441a_bool ).
tff(decl_2182,type,
produc6544324848051098391t_unit: ref_a > fun_he3288789352778960325t_unit ).
tff(decl_2445,type,
produc473321116828791851t_unit: fun_Pr1332931745038653183_ref_a ).
tff(decl_2475,type,
produc1126150082675451753t_unit: fun_Pr7082408943852936193t_unit ).
tff(decl_2513,type,
alloc_a: a > fun_he3288789352778960325t_unit ).
tff(decl_2522,type,
ref_a2: fun_a_7797985579152759073_ref_a ).
tff(decl_3217,type,
aa_hea1409956391221964662t_unit: ( heap_e7401611519738050253t_unit * fun_he3288789352778960325t_unit ) > produc7812382424243267045t_unit ).
tff(decl_3221,type,
aa_hea8135729668157506370a_bool: ( heap_e7401611519738050253t_unit * fun_he1716177789110362441a_bool ) > fun_ref_a_bool ).
tff(decl_3226,type,
aa_ref_a_bool: ( ref_a * fun_ref_a_bool ) > bool ).
tff(decl_3407,type,
aa_Pro8575920914306358506t_unit: ( produc7812382424243267045t_unit * fun_Pr7082408943852936193t_unit ) > heap_e7401611519738050253t_unit ).
tff(decl_3408,type,
aa_Pro7711270743135521984_ref_a: ( produc7812382424243267045t_unit * fun_Pr1332931745038653183_ref_a ) > ref_a ).
tff(decl_4071,type,
aa_a_Heap_Heap_ref_a: ( a * fun_a_7797985579152759073_ref_a ) > heap_Heap_ref_a ).
tff(decl_4148,type,
pp: bool > $o ).
tff(decl_4149,type,
h: heap_e7401611519738050253t_unit ).
tff(decl_4150,type,
h2: heap_e7401611519738050253t_unit ).
tff(decl_4151,type,
r: ref_a ).
tff(decl_4152,type,
thesis: $o ).
tff(decl_4153,type,
x: a ).
tff(decl_4156,type,
esk3_2: ( produc7812382424243267045t_unit * heap_e7401611519738050253t_unit ) > ref_a ).
fof(conj_1,conjecture,
thesis,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
tff(fact_183_effect__deterministic_I2_J,axiom,
! [X393: heap_Heap_ref_a,X11: heap_e7401611519738050253t_unit,X17: heap_e7401611519738050253t_unit,X394: ref_a,X395: heap_e7401611519738050253t_unit,X396: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X393,X11),X17),X394))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X393,X11),X395),X396))
=> ( X17 = X395 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_effect__deterministic_I2_J) ).
tff(fact_1_assms,axiom,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_assms) ).
tff(fact_28_effect__refI,axiom,
! [X15: ref_a,X17: heap_e7401611519738050253t_unit,X13: a,X11: heap_e7401611519738050253t_unit] :
( ( aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X15),X17) = aa_hea1409956391221964662t_unit(alloc_a(X13),X11) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,X13),X11),X17),X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_effect__refI) ).
tff(fact_167_eq__snd__iff,axiom,
! [X351: heap_e7401611519738050253t_unit,X3: produc7812382424243267045t_unit] :
( ( X351 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X3) )
<=> ? [X352: ref_a] : ( X3 = aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X352),X351) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_eq__snd__iff) ).
tff(fact_184_effect__deterministic_I1_J,axiom,
! [X397: heap_Heap_ref_a,X11: heap_e7401611519738050253t_unit,X17: heap_e7401611519738050253t_unit,X398: ref_a,X395: heap_e7401611519738050253t_unit,X399: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X397,X11),X17),X398))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X397,X11),X395),X399))
=> ( X398 = X399 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_effect__deterministic_I1_J) ).
tff(fact_0_that,axiom,
( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> thesis ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_that) ).
tff(fact_101_fst__conv,axiom,
! [X208: ref_a,X209: heap_e7401611519738050253t_unit] : ( aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X208),X209)) = X208 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_fst__conv) ).
fof(c_0_8,negated_conjecture,
~ thesis,
inference(assume_negation,[status(cth)],[conj_1]) ).
tff(c_0_9,plain,
! [X14833: heap_Heap_ref_a,X14834: heap_e7401611519738050253t_unit,X14835: heap_e7401611519738050253t_unit,X14836: ref_a,X14837: heap_e7401611519738050253t_unit,X14838: ref_a] :
( ( X14835 = X14837 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X14833,X14834),X14837),X14838))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X14833,X14834),X14835),X14836)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_183_effect__deterministic_I2_J])])]) ).
fof(c_0_10,negated_conjecture,
~ thesis,
inference(fof_simplification,[status(thm)],[c_0_8]) ).
tcf(c_0_11,plain,
! [X6: ref_a,X7: heap_e7401611519738050253t_unit,X11: heap_e7401611519738050253t_unit,X391: heap_Heap_ref_a,X17: heap_e7401611519738050253t_unit,X15: ref_a] :
( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X391,X7),X17),X15))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X391,X7),X11),X6))
| ( X11 = X17 ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_12,plain,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)),
inference(split_conjunct,[status(thm)],[fact_1_assms]) ).
tff(c_0_13,plain,
! [X14849: ref_a,X14850: heap_e7401611519738050253t_unit,X14851: a,X14852: heap_e7401611519738050253t_unit] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,X14851),X14852),X14850),X14849))
| ( aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X14849),X14850) != aa_hea1409956391221964662t_unit(alloc_a(X14851),X14852) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_28_effect__refI])])]) ).
tff(c_0_14,plain,
! [X14886: heap_e7401611519738050253t_unit,X14887: produc7812382424243267045t_unit,X14889: heap_e7401611519738050253t_unit,X14890: produc7812382424243267045t_unit,X14891: ref_a] :
( ( ( X14889 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X14890) )
| ( X14890 != aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X14891),X14889) ) )
& ( ( X14887 = aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(esk3_2(X14886,X14887)),X14886) )
| ( X14886 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X14887) ) ) ),
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)],[fact_167_eq__snd__iff])])])])])]) ).
tff(c_0_15,plain,
! [X14839: heap_Heap_ref_a,X14840: heap_e7401611519738050253t_unit,X14841: heap_e7401611519738050253t_unit,X14842: ref_a,X14843: heap_e7401611519738050253t_unit,X14844: ref_a] :
( ( X14842 = X14844 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X14839,X14840),X14843),X14844))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X14839,X14840),X14841),X14842)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_184_effect__deterministic_I1_J])])]) ).
tff(c_0_16,plain,
( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ),
inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_0_that])]) ).
fof(c_0_17,negated_conjecture,
~ thesis,
inference(fof_nnf,[status(thm)],[c_0_10]) ).
tcf(c_0_18,plain,
! [X7: heap_e7401611519738050253t_unit,X6: ref_a] :
( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),X7),X6))
| ( X7 = h2 ) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
tcf(c_0_19,plain,
! [X6: ref_a,X7: heap_e7401611519738050253t_unit,X10: a,X11: heap_e7401611519738050253t_unit] :
( ( aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X6),X7) != aa_hea1409956391221964662t_unit(alloc_a(X10),X11) )
| pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,X10),X11),X7),X6)) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
tcf(c_0_20,plain,
! [X7: heap_e7401611519738050253t_unit,X1: produc7812382424243267045t_unit] :
( ( X7 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X1) )
| ( X1 = aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(esk3_2(X7,X1)),X7) ) ),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tcf(c_0_21,plain,
! [X6: ref_a,X11: heap_e7401611519738050253t_unit,X7: heap_e7401611519738050253t_unit,X391: heap_Heap_ref_a,X17: heap_e7401611519738050253t_unit,X15: ref_a] :
( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X391,X7),X17),X15))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(X391,X7),X11),X6))
| ( X6 = X15 ) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tff(c_0_22,plain,
! [X14867: ref_a,X14868: heap_e7401611519738050253t_unit] : ( aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X14867),X14868)) = X14867 ),
inference(variable_rename,[status(thm)],[fact_101_fst__conv]) ).
tcf(c_0_23,plain,
( ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| thesis ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_24,negated_conjecture,
~ thesis,
inference(split_conjunct,[status(thm)],[c_0_17]) ).
tcf(c_0_25,plain,
! [X6: ref_a,X7: heap_e7401611519738050253t_unit] :
( ( aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X6),X7) != aa_hea1409956391221964662t_unit(alloc_a(x),h) )
| ( X7 = h2 ) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
tcf(c_0_26,plain,
! [X1: produc7812382424243267045t_unit] : aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(esk3_2(aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X1),X1)),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X1)) = X1,
inference(er,[status(thm)],[c_0_20]) ).
tcf(c_0_27,plain,
! [X7: heap_e7401611519738050253t_unit,X6: ref_a] :
( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),X7),X6))
| ( X6 = r ) ),
inference(spm,[status(thm)],[c_0_21,c_0_12]) ).
tcf(c_0_28,plain,
! [X7: heap_e7401611519738050253t_unit,X6: ref_a] : aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X6),X7)) = X6,
inference(split_conjunct,[status(thm)],[c_0_22]) ).
tcf(c_0_29,plain,
( ( aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) != r )
| ( aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) != h2 ) ),
inference(sr,[status(thm)],[c_0_23,c_0_24]) ).
tcf(c_0_30,plain,
aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) = h2,
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26])]) ).
tcf(c_0_31,plain,
! [X6: ref_a,X7: heap_e7401611519738050253t_unit] :
( ( aa_hea1409956391221964662t_unit(produc6544324848051098391t_unit(X6),X7) != aa_hea1409956391221964662t_unit(alloc_a(x),h) )
| ( X6 = r ) ),
inference(spm,[status(thm)],[c_0_27,c_0_19]) ).
tcf(c_0_32,plain,
! [X1: produc7812382424243267045t_unit] : esk3_2(aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,X1),X1) = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,X1),
inference(spm,[status(thm)],[c_0_28,c_0_26]) ).
tcf(c_0_33,plain,
aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) != r,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29,c_0_30])]) ).
cnf(c_0_34,plain,
$false,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_26]),c_0_32])]),c_0_33]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ITP206_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.03 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.31 % Computer : n012.cluster.edu
% 0.05/0.31 % Model : x86_64 x86_64
% 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.31 % Memory : 8046.5625MB
% 0.05/0.31 % OS : Linux 6.8.0-71-generic
% 0.05/0.32 % CPULimit : 300
% 0.05/0.32 % WCLimit : 300
% 0.05/0.32 % DateTime : Sun Sep 20 22:06:37 UTC 2026
% 0.05/0.32 % CPUTime :
% 0.05/0.32 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.34 Running first-order theorem proving
% 0.05/0.34 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
% 0.41/0.79 % Version: 3.5.1
% 0.41/0.79 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.41/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.41/0.79 % Starting new_bool_3 with 900s (3) cores
% 0.41/0.79 % Starting new_bool_1 with 900s (3) cores
% 0.41/0.79 % Starting sh5l with 300s (1) cores
% 0.41/0.79 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 300s (1) cores
% 0.41/0.79 % new_bool_3 with pid 945276 completed with status 0
% 0.41/0.79 % Result found by new_bool_3
% 0.41/0.79 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.41/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.41/0.79 % Starting new_bool_3 with 900s (3) cores
% 0.41/0.79 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.41/0.79 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.41/0.79 % Search class: FHHSM-FFMF21-MFFFFFNN
% 0.41/0.79 % Scheduled 6 strats onto 3 cores with 900 seconds (900 total)
% 0.41/0.79 % Starting SubtermCWHack with 91s (1) cores
% 0.41/0.79 % Starting G-E--_200_B02_F1_AE_CS_SP_PI_S0Y with 450s (1) cores
% 0.41/0.79 % Starting H----_011_C07_F1_PI_SE_SP_S0V with 113s (1) cores
% 0.41/0.79 % SubtermCWHack with pid 945281 completed with status 0
% 0.41/0.79 % Result found by SubtermCWHack
% 0.41/0.79 % Preprocessing class: FMLLSMLLSSSNFFN.
% 0.41/0.79 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.41/0.79 % Starting new_bool_3 with 900s (3) cores
% 0.41/0.79 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.41/0.79 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.41/0.79 % Search class: FHHSM-FFMF21-MFFFFFNN
% 0.41/0.79 % Scheduled 6 strats onto 3 cores with 900 seconds (900 total)
% 0.41/0.79 % Starting SubtermCWHack with 91s (1) cores
% 0.41/0.79 % Preprocessing time : 0.004 s
% 0.41/0.79
% 0.41/0.79 % Proof found!
% 0.41/0.79 % SZS status Theorem
% 0.41/0.79 % SZS output start CNFRefutation
% See solution above
% 0.41/0.79 % Parsed axioms : 10637
% 0.41/0.79 % Removed by relevancy pruning/SinE : 10602
% 0.41/0.79 % Initial clauses : 42
% 0.41/0.79 % Removed in clause preprocessing : 3
% 0.41/0.79 % Initial clauses in saturation : 39
% 0.41/0.79 % Processed clauses : 92
% 0.41/0.79 % ...of these trivial : 15
% 0.41/0.79 % ...subsumed : 17
% 0.41/0.79 % ...remaining for further processing : 60
% 0.41/0.79 % Other redundant clauses eliminated : 19
% 0.41/0.79 % Clauses deleted for lack of memory : 0
% 0.41/0.79 % Backward-subsumed : 1
% 0.41/0.79 % Backward-rewritten : 3
% 0.41/0.79 % Generated clauses : 149
% 0.41/0.79 % ...of the previous two non-redundant : 101
% 0.41/0.79 % ...aggressively subsumed : 0
% 0.41/0.79 % Contextual simplify-reflections : 0
% 0.41/0.79 % Paramodulations : 129
% 0.41/0.79 % Factorizations : 0
% 0.41/0.79 % NegExts : 0
% 0.41/0.79 % Equation resolutions : 20
% 0.41/0.79 % Disequality decompositions : 0
% 0.41/0.79 % Total rewrite steps : 77
% 0.41/0.79 % ...of those cached : 49
% 0.41/0.79 % Propositional unsat checks : 0
% 0.41/0.79 % Propositional check models : 0
% 0.41/0.79 % Propositional check unsatisfiable : 0
% 0.41/0.79 % Propositional clauses : 0
% 0.41/0.79 % Propositional clauses after purity: 0
% 0.41/0.79 % Propositional unsat core size : 0
% 0.41/0.79 % Propositional preprocessing time : 0.000
% 0.41/0.79 % Propositional encoding time : 0.000
% 0.41/0.79 % Propositional solver time : 0.000
% 0.41/0.79 % Success case prop preproc time : 0.000
% 0.41/0.79 % Success case prop encoding time : 0.000
% 0.41/0.79 % Success case prop solver time : 0.000
% 0.41/0.79 % Current number of processed clauses : 50
% 0.41/0.79 % Positive orientable unit clauses : 23
% 0.41/0.79 % Positive unorientable unit clauses: 1
% 0.41/0.79 % Negative unit clauses : 9
% 0.41/0.79 % Non-unit-clauses : 17
% 0.41/0.79 % Current number of unprocessed clauses: 44
% 0.41/0.79 % ...number of literals in the above : 61
% 0.41/0.79 % Current number of archived formulas : 0
% 0.41/0.79 % Current number of archived clauses : 4
% 0.41/0.79 % Clause-clause subsumption calls (NU) : 44
% 0.41/0.79 % Rec. Clause-clause subsumption calls : 30
% 0.41/0.79 % Non-unit clause-clause subsumptions : 8
% 0.41/0.79 % Unit Clause-clause subsumption calls : 14
% 0.41/0.79 % Rewrite failures with RHS unbound : 16
% 0.41/0.79 % BW rewrite match attempts : 16
% 0.41/0.79 % BW rewrite match successes : 3
% 0.41/0.79 % Condensation attempts : 0
% 0.41/0.79 % Condensation successes : 0
% 0.41/0.79 % Termbank termtop insertions : 101149
% 0.41/0.79 % Search garbage collected termcells : 78071
% 0.41/0.79
% 0.41/0.79 % -------------------------------------------------
% 0.41/0.79 % User time : 0.050 s
% 0.41/0.79 % System time : 0.039 s
% 0.41/0.79 % Total time : 0.089 s
% 0.41/0.79 % Maximum resident set size: 30276 pages
% 0.41/0.79
% 0.41/0.79 % -------------------------------------------------
% 0.41/0.79 % User time : 0.403 s
% 0.41/0.79 % System time : 0.098 s
% 0.41/0.79 % Total time : 0.501 s
% 0.41/0.79 % Maximum resident set size: 23808 pages
% 0.41/0.79 % E exiting
%------------------------------------------------------------------------------