%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP020^5 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 : Wed Sep 30 08:04:06 AM UTC 2026
% Result : Theorem 128.38s 30.25s
% Output : CNFRefutation 128.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 23 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 63 ( 3 equ; 0 cnn)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 557 ( 33 ~; 28 |; 6 &; 484 @)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 11 avg)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 12 usr; 3 con; 0-4 aty)
% Number of variables : 44 ( 0 ^; 41 !; 3 ?; 44 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
del: $tType ).
thf(decl_23,type,
bool: del ).
thf(decl_25,type,
arr: del > del > del ).
thf(decl_26,type,
mem: $i > del > $o ).
thf(decl_27,type,
ap: $i > $i > $i ).
thf(decl_29,type,
p: $i > $o ).
thf(decl_87,type,
ty_2Enum_2Enum: del ).
thf(decl_196,type,
ty_2Epair_2Eprod: del > del > del ).
thf(decl_407,type,
c_2Epred__set_2EBIJ: del > del > $i ).
thf(decl_411,type,
c_2Epred__set_2ECROSS: del > del > $i ).
thf(decl_443,type,
c_2Epred__set_2EUNIV: del > $i ).
thf(decl_1129,type,
c_2Ecardinal_2Ecardeq: del > del > $i ).
thf(decl_3040,type,
esk22_4: del > del > $i > $i > $i ).
thf(conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture,
? [X29: $i] :
( ( mem @ X29 @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) )
& ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ X29 ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV) ).
thf(conj_thm_2Epred__set_2ECROSS__UNIV,axiom,
! [X13: del,X20: del] :
( ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ X13 @ X20 ) )
= ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ X13 @ X20 ) @ ( c_2Epred__set_2EUNIV @ X13 ) ) @ ( c_2Epred__set_2EUNIV @ X20 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',conj_thm_2Epred__set_2ECROSS__UNIV) ).
thf(conj_thm_2Ecardinal_2Ecardeq__SYM,axiom,
! [X13: del,X20: del,X197: $i] :
( ( mem @ X197 @ ( arr @ X13 @ bool ) )
=> ! [X55: $i] :
( ( mem @ X55 @ ( arr @ X20 @ bool ) )
=> ( ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X13 @ X20 ) @ X197 ) @ X55 ) )
<=> ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X20 @ X13 ) @ X55 ) @ X197 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',conj_thm_2Ecardinal_2Ecardeq__SYM) ).
thf(mem_c_2Epred__set_2EUNIV,axiom,
! [X13: del] : ( mem @ ( c_2Epred__set_2EUNIV @ X13 ) @ ( arr @ X13 @ bool ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',mem_c_2Epred__set_2EUNIV) ).
thf(ax_thm_2Ecardinal_2Ecardeq__def,axiom,
! [X13: del,X20: del,X1710: $i] :
( ( mem @ X1710 @ ( arr @ X13 @ bool ) )
=> ! [X1711: $i] :
( ( mem @ X1711 @ ( arr @ X20 @ bool ) )
=> ( ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X13 @ X20 ) @ X1710 ) @ X1711 ) )
<=> ? [X84: $i] :
( ( mem @ X84 @ ( arr @ X13 @ X20 ) )
& ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ X13 @ X20 ) @ X84 ) @ X1710 ) @ X1711 ) ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',ax_thm_2Ecardinal_2Ecardeq__def) ).
thf(conj_thm_2Ecardinal_2ECARD__SQUARE__NUM,axiom,
p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ty_2Enum_2Enum ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ),
file('/export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p',conj_thm_2Ecardinal_2ECARD__SQUARE__NUM) ).
thf(c_0_6,negated_conjecture,
~ ? [X29: $i] :
( ( mem @ X29 @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) )
& ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ X29 ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) ) ),
inference(assume_negation,[status(cth)],[conj_thm_2Eutil__prob_2ENUM__2D__BIJ__INV]) ).
thf(c_0_7,negated_conjecture,
! [X32221: $i] :
( ~ ( mem @ X32221 @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) )
| ~ ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ X32221 ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_6])])]) ).
thf(c_0_8,plain,
! [X32337: del,X32338: del] :
( ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ X32337 @ X32338 ) )
= ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ X32337 @ X32338 ) @ ( c_2Epred__set_2EUNIV @ X32337 ) ) @ ( c_2Epred__set_2EUNIV @ X32338 ) ) ),
inference(variable_rename,[status(thm)],[conj_thm_2Epred__set_2ECROSS__UNIV]) ).
thf(c_0_9,plain,
! [X34990: del,X34991: del,X34992: $i,X34993: $i] :
( ( ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X34990 @ X34991 ) @ X34992 ) @ X34993 ) )
| ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X34991 @ X34990 ) @ X34993 ) @ X34992 ) )
| ~ ( mem @ X34993 @ ( arr @ X34991 @ bool ) )
| ~ ( mem @ X34992 @ ( arr @ X34990 @ bool ) ) )
& ( ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X34991 @ X34990 ) @ X34993 ) @ X34992 ) )
| ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X34990 @ X34991 ) @ X34992 ) @ X34993 ) )
| ~ ( mem @ X34993 @ ( arr @ X34991 @ bool ) )
| ~ ( mem @ X34992 @ ( arr @ X34990 @ bool ) ) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[conj_thm_2Ecardinal_2Ecardeq__SYM])])])])]) ).
thf(c_0_10,plain,
! [X32222: del] : ( mem @ ( c_2Epred__set_2EUNIV @ X32222 ) @ ( arr @ X32222 @ bool ) ),
inference(variable_rename,[status(thm)],[mem_c_2Epred__set_2EUNIV]) ).
thf(c_0_11,negated_conjecture,
! [X2: $i] :
( ~ ( mem @ X2 @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) )
| ~ ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ X2 ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) ) ),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
thf(c_0_12,plain,
! [X3: del,X4: del] :
( ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ X3 @ X4 ) )
= ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ X3 @ X4 ) @ ( c_2Epred__set_2EUNIV @ X3 ) ) @ ( c_2Epred__set_2EUNIV @ X4 ) ) ),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
thf(c_0_13,plain,
! [X32587: del,X32588: del,X32589: $i,X32590: $i,X32592: $i] :
( ( ( mem @ ( esk22_4 @ X32587 @ X32588 @ X32589 @ X32590 ) @ ( arr @ X32587 @ X32588 ) )
| ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X32587 @ X32588 ) @ X32589 ) @ X32590 ) )
| ~ ( mem @ X32590 @ ( arr @ X32588 @ bool ) )
| ~ ( mem @ X32589 @ ( arr @ X32587 @ bool ) ) )
& ( ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ X32587 @ X32588 ) @ ( esk22_4 @ X32587 @ X32588 @ X32589 @ X32590 ) ) @ X32589 ) @ X32590 ) )
| ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X32587 @ X32588 ) @ X32589 ) @ X32590 ) )
| ~ ( mem @ X32590 @ ( arr @ X32588 @ bool ) )
| ~ ( mem @ X32589 @ ( arr @ X32587 @ bool ) ) )
& ( ~ ( mem @ X32592 @ ( arr @ X32587 @ X32588 ) )
| ~ ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ X32587 @ X32588 ) @ X32592 ) @ X32589 ) @ X32590 ) )
| ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X32587 @ X32588 ) @ X32589 ) @ X32590 ) )
| ~ ( mem @ X32590 @ ( arr @ X32588 @ bool ) )
| ~ ( mem @ X32589 @ ( arr @ X32587 @ bool ) ) ) ),
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)],[ax_thm_2Ecardinal_2Ecardeq__def])])])])])]) ).
thf(c_0_14,plain,
! [X2: $i,X3: del,X5: $i,X4: del] :
( ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X4 @ X3 ) @ X5 ) @ X2 ) )
| ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X3 @ X4 ) @ X2 ) @ X5 ) )
| ~ ( mem @ X2 @ ( arr @ X3 @ bool ) )
| ~ ( mem @ X5 @ ( arr @ X4 @ bool ) ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
thf(c_0_15,plain,
p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ty_2Enum_2Enum ) @ ( ap @ ( ap @ ( c_2Epred__set_2ECROSS @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ),
inference(split_conjunct,[status(thm)],[conj_thm_2Ecardinal_2ECARD__SQUARE__NUM]) ).
thf(c_0_16,plain,
! [X3: del] : ( mem @ ( c_2Epred__set_2EUNIV @ X3 ) @ ( arr @ X3 @ bool ) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
thf(c_0_17,negated_conjecture,
! [X2: $i] :
( ~ ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ X2 ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) ) )
| ~ ( mem @ X2 @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) ) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
thf(c_0_18,plain,
! [X2: $i,X5: $i,X4: del,X3: del] :
( ( p @ ( ap @ ( ap @ ( ap @ ( c_2Epred__set_2EBIJ @ X3 @ X4 ) @ ( esk22_4 @ X3 @ X4 @ X2 @ X5 ) ) @ X2 ) @ X5 ) )
| ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X3 @ X4 ) @ X2 ) @ X5 ) )
| ~ ( mem @ X5 @ ( arr @ X4 @ bool ) )
| ~ ( mem @ X2 @ ( arr @ X3 @ bool ) ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
thf(c_0_19,plain,
p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) ) @ ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_14,c_0_15]),c_0_12]),c_0_16]),c_0_12]),c_0_16])]) ).
thf(c_0_20,negated_conjecture,
~ ( mem @ ( esk22_4 @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ty_2Enum_2Enum ) @ ( c_2Epred__set_2EUNIV @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) ) @ ( arr @ ty_2Enum_2Enum @ ( ty_2Epair_2Eprod @ ty_2Enum_2Enum @ ty_2Enum_2Enum ) ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_19]),c_0_16]),c_0_16])]) ).
thf(c_0_21,plain,
! [X2: $i,X5: $i,X4: del,X3: del] :
( ( mem @ ( esk22_4 @ X3 @ X4 @ X2 @ X5 ) @ ( arr @ X3 @ X4 ) )
| ~ ( p @ ( ap @ ( ap @ ( c_2Ecardinal_2Ecardeq @ X3 @ X4 ) @ X2 ) @ X5 ) )
| ~ ( mem @ X5 @ ( arr @ X4 @ bool ) )
| ~ ( mem @ X2 @ ( arr @ X3 @ bool ) ) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
thf(c_0_22,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_21]),c_0_19]),c_0_16]),c_0_16])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP020^5 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 % Computer : n007.cluster.edu
% 0.08/0.23 % Model : x86_64 x86_64
% 0.08/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.23 % Memory : 8046.5625MB
% 0.08/0.23 % OS : Linux 6.8.0-71-generic
% 0.08/0.23 % CPULimit : 300
% 0.08/0.23 % WCLimit : 300
% 0.08/0.23 % DateTime : Tue Sep 29 19:31:58 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.23 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.29 Running higher-order theorem proving
% 7.59/7.70 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.ZCDrvXf7NB/E---3.1_3812745.p
% 128.38/30.25 % Version: 3.5.1-ho
% 128.38/30.25 % Preprocessing class: HMLLSMLLSSLNSFA.
% 128.38/30.25 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 128.38/30.25 % Starting new_bool_8 with 1184s (4) cores
% 128.38/30.25 % Starting post_as_ho5 with 592s (2) cores
% 128.38/30.25 % Starting new_bool_9 with 296s (1) cores
% 128.38/30.25 % Starting new_bool_3 with 296s (1) cores
% 128.38/30.25 % new_bool_8 with pid 3812838 completed with status 0
% 128.38/30.25 % Result found by new_bool_8
% 128.38/30.25 % Preprocessing class: HMLLSMLLSSLNSFA.
% 128.38/30.25 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 128.38/30.25 % Starting new_bool_8 with 1184s (4) cores
% 128.38/30.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 128.38/30.25 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 128.38/30.25 % Search class: HGHSM-SMLM33-DSFFFFNN
% 128.38/30.25 % partial match(2): FGHSM-SMLM33-DFFFFFNN
% 128.38/30.25 % Scheduled 7 strats onto 4 cores with 1183 seconds (1183 total)
% 128.38/30.25 % Starting SubtermCWHack with 107s (1) cores
% 128.38/30.25 % Starting new_bool_8 with 119s (1) cores
% 128.38/30.25 % Starting U----_206e_00_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 107s (1) cores
% 128.38/30.25 % Starting SAT001_CA_MinMin_p005000_rr with 107s (1) cores
% 128.38/30.25 % new_bool_8 with pid 3812852 completed with status 0
% 128.38/30.25 % Result found by new_bool_8
% 128.38/30.25 % Preprocessing class: HMLLSMLLSSLNSFA.
% 128.38/30.25 % Scheduled 4 strats onto 8 cores with 296 seconds (2368 total)
% 128.38/30.25 % Starting new_bool_8 with 1184s (4) cores
% 128.38/30.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,1,,2,20000,1.0))
% 128.38/30.25 % SinE strategy is GSinE(CountFormulas,hypos,1,,2,20000,1.0)
% 128.38/30.25 % Search class: HGHSM-SMLM33-DSFFFFNN
% 128.38/30.25 % partial match(2): FGHSM-SMLM33-DFFFFFNN
% 128.38/30.25 % Scheduled 7 strats onto 4 cores with 1183 seconds (1183 total)
% 128.38/30.25 % Starting SubtermCWHack with 107s (1) cores
% 128.38/30.25 % Starting new_bool_8 with 119s (1) cores
% 128.38/30.25 % Preprocessing time : 0.308 s
% 128.38/30.25 % Presaturation interreduction done
% 128.38/30.25
% 128.38/30.25 % Proof found!
% 128.38/30.25 % SZS status Theorem
% 128.38/30.25 % SZS output start CNFRefutation
% See solution above
% 128.38/30.25 % Parsed axioms : 18687
% 128.38/30.25 % Removed by relevancy pruning/SinE : 17669
% 128.38/30.25 % Initial clauses : 4392
% 128.38/30.25 % Removed in clause preprocessing : 1445
% 128.38/30.25 % Initial clauses in saturation : 2947
% 128.38/30.25 % Processed clauses : 5238
% 128.38/30.25 % ...of these trivial : 33
% 128.38/30.25 % ...subsumed : 694
% 128.38/30.25 % ...remaining for further processing : 4511
% 128.38/30.25 % Other redundant clauses eliminated : 1282
% 128.38/30.25 % Clauses deleted for lack of memory : 0
% 128.38/30.25 % Backward-subsumed : 11
% 128.38/30.25 % Backward-rewritten : 5
% 128.38/30.25 % Generated clauses : 94269
% 128.38/30.25 % ...of the previous two non-redundant : 92252
% 128.38/30.25 % ...aggressively subsumed : 0
% 128.38/30.25 % Contextual simplify-reflections : 15
% 128.38/30.25 % Paramodulations : 91992
% 128.38/30.25 % Factorizations : 2
% 128.38/30.25 % NegExts : 66
% 128.38/30.25 % Equation resolutions : 1307
% 128.38/30.25 % Disequality decompositions : 0
% 128.38/30.25 % Total rewrite steps : 2779
% 128.38/30.25 % ...of those cached : 2431
% 128.38/30.25 % Propositional unsat checks : 0
% 128.38/30.25 % Propositional check models : 0
% 128.38/30.25 % Propositional check unsatisfiable : 0
% 128.38/30.25 % Propositional clauses : 0
% 128.38/30.25 % Propositional clauses after purity: 0
% 128.38/30.25 % Propositional unsat core size : 0
% 128.38/30.25 % Propositional preprocessing time : 0.000
% 128.38/30.25 % Propositional encoding time : 0.000
% 128.38/30.25 % Propositional solver time : 0.000
% 128.38/30.25 % Success case prop preproc time : 0.000
% 128.38/30.25 % Success case prop encoding time : 0.000
% 128.38/30.25 % Success case prop solver time : 0.000
% 128.38/30.25 % Current number of processed clauses : 1805
% 128.38/30.25 % Positive orientable unit clauses : 236
% 128.38/30.25 % Positive unorientable unit clauses: 20
% 128.38/30.25 % Negative unit clauses : 30
% 128.38/30.25 % Non-unit-clauses : 1519
% 128.38/30.25 % Current number of unprocessed clauses: 92481
% 128.38/30.25 % ...number of literals in the above : 547157
% 128.38/30.25 % Current number of archived formulas : 0
% 128.38/30.25 % Current number of archived clauses : 2583
% 128.38/30.25 % Clause-clause subsumption calls (NU) : 5055862
% 128.38/30.25 % Rec. Clause-clause subsumption calls : 116394
% 128.38/30.25 % Non-unit clause-clause subsumptions : 591
% 128.38/30.25 % Unit Clause-clause subsumption calls : 24778
% 128.38/30.25 % Rewrite failures with RHS unbound : 0
% 128.38/30.25 % BW rewrite match attempts : 3190
% 128.38/30.25 % BW rewrite match successes : 61
% 128.38/30.25 % Condensation attempts : 0
% 128.38/30.25 % Condensation successes : 0
% 128.38/30.25 % Termbank termtop insertions : 4548063
% 128.38/30.25 % Search garbage collected termcells : 465144
% 128.38/30.25
% 128.38/30.25 % -------------------------------------------------
% 128.38/30.25 % User time : 16.627 s
% 128.38/30.25 % System time : 0.426 s
% 128.38/30.25 % Total time : 17.053 s
% 128.38/30.25 % Maximum resident set size: 87104 pages
% 128.38/30.25
% 128.38/30.25 % -------------------------------------------------
% 128.38/30.25 % User time : 65.971 s
% 128.38/30.25 % System time : 1.563 s
% 128.38/30.25 % Total time : 67.534 s
% 128.38/30.25 % Maximum resident set size: 73728 pages
% 128.38/30.25 % E exiting
%------------------------------------------------------------------------------