%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYO903^10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:43:32 AM UTC 2026
% Result : ContradictoryAxioms 0.35s 0.31s
% Output : CNFRefutation 0.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 30
% Syntax : Number of formulae : 207 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 1271 ( 10 equ; 0 cnn)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 2947 ( 547 ~; 699 |; 5 &;1619 @)
% ( 0 <=>; 77 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 8 avg)
% Number of types : 2 ( 1 usr)
% Number of type conns : 12 ( 12 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 12 usr; 4 con; 0-3 aty)
% Number of variables : 400 ( 21 ^; 376 !; 3 ?; 400 :)
% Comments :
%------------------------------------------------------------------------------
thf(decl_sort1,type,
mworld: $tType ).
thf(decl_23,type,
mrel: mworld > mworld > $o ).
thf(decl_24,type,
mactual: mworld ).
thf(decl_25,type,
mlocal: ( mworld > $o ) > $o ).
thf(decl_26,type,
mnot: ( mworld > $o ) > mworld > $o ).
thf(decl_28,type,
mor: ( mworld > $o ) > ( mworld > $o ) > mworld > $o ).
thf(decl_31,type,
mbox: ( mworld > $o ) > mworld > $o ).
thf(decl_32,type,
mdia: ( mworld > $o ) > mworld > $o ).
thf(decl_33,type,
v1: mworld > $o ).
thf(decl_34,type,
v2: mworld > $o ).
thf(decl_35,type,
v3: mworld > $o ).
thf(decl_36,type,
v4: mworld > $o ).
thf(decl_37,type,
esk1_0: mworld ).
thf(mlocal_def,axiom,
( mlocal
= ( ^ [X1: mworld > $o] : ( X1 @ mactual ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mlocal_def) ).
thf(mnot_def,axiom,
( mnot
= ( ^ [X2: mworld > $o,X3: mworld] :
~ ( X2 @ X3 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mnot_def) ).
thf(mor_def,axiom,
( mor
= ( ^ [X2: mworld > $o,X4: mworld > $o,X3: mworld] :
( ( X2 @ X3 )
| ( X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mor_def) ).
thf(mbox_def,axiom,
( mbox
= ( ^ [X1: mworld > $o,X3: mworld] :
! [X5: mworld] :
( ( mrel @ X3 @ X5 )
=> ( X1 @ X5 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mbox_def) ).
thf(mdia_def,axiom,
( mdia
= ( ^ [X1: mworld > $o,X3: mworld] :
? [X5: mworld] :
( ( mrel @ X3 @ X5 )
& ( X1 @ X5 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mdia_def) ).
thf(persat30,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v1 ) @ ( mbox @ ( mbox @ v2 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat30) ).
thf(deontic1,axiom,
( mlocal
@ ( mdia
@ ^ [X3: mworld] : $true ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',deontic1) ).
thf(persat22,axiom,
mlocal @ ( mor @ v3 @ ( mor @ v4 @ ( mor @ ( mbox @ v2 ) @ ( mbox @ ( mbox @ v1 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat22) ).
thf(mrel_reflexive,axiom,
! [X3: mworld] : ( mrel @ X3 @ X3 ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mrel_reflexive) ).
thf(persat5,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat5) ).
thf(mrel_transitive,axiom,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( ( mrel @ X3 @ X5 )
& ( mrel @ X5 @ X6 ) )
=> ( mrel @ X3 @ X6 ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',mrel_transitive) ).
thf(persat18,axiom,
mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat18) ).
thf(persat11,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v3 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat11) ).
thf(persat4,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v1 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat4) ).
thf(persat1,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ v3 @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat1) ).
thf(persat29,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat29) ).
thf(persat26,axiom,
mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat26) ).
thf(persat2,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat2) ).
thf(persat7,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mnot @ v4 ) @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat7) ).
thf(persat8,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat8) ).
thf(persat23,axiom,
mlocal @ ( mor @ v3 @ ( mor @ v4 @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat23) ).
thf(persat6,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v4 @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat6) ).
thf(persat46,axiom,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat46) ).
thf(persat9,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v4 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat9) ).
thf(persat40,axiom,
mlocal @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat40) ).
thf(persat10,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat10) ).
thf(persat28,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ v1 ) @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat28) ).
thf(persat32,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat32) ).
thf(persat34,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat34) ).
thf(persat38,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p',persat38) ).
thf(c_0_30,plain,
( mlocal
= ( ^ [Z0: mworld > $o] : ( Z0 @ mactual ) ) ),
inference(fof_simplification,[status(thm)],[mlocal_def]) ).
thf(c_0_31,plain,
( mnot
= ( ^ [Z0: mworld > $o,Z1: mworld] :
~ ( Z0 @ Z1 ) ) ),
inference(fof_simplification,[status(thm)],[mnot_def]) ).
thf(c_0_32,plain,
( mor
= ( ^ [Z0: mworld > $o,Z1: mworld > $o,Z2: mworld] :
( ( Z0 @ Z2 )
| ( Z1 @ Z2 ) ) ) ),
inference(fof_simplification,[status(thm)],[mor_def]) ).
thf(c_0_33,plain,
( mbox
= ( ^ [Z0: mworld > $o,Z1: mworld] :
! [X5: mworld] :
( ( mrel @ Z1 @ X5 )
=> ( Z0 @ X5 ) ) ) ),
inference(fof_simplification,[status(thm)],[mbox_def]) ).
thf(c_0_34,plain,
( mdia
= ( ^ [Z0: mworld > $o,Z1: mworld] :
? [X5: mworld] :
( ( mrel @ Z1 @ X5 )
& ( Z0 @ X5 ) ) ) ),
inference(fof_simplification,[status(thm)],[mdia_def]) ).
thf(c_0_35,plain,
( ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ! [X110: mworld] :
( ( mrel @ mactual @ X110 )
=> ( v1 @ X110 ) )
| ! [X112: mworld] :
( ( mrel @ mactual @ X112 )
=> ! [X111: mworld] :
( ( mrel @ X112 @ X111 )
=> ( v2 @ X111 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat30,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_36,plain,
? [X200: mworld] :
( ( mrel @ mactual @ X200 )
& $true ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[deontic1]),c_0_30]),c_0_34]) ).
thf(c_0_37,plain,
( ( v3 @ mactual )
| ( v4 @ mactual )
| ! [X81: mworld] :
( ( mrel @ mactual @ X81 )
=> ( v2 @ X81 ) )
| ! [X83: mworld] :
( ( mrel @ mactual @ X83 )
=> ! [X82: mworld] :
( ( mrel @ X83 @ X82 )
=> ( v1 @ X82 ) ) ) ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat22,c_0_30]),c_0_32]),c_0_33]) ).
thf(c_0_38,plain,
! [X304: mworld,X305: mworld,X306: mworld] :
( ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X304 )
| ( v1 @ X304 )
| ~ ( mrel @ mactual @ X305 )
| ~ ( mrel @ X305 @ X306 )
| ( v2 @ X306 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])])]) ).
thf(c_0_39,plain,
! [X201: mworld] : ( mrel @ X201 @ X201 ),
inference(variable_rename,[status(thm)],[mrel_reflexive]) ).
thf(c_0_40,plain,
( ( v1 @ mactual )
| ( v3 @ mactual )
| ! [X21: mworld] :
( ( mrel @ mactual @ X21 )
=> ! [X20: mworld] :
( ( mrel @ X21 @ X20 )
=> ( v3 @ X20 ) ) )
| ! [X23: mworld] :
( ( mrel @ mactual @ X23 )
=> ! [X22: mworld] :
( ( mrel @ X23 @ X22 )
=> ( v4 @ X22 ) ) ) ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat5,c_0_30]),c_0_32]),c_0_33]) ).
thf(c_0_41,plain,
! [X202: mworld,X203: mworld,X204: mworld] :
( ~ ( mrel @ X202 @ X203 )
| ~ ( mrel @ X203 @ X204 )
| ( mrel @ X202 @ X204 ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[mrel_transitive])])]) ).
thf(c_0_42,plain,
( ( mrel @ mactual @ esk1_0 )
& $true ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_36])])])]) ).
thf(c_0_43,plain,
! [X275: mworld,X276: mworld,X277: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X275 )
| ( v2 @ X275 )
| ~ ( mrel @ mactual @ X276 )
| ~ ( mrel @ X276 @ X277 )
| ( v1 @ X277 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])]) ).
thf(c_0_44,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ( v2 @ X6 )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
thf(c_0_45,plain,
! [X3: mworld] : ( mrel @ X3 @ X3 ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
thf(c_0_46,plain,
! [X214: mworld,X215: mworld,X216: mworld,X217: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X214 )
| ~ ( mrel @ X214 @ X215 )
| ( v3 @ X215 )
| ~ ( mrel @ mactual @ X216 )
| ~ ( mrel @ X216 @ X217 )
| ( v4 @ X217 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])])]) ).
thf(c_0_47,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( mrel @ X3 @ X6 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
thf(c_0_48,plain,
mrel @ mactual @ esk1_0,
inference(split_conjunct,[status(thm)],[c_0_42]) ).
thf(c_0_49,plain,
( ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ! [X62: mworld] :
( ( mrel @ mactual @ X62 )
=> ~ ( v1 @ X62 ) )
| ! [X64: mworld] :
( ( mrel @ mactual @ X64 )
=> ! [X63: mworld] :
( ( mrel @ X64 @ X63 )
=> ~ ( v1 @ X63 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat18,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_50,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ( v2 @ X3 )
| ( v1 @ X6 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
thf(c_0_51,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v2 @ X3 )
| ( v1 @ X5 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual ) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
thf(c_0_52,plain,
( ( v1 @ mactual )
| ~ ( v4 @ mactual )
| ! [X39: mworld] :
( ( mrel @ mactual @ X39 )
=> ! [X38: mworld] :
( ( mrel @ X39 @ X38 )
=> ~ ( v3 @ X38 ) ) )
| ! [X41: mworld] :
( ( mrel @ mactual @ X41 )
=> ! [X40: mworld] :
( ( mrel @ X41 @ X40 )
=> ~ ( v4 @ X40 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat11,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_53,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ! [X17: mworld] :
( ( mrel @ mactual @ X17 )
=> ~ ( v3 @ X17 ) )
| ! [X19: mworld] :
( ( mrel @ mactual @ X19 )
=> ! [X18: mworld] :
( ( mrel @ X19 @ X18 )
=> ( v1 @ X18 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat4,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_54,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X5 )
| ( v4 @ X7 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
thf(c_0_55,plain,
! [X3: mworld] :
( ( mrel @ X3 @ esk1_0 )
| ~ ( mrel @ X3 @ mactual ) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
thf(c_0_56,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v3 @ mactual )
| ! [X12: mworld] :
( ( mrel @ mactual @ X12 )
=> ! [X11: mworld] :
( ( mrel @ X12 @ X11 )
=> ~ ( v1 @ X11 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat1,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_57,plain,
( ( v4 @ mactual )
| ~ ( v1 @ mactual )
| ! [X107: mworld] :
( ( mrel @ mactual @ X107 )
=> ~ ( v1 @ X107 ) )
| ! [X109: mworld] :
( ( mrel @ mactual @ X109 )
=> ! [X108: mworld] :
( ( mrel @ X109 @ X108 )
=> ( v3 @ X108 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat29,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_58,plain,
! [X256: mworld,X257: mworld,X258: mworld] :
( ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X256 )
| ~ ( v1 @ X256 )
| ~ ( mrel @ mactual @ X257 )
| ~ ( mrel @ X257 @ X258 )
| ~ ( v1 @ X258 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_49])])])]) ).
thf(c_0_59,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v2 @ X3 )
| ( v1 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_45]),c_0_51]) ).
thf(c_0_60,plain,
( ( v3 @ mactual )
| ~ ( v4 @ mactual )
| ! [X97: mworld] :
( ( mrel @ mactual @ X97 )
=> ! [X96: mworld] :
( ( mrel @ X97 @ X96 )
=> ( v3 @ X96 ) ) )
| ! [X99: mworld] :
( ( mrel @ mactual @ X99 )
=> ! [X98: mworld] :
( ( mrel @ X99 @ X98 )
=> ~ ( v4 @ X98 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat26,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_61,plain,
! [X232: mworld,X233: mworld,X234: mworld,X235: mworld] :
( ( v1 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X232 )
| ~ ( mrel @ X232 @ X233 )
| ~ ( v3 @ X233 )
| ~ ( mrel @ mactual @ X234 )
| ~ ( mrel @ X234 @ X235 )
| ~ ( v4 @ X235 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_52])])])]) ).
thf(c_0_62,plain,
! [X211: mworld,X212: mworld,X213: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X211 )
| ~ ( v3 @ X211 )
| ~ ( mrel @ mactual @ X212 )
| ~ ( mrel @ X212 @ X213 )
| ( v1 @ X213 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_53])])])]) ).
thf(c_0_63,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v1 @ mactual )
| ( v4 @ X3 )
| ( v3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( mrel @ X6 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_45])]) ).
thf(c_0_64,plain,
! [X205: mworld,X206: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X205 )
| ~ ( mrel @ X205 @ X206 )
| ~ ( v1 @ X206 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_56])])])]) ).
thf(c_0_65,plain,
! [X301: mworld,X302: mworld,X303: mworld] :
( ( v4 @ mactual )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X301 )
| ~ ( v1 @ X301 )
| ~ ( mrel @ mactual @ X302 )
| ~ ( mrel @ X302 @ X303 )
| ( v3 @ X303 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_57])])])]) ).
thf(c_0_66,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v1 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_58]) ).
thf(c_0_67,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(spm,[status(thm)],[c_0_59,c_0_45]) ).
thf(c_0_68,plain,
! [X290: mworld,X291: mworld,X292: mworld,X293: mworld] :
( ( v3 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X290 )
| ~ ( mrel @ X290 @ X291 )
| ( v3 @ X291 )
| ~ ( mrel @ mactual @ X292 )
| ~ ( mrel @ X292 @ X293 )
| ~ ( v4 @ X293 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])]) ).
thf(c_0_69,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v1 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( v4 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
thf(c_0_70,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v1 @ X6 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
thf(c_0_71,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ( v4 @ X5 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_55]),c_0_45])]) ).
thf(c_0_72,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v1 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
thf(c_0_73,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v3 @ X6 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_65]) ).
thf(c_0_74,plain,
! [X5: mworld,X3: mworld] :
( ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v3 @ mactual )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(spm,[status(thm)],[c_0_66,c_0_45]) ).
thf(c_0_75,plain,
( ( v1 @ esk1_0 )
| ( v4 @ mactual )
| ( v2 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_55]),c_0_45])]) ).
thf(c_0_76,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ! [X14: mworld] :
( ( mrel @ mactual @ X14 )
=> ! [X13: mworld] :
( ( mrel @ X14 @ X13 )
=> ~ ( v3 @ X13 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat2,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_77,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v3 @ mactual )
| ( v3 @ X5 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( v4 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
thf(c_0_78,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X3 @ X6 )
| ~ ( v3 @ X6 )
| ~ ( v4 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_55]),c_0_45])]) ).
thf(c_0_79,plain,
! [X3: mworld,X5: mworld] :
( ( v2 @ mactual )
| ( v1 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v3 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70,c_0_55]),c_0_45])]) ).
thf(c_0_80,plain,
! [X3: mworld] :
( ( v4 @ esk1_0 )
| ( v3 @ mactual )
| ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(spm,[status(thm)],[c_0_71,c_0_45]) ).
thf(c_0_81,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v2 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_55]),c_0_45])]) ).
thf(c_0_82,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual )
| ~ ( v1 @ X5 ) ),
inference(spm,[status(thm)],[c_0_73,c_0_45]) ).
thf(c_0_83,plain,
( ( v1 @ mactual )
| ( v4 @ mactual )
| ( v2 @ mactual ) ),
inference(spm,[status(thm)],[c_0_67,c_0_45]) ).
thf(c_0_84,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_75]),c_0_48])]),c_0_67]) ).
thf(c_0_85,plain,
! [X207: mworld,X208: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X207 )
| ~ ( mrel @ X207 @ X208 )
| ~ ( v3 @ X208 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_76])])])]) ).
thf(c_0_86,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(spm,[status(thm)],[c_0_77,c_0_45]) ).
thf(c_0_87,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v4 @ mactual )
| ~ ( v3 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_78,c_0_45]) ).
thf(c_0_88,plain,
! [X3: mworld] :
( ( v1 @ esk1_0 )
| ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X3 ) ),
inference(spm,[status(thm)],[c_0_79,c_0_45]) ).
thf(c_0_89,plain,
( ( v3 @ esk1_0 )
| ( v1 @ mactual )
| ( v3 @ mactual )
| ( v4 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_80,c_0_45]) ).
thf(c_0_90,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v3 @ mactual )
| ~ ( v1 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_81,c_0_45]) ).
thf(c_0_91,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_75]),c_0_48])]),c_0_83]) ).
thf(c_0_92,plain,
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( v3 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_55]),c_0_45])]) ).
thf(c_0_93,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v3 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_85]) ).
thf(c_0_94,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v4 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_55]),c_0_45])]) ).
thf(c_0_95,plain,
( ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( v4 @ mactual )
| ! [X28: mworld] :
( ( mrel @ mactual @ X28 )
=> ! [X27: mworld] :
( ( mrel @ X28 @ X27 )
=> ~ ( v2 @ X27 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat7,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_96,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v4 @ esk1_0 )
| ~ ( v3 @ X3 ) ),
inference(spm,[status(thm)],[c_0_87,c_0_45]) ).
thf(c_0_97,plain,
( ( v4 @ esk1_0 )
| ( v3 @ mactual )
| ( v2 @ mactual )
| ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88,c_0_89]),c_0_48])]),c_0_90]) ).
thf(c_0_98,plain,
( ( v4 @ mactual )
| ( v2 @ mactual ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_45]),c_0_92]) ).
thf(c_0_99,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual )
| ~ ( v3 @ X3 ) ),
inference(spm,[status(thm)],[c_0_93,c_0_45]) ).
thf(c_0_100,plain,
! [X3: mworld] :
( ( v3 @ esk1_0 )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_94,c_0_45]) ).
thf(c_0_101,plain,
! [X221: mworld,X222: mworld] :
( ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X221 )
| ~ ( mrel @ X221 @ X222 )
| ~ ( v2 @ X222 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_95])])])]) ).
thf(c_0_102,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X3 ) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_97]),c_0_98]),c_0_99]) ).
thf(c_0_103,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ( v3 @ mactual )
| ( v3 @ esk1_0 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100,c_0_97]),c_0_48])]),c_0_98]) ).
thf(c_0_104,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v2 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_101]) ).
thf(c_0_105,plain,
( ( v3 @ mactual )
| ( v1 @ mactual )
| ( v2 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_103]),c_0_48])]) ).
thf(c_0_106,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v2 @ X5 ) ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
thf(c_0_107,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v2 @ X3 ) ),
inference(spm,[status(thm)],[c_0_106,c_0_45]) ).
thf(c_0_108,plain,
( ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ! [X29: mworld] :
( ( mrel @ mactual @ X29 )
=> ~ ( v3 @ X29 ) )
| ! [X31: mworld] :
( ( mrel @ mactual @ X31 )
=> ! [X30: mworld] :
( ( mrel @ X31 @ X30 )
=> ( v3 @ X30 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat8,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_109,plain,
( ( v3 @ mactual )
| ( v1 @ mactual )
| ~ ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107,c_0_105]),c_0_45])]) ).
thf(c_0_110,plain,
( ( v3 @ mactual )
| ( v4 @ mactual )
| ! [X85: mworld] :
( ( mrel @ mactual @ X85 )
=> ! [X84: mworld] :
( ( mrel @ X85 @ X84 )
=> ( v1 @ X84 ) ) )
| ! [X87: mworld] :
( ( mrel @ mactual @ X87 )
=> ! [X86: mworld] :
( ( mrel @ X87 @ X86 )
=> ~ ( v4 @ X86 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat23,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_111,plain,
! [X223: mworld,X224: mworld,X225: mworld] :
( ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( mrel @ mactual @ X223 )
| ~ ( v3 @ X223 )
| ~ ( mrel @ mactual @ X224 )
| ~ ( mrel @ X224 @ X225 )
| ( v3 @ X225 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_108])])])]) ).
thf(c_0_112,plain,
( ( v1 @ mactual )
| ( v2 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_109]),c_0_45])]),c_0_98]) ).
thf(c_0_113,plain,
! [X278: mworld,X279: mworld,X280: mworld,X281: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X278 )
| ~ ( mrel @ X278 @ X279 )
| ( v1 @ X279 )
| ~ ( mrel @ mactual @ X280 )
| ~ ( mrel @ X280 @ X281 )
| ~ ( v4 @ X281 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_110])])])]) ).
thf(c_0_114,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v3 @ X6 )
| ~ ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_111]) ).
thf(c_0_115,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v2 @ X5 ) ),
inference(spm,[status(thm)],[c_0_104,c_0_112]) ).
thf(c_0_116,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ( v1 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( v4 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_113]) ).
thf(c_0_117,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v3 @ X6 ) ),
inference(spm,[status(thm)],[c_0_114,c_0_98]) ).
thf(c_0_118,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v2 @ X3 ) ),
inference(spm,[status(thm)],[c_0_115,c_0_45]) ).
thf(c_0_119,plain,
( ( v1 @ mactual )
| ( v4 @ mactual )
| ! [X24: mworld] :
( ( mrel @ mactual @ X24 )
=> ~ ( v1 @ X24 ) )
| ! [X26: mworld] :
( ( mrel @ mactual @ X26 )
=> ! [X25: mworld] :
( ( mrel @ X26 @ X25 )
=> ~ ( v1 @ X25 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat6,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_120,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v3 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(spm,[status(thm)],[c_0_116,c_0_45]) ).
thf(c_0_121,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X5 ) ),
inference(spm,[status(thm)],[c_0_117,c_0_45]) ).
thf(c_0_122,plain,
( ( v1 @ mactual )
| ~ ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118,c_0_112]),c_0_45])]) ).
thf(c_0_123,plain,
( ~ ( v3 @ mactual )
| ! [X176: mworld] :
( ( mrel @ mactual @ X176 )
=> ~ ( v4 @ X176 ) )
| ! [X178: mworld] :
( ( mrel @ mactual @ X178 )
=> ! [X177: mworld] :
( ( mrel @ X178 @ X177 )
=> ~ ( v2 @ X177 ) ) )
| ! [X180: mworld] :
( ( mrel @ mactual @ X180 )
=> ! [X179: mworld] :
( ( mrel @ X180 @ X179 )
=> ~ ( v4 @ X179 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat46,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_124,plain,
! [X218: mworld,X219: mworld,X220: mworld] :
( ( v1 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X218 )
| ~ ( v1 @ X218 )
| ~ ( mrel @ mactual @ X219 )
| ~ ( mrel @ X219 @ X220 )
| ~ ( v1 @ X220 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_119])])])]) ).
thf(c_0_125,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v4 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_55]),c_0_45])]) ).
thf(c_0_126,plain,
! [X3: mworld] :
( ( v4 @ esk1_0 )
| ( v3 @ mactual )
| ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_89]),c_0_48])]),c_0_122]) ).
thf(c_0_127,plain,
! [X370: mworld,X371: mworld,X372: mworld,X373: mworld,X374: mworld] :
( ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X370 )
| ~ ( v4 @ X370 )
| ~ ( mrel @ mactual @ X371 )
| ~ ( mrel @ X371 @ X372 )
| ~ ( v2 @ X372 )
| ~ ( mrel @ mactual @ X373 )
| ~ ( mrel @ X373 @ X374 )
| ~ ( v4 @ X374 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_123])])])]) ).
thf(c_0_128,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v1 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_124]) ).
thf(c_0_129,plain,
! [X3: mworld] :
( ( v1 @ esk1_0 )
| ( v4 @ mactual )
| ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_125,c_0_45]) ).
thf(c_0_130,plain,
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v4 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_126,c_0_45]) ).
thf(c_0_131,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld] :
( ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v2 @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( v4 @ X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_127]) ).
thf(c_0_132,plain,
( ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ! [X32: mworld] :
( ( mrel @ mactual @ X32 )
=> ( v4 @ X32 ) )
| ! [X34: mworld] :
( ( mrel @ mactual @ X34 )
=> ! [X33: mworld] :
( ( mrel @ X34 @ X33 )
=> ~ ( v4 @ X33 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat9,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_133,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(spm,[status(thm)],[c_0_128,c_0_45]) ).
thf(c_0_134,plain,
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v1 @ esk1_0 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_130]),c_0_48])]),c_0_122]) ).
thf(c_0_135,plain,
! [X3: mworld,X7: mworld,X6: mworld,X5: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v3 @ mactual )
| ~ ( mrel @ X3 @ X7 )
| ~ ( v2 @ X7 )
| ~ ( v4 @ X6 )
| ~ ( v4 @ X5 ) ),
inference(spm,[status(thm)],[c_0_131,c_0_45]) ).
thf(c_0_136,plain,
! [X226: mworld,X227: mworld,X228: mworld] :
( ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X226 )
| ( v4 @ X226 )
| ~ ( mrel @ mactual @ X227 )
| ~ ( mrel @ X227 @ X228 )
| ~ ( v4 @ X228 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_132])])])]) ).
thf(c_0_137,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_133,c_0_134]),c_0_48])]),c_0_122]) ).
thf(c_0_138,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v3 @ mactual )
| ~ ( v2 @ X6 )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_135,c_0_45]) ).
thf(c_0_139,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v4 @ X3 )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v4 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_136]) ).
thf(c_0_140,plain,
( ( v1 @ mactual )
| ( v3 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_134]),c_0_48])]) ).
thf(c_0_141,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v3 @ mactual )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_138,c_0_112]),c_0_45])]) ).
thf(c_0_142,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v4 @ X6 ) ),
inference(spm,[status(thm)],[c_0_139,c_0_140]) ).
thf(c_0_143,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_141,c_0_140]) ).
thf(c_0_144,plain,
( ~ ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ! [X152: mworld] :
( ( mrel @ mactual @ X152 )
=> ! [X151: mworld] :
( ( mrel @ X152 @ X151 )
=> ( v1 @ X151 ) ) )
| ! [X154: mworld] :
( ( mrel @ mactual @ X154 )
=> ! [X153: mworld] :
( ( mrel @ X154 @ X153 )
=> ( v4 @ X153 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat40,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_145,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v4 @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_45]),c_0_143]) ).
thf(c_0_146,plain,
! [X345: mworld,X346: mworld,X347: mworld,X348: mworld] :
( ~ ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X345 )
| ~ ( mrel @ X345 @ X346 )
| ( v1 @ X346 )
| ~ ( mrel @ mactual @ X347 )
| ~ ( mrel @ X347 @ X348 )
| ( v4 @ X348 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_144])])])]) ).
thf(c_0_147,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145,c_0_55]),c_0_45])]) ).
thf(c_0_148,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v1 @ X5 )
| ( v4 @ X7 )
| ~ ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_146]) ).
thf(c_0_149,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_55]),c_0_45])]),c_0_147]) ).
thf(c_0_150,plain,
( ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ! [X35: mworld] :
( ( mrel @ mactual @ X35 )
=> ~ ( v1 @ X35 ) )
| ! [X37: mworld] :
( ( mrel @ mactual @ X37 )
=> ! [X36: mworld] :
( ( mrel @ X37 @ X36 )
=> ~ ( v1 @ X36 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat10,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_151,plain,
! [X3: mworld,X6: mworld,X7: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v4 @ X3 )
| ( v1 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X6 @ X3 )
| ~ ( mrel @ X7 @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_148,c_0_112]),c_0_140]) ).
thf(c_0_152,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_149,c_0_55]),c_0_45])]) ).
thf(c_0_153,plain,
! [X229: mworld,X230: mworld,X231: mworld] :
( ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X229 )
| ~ ( v1 @ X229 )
| ~ ( mrel @ mactual @ X230 )
| ~ ( mrel @ X230 @ X231 )
| ~ ( v1 @ X231 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_150])])])]) ).
thf(c_0_154,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X6 )
| ~ ( mrel @ X5 @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_151,c_0_55]),c_0_45])]),c_0_152]) ).
thf(c_0_155,plain,
( ( v4 @ mactual )
| ~ ( v1 @ mactual )
| ! [X104: mworld] :
( ( mrel @ mactual @ X104 )
=> ( v1 @ X104 ) )
| ! [X106: mworld] :
( ( mrel @ mactual @ X106 )
=> ! [X105: mworld] :
( ( mrel @ X106 @ X105 )
=> ~ ( v2 @ X105 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat28,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_156,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v1 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_153]) ).
thf(c_0_157,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_154,c_0_55]),c_0_45])]) ).
thf(c_0_158,plain,
( ( v4 @ mactual )
| ! [X117: mworld] :
( ( mrel @ mactual @ X117 )
=> ~ ( v1 @ X117 ) )
| ! [X119: mworld] :
( ( mrel @ mactual @ X119 )
=> ! [X118: mworld] :
( ( mrel @ X119 @ X118 )
=> ( v4 @ X118 ) ) )
| ! [X121: mworld] :
( ( mrel @ mactual @ X121 )
=> ! [X120: mworld] :
( ( mrel @ X121 @ X120 )
=> ~ ( v1 @ X120 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat32,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_159,plain,
( ~ ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ! [X125: mworld] :
( ( mrel @ mactual @ X125 )
=> ~ ( v4 @ X125 ) )
| ! [X127: mworld] :
( ( mrel @ mactual @ X127 )
=> ! [X126: mworld] :
( ( mrel @ X127 @ X126 )
=> ~ ( v1 @ X126 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat34,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_160,plain,
! [X298: mworld,X299: mworld,X300: mworld] :
( ( v4 @ mactual )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X298 )
| ( v1 @ X298 )
| ~ ( mrel @ mactual @ X299 )
| ~ ( mrel @ X299 @ X300 )
| ~ ( v2 @ X300 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_155])])])]) ).
thf(c_0_161,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X3 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( v1 @ X5 ) ),
inference(spm,[status(thm)],[c_0_156,c_0_140]) ).
thf(c_0_162,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(spm,[status(thm)],[c_0_157,c_0_45]) ).
thf(c_0_163,plain,
! [X311: mworld,X312: mworld,X313: mworld,X314: mworld,X315: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X311 )
| ~ ( v1 @ X311 )
| ~ ( mrel @ mactual @ X312 )
| ~ ( mrel @ X312 @ X313 )
| ( v4 @ X313 )
| ~ ( mrel @ mactual @ X314 )
| ~ ( mrel @ X314 @ X315 )
| ~ ( v1 @ X315 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_158])])])]) ).
thf(c_0_164,plain,
( ~ ( v1 @ mactual )
| ! [X140: mworld] :
( ( mrel @ mactual @ X140 )
=> ~ ( v4 @ X140 ) )
| ! [X142: mworld] :
( ( mrel @ mactual @ X142 )
=> ! [X141: mworld] :
( ( mrel @ X142 @ X141 )
=> ( v4 @ X141 ) ) )
| ! [X144: mworld] :
( ( mrel @ mactual @ X144 )
=> ! [X143: mworld] :
( ( mrel @ X144 @ X143 )
=> ~ ( v4 @ X143 ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[persat38,c_0_30]),c_0_31]),c_0_32]),c_0_33])]) ).
thf(c_0_165,plain,
! [X319: mworld,X320: mworld,X321: mworld] :
( ~ ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( mrel @ mactual @ X319 )
| ~ ( v4 @ X319 )
| ~ ( mrel @ mactual @ X320 )
| ~ ( mrel @ X320 @ X321 )
| ~ ( v1 @ X321 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_159])])])]) ).
thf(c_0_166,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v2 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_160]) ).
thf(c_0_167,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(spm,[status(thm)],[c_0_161,c_0_45]) ).
thf(c_0_168,plain,
( ( v1 @ esk1_0 )
| ( v1 @ mactual ) ),
inference(spm,[status(thm)],[c_0_162,c_0_45]) ).
thf(c_0_169,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld] :
( ( v4 @ mactual )
| ( v4 @ X6 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( v1 @ X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_163]) ).
thf(c_0_170,plain,
! [X334: mworld,X335: mworld,X336: mworld,X337: mworld,X338: mworld] :
( ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X334 )
| ~ ( v4 @ X334 )
| ~ ( mrel @ mactual @ X335 )
| ~ ( mrel @ X335 @ X336 )
| ( v4 @ X336 )
| ~ ( mrel @ mactual @ X337 )
| ~ ( mrel @ X337 @ X338 )
| ~ ( v4 @ X338 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_164])])])]) ).
thf(c_0_171,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ~ ( v1 @ mactual )
| ~ ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( v1 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_165]) ).
thf(c_0_172,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual )
| ~ ( v2 @ X5 ) ),
inference(spm,[status(thm)],[c_0_166,c_0_45]) ).
thf(c_0_173,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_167,c_0_168]),c_0_48])]) ).
thf(c_0_174,plain,
! [X3: mworld,X5: mworld,X7: mworld,X6: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v1 @ X7 )
| ~ ( v1 @ X6 ) ),
inference(spm,[status(thm)],[c_0_169,c_0_45]) ).
thf(c_0_175,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld] :
( ( v4 @ X6 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X7 @ X8 )
| ~ ( v4 @ X8 ) ),
inference(split_conjunct,[status(thm)],[c_0_170]) ).
thf(c_0_176,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ X3 @ X6 )
| ~ ( v1 @ X6 )
| ~ ( v4 @ X5 ) ),
inference(spm,[status(thm)],[c_0_171,c_0_98]) ).
thf(c_0_177,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_98]),c_0_45])]) ).
thf(c_0_178,plain,
v1 @ mactual,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_168]),c_0_48])]) ).
thf(c_0_179,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v1 @ X6 )
| ~ ( v1 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_174,c_0_55]),c_0_45])]) ).
thf(c_0_180,plain,
! [X3: mworld,X5: mworld,X7: mworld,X6: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X7 )
| ~ ( v4 @ X6 ) ),
inference(spm,[status(thm)],[c_0_175,c_0_45]) ).
thf(c_0_181,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( v1 @ mactual )
| ~ ( v1 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_55]),c_0_45])]) ).
thf(c_0_182,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_177,c_0_178])]) ).
thf(c_0_183,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ esk1_0 )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(spm,[status(thm)],[c_0_179,c_0_45]) ).
thf(c_0_184,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v1 @ mactual )
| ~ ( v4 @ X6 )
| ~ ( v4 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180,c_0_55]),c_0_45])]) ).
thf(c_0_185,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual )
| ~ ( v1 @ esk1_0 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_181,c_0_45]) ).
thf(c_0_186,plain,
( ( v1 @ esk1_0 )
| ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_182,c_0_55]),c_0_45])]) ).
thf(c_0_187,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v4 @ esk1_0 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_183,c_0_178]),c_0_45])]),c_0_182]) ).
thf(c_0_188,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X6 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_55]),c_0_45])]) ).
thf(c_0_189,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ esk1_0 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_184,c_0_45]) ).
thf(c_0_190,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_185,c_0_178])]),c_0_186]) ).
thf(c_0_191,plain,
( ( v4 @ esk1_0 )
| ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_55]),c_0_45])]) ).
thf(c_0_192,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v4 @ X5 ) ),
inference(spm,[status(thm)],[c_0_188,c_0_45]) ).
thf(c_0_193,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ esk1_0 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_189,c_0_178])]) ).
thf(c_0_194,plain,
v4 @ mactual,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_191]),c_0_48])]) ).
thf(c_0_195,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v4 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_192,c_0_45]) ).
thf(c_0_196,plain,
! [X3: mworld] :
( ( v4 @ esk1_0 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_193,c_0_194]),c_0_45])]) ).
thf(c_0_197,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_178]),c_0_45])]) ).
thf(c_0_198,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ esk1_0 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_195,c_0_194])]) ).
thf(c_0_199,plain,
v4 @ esk1_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_194]),c_0_45])]) ).
thf(c_0_200,plain,
( ( v2 @ mactual )
| ~ ( v3 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_197,c_0_178]),c_0_45])]) ).
thf(c_0_201,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_198,c_0_199])]) ).
thf(c_0_202,plain,
! [X5: mworld,X3: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v3 @ mactual )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_138,c_0_200]),c_0_45])]) ).
thf(c_0_203,plain,
v3 @ mactual,
inference(spm,[status(thm)],[c_0_201,c_0_45]) ).
thf(c_0_204,plain,
! [X5: mworld,X3: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v4 @ X5 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_202,c_0_203])]) ).
thf(c_0_205,plain,
! [X3: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_204,c_0_199]),c_0_48])]) ).
thf(c_0_206,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_199]),c_0_48])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO903^10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.18 % Computer : n016.cluster.edu
% 0.13/0.18 % Model : x86_64 x86_64
% 0.13/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.18 % Memory : 8046.5625MB
% 0.13/0.18 % OS : Linux 6.8.0-71-generic
% 0.13/0.18 % CPULimit : 300
% 0.13/0.18 % WCLimit : 300
% 0.13/0.18 % DateTime : Tue Sep 29 17:31:19 UTC 2026
% 0.13/0.18 % CPUTime :
% 0.13/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.22 Running higher-order theorem proving
% 0.13/0.23 Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.YJZsxf6KLy/E---3.1_652945.p
% 0.35/0.31 % Version: 3.5.1-ho
% 0.35/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.35/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.35/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.35/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.35/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.35/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.35/0.31 % Starting post_as_ho1 with 300s (1) cores
% 0.35/0.31 % ho_unfolding_3 with pid 652958 completed with status 0
% 0.35/0.31 % Result found by ho_unfolding_3
% 0.35/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.35/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.35/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.35/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.35/0.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.35/0.31 % No SInE strategy applied
% 0.35/0.31 % Search class: HGHNF-FFMF00-SHSSMFNN
% 0.35/0.31 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.35/0.31 % Starting SubtermCWHack with 136s (1) cores
% 0.35/0.31 % Starting ho_unfolding_3 with 151s (1) cores
% 0.35/0.31 % Starting sh5l with 136s (1) cores
% 0.35/0.31 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.35/0.31 % Starting lpo1_def_fix with 136s (1) cores
% 0.35/0.31 % lpo1_def_fix with pid 652966 completed with status 0
% 0.35/0.31 % Result found by lpo1_def_fix
% 0.35/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.35/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.35/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.35/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.35/0.31 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.35/0.31 % No SInE strategy applied
% 0.35/0.31 % Search class: HGHNF-FFMF00-SHSSMFNN
% 0.35/0.31 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.35/0.31 % Starting SubtermCWHack with 136s (1) cores
% 0.35/0.31 % Starting ho_unfolding_3 with 151s (1) cores
% 0.35/0.31 % Starting sh5l with 136s (1) cores
% 0.35/0.31 % Starting ehoh_best_sine_rwall with 136s (1) cores
% 0.35/0.31 % Starting lpo1_def_fix with 136s (1) cores
% 0.35/0.31 % Preprocessing time : 0.002 s
% 0.35/0.31 % Presaturation interreduction done
% 0.35/0.31
% 0.35/0.31 % Proof found!
% 0.35/0.31 % SZS status ContradictoryAxioms
% 0.35/0.31 % SZS output start CNFRefutation
% See solution above
% 0.35/0.31 % Parsed axioms : 77
% 0.35/0.31 % Removed by relevancy pruning/SinE : 0
% 0.35/0.31 % Initial clauses : 70
% 0.35/0.31 % Removed in clause preprocessing : 17
% 0.35/0.31 % Initial clauses in saturation : 53
% 0.35/0.31 % Processed clauses : 593
% 0.35/0.31 % ...of these trivial : 1
% 0.35/0.31 % ...subsumed : 187
% 0.35/0.31 % ...remaining for further processing : 405
% 0.35/0.31 % Other redundant clauses eliminated : 0
% 0.35/0.31 % Clauses deleted for lack of memory : 0
% 0.35/0.31 % Backward-subsumed : 145
% 0.35/0.31 % Backward-rewritten : 196
% 0.35/0.31 % Generated clauses : 841
% 0.35/0.31 % ...of the previous two non-redundant : 819
% 0.35/0.31 % ...aggressively subsumed : 0
% 0.35/0.31 % Contextual simplify-reflections : 29
% 0.35/0.31 % Paramodulations : 841
% 0.35/0.31 % Factorizations : 0
% 0.35/0.31 % NegExts : 0
% 0.35/0.31 % Equation resolutions : 0
% 0.35/0.31 % Disequality decompositions : 0
% 0.35/0.31 % Total rewrite steps : 510
% 0.35/0.31 % ...of those cached : 503
% 0.35/0.31 % Propositional unsat checks : 0
% 0.35/0.31 % Propositional check models : 0
% 0.35/0.31 % Propositional check unsatisfiable : 0
% 0.35/0.31 % Propositional clauses : 0
% 0.35/0.31 % Propositional clauses after purity: 0
% 0.35/0.31 % Propositional unsat core size : 0
% 0.35/0.31 % Propositional preprocessing time : 0.000
% 0.35/0.31 % Propositional encoding time : 0.000
% 0.35/0.31 % Propositional solver time : 0.000
% 0.35/0.31 % Success case prop preproc time : 0.000
% 0.35/0.31 % Success case prop encoding time : 0.000
% 0.35/0.31 % Success case prop solver time : 0.000
% 0.35/0.31 % Current number of processed clauses : 12
% 0.35/0.31 % Positive orientable unit clauses : 7
% 0.35/0.31 % Positive unorientable unit clauses: 0
% 0.35/0.31 % Negative unit clauses : 0
% 0.35/0.31 % Non-unit-clauses : 5
% 0.35/0.31 % Current number of unprocessed clauses: 234
% 0.35/0.31 % ...number of literals in the above : 1447
% 0.35/0.31 % Current number of archived formulas : 0
% 0.35/0.31 % Current number of archived clauses : 393
% 0.35/0.31 % Clause-clause subsumption calls (NU) : 3985
% 0.35/0.31 % Rec. Clause-clause subsumption calls : 1421
% 0.35/0.31 % Non-unit clause-clause subsumptions : 359
% 0.35/0.31 % Unit Clause-clause subsumption calls : 49
% 0.35/0.31 % Rewrite failures with RHS unbound : 0
% 0.35/0.31 % BW rewrite match attempts : 6
% 0.35/0.31 % BW rewrite match successes : 5
% 0.35/0.31 % Condensation attempts : 0
% 0.35/0.31 % Condensation successes : 0
% 0.35/0.31 % Termbank termtop insertions : 43495
% 0.35/0.31 % Search garbage collected termcells : 8636
% 0.35/0.31
% 0.35/0.31 % -------------------------------------------------
% 0.35/0.31 % User time : 0.047 s
% 0.35/0.31 % System time : 0.005 s
% 0.35/0.31 % Total time : 0.051 s
% 0.35/0.31 % Maximum resident set size: 4972 pages
% 0.35/0.31
% 0.35/0.31 % -------------------------------------------------
% 0.35/0.31 % User time : 0.208 s
% 0.35/0.31 % System time : 0.019 s
% 0.35/0.31 % Total time : 0.227 s
% 0.35/0.31 % Maximum resident set size: 4608 pages
% 0.35/0.31 % E exiting
%------------------------------------------------------------------------------