%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : COM308_1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:11:54 PM UTC 2026
% Result : Theorem 0.23s 0.96s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 60 ( 25 unt; 0 typ; 0 def)
% Number of atoms : 137 ( 52 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 128 ( 51 ~; 46 |; 22 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 112 ( 0 sgn 107 !; 5 ?; 112 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
vRow: $tType ).
tff(decl_sort2,type,
vTType: $tType ).
tff(decl_sort3,type,
vRawTable: $tType ).
tff(decl_33,type,
vtempty: vRawTable ).
tff(decl_37,type,
vtcons: ( vRawTable * vRow ) > vRawTable ).
tff(decl_42,type,
vrt2: vRawTable ).
tff(decl_79,type,
vwelltypedRawtable: ( vRawTable * vTType ) > $o ).
tff(decl_93,type,
vrowIn: ( vRawTable * vRow ) > $o ).
tff(decl_106,type,
vwelltypedRow: ( vRow * vTType ) > $o ).
tff(decl_110,type,
vrawDifference: ( vRawTable * vRawTable ) > vRawTable ).
tff(decl_129,type,
esk1_0: vRow ).
tff(decl_130,type,
esk2_0: vTType ).
tff(decl_144,type,
esk16_3: ( vRawTable * ( vRawTable * vRow ) ) > vRow ).
tff(decl_154,type,
esk26_1: vRawTable > vRow ).
tff(decl_155,type,
esk27_1: vRawTable > vRawTable ).
tff(decl_156,type,
esk28_2: ( vRawTable * vRow ) > vRow ).
tff(decl_157,type,
esk29_2: ( vRawTable * vRow ) > vRawTable ).
tff(decl_158,type,
esk30_2: ( vRawTable * vRow ) > vRow ).
tff('DIFF-tempty-tcons',axiom,
! [X32: vRow,X27: vRawTable] : ( vtempty != vtcons(X32,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','DIFF-tempty-tcons') ).
tff('EQ-tcons',axiom,
! [X32: vRow,X27: vRawTable,X34: vRow,X28: vRawTable] :
( ( vtcons(X32,X27) = vtcons(X34,X28) )
=> ( ( X27 = X28 )
& ( X32 = X34 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','EQ-tcons') ).
tff('dom-RawTable',axiom,
! [X35: vRawTable] :
( ? [X32: vRow,X27: vRawTable] : ( X35 = vtcons(X32,X27) )
| ( X35 = vtempty ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','dom-RawTable') ).
tff('rowIn-1',axiom,
! [X104: vRow,X105: vRow,X106: vRawTable] :
( vrowIn(X104,vtcons(X105,X106))
<=> ( vrowIn(X104,X106)
| ( X104 = X105 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rowIn-1') ).
tff('rowIn-true-INV',axiom,
! [X32: vRow,X27: vRawTable] :
( vrowIn(X32,X27)
=> ? [X105: vRow,X106: vRawTable,X104: vRow] :
( ( vrowIn(X104,X106)
| ( X104 = X105 ) )
& ( X27 = vtcons(X105,X106) )
& ( X32 = X104 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rowIn-true-INV') ).
tff('rawDifferencePreservesWellTypedRaw-tcons-tempty-rowIn-False',conjecture,
! [X88: vRow,X54: vTType] :
( ( vwelltypedRawtable(X54,vtempty)
& vwelltypedRawtable(X54,vtcons(X88,vrt2))
& vrowIn(X88,vrt2) )
=> vwelltypedRawtable(X54,vrawDifference(vtcons(X88,vrt2),vtempty)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rawDifferencePreservesWellTypedRaw-tcons-tempty-rowIn-False') ).
tff('rawDifference-3',axiom,
! [X88: vRow,X151: vRawTable,X106: vRawTable] :
( ( ~ vrowIn(X88,X106)
& ! [X157: vRow] :
( ( X151 != vtempty )
| ( X88 != X157 ) ) )
=> ( vrawDifference(vtcons(X88,X151),X106) = vtcons(X88,vrawDifference(X151,X106)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rawDifference-3') ).
tff('rowIn-0',axiom,
! [X103: vRow] : ~ vrowIn(X103,vtempty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rowIn-0') ).
tff('welltypedRawtable-1',axiom,
! [X54: vTType,X88: vRow,X101: vRawTable] :
( vwelltypedRawtable(X54,vtcons(X88,X101))
<=> ( vwelltypedRawtable(X54,X101)
& vwelltypedRow(X54,X88) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','welltypedRawtable-1') ).
tff('rawDifferencePreservesWellTypedRaw-tcons-IH0',axiom,
! [X54: vTType,X108: vRawTable] :
( ( vwelltypedRawtable(X54,X108)
& vwelltypedRawtable(X54,vrt2) )
=> vwelltypedRawtable(X54,vrawDifference(vrt2,X108)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','rawDifferencePreservesWellTypedRaw-tcons-IH0') ).
tff('welltypedRawtable-0',axiom,
! [X100: vTType] : vwelltypedRawtable(X100,vtempty),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','welltypedRawtable-0') ).
tff(c_0_11,plain,
! [X32: vRow,X27: vRawTable] : ( vtempty != vtcons(X32,X27) ),
inference(fof_simplification,[status(thm)],['DIFF-tempty-tcons']) ).
tff(c_0_12,plain,
! [X523: vRow,X524: vRawTable,X525: vRow,X526: vRawTable] :
( ( ( vtcons(X523,X524) != vtcons(X525,X526) )
| ( X524 = X526 ) )
& ( ( vtcons(X523,X524) != vtcons(X525,X526) )
| ( X523 = X525 ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['EQ-tcons'])])])]) ).
tff(c_0_13,plain,
! [X518: vRawTable] :
( ( X518 = vtcons(esk26_1(X518),esk27_1(X518)) )
| ( X518 = vtempty ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],['dom-RawTable'])]) ).
tff(c_0_14,plain,
! [X521: vRow,X522: vRawTable] : ( vtempty != vtcons(X521,X522) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_11])]) ).
tff(c_0_15,plain,
! [X530: vRow,X531: vRow,X532: vRawTable] :
( ( vrowIn(X530,vtcons(X531,X532))
| ~ vrowIn(X530,X532) )
& ( vrowIn(X530,vtcons(X531,X532))
| ( X530 != X531 ) )
& ( vrowIn(X530,X532)
| ( X530 = X531 )
| ~ vrowIn(X530,vtcons(X531,X532)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['rowIn-1'])])])]) ).
tcf(c_0_16,plain,
! [X27: vRawTable,X32: vRow,X30: vRow,X28: vRawTable] :
( ( vtcons(X30,X27) != vtcons(X32,X28) )
| ( X30 = X32 ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_17,plain,
! [X27: vRawTable] :
( ( X27 = vtcons(esk26_1(X27),esk27_1(X27)) )
| ( X27 = vtempty ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
tcf(c_0_18,plain,
! [X30: vRow,X27: vRawTable] : vtempty != vtcons(X30,X27),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
tff(c_0_19,plain,
! [X533: vRow,X534: vRawTable] :
( ( ~ vrowIn(X533,X534)
| vrowIn(esk30_2(X533,X534),esk29_2(X533,X534))
| ( esk30_2(X533,X534) = esk28_2(X533,X534) ) )
& ( ~ vrowIn(X533,X534)
| ( X534 = vtcons(esk28_2(X533,X534),esk29_2(X533,X534)) ) )
& ( ~ vrowIn(X533,X534)
| ( X533 = esk30_2(X533,X534) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['rowIn-true-INV'])])])])]) ).
tcf(c_0_20,plain,
! [X27: vRawTable,X30: vRow,X32: vRow] :
( ( X30 != X32 )
| vrowIn(X30,vtcons(X32,X27)) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_21,plain,
! [X27: vRawTable,X30: vRow] : esk26_1(vtcons(X30,X27)) = X30,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_16,c_0_17])]),c_0_18]) ).
tcf(c_0_22,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| ( X27 = vtcons(esk28_2(X30,X27),esk29_2(X30,X27)) ) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_23,plain,
! [X27: vRawTable,X32: vRow,X30: vRow,X28: vRawTable] :
( ( vtcons(X30,X27) != vtcons(X32,X28) )
| ( X27 = X28 ) ),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_24,plain,
! [X30: vRow,X27: vRawTable] : vrowIn(X30,vtcons(X30,X27)),
inference(er,[status(thm)],[c_0_20]) ).
tff(c_0_25,negated_conjecture,
~ ! [X88: vRow,X54: vTType] :
( ( vwelltypedRawtable(X54,vtempty)
& vwelltypedRawtable(X54,vtcons(X88,vrt2))
& vrowIn(X88,vrt2) )
=> vwelltypedRawtable(X54,vrawDifference(vtcons(X88,vrt2),vtempty)) ),
inference(assume_negation,[status(cth)],['rawDifferencePreservesWellTypedRaw-tcons-tempty-rowIn-False']) ).
tcf(c_0_26,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| ( esk26_1(X27) = esk28_2(X30,X27) ) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
tcf(c_0_27,plain,
! [X30: vRow,X27: vRawTable] : esk27_1(vtcons(X30,X27)) = X27,
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_23,c_0_17])]),c_0_18]) ).
tcf(c_0_28,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| vrowIn(esk28_2(X30,X27),X27) ),
inference(spm,[status(thm)],[c_0_24,c_0_22]) ).
tff(c_0_29,negated_conjecture,
( ~ vwelltypedRawtable(esk2_0,vrawDifference(vtcons(esk1_0,vrt2),vtempty))
& vwelltypedRawtable(esk2_0,vtempty)
& vwelltypedRawtable(esk2_0,vtcons(esk1_0,vrt2))
& vrowIn(esk1_0,vrt2) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])])]) ).
tcf(c_0_30,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| ( vtcons(esk26_1(X27),esk29_2(X30,X27)) = X27 ) ),
inference(spm,[status(thm)],[c_0_22,c_0_26]) ).
tcf(c_0_31,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| ( esk27_1(X27) = esk29_2(X30,X27) ) ),
inference(spm,[status(thm)],[c_0_27,c_0_22]) ).
tcf(c_0_32,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| vrowIn(esk26_1(X27),X27) ),
inference(spm,[status(thm)],[c_0_28,c_0_26]) ).
tcf(c_0_33,negated_conjecture,
vrowIn(esk1_0,vrt2),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tff(c_0_34,plain,
! [X88: vRow,X151: vRawTable,X106: vRawTable] :
( ( ~ vrowIn(X88,X106)
& ! [X157: vRow] :
( ( X151 != vtempty )
| ( X88 != X157 ) ) )
=> ( vrawDifference(vtcons(X88,X151),X106) = vtcons(X88,vrawDifference(X151,X106)) ) ),
inference(fof_simplification,[status(thm)],['rawDifference-3']) ).
tcf(c_0_35,plain,
! [X30: vRow,X27: vRawTable] :
( ~ vrowIn(X30,X27)
| ( vtcons(esk26_1(X27),esk27_1(X27)) = X27 ) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
tcf(c_0_36,negated_conjecture,
vrowIn(esk26_1(vrt2),vrt2),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
tff(c_0_37,plain,
! [X103: vRow] : ~ vrowIn(X103,vtempty),
inference(fof_simplification,[status(thm)],['rowIn-0']) ).
tff(c_0_38,plain,
! [X463: vTType,X464: vRow,X465: vRawTable] :
( ( vwelltypedRawtable(X463,vtcons(X464,X465))
| ~ vwelltypedRawtable(X463,X465)
| ~ vwelltypedRow(X463,X464) )
& ( ~ vwelltypedRawtable(X463,vtcons(X464,X465))
| vwelltypedRawtable(X463,X465) )
& ( ~ vwelltypedRawtable(X463,vtcons(X464,X465))
| vwelltypedRow(X463,X464) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['welltypedRawtable-1'])])])]) ).
tff(c_0_39,plain,
! [X495: vRow,X496: vRawTable,X497: vRawTable] :
( ( ( vrawDifference(vtcons(X495,X496),X497) = vtcons(X495,vrawDifference(X496,X497)) )
| vrowIn(X495,X497)
| ( X496 = vtempty ) )
& ( ( vrawDifference(vtcons(X495,X496),X497) = vtcons(X495,vrawDifference(X496,X497)) )
| vrowIn(X495,X497)
| ( X495 = esk16_3(X495,X496,X497) ) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])])]) ).
tcf(c_0_40,negated_conjecture,
vtcons(esk26_1(vrt2),esk27_1(vrt2)) = vrt2,
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
tff(c_0_41,plain,
! [X529: vRow] : ~ vrowIn(X529,vtempty),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_37])]) ).
tcf(c_0_42,plain,
! [X18: vTType,X30: vRow,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,vtcons(X30,X27))
| vwelltypedRow(X18,X30) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
tcf(c_0_43,negated_conjecture,
vwelltypedRawtable(esk2_0,vtcons(esk1_0,vrt2)),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tcf(c_0_44,negated_conjecture,
~ vwelltypedRawtable(esk2_0,vrawDifference(vtcons(esk1_0,vrt2),vtempty)),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
tcf(c_0_45,plain,
! [X27: vRawTable,X30: vRow,X28: vRawTable] :
( ( vrawDifference(vtcons(X30,X27),X28) = vtcons(X30,vrawDifference(X27,X28)) )
| vrowIn(X30,X28)
| ( X27 = vtempty ) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
tcf(c_0_46,negated_conjecture,
vrt2 != vtempty,
inference(spm,[status(thm)],[c_0_18,c_0_40]) ).
tcf(c_0_47,plain,
! [X30: vRow] : ~ vrowIn(X30,vtempty),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
tcf(c_0_48,plain,
! [X18: vTType,X30: vRow,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,X27)
| ~ vwelltypedRow(X18,X30)
| vwelltypedRawtable(X18,vtcons(X30,X27)) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
tcf(c_0_49,negated_conjecture,
vwelltypedRow(esk2_0,esk1_0),
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
tcf(c_0_50,negated_conjecture,
~ vwelltypedRawtable(esk2_0,vtcons(esk1_0,vrawDifference(vrt2,vtempty))),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_46]),c_0_47]) ).
tcf(c_0_51,negated_conjecture,
! [X27: vRawTable] :
( ~ vwelltypedRawtable(esk2_0,X27)
| vwelltypedRawtable(esk2_0,vtcons(esk1_0,X27)) ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
tff(c_0_52,plain,
! [X527: vTType,X528: vRawTable] :
( vwelltypedRawtable(X527,vrawDifference(vrt2,X528))
| ~ vwelltypedRawtable(X527,X528)
| ~ vwelltypedRawtable(X527,vrt2) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['rawDifferencePreservesWellTypedRaw-tcons-IH0'])])]) ).
tcf(c_0_53,plain,
! [X18: vTType,X30: vRow,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,vtcons(X30,X27))
| vwelltypedRawtable(X18,X27) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
tff(c_0_54,plain,
! [X462: vTType] : vwelltypedRawtable(X462,vtempty),
inference(variable_rename,[status(thm)],['welltypedRawtable-0']) ).
tcf(c_0_55,negated_conjecture,
~ vwelltypedRawtable(esk2_0,vrawDifference(vrt2,vtempty)),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
tcf(c_0_56,plain,
! [X18: vTType,X27: vRawTable] :
( ~ vwelltypedRawtable(X18,X27)
| ~ vwelltypedRawtable(X18,vrt2)
| vwelltypedRawtable(X18,vrawDifference(vrt2,X27)) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
tcf(c_0_57,negated_conjecture,
vwelltypedRawtable(esk2_0,vrt2),
inference(spm,[status(thm)],[c_0_53,c_0_43]) ).
tcf(c_0_58,plain,
! [X18: vTType] : vwelltypedRawtable(X18,vtempty),
inference(split_conjunct,[status(thm)],[c_0_54]) ).
cnf(c_0_59,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_58])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM308_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.62 % Computer : n005.cluster.edu
% 0.17/0.62 % Model : x86_64 x86_64
% 0.17/0.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.62 % Memory : 8046.5625MB
% 0.17/0.62 % OS : Linux 6.8.0-71-generic
% 0.17/0.62 % CPULimit : 300
% 0.17/0.62 % WCLimit : 300
% 0.17/0.62 % DateTime : Mon Sep 21 14:23:18 UTC 2026
% 0.17/0.63 % CPUTime :
% 0.17/0.63 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.70 Running first-order theorem proving
% 0.23/0.70 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
% 0.23/0.96 % Version: 3.5.1
% 0.23/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.23/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.23/0.96 % Starting new_bool_3 with 300s (1) cores
% 0.23/0.96 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.96 % Starting sh5l with 300s (1) cores
% 0.23/0.96 % new_bool_1 with pid 3723477 completed with status 0
% 0.23/0.96 % Result found by new_bool_1
% 0.23/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.23/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.23/0.96 % Starting new_bool_3 with 300s (1) cores
% 0.23/0.96 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.96 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.23/0.96 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.23/0.96 % Search class: FGUSM-SMLS32-DFFFFFNN
% 0.23/0.96 % partial match(1): FGUSM-SMLM32-DFFFFFNN
% 0.23/0.96 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.96 % Starting SubtermCWHack with 28s (1) cores
% 0.23/0.96 % SubtermCWHack with pid 3723479 completed with status 0
% 0.23/0.96 % Result found by SubtermCWHack
% 0.23/0.96 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.23/0.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.96 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.23/0.96 % Starting new_bool_3 with 300s (1) cores
% 0.23/0.96 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.96 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.23/0.96 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.23/0.96 % Search class: FGUSM-SMLS32-DFFFFFNN
% 0.23/0.96 % partial match(1): FGUSM-SMLM32-DFFFFFNN
% 0.23/0.96 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.96 % Starting SubtermCWHack with 28s (1) cores
% 0.23/0.96 % Preprocessing time : 0.013 s
% 0.23/0.96
% 0.23/0.96 % Proof found!
% 0.23/0.96 % SZS status Theorem
% 0.23/0.96 % SZS output start CNFRefutation
% See solution above
% 0.23/0.96 % Parsed axioms : 410
% 0.23/0.96 % Removed by relevancy pruning/SinE : 288
% 0.23/0.96 % Initial clauses : 1275
% 0.23/0.96 % Removed in clause preprocessing : 0
% 0.23/0.96 % Initial clauses in saturation : 1275
% 0.23/0.96 % Processed clauses : 1740
% 0.23/0.96 % ...of these trivial : 19
% 0.23/0.96 % ...subsumed : 1032
% 0.23/0.96 % ...remaining for further processing : 689
% 0.23/0.96 % Other redundant clauses eliminated : 278
% 0.23/0.96 % Clauses deleted for lack of memory : 0
% 0.23/0.96 % Backward-subsumed : 5
% 0.23/0.96 % Backward-rewritten : 6
% 0.23/0.96 % Generated clauses : 6849
% 0.23/0.96 % ...of the previous two non-redundant : 6072
% 0.23/0.96 % ...aggressively subsumed : 0
% 0.23/0.96 % Contextual simplify-reflections : 2
% 0.23/0.96 % Paramodulations : 6547
% 0.23/0.96 % Factorizations : 0
% 0.23/0.96 % NegExts : 0
% 0.23/0.96 % Equation resolutions : 301
% 0.23/0.96 % Disequality decompositions : 0
% 0.23/0.96 % Total rewrite steps : 998
% 0.23/0.96 % ...of those cached : 873
% 0.23/0.96 % Propositional unsat checks : 0
% 0.23/0.96 % Propositional check models : 0
% 0.23/0.96 % Propositional check unsatisfiable : 0
% 0.23/0.96 % Propositional clauses : 0
% 0.23/0.96 % Propositional clauses after purity: 0
% 0.23/0.96 % Propositional unsat core size : 0
% 0.23/0.96 % Propositional preprocessing time : 0.000
% 0.23/0.96 % Propositional encoding time : 0.000
% 0.23/0.96 % Propositional solver time : 0.000
% 0.23/0.96 % Success case prop preproc time : 0.000
% 0.23/0.96 % Success case prop encoding time : 0.000
% 0.23/0.96 % Success case prop solver time : 0.000
% 0.23/0.96 % Current number of processed clauses : 668
% 0.23/0.96 % Positive orientable unit clauses : 49
% 0.23/0.96 % Positive unorientable unit clauses: 2
% 0.23/0.96 % Negative unit clauses : 25
% 0.23/0.96 % Non-unit-clauses : 592
% 0.23/0.96 % Current number of unprocessed clauses: 5602
% 0.23/0.96 % ...number of literals in the above : 20967
% 0.23/0.96 % Current number of archived formulas : 0
% 0.23/0.96 % Current number of archived clauses : 12
% 0.23/0.96 % Clause-clause subsumption calls (NU) : 74206
% 0.23/0.96 % Rec. Clause-clause subsumption calls : 63946
% 0.23/0.96 % Non-unit clause-clause subsumptions : 1016
% 0.23/0.96 % Unit Clause-clause subsumption calls : 1211
% 0.23/0.96 % Rewrite failures with RHS unbound : 16
% 0.23/0.96 % BW rewrite match attempts : 8
% 0.23/0.96 % BW rewrite match successes : 8
% 0.23/0.96 % Condensation attempts : 0
% 0.23/0.96 % Condensation successes : 0
% 0.23/0.96 % Termbank termtop insertions : 128770
% 0.23/0.96 % Search garbage collected termcells : 11749
% 0.23/0.96
% 0.23/0.96 % -------------------------------------------------
% 0.23/0.96 % User time : 0.187 s
% 0.23/0.96 % System time : 0.014 s
% 0.23/0.96 % Total time : 0.201 s
% 0.23/0.96 % Maximum resident set size: 6484 pages
% 0.23/0.96
% 0.23/0.96 % -------------------------------------------------
% 0.23/0.96 % User time : 0.214 s
% 0.23/0.96 % System time : 0.020 s
% 0.23/0.96 % Total time : 0.234 s
% 0.23/0.96 % Maximum resident set size: 5632 pages
% 0.23/0.96 % E exiting
%------------------------------------------------------------------------------