%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP006_1 : 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 : Thu Sep 24 12:53:29 PM UTC 2026
% Result : Theorem 0.17s 0.51s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 38 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 147 ( 40 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 158 ( 49 ~; 35 |; 40 &)
% ( 20 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 76 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 8 con; 0-5 aty)
% Number of variables : 141 ( 0 sgn 133 !; 8 ?; 141 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
u: $tType ).
tff(decl_sort2,type,
d: $tType ).
tff(decl_sort3,type,
du: $tType ).
tff(decl_sort4,type,
mono_2Etyop_2Emin_2Ebool: $tType ).
tff(decl_23,type,
tyop_2Emin_2Ebool: d ).
tff(decl_24,type,
tyop_2Emin_2Efun: ( d * d ) > d ).
tff(decl_25,type,
s: ( u * d ) > du ).
tff(decl_26,type,
app_2E2: ( du * du ) > u ).
tff(decl_27,type,
p: mono_2Etyop_2Emin_2Ebool > $o ).
tff(decl_43,type,
c_2EquantHeuristics_2EGUESS__EXISTS_2E2: ( du * du ) > u ).
tff(decl_45,type,
c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2: ( du * du ) > u ).
tff(decl_47,type,
c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2: ( du * du ) > u ).
tff(decl_49,type,
c_2EquantHeuristics_2EGUESS__FORALL_2E2: ( du * du ) > u ).
tff(decl_51,type,
c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2: ( du * du ) > u ).
tff(decl_53,type,
c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2: ( du * du ) > u ).
tff(decl_65,type,
mono_2Ec_2Ebool_2EF_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(decl_66,type,
mono_2Ec_2Ebool_2ET_2E0: mono_2Etyop_2Emin_2Ebool ).
tff(decl_71,type,
i_mono_2Etyop_2Emin_2Ebool: mono_2Etyop_2Emin_2Ebool > u ).
tff(decl_74,type,
j_mono_2Etyop_2Emin_2Ebool: du > mono_2Etyop_2Emin_2Ebool ).
tff(decl_81,type,
esk4_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_82,type,
esk5_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_83,type,
esk6_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_84,type,
esk7_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_85,type,
esk8_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_86,type,
esk9_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_87,type,
esk10_5: ( u * ( u * ( u * ( d * d ) ) ) ) > u ).
tff(decl_88,type,
esk11_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_89,type,
esk12_5: ( u * ( u * ( u * ( d * d ) ) ) ) > u ).
tff(decl_90,type,
esk13_4: ( u * ( u * ( d * d ) ) ) > u ).
tff(decl_91,type,
esk14_0: d ).
tff(decl_92,type,
esk15_0: d ).
tff(decl_93,type,
esk16_0: u ).
tff(decl_94,type,
esk17_0: u ).
tff(decl_95,type,
esk18_0: u ).
tff(thm_2Ebool_2EEQ__CLAUSES,axiom,
! [X8: mono_2Etyop_2Emin_2Ebool] :
( ( ( X8 = mono_2Ec_2Ebool_2EF_2E0 )
<=> ~ p(X8) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X8 )
<=> ~ p(X8) )
& ( ( X8 = mono_2Ec_2Ebool_2ET_2E0 )
<=> p(X8) )
& ( ( mono_2Ec_2Ebool_2ET_2E0 = X8 )
<=> p(X8) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES) ).
tff(thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT,conjecture,
! [X1: d,X2: d,X43: u,X44: u,X71: u] :
( ! [X72: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X71),s(X1,X72)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X44),s(X1,X72))))) )
=> ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X2,X1),X43),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X44)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X2,X1),X43),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X71))))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT) ).
tff(thm_2EquantHeuristics_2EGUESS__REWRITES,axiom,
! [X1: d,X2: d,X43: u,X44: u] :
( ! [X59: u,X60: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X1,X2),X59),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X60)))))
<=> ! [X61: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X60),s(X2,X61)))))
=> ? [X62: u] : ( s(X2,X61) = s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X59),s(X1,X62))) ) ) )
& ! [X55: u,X56: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X1,X2),X55),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X56)))))
<=> ! [X57: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X56),s(X2,X57)))))
=> ? [X58: u] : ( s(X2,X57) = s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X55),s(X1,X58))) ) ) )
& ! [X52: u,X53: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X52),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X53)))))
<=> ! [X54: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X53),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X52),s(X1,X54))))))) )
& ! [X49: u,X50: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X49),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X50)))))
<=> ! [X51: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X50),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X49),s(X1,X51))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44)))))
<=> ! [X47: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,X47)))))
=> ? [X48: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(X1,X48))))))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44)))))
<=> ! [X45: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,X45)))))
=> ? [X46: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(X1,X46))))))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES) ).
tff(ij_2Emono_2Etyop_2Emin_2Ebool,axiom,
! [X15: u] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,X15)))) = s(tyop_2Emin_2Ebool,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Ebool) ).
tff(ji_2Emono_2Etyop_2Emin_2Ebool,axiom,
! [X6: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X6))) = X6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Ebool) ).
tff(reserved_2Eho_2Etruth,axiom,
p(mono_2Ec_2Ebool_2ET_2E0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Etruth) ).
tff(reserved_2Eho_2Enotfalse,axiom,
~ p(mono_2Ec_2Ebool_2EF_2E0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Enotfalse) ).
tff(c_0_7,plain,
! [X8: mono_2Etyop_2Emin_2Ebool] :
( ( ( X8 = mono_2Ec_2Ebool_2EF_2E0 )
<=> ~ p(X8) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X8 )
<=> ~ p(X8) )
& ( ( X8 = mono_2Ec_2Ebool_2ET_2E0 )
<=> p(X8) )
& ( ( mono_2Ec_2Ebool_2ET_2E0 = X8 )
<=> p(X8) ) ),
inference(fof_simplification,[status(thm)],[thm_2Ebool_2EEQ__CLAUSES]) ).
tff(c_0_8,negated_conjecture,
~ ! [X1: d,X2: d,X43: u,X44: u,X71: u] :
( ! [X72: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X71),s(X1,X72)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X44),s(X1,X72))))) )
=> ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X2,X1),X43),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X44)))))
=> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X2,X1),X43),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X71))))) ) ),
inference(assume_negation,[status(cth)],[thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT]) ).
tff(c_0_9,plain,
! [X171: mono_2Etyop_2Emin_2Ebool] :
( ( ( X171 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X171) )
& ( ~ p(X171)
| ( X171 != mono_2Ec_2Ebool_2EF_2E0 ) )
& ( ( mono_2Ec_2Ebool_2EF_2E0 = X171 )
| p(X171) )
& ( ~ p(X171)
| ( mono_2Ec_2Ebool_2EF_2E0 != X171 ) )
& ( ( X171 = mono_2Ec_2Ebool_2ET_2E0 )
| ~ p(X171) )
& ( p(X171)
| ( X171 != mono_2Ec_2Ebool_2ET_2E0 ) )
& ( ( mono_2Ec_2Ebool_2ET_2E0 = X171 )
| ~ p(X171) )
& ( p(X171)
| ( mono_2Ec_2Ebool_2ET_2E0 != X171 ) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_7])])]) ).
tff(c_0_10,negated_conjecture,
! [X273: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0)))))
& p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0)))))
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0),s(esk14_0,X273)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0),s(esk14_0,X273))))) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_8])])])])]) ).
tff(c_0_11,plain,
! [X1: d,X2: d,X43: u,X44: u] :
( ! [X59: u,X60: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X1,X2),X59),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X60)))))
<=> ! [X61: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X60),s(X2,X61)))))
=> ? [X62: u] : ( s(X2,X61) = s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X59),s(X1,X62))) ) ) )
& ! [X55: u,X56: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X1,X2),X55),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X56)))))
<=> ! [X57: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X56),s(X2,X57)))))
=> ? [X58: u] : ( s(X2,X57) = s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X55),s(X1,X58))) ) ) )
& ! [X52: u,X53: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X52),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X53)))))
<=> ! [X54: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X53),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X52),s(X1,X54))))))) )
& ! [X49: u,X50: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X49),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X50)))))
<=> ! [X51: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X50),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X49),s(X1,X51))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44)))))
<=> ! [X47: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,X47)))))
=> ? [X48: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(X1,X48))))))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44)))))
<=> ! [X45: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,X45)))))
=> ? [X46: u] : p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X44),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X43),s(X1,X46))))))) ) ) ),
inference(fof_simplification,[status(thm)],[thm_2EquantHeuristics_2EGUESS__REWRITES]) ).
tff(c_0_12,plain,
! [X115: u] : ( s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,X115)))) = s(tyop_2Emin_2Ebool,X115) ),
inference(variable_rename,[status(thm)],[ij_2Emono_2Etyop_2Emin_2Ebool]) ).
tcf(c_0_13,plain,
! [X6: mono_2Etyop_2Emin_2Ebool] :
( ~ p(X6)
| ( X6 = mono_2Ec_2Ebool_2ET_2E0 ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_14,negated_conjecture,
p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0))))),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tff(c_0_15,plain,
! [X179: d,X180: d,X181: u,X182: u,X183: u,X185: d,X186: d,X187: u,X188: u,X190: u,X191: d,X192: d,X193: u,X194: u,X195: u,X197: d,X198: d,X199: u,X200: u,X202: u,X203: d,X204: d,X205: u,X206: u,X207: u,X208: d,X209: d,X210: u,X211: u,X213: d,X214: d,X215: u,X216: u,X217: u,X218: d,X219: d,X220: u,X221: u,X223: d,X224: d,X225: u,X226: u,X227: u,X229: d,X230: d,X231: u,X232: u,X234: u,X235: d,X236: d,X237: u,X238: u,X239: u,X241: d,X242: d,X243: u,X244: u,X246: u] :
( ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X241,X242),X243),s(tyop_2Emin_2Efun(X242,tyop_2Emin_2Ebool),X244)))))
| ( s(X242,esk13_4(X241,X242,X243,X244)) != s(X242,app_2E2(s(tyop_2Emin_2Efun(X241,X242),X243),s(X241,X246))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X241,X242),X243),s(tyop_2Emin_2Efun(X242,tyop_2Emin_2Ebool),X244)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X242,tyop_2Emin_2Ebool),X244),s(X242,esk13_4(X241,X242,X243,X244)))))) )
& ( ( s(X236,X239) = s(X236,app_2E2(s(tyop_2Emin_2Efun(X235,X236),X237),s(X235,esk12_5(X235,X236,X237,X238,X239)))) )
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X236,tyop_2Emin_2Ebool),X238),s(X236,X239)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__GAP_2E2(s(tyop_2Emin_2Efun(X235,X236),X237),s(tyop_2Emin_2Efun(X236,tyop_2Emin_2Ebool),X238))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X229,X230),X231),s(tyop_2Emin_2Efun(X230,tyop_2Emin_2Ebool),X232)))))
| ( s(X230,esk11_4(X229,X230,X231,X232)) != s(X230,app_2E2(s(tyop_2Emin_2Efun(X229,X230),X231),s(X229,X234))) ) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X229,X230),X231),s(tyop_2Emin_2Efun(X230,tyop_2Emin_2Ebool),X232)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X230,tyop_2Emin_2Ebool),X232),s(X230,esk11_4(X229,X230,X231,X232)))))) )
& ( ( s(X224,X227) = s(X224,app_2E2(s(tyop_2Emin_2Efun(X223,X224),X225),s(X223,esk10_5(X223,X224,X225,X226,X227)))) )
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X224,tyop_2Emin_2Ebool),X226),s(X224,X227)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__GAP_2E2(s(tyop_2Emin_2Efun(X223,X224),X225),s(tyop_2Emin_2Efun(X224,tyop_2Emin_2Ebool),X226))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X218,X219),X220),s(tyop_2Emin_2Efun(X219,tyop_2Emin_2Ebool),X221)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X219,tyop_2Emin_2Ebool),X221),s(X219,app_2E2(s(tyop_2Emin_2Efun(X218,X219),X220),s(X218,esk9_4(X218,X219,X220,X221)))))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X214,tyop_2Emin_2Ebool),X216),s(X214,app_2E2(s(tyop_2Emin_2Efun(X213,X214),X215),s(X213,X217)))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X213,X214),X215),s(tyop_2Emin_2Efun(X214,tyop_2Emin_2Ebool),X216))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X208,X209),X210),s(tyop_2Emin_2Efun(X209,tyop_2Emin_2Ebool),X211)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X209,tyop_2Emin_2Ebool),X211),s(X209,app_2E2(s(tyop_2Emin_2Efun(X208,X209),X210),s(X208,esk8_4(X208,X209,X210,X211)))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X204,tyop_2Emin_2Ebool),X206),s(X204,app_2E2(s(tyop_2Emin_2Efun(X203,X204),X205),s(X203,X207)))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS__POINT_2E2(s(tyop_2Emin_2Efun(X203,X204),X205),s(tyop_2Emin_2Efun(X204,tyop_2Emin_2Ebool),X206))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X197,X198),X199),s(tyop_2Emin_2Efun(X198,tyop_2Emin_2Ebool),X200)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X198,tyop_2Emin_2Ebool),X200),s(X198,app_2E2(s(tyop_2Emin_2Efun(X197,X198),X199),s(X197,X202))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X197,X198),X199),s(tyop_2Emin_2Efun(X198,tyop_2Emin_2Ebool),X200)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X198,tyop_2Emin_2Ebool),X200),s(X198,esk7_4(X197,X198,X199,X200)))))) )
& ( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),X194),s(X192,app_2E2(s(tyop_2Emin_2Efun(X191,X192),X193),s(X191,esk6_4(X191,X192,X193,X194))))))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),X194),s(X192,X195)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL_2E2(s(tyop_2Emin_2Efun(X191,X192),X193),s(tyop_2Emin_2Efun(X192,tyop_2Emin_2Ebool),X194))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X185,X186),X187),s(tyop_2Emin_2Efun(X186,tyop_2Emin_2Ebool),X188)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X186,tyop_2Emin_2Ebool),X188),s(X186,app_2E2(s(tyop_2Emin_2Efun(X185,X186),X187),s(X185,X190))))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X185,X186),X187),s(tyop_2Emin_2Efun(X186,tyop_2Emin_2Ebool),X188)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X186,tyop_2Emin_2Ebool),X188),s(X186,esk5_4(X185,X186,X187,X188)))))) )
& ( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X180,tyop_2Emin_2Ebool),X182),s(X180,app_2E2(s(tyop_2Emin_2Efun(X179,X180),X181),s(X179,esk4_4(X179,X180,X181,X182))))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X180,tyop_2Emin_2Ebool),X182),s(X180,X183)))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__EXISTS_2E2(s(tyop_2Emin_2Efun(X179,X180),X181),s(tyop_2Emin_2Efun(X180,tyop_2Emin_2Ebool),X182))))) ) ),
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)],[c_0_11])])])])])])]) ).
tcf(c_0_16,plain,
! [X3: u] : s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,X3)))) = s(tyop_2Emin_2Ebool,X3),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
tcf(c_0_17,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0)))) = mono_2Ec_2Ebool_2ET_2E0,
inference(spm,[status(thm)],[c_0_13,c_0_14]) ).
tff(c_0_18,plain,
! [X118: mono_2Etyop_2Emin_2Ebool] : ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X118))) = X118 ),
inference(variable_rename,[status(thm)],[ji_2Emono_2Etyop_2Emin_2Ebool]) ).
tcf(c_0_19,plain,
! [X1: d,X3: u,X2: d,X4: u,X5: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4),s(X2,app_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(X1,X5)))))))
| ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X1,X2),X3),s(tyop_2Emin_2Efun(X2,tyop_2Emin_2Ebool),X4))))) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_20,negated_conjecture,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
tcf(c_0_21,plain,
! [X6: mono_2Etyop_2Emin_2Ebool] : j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(X6))) = X6,
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tcf(c_0_22,plain,
p(mono_2Ec_2Ebool_2ET_2E0),
inference(split_conjunct,[status(thm)],[reserved_2Eho_2Etruth]) ).
tff(c_0_23,plain,
~ p(mono_2Ec_2Ebool_2EF_2E0),
inference(fof_simplification,[status(thm)],[reserved_2Eho_2Enotfalse]) ).
tcf(c_0_24,negated_conjecture,
! [X3: u] :
( ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0),s(esk14_0,X3)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0),s(esk14_0,X3))))) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tcf(c_0_25,plain,
! [X6: mono_2Etyop_2Emin_2Ebool] :
( ( X6 = mono_2Ec_2Ebool_2EF_2E0 )
| p(X6) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_26,negated_conjecture,
! [X3: u] : ~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0),s(esk14_0,app_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(esk15_0,X3))))))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19,c_0_20]),c_0_21]),c_0_22])]) ).
tff(c_0_27,plain,
~ p(mono_2Ec_2Ebool_2EF_2E0),
inference(fof_nnf,[status(thm)],[c_0_23]) ).
tcf(c_0_28,negated_conjecture,
! [X3: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0),s(esk14_0,X3)))))
| ( j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0),s(esk14_0,X3)))) = mono_2Ec_2Ebool_2EF_2E0 ) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
tcf(c_0_29,negated_conjecture,
! [X3: u] : j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk17_0),s(esk14_0,app_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(esk15_0,X3)))))) = mono_2Ec_2Ebool_2EF_2E0,
inference(spm,[status(thm)],[c_0_26,c_0_25]) ).
tcf(c_0_30,plain,
~ p(mono_2Ec_2Ebool_2EF_2E0),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
tcf(c_0_31,negated_conjecture,
~ p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0))))),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tcf(c_0_32,negated_conjecture,
! [X3: u] : j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0),s(esk14_0,app_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(esk15_0,X3)))))) = mono_2Ec_2Ebool_2EF_2E0,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30]) ).
tcf(c_0_33,negated_conjecture,
j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0)))) = mono_2Ec_2Ebool_2EF_2E0,
inference(spm,[status(thm)],[c_0_31,c_0_25]) ).
tcf(c_0_34,plain,
! [X1: d,X2: d,X4: u,X3: u] :
( p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(X2,X1),X4),s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3)))))
| p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(X1,tyop_2Emin_2Ebool),X3),s(X1,app_2E2(s(tyop_2Emin_2Efun(X2,X1),X4),s(X2,esk9_4(X2,X1,X4,X3)))))))) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_35,negated_conjecture,
! [X3: u] : s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0),s(esk14_0,app_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(esk15_0,X3))))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)),
inference(spm,[status(thm)],[c_0_16,c_0_32]) ).
tcf(c_0_36,negated_conjecture,
s(tyop_2Emin_2Ebool,c_2EquantHeuristics_2EGUESS__FORALL__POINT_2E2(s(tyop_2Emin_2Efun(esk15_0,esk14_0),esk16_0),s(tyop_2Emin_2Efun(esk14_0,tyop_2Emin_2Ebool),esk18_0))) = s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)),
inference(spm,[status(thm)],[c_0_16,c_0_33]) ).
cnf(c_0_37,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_21]),c_0_36]),c_0_21])]),c_0_30]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP006_1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n007.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 20 21:39:36 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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.17/0.51 % Version: 3.5.1
% 0.17/0.51 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.51 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.51 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.51 % Starting new_bool_3 with 300s (1) cores
% 0.17/0.51 % Starting new_bool_1 with 300s (1) cores
% 0.17/0.51 % Starting sh5l with 300s (1) cores
% 0.17/0.51 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 3610851 completed with status 0
% 0.17/0.51 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 0.17/0.51 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.51 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.51 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.51 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.17/0.51 % No SInE strategy applied
% 0.17/0.51 % Search class: FGHSM-FFLM32-DFFFFFNN
% 0.17/0.51 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.17/0.51 % Starting SubtermCWHack with 136s (1) cores
% 0.17/0.51 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 0.17/0.51 % Starting new_bool_3 with 277s (1) cores
% 0.17/0.51 % Starting new_bool_1 with 277s (1) cores
% 0.17/0.51 % Starting sh5l with 277s (1) cores
% 0.17/0.51 % new_bool_3 with pid 3610860 completed with status 0
% 0.17/0.51 % Result found by new_bool_3
% 0.17/0.51 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.17/0.51 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.17/0.51 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.17/0.51 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.17/0.51 % No SInE strategy applied
% 0.17/0.51 % Search class: FGHSM-FFLM32-DFFFFFNN
% 0.17/0.51 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.17/0.51 % Starting SubtermCWHack with 136s (1) cores
% 0.17/0.51 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 0.17/0.51 % Starting new_bool_3 with 277s (1) cores
% 0.17/0.51 % Preprocessing time : 0.002 s
% 0.17/0.51 % Presaturation interreduction done
% 0.17/0.51
% 0.17/0.51 % Proof found!
% 0.17/0.51 % SZS status Theorem
% 0.17/0.51 % SZS output start CNFRefutation
% See solution above
% 0.17/0.51 % Parsed axioms : 117
% 0.17/0.51 % Removed by relevancy pruning/SinE : 0
% 0.17/0.51 % Initial clauses : 342
% 0.17/0.51 % Removed in clause preprocessing : 225
% 0.17/0.51 % Initial clauses in saturation : 117
% 0.17/0.51 % Processed clauses : 633
% 0.17/0.51 % ...of these trivial : 9
% 0.17/0.51 % ...subsumed : 385
% 0.17/0.51 % ...remaining for further processing : 239
% 0.17/0.51 % Other redundant clauses eliminated : 63
% 0.17/0.51 % Clauses deleted for lack of memory : 0
% 0.17/0.51 % Backward-subsumed : 1
% 0.17/0.51 % Backward-rewritten : 12
% 0.17/0.51 % Generated clauses : 3918
% 0.17/0.51 % ...of the previous two non-redundant : 3197
% 0.17/0.51 % ...aggressively subsumed : 0
% 0.17/0.51 % Contextual simplify-reflections : 2
% 0.17/0.51 % Paramodulations : 3786
% 0.17/0.51 % Factorizations : 66
% 0.17/0.51 % NegExts : 0
% 0.17/0.51 % Equation resolutions : 66
% 0.17/0.51 % Disequality decompositions : 0
% 0.17/0.51 % Total rewrite steps : 711
% 0.17/0.51 % ...of those cached : 554
% 0.17/0.51 % Propositional unsat checks : 0
% 0.17/0.51 % Propositional check models : 0
% 0.17/0.51 % Propositional check unsatisfiable : 0
% 0.17/0.51 % Propositional clauses : 0
% 0.17/0.51 % Propositional clauses after purity: 0
% 0.17/0.51 % Propositional unsat core size : 0
% 0.17/0.51 % Propositional preprocessing time : 0.000
% 0.17/0.51 % Propositional encoding time : 0.000
% 0.17/0.51 % Propositional solver time : 0.000
% 0.17/0.51 % Success case prop preproc time : 0.000
% 0.17/0.51 % Success case prop encoding time : 0.000
% 0.17/0.51 % Success case prop solver time : 0.000
% 0.17/0.51 % Current number of processed clauses : 130
% 0.17/0.51 % Positive orientable unit clauses : 27
% 0.17/0.51 % Positive unorientable unit clauses: 1
% 0.17/0.51 % Negative unit clauses : 1
% 0.17/0.51 % Non-unit-clauses : 101
% 0.17/0.51 % Current number of unprocessed clauses: 2700
% 0.17/0.51 % ...number of literals in the above : 9004
% 0.17/0.51 % Current number of archived formulas : 0
% 0.17/0.51 % Current number of archived clauses : 101
% 0.17/0.51 % Clause-clause subsumption calls (NU) : 5408
% 0.17/0.51 % Rec. Clause-clause subsumption calls : 4252
% 0.17/0.51 % Non-unit clause-clause subsumptions : 318
% 0.17/0.51 % Unit Clause-clause subsumption calls : 15
% 0.17/0.51 % Rewrite failures with RHS unbound : 0
% 0.17/0.51 % BW rewrite match attempts : 413
% 0.17/0.51 % BW rewrite match successes : 12
% 0.17/0.51 % Condensation attempts : 0
% 0.17/0.51 % Condensation successes : 0
% 0.17/0.51 % Termbank termtop insertions : 86595
% 0.17/0.51 % Search garbage collected termcells : 2677
% 0.17/0.51
% 0.17/0.51 % -------------------------------------------------
% 0.17/0.51 % User time : 0.054 s
% 0.17/0.51 % System time : 0.009 s
% 0.17/0.51 % Total time : 0.063 s
% 0.17/0.51 % Maximum resident set size: 4316 pages
% 0.17/0.51
% 0.17/0.51 % -------------------------------------------------
% 0.17/0.51 % User time : 0.216 s
% 0.17/0.51 % System time : 0.031 s
% 0.17/0.51 % Total time : 0.247 s
% 0.17/0.51 % Maximum resident set size: 5120 pages
% 0.17/0.51 % E exiting
%------------------------------------------------------------------------------