%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEV666+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 : n001.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 02:35:24 PM UTC 2026
% Result : ContradictoryAxioms 5.76s 1.96s
% Output : CNFRefutation 5.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 45 ( 26 unt; 0 def)
% Number of atoms : 114 ( 28 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 118 ( 49 ~; 44 |; 12 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-4 aty)
% Number of variables : 78 ( 10 sgn 44 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof('$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S',axiom,
! [X589] : cCoq_2eInit_2eDatatypes_2eO != cCoq_2eInit_2eDatatypes_2eS___24a1(X589),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S') ).
fof('$_inversion_QuicksortComplexity.nat_below.natBelow',axiom,
! [X2196,X2197] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X2196)
=> ( cQuicksortComplexity_2enat__below_2enatBelow___24t(X2196,X2197)
=> ? [X2198] :
( ? [X2199] :
( X2197 = cQuicksortComplexity_2enat__below_2emkNatBelow___24a2(X2198,X2199)
& X2196 = cCoq_2eInit_2eDatatypes_2eS___24a1(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X2196,X2198,X2199))
& cCoq_2eInit_2eDatatypes_2enat___24t(X2199) )
& cCoq_2eInit_2eDatatypes_2enat___24t(X2198) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_inversion_QuicksortComplexity.nat_below.natBelow') ).
fof('$adef_$_case_Coq.Init.Datatypes.nat$11029_$a3',axiom,
! [X2794,X2795,X2796] : happ(happ(happ(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029,X2794),X2795),X2796) = c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X2794,X2795,X2796),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_$_case_Coq.Init.Datatypes.nat$11029_$a3') ).
fof('$tdef_QuicksortComplexity.nat_below.natBelow',axiom,
! [X2794,X2816] :
( cQuicksortComplexity_2enat__below_2enatBelow___24t(X2794,X2816)
<=> t(X2816,cQuicksortComplexity_2enat__below_2enatBelow___24a1(X2794)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$tdef_QuicksortComplexity.nat_below.natBelow') ).
fof('$adef_QuicksortComplexity.nat_below.natBelow_$a1',axiom,
! [X2794] : happ(cQuicksortComplexity_2enat__below_2enatBelow,X2794) = cQuicksortComplexity_2enat__below_2enatBelow___24a1(X2794),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$adef_QuicksortComplexity.nat_below.natBelow_$a1') ).
fof('$_typeof_Coq.Init.Datatypes.O',axiom,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_Coq.Init.Datatypes.O') ).
fof('$_type_11050',axiom,
! [X2277] :
( c_24__type__11050___24t(X2277)
<=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2enat___24t(X1)
=> cType___24t(happ(X2277,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_11050') ).
fof('$_type_2726',axiom,
! [X1,X2,X2431] :
( c_24__type__2726___24t(X1,X2,X2431)
<=> ! [X3] :
( t(X3,X1)
=> t(happ(X2431,X3),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_type_2726') ).
fof('$_typeof_QuicksortComplexity.nat_below.natBelow',axiom,
c_24__type__11050___24t(cQuicksortComplexity_2enat__below_2enatBelow),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_QuicksortComplexity.nat_below.natBelow') ).
fof('Coq.Logic.FunctionalExtensionality.functional_extensionality',axiom,
! [X55] :
( cType___24t(X55)
=> ! [X86] :
( cType___24t(X86)
=> ! [X136] :
( c_24__type__2726___24t(X55,X86,X136)
=> ! [X174] :
( c_24__type__2726___24t(X55,X86,X174)
=> ( ! [X164] :
( t(X164,X55)
=> happ(X136,X164) = happ(X174,X164) )
=> X136 = X174 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','Coq.Logic.FunctionalExtensionality.functional_extensionality') ).
fof('$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false',axiom,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false') ).
fof('$_typeof_A',axiom,
cType___24t(cA),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$_typeof_A') ).
fof(c_0_12,plain,
! [X589] : cCoq_2eInit_2eDatatypes_2eO != cCoq_2eInit_2eDatatypes_2eS___24a1(X589),
inference(fof_simplification,[status(thm)],['$_discrim_Coq.Init.Datatypes.O$Coq.Init.Datatypes.S']) ).
fof(c_0_13,plain,
! [X3621,X3622] :
( ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3621)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X3621,X3622)
| X3622 = cQuicksortComplexity_2enat__below_2emkNatBelow___24a2(esk119_2(X3621,X3622),esk120_2(X3621,X3622)) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3621)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X3621,X3622)
| X3621 = cCoq_2eInit_2eDatatypes_2eS___24a1(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X3621,esk119_2(X3621,X3622),esk120_2(X3621,X3622))) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3621)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X3621,X3622)
| cCoq_2eInit_2eDatatypes_2enat___24t(esk120_2(X3621,X3622)) )
& ( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X3621)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X3621,X3622)
| cCoq_2eInit_2eDatatypes_2enat___24t(esk119_2(X3621,X3622)) ) ),
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)],['$_inversion_QuicksortComplexity.nat_below.natBelow'])])])])])])]) ).
fof(c_0_14,plain,
! [X4707,X4708,X4709] : happ(happ(happ(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029,X4707),X4708),X4709) = c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X4707,X4708,X4709),
inference(variable_rename,[status(thm)],['$adef_$_case_Coq.Init.Datatypes.nat$11029_$a3']) ).
fof(c_0_15,plain,
! [X3507] : cCoq_2eInit_2eDatatypes_2eO != cCoq_2eInit_2eDatatypes_2eS___24a1(X3507),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_12])]) ).
cnf(c_0_16,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X1,X2)
| X1 = cCoq_2eInit_2eDatatypes_2eS___24a1(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X1,esk119_2(X1,X2),esk120_2(X1,X2))) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_17,plain,
happ(happ(happ(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029,X1),X2),X3) = c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029___24a3(X1,X2,X3),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
fof(c_0_18,plain,
! [X3095,X3096] :
( ( cQuicksortComplexity_2enat__below_2enatBelow___24t(X3095,X3096)
| ~ t(X3096,cQuicksortComplexity_2enat__below_2enatBelow___24a1(X3095)) )
& ( t(X3096,cQuicksortComplexity_2enat__below_2enatBelow___24a1(X3095))
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X3095,X3096) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['$tdef_QuicksortComplexity.nat_below.natBelow'])])]) ).
fof(c_0_19,plain,
! [X3094] : happ(cQuicksortComplexity_2enat__below_2enatBelow,X3094) = cQuicksortComplexity_2enat__below_2enatBelow___24a1(X3094),
inference(variable_rename,[status(thm)],['$adef_QuicksortComplexity.nat_below.natBelow_$a1']) ).
cnf(c_0_20,plain,
cCoq_2eInit_2eDatatypes_2eO != cCoq_2eInit_2eDatatypes_2eS___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_21,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| ~ cQuicksortComplexity_2enat__below_2enatBelow___24t(X1,X2)
| cCoq_2eInit_2eDatatypes_2eS___24a1(happ(happ(happ(c_24__case__Coq_2eInit_2eDatatypes_2enat_2411029,X1),esk119_2(X1,X2)),esk120_2(X1,X2))) = X1 ),
inference(rw,[status(thm)],[c_0_16,c_0_17]) ).
cnf(c_0_22,plain,
cCoq_2eInit_2eDatatypes_2enat___24t(cCoq_2eInit_2eDatatypes_2eO),
inference(split_conjunct,[status(thm)],['$_typeof_Coq.Init.Datatypes.O']) ).
cnf(c_0_23,plain,
( ~ t(X1,cQuicksortComplexity_2enat__below_2enatBelow___24a1(X2))
| cQuicksortComplexity_2enat__below_2enatBelow___24t(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_24,plain,
happ(cQuicksortComplexity_2enat__below_2enatBelow,X1) = cQuicksortComplexity_2enat__below_2enatBelow___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_25,plain,
! [X4807,X4808,X4809] :
( ( c_24__type__11050___24t(X4809)
| ~ cType___24t(happ(X4809,esk250_1(X4809))) )
& ( c_24__type__11050___24t(X4809)
| cCoq_2eInit_2eDatatypes_2enat___24t(esk250_1(X4809)) )
& ( cType___24t(happ(X4807,X4808))
| ~ cCoq_2eInit_2eDatatypes_2enat___24t(X4808)
| ~ c_24__type__11050___24t(X4807) ) ),
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)],['$_type_11050'])])])])])])]) ).
cnf(c_0_26,plain,
~ cQuicksortComplexity_2enat__below_2enatBelow___24t(cCoq_2eInit_2eDatatypes_2eO,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_21])]),c_0_22])]) ).
cnf(c_0_27,plain,
( ~ t(X2,happ(cQuicksortComplexity_2enat__below_2enatBelow,X1))
| cQuicksortComplexity_2enat__below_2enatBelow___24t(X1,X2) ),
inference(rw,[status(thm)],[c_0_23,c_0_24]) ).
fof(c_0_28,plain,
! [X3020,X3021,X3022,X3023,X3024,X3025,X3026] :
( ( c_24__type__2726___24t(X3024,X3025,X3026)
| ~ t(happ(X3026,esk36_3(X3024,X3025,X3026)),X3025) )
& ( c_24__type__2726___24t(X3024,X3025,X3026)
| t(esk36_3(X3024,X3025,X3026),X3024) )
& ( t(happ(X3022,X3023),X3021)
| ~ t(X3023,X3020)
| ~ c_24__type__2726___24t(X3020,X3021,X3022) ) ),
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)],['$_type_2726'])])])])])])]) ).
cnf(c_0_29,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X2)
| ~ c_24__type__11050___24t(X1)
| cType___24t(happ(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_30,plain,
c_24__type__11050___24t(cQuicksortComplexity_2enat__below_2enatBelow),
inference(split_conjunct,[status(thm)],['$_typeof_QuicksortComplexity.nat_below.natBelow']) ).
fof(c_0_31,plain,
! [X3033,X3034,X3035,X3036] :
( ( ~ cType___24t(X3033)
| ~ cType___24t(X3034)
| ~ c_24__type__2726___24t(X3033,X3034,X3035)
| ~ c_24__type__2726___24t(X3033,X3034,X3036)
| X3035 = X3036
| happ(X3035,esk37_4(X3033,X3034,X3035,X3036)) != happ(X3036,esk37_4(X3033,X3034,X3035,X3036)) )
& ( ~ cType___24t(X3033)
| ~ cType___24t(X3034)
| ~ c_24__type__2726___24t(X3033,X3034,X3035)
| ~ c_24__type__2726___24t(X3033,X3034,X3036)
| X3035 = X3036
| t(esk37_4(X3033,X3034,X3035,X3036),X3033) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Coq.Logic.FunctionalExtensionality.functional_extensionality'])])])])])]) ).
cnf(c_0_32,plain,
~ t(X1,happ(cQuicksortComplexity_2enat__below_2enatBelow,cCoq_2eInit_2eDatatypes_2eO)),
inference(spm,[status(thm)],[c_0_26,c_0_27]) ).
cnf(c_0_33,plain,
( c_24__type__2726___24t(X1,X2,X3)
| t(esk36_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_34,plain,
( ~ cCoq_2eInit_2eDatatypes_2enat___24t(X1)
| cType___24t(happ(cQuicksortComplexity_2enat__below_2enatBelow,X1)) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
fof(c_0_35,plain,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
inference(fof_simplification,[status(thm)],['$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false']) ).
cnf(c_0_36,plain,
( ~ cType___24t(X1)
| ~ cType___24t(X2)
| ~ c_24__type__2726___24t(X1,X2,X3)
| ~ c_24__type__2726___24t(X1,X2,X4)
| X3 = X4
| t(esk37_4(X1,X2,X3,X4),X1) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_37,plain,
c_24__type__2726___24t(happ(cQuicksortComplexity_2enat__below_2enatBelow,cCoq_2eInit_2eDatatypes_2eO),X1,X2),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_38,plain,
cType___24t(happ(cQuicksortComplexity_2enat__below_2enatBelow,cCoq_2eInit_2eDatatypes_2eO)),
inference(spm,[status(thm)],[c_0_34,c_0_22]) ).
fof(c_0_39,plain,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
inference(fof_nnf,[status(thm)],[c_0_35]) ).
cnf(c_0_40,plain,
( ~ cType___24t(X3)
| X1 = X2 ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_36]),c_0_37]),c_0_37]),c_0_38])]) ).
cnf(c_0_41,plain,
cType___24t(cA),
inference(split_conjunct,[status(thm)],['$_typeof_A']) ).
cnf(c_0_42,plain,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_43,plain,
X1 = X2,
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_44,plain,
$false,
inference(sr,[status(thm)],[c_0_42,c_0_43]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV666+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n001.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 21 07:40:45 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 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
% 5.76/1.96 % Version: 3.5.1
% 5.76/1.96 % Preprocessing class: FMLLSMLLSSSNFFN.
% 5.76/1.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.76/1.96 % Starting new_bool_3 with 900s (3) cores
% 5.76/1.96 % Starting new_bool_1 with 900s (3) cores
% 5.76/1.96 % Starting sh5l with 300s (1) cores
% 5.76/1.96 % Starting G-E--_301_C18_F1_URBAN_S5PRR_RG_S0Y with 300s (1) cores
% 5.76/1.96 % sh5l with pid 2582364 completed with status 0
% 5.76/1.96 % Result found by sh5l
% 5.76/1.96 % Preprocessing class: FMLLSMLLSSSNFFN.
% 5.76/1.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.76/1.96 % Starting new_bool_3 with 900s (3) cores
% 5.76/1.96 % Starting new_bool_1 with 900s (3) cores
% 5.76/1.96 % Starting sh5l with 300s (1) cores
% 5.76/1.96 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 5.76/1.96 % SinE strategy is gf500_gu_R04_F100_L20000
% 5.76/1.96 % Search class: FGHSM-SMLM32-DFFFFFNN
% 5.76/1.96 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 5.76/1.96 % Starting SubtermCWHack with 28s (1) cores
% 5.76/1.96 % SubtermCWHack with pid 2582390 completed with status 0
% 5.76/1.96 % Result found by SubtermCWHack
% 5.76/1.96 % Preprocessing class: FMLLSMLLSSSNFFN.
% 5.76/1.96 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 5.76/1.96 % Starting new_bool_3 with 900s (3) cores
% 5.76/1.96 % Starting new_bool_1 with 900s (3) cores
% 5.76/1.96 % Starting sh5l with 300s (1) cores
% 5.76/1.96 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 5.76/1.96 % SinE strategy is gf500_gu_R04_F100_L20000
% 5.76/1.96 % Search class: FGHSM-SMLM32-DFFFFFNN
% 5.76/1.96 % Scheduled 13 strats onto 1 cores with 300 seconds (300 total)
% 5.76/1.96 % Starting SubtermCWHack with 28s (1) cores
% 5.76/1.96 % Preprocessing time : 0.038 s
% 5.76/1.96
% 5.76/1.96 % Proof found!
% 5.76/1.96 % SZS status ContradictoryAxioms
% 5.76/1.96 % SZS output start CNFRefutation
% See solution above
% 5.76/1.96 % Parsed axioms : 3536
% 5.76/1.96 % Removed by relevancy pruning/SinE : 2889
% 5.76/1.96 % Initial clauses : 1951
% 5.76/1.96 % Removed in clause preprocessing : 70
% 5.76/1.96 % Initial clauses in saturation : 1881
% 5.76/1.96 % Processed clauses : 6371
% 5.76/1.96 % ...of these trivial : 24
% 5.76/1.96 % ...subsumed : 3219
% 5.76/1.96 % ...remaining for further processing : 3128
% 5.76/1.96 % Other redundant clauses eliminated : 394
% 5.76/1.96 % Clauses deleted for lack of memory : 0
% 5.76/1.96 % Backward-subsumed : 1067
% 5.76/1.96 % Backward-rewritten : 72
% 5.76/1.96 % Generated clauses : 33409
% 5.76/1.96 % ...of the previous two non-redundant : 22331
% 5.76/1.96 % ...aggressively subsumed : 0
% 5.76/1.96 % Contextual simplify-reflections : 58
% 5.76/1.96 % Paramodulations : 32946
% 5.76/1.96 % Factorizations : 17
% 5.76/1.96 % NegExts : 0
% 5.76/1.96 % Equation resolutions : 426
% 5.76/1.96 % Disequality decompositions : 0
% 5.76/1.96 % Total rewrite steps : 3521
% 5.76/1.96 % ...of those cached : 3153
% 5.76/1.96 % Propositional unsat checks : 0
% 5.76/1.96 % Propositional check models : 0
% 5.76/1.96 % Propositional check unsatisfiable : 0
% 5.76/1.96 % Propositional clauses : 0
% 5.76/1.96 % Propositional clauses after purity: 0
% 5.76/1.96 % Propositional unsat core size : 0
% 5.76/1.96 % Propositional preprocessing time : 0.000
% 5.76/1.96 % Propositional encoding time : 0.000
% 5.76/1.96 % Propositional solver time : 0.000
% 5.76/1.96 % Success case prop preproc time : 0.000
% 5.76/1.96 % Success case prop encoding time : 0.000
% 5.76/1.96 % Success case prop solver time : 0.000
% 5.76/1.96 % Current number of processed clauses : 1960
% 5.76/1.96 % Positive orientable unit clauses : 199
% 5.76/1.96 % Positive unorientable unit clauses: 1
% 5.76/1.96 % Negative unit clauses : 7
% 5.76/1.96 % Non-unit-clauses : 1753
% 5.76/1.96 % Current number of unprocessed clauses: 17767
% 5.76/1.96 % ...number of literals in the above : 82548
% 5.76/1.96 % Current number of archived formulas : 0
% 5.76/1.96 % Current number of archived clauses : 1159
% 5.76/1.96 % Clause-clause subsumption calls (NU) : 996553
% 5.76/1.96 % Rec. Clause-clause subsumption calls : 609714
% 5.76/1.96 % Non-unit clause-clause subsumptions : 3320
% 5.76/1.96 % Unit Clause-clause subsumption calls : 26813
% 5.76/1.96 % Rewrite failures with RHS unbound : 4928
% 5.76/1.96 % BW rewrite match attempts : 10610
% 5.76/1.96 % BW rewrite match successes : 4918
% 5.76/1.96 % Condensation attempts : 0
% 5.76/1.96 % Condensation successes : 0
% 5.76/1.96 % Termbank termtop insertions : 635898
% 5.76/1.96 % Search garbage collected termcells : 65040
% 5.76/1.96
% 5.76/1.96 % -------------------------------------------------
% 5.76/1.96 % User time : 1.186 s
% 5.76/1.96 % System time : 0.084 s
% 5.76/1.96 % Total time : 1.270 s
% 5.76/1.96 % Maximum resident set size: 22036 pages
% 5.76/1.96
% 5.76/1.96 % -------------------------------------------------
% 5.76/1.96 % User time : 1.388 s
% 5.76/1.96 % System time : 0.105 s
% 5.76/1.96 % Total time : 1.493 s
% 5.76/1.96 % Maximum resident set size: 12544 pages
% 5.76/1.96 % E exiting
%------------------------------------------------------------------------------