%------------------------------------------------------------------------------
% File : E-SAT---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 : n002.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:44:58 AM UTC 2026
% Result : ContradictoryAxioms 0.20s 0.31s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 29
% Syntax : Number of formulae : 197 ( 18 unt; 0 typ; 0 def)
% Number of atoms : 1162 ( 10 equ; 0 cnn)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 2677 ( 488 ~; 628 |; 5 &;1489 @)
% ( 0 <=>; 67 =>; 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 : 378 ( 21 ^; 354 !; 3 ?; 378 :)
% 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.mh9iaRe9zE/E---3.1_1600899.p',mlocal_def) ).
thf(mor_def,axiom,
( mor
= ( ^ [X2: mworld > $o,X4: mworld > $o,X3: mworld] :
( ( X2 @ X3 )
| ( X4 @ X3 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.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.mh9iaRe9zE/E---3.1_1600899.p',mbox_def) ).
thf(mnot_def,axiom,
( mnot
= ( ^ [X2: mworld > $o,X3: mworld] :
~ ( X2 @ X3 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',mnot_def) ).
thf(persat22,axiom,
mlocal @ ( mor @ v3 @ ( mor @ v4 @ ( mor @ ( mbox @ v2 ) @ ( mbox @ ( mbox @ v1 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat22) ).
thf(persat30,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v1 ) @ ( mbox @ ( mbox @ v2 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat30) ).
thf(mrel_reflexive,axiom,
! [X3: mworld] : ( mrel @ X3 @ X3 ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',mrel_reflexive) ).
thf(mdia_def,axiom,
( mdia
= ( ^ [X1: mworld > $o,X3: mworld] :
? [X5: mworld] :
( ( mrel @ X3 @ X5 )
& ( X1 @ X5 ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',mdia_def) ).
thf(persat28,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ v1 ) @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat28) ).
thf(deontic1,axiom,
( mlocal
@ ( mdia
@ ^ [X3: mworld] : $true ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',deontic1) ).
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.mh9iaRe9zE/E---3.1_1600899.p',mrel_transitive) ).
thf(persat5,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v3 @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat5) ).
thf(persat29,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat29) ).
thf(persat8,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v3 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat8) ).
thf(persat2,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat2) ).
thf(persat26,axiom,
mlocal @ ( mor @ v3 @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mbox @ v3 ) ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat26) ).
thf(persat7,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mnot @ v4 ) @ ( mbox @ ( mbox @ ( mnot @ v2 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat7) ).
thf(persat17,axiom,
mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mbox @ ( mbox @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v3 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat17) ).
thf(persat15,axiom,
mlocal @ ( mor @ v2 @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat15) ).
thf(persat14,axiom,
mlocal @ ( mor @ v2 @ ( mor @ v3 @ ( mor @ v4 @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat14) ).
thf(persat35,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v3 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat35) ).
thf(persat34,axiom,
mlocal @ ( mor @ ( mnot @ v1 ) @ ( mor @ ( mnot @ v2 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat34) ).
thf(persat3,axiom,
mlocal @ ( mor @ v1 @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat3) ).
thf(persat31,axiom,
mlocal @ ( mor @ v4 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mbox @ v1 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat31) ).
thf(persat9,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ v4 ) @ ( mbox @ ( mbox @ ( mnot @ v4 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat9) ).
thf(persat10,axiom,
mlocal @ ( mor @ v1 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat10) ).
thf(persat44,axiom,
mlocal @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mnot @ v4 ) @ ( mor @ ( mbox @ ( mnot @ v4 ) ) @ ( mbox @ ( mbox @ v4 ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat44) ).
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.mh9iaRe9zE/E---3.1_1600899.p',persat46) ).
thf(persat18,axiom,
mlocal @ ( mor @ v2 @ ( mor @ ( mnot @ v3 ) @ ( mor @ ( mbox @ ( mnot @ v1 ) ) @ ( mbox @ ( mbox @ ( mnot @ v1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.mh9iaRe9zE/E---3.1_1600899.p',persat18) ).
thf(c_0_29,plain,
( mlocal
= ( ^ [Z0: mworld > $o] : ( Z0 @ mactual ) ) ),
inference(fof_simplification,[status(thm)],[mlocal_def]) ).
thf(c_0_30,plain,
( mor
= ( ^ [Z0: mworld > $o,Z1: mworld > $o,Z2: mworld] :
( ( Z0 @ Z2 )
| ( Z1 @ Z2 ) ) ) ),
inference(fof_simplification,[status(thm)],[mor_def]) ).
thf(c_0_31,plain,
( mbox
= ( ^ [Z0: mworld > $o,Z1: mworld] :
! [X5: mworld] :
( ( mrel @ Z1 @ X5 )
=> ( Z0 @ X5 ) ) ) ),
inference(fof_simplification,[status(thm)],[mbox_def]) ).
thf(c_0_32,plain,
( mnot
= ( ^ [Z0: mworld > $o,Z1: mworld] :
~ ( Z0 @ Z1 ) ) ),
inference(fof_simplification,[status(thm)],[mnot_def]) ).
thf(c_0_33,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_29]),c_0_30]),c_0_31]) ).
thf(c_0_34,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_35,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_33])])])]) ).
thf(c_0_36,plain,
! [X201: mworld] : ( mrel @ X201 @ X201 ),
inference(variable_rename,[status(thm)],[mrel_reflexive]) ).
thf(c_0_37,plain,
( mdia
= ( ^ [Z0: mworld > $o,Z1: mworld] :
? [X5: mworld] :
( ( mrel @ Z1 @ X5 )
& ( Z0 @ X5 ) ) ) ),
inference(fof_simplification,[status(thm)],[mdia_def]) ).
thf(c_0_38,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_39,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_34])])])]) ).
thf(c_0_40,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_35]) ).
thf(c_0_41,plain,
! [X3: mworld] : ( mrel @ X3 @ X3 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
thf(c_0_42,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_29]),c_0_37]) ).
thf(c_0_43,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_38])])])]) ).
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_39]) ).
thf(c_0_45,plain,
! [X5: mworld,X3: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ( v1 @ X3 )
| ( v2 @ X5 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
thf(c_0_46,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_47,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_42])])])]) ).
thf(c_0_48,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_29]),c_0_30]),c_0_31]) ).
thf(c_0_49,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_50,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_43]) ).
thf(c_0_51,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ( v2 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_41]),c_0_45]) ).
thf(c_0_52,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( mrel @ X3 @ X6 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
thf(c_0_53,plain,
mrel @ mactual @ esk1_0,
inference(split_conjunct,[status(thm)],[c_0_47]) ).
thf(c_0_54,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_48])])])]) ).
thf(c_0_55,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_49])])])]) ).
thf(c_0_56,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_41]),c_0_51]) ).
thf(c_0_57,plain,
! [X3: mworld] :
( ( mrel @ X3 @ esk1_0 )
| ~ ( mrel @ X3 @ mactual ) ),
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
thf(c_0_58,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_59,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_54]) ).
thf(c_0_60,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_55]) ).
thf(c_0_61,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_56,c_0_57]),c_0_41])]) ).
thf(c_0_62,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_58])])])]) ).
thf(c_0_63,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ( v4 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X6 @ X3 ) ),
inference(spm,[status(thm)],[c_0_59,c_0_41]) ).
thf(c_0_64,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_57]),c_0_41])]),c_0_61]) ).
thf(c_0_65,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_62]) ).
thf(c_0_66,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v4 @ mactual )
| ( v2 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(spm,[status(thm)],[c_0_51,c_0_41]) ).
thf(c_0_67,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_41]),c_0_61]) ).
thf(c_0_68,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v1 @ mactual )
| ( v4 @ X3 )
| ( v3 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_57]),c_0_41])]) ).
thf(c_0_69,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_57]),c_0_41])]) ).
thf(c_0_70,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_71,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ( v4 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ X6 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_57]),c_0_41])]) ).
thf(c_0_72,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(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_66]),c_0_41])]) ).
thf(c_0_73,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67,c_0_57]),c_0_41])]) ).
thf(c_0_74,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_41]),c_0_69]) ).
thf(c_0_75,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_70])])])]) ).
thf(c_0_76,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v1 @ mactual )
| ( v4 @ X3 )
| ( v3 @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( mrel @ mactual @ X5 ) ),
inference(spm,[status(thm)],[c_0_71,c_0_41]) ).
thf(c_0_77,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_78,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_41]),c_0_73]) ).
thf(c_0_79,plain,
( ( v3 @ esk1_0 )
| ( v3 @ mactual )
| ( v4 @ mactual ) ),
inference(spm,[status(thm)],[c_0_74,c_0_41]) ).
thf(c_0_80,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_81,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_75]) ).
thf(c_0_82,plain,
! [X3: mworld] :
( ( v4 @ esk1_0 )
| ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(spm,[status(thm)],[c_0_76,c_0_41]) ).
thf(c_0_83,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_77])])])]) ).
thf(c_0_84,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78,c_0_79]),c_0_53])]) ).
thf(c_0_85,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_80])])])]) ).
thf(c_0_86,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual )
| ~ ( v3 @ X3 ) ),
inference(spm,[status(thm)],[c_0_81,c_0_41]) ).
thf(c_0_87,plain,
( ( v3 @ mactual )
| ( v1 @ mactual )
| ( v4 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_82,c_0_41]) ).
thf(c_0_88,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_83]) ).
thf(c_0_89,plain,
( ( v4 @ mactual )
| ( v3 @ mactual ) ),
inference(spm,[status(thm)],[c_0_84,c_0_41]) ).
thf(c_0_90,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_85]) ).
thf(c_0_91,plain,
( ( v4 @ esk1_0 )
| ( v2 @ mactual )
| ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_41])]),c_0_87]) ).
thf(c_0_92,plain,
! [X3: mworld,X6: mworld,X5: mworld,X7: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X7 )
| ~ ( mrel @ X6 @ X3 )
| ~ ( v4 @ X7 ) ),
inference(csr,[status(thm)],[c_0_88,c_0_89]) ).
thf(c_0_93,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ esk1_0 )
| ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v2 @ X5 ) ),
inference(spm,[status(thm)],[c_0_90,c_0_91]) ).
thf(c_0_94,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_57]),c_0_41])]) ).
thf(c_0_95,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v4 @ esk1_0 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v2 @ X3 ) ),
inference(spm,[status(thm)],[c_0_93,c_0_41]) ).
thf(c_0_96,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X5 ) ),
inference(spm,[status(thm)],[c_0_94,c_0_41]) ).
thf(c_0_97,plain,
( ( v4 @ esk1_0 )
| ( v1 @ mactual )
| ~ ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95,c_0_91]),c_0_41])]) ).
thf(c_0_98,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_78,c_0_89]),c_0_41])]) ).
thf(c_0_99,plain,
( ( v2 @ mactual )
| ~ ( v1 @ mactual )
| ! [X59: mworld] :
( ( mrel @ mactual @ X59 )
=> ! [X58: mworld] :
( ( mrel @ X59 @ X58 )
=> ( v4 @ X58 ) ) )
| ! [X61: mworld] :
( ( mrel @ mactual @ X61 )
=> ! [X60: mworld] :
( ( mrel @ X61 @ X60 )
=> ~ ( v3 @ X60 ) ) ) ),
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)],[persat17,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_100,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96,c_0_97]),c_0_41])]),c_0_98]) ).
thf(c_0_101,plain,
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ! [X54: mworld] :
( ( mrel @ mactual @ X54 )
=> ! [X53: mworld] :
( ( mrel @ X54 @ X53 )
=> ~ ( v4 @ X53 ) ) ) ),
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)],[persat15,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_102,plain,
( ( v2 @ mactual )
| ( v3 @ mactual )
| ( v4 @ mactual )
| ! [X52: mworld] :
( ( mrel @ mactual @ X52 )
=> ! [X51: mworld] :
( ( mrel @ X52 @ X51 )
=> ~ ( v4 @ X51 ) ) ) ),
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)],[persat14,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_103,plain,
! [X252: mworld,X253: mworld,X254: mworld,X255: mworld] :
( ( v2 @ mactual )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X252 )
| ~ ( mrel @ X252 @ X253 )
| ( v4 @ X253 )
| ~ ( mrel @ mactual @ X254 )
| ~ ( mrel @ X254 @ X255 )
| ~ ( v3 @ X255 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_99])])])]) ).
thf(c_0_104,plain,
( ( v3 @ mactual )
| ( v1 @ mactual ) ),
inference(spm,[status(thm)],[c_0_100,c_0_41]) ).
thf(c_0_105,plain,
! [X247: mworld,X248: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X247 )
| ~ ( mrel @ X247 @ X248 )
| ~ ( v4 @ X248 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_101])])])]) ).
thf(c_0_106,plain,
! [X245: mworld,X246: mworld] :
( ( v2 @ mactual )
| ( v3 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X245 )
| ~ ( mrel @ X245 @ X246 )
| ~ ( v4 @ X246 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_102])])])]) ).
thf(c_0_107,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v2 @ mactual )
| ( v4 @ X5 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 )
| ~ ( v3 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
thf(c_0_108,plain,
( ( v2 @ mactual )
| ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_104]),c_0_41])]),c_0_104]) ).
thf(c_0_109,plain,
! [X3: mworld,X5: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_105]) ).
thf(c_0_110,plain,
! [X3: mworld,X5: mworld] :
( ( v2 @ mactual )
| ( v3 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_106]) ).
thf(c_0_111,plain,
( ~ ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ! [X128: mworld] :
( ( mrel @ mactual @ X128 )
=> ~ ( v3 @ X128 ) )
| ! [X130: mworld] :
( ( mrel @ mactual @ X130 )
=> ! [X129: mworld] :
( ( mrel @ X130 @ X129 )
=> ( v4 @ X129 ) ) ) ),
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)],[persat35,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_112,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v2 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v3 @ X6 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107,c_0_57]),c_0_41])]),c_0_108]) ).
thf(c_0_113,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v3 @ X5 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_57]),c_0_41])]),c_0_69]) ).
thf(c_0_114,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(csr,[status(thm)],[c_0_109,c_0_110]) ).
thf(c_0_115,plain,
! [X322: mworld,X323: mworld,X324: mworld] :
( ~ ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X322 )
| ~ ( v3 @ X322 )
| ~ ( mrel @ mactual @ X323 )
| ~ ( mrel @ X323 @ X324 )
| ( v4 @ X324 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_111])])])]) ).
thf(c_0_116,plain,
! [X3: mworld,X5: mworld] :
( ( v2 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v3 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112,c_0_57]),c_0_41])]) ).
thf(c_0_117,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_89]),c_0_41])]) ).
thf(c_0_118,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( v4 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_114,c_0_57]),c_0_41])]) ).
thf(c_0_119,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ X6 )
| ~ ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_115]) ).
thf(c_0_120,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_121,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 )
| ~ ( mrel @ esk1_0 @ X5 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116,c_0_117]),c_0_118]) ).
thf(c_0_122,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ X5 @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_73]),c_0_41])]),c_0_73]) ).
thf(c_0_123,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_120])])])]) ).
thf(c_0_124,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ( v4 @ mactual )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(spm,[status(thm)],[c_0_121,c_0_41]) ).
thf(c_0_125,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(spm,[status(thm)],[c_0_122,c_0_41]) ).
thf(c_0_126,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_123]) ).
thf(c_0_127,plain,
( ( v4 @ mactual )
| ( v2 @ mactual ) ),
inference(spm,[status(thm)],[c_0_124,c_0_41]) ).
thf(c_0_128,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_57]),c_0_41])]) ).
thf(c_0_129,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ X3 @ X6 )
| ~ ( v1 @ X6 ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_126,c_0_127]),c_0_128]) ).
thf(c_0_130,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_41]),c_0_61]) ).
thf(c_0_131,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v3 @ X6 ) ),
inference(spm,[status(thm)],[c_0_65,c_0_108]) ).
thf(c_0_132,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(spm,[status(thm)],[c_0_92,c_0_41]) ).
thf(c_0_133,plain,
! [X3: mworld] :
( ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_57]),c_0_41])]) ).
thf(c_0_134,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ X5 ) ),
inference(spm,[status(thm)],[c_0_131,c_0_41]) ).
thf(c_0_135,plain,
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ! [X16: mworld] :
( ( mrel @ mactual @ X16 )
=> ! [X15: mworld] :
( ( mrel @ X16 @ X15 )
=> ~ ( v4 @ X15 ) ) ) ),
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)],[persat3,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_136,plain,
( ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ! [X114: mworld] :
( ( mrel @ mactual @ X114 )
=> ! [X113: mworld] :
( ( mrel @ X114 @ X113 )
=> ( v1 @ X113 ) ) )
| ! [X116: mworld] :
( ( mrel @ mactual @ X116 )
=> ! [X115: mworld] :
( ( mrel @ X116 @ X115 )
=> ( v4 @ X115 ) ) ) ),
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)],[persat31,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_137,plain,
! [X3: mworld,X5: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X5 ) ),
inference(spm,[status(thm)],[c_0_132,c_0_41]) ).
thf(c_0_138,plain,
( ( v4 @ mactual )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_133,c_0_57]),c_0_41])]) ).
thf(c_0_139,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_104]),c_0_41])]) ).
thf(c_0_140,plain,
! [X209: mworld,X210: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X209 )
| ~ ( mrel @ X209 @ X210 )
| ~ ( v4 @ X210 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_135])])])]) ).
thf(c_0_141,plain,
! [X307: mworld,X308: mworld,X309: mworld,X310: mworld] :
( ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X307 )
| ~ ( mrel @ X307 @ X308 )
| ( v1 @ X308 )
| ~ ( mrel @ mactual @ X309 )
| ~ ( mrel @ X309 @ X310 )
| ( v4 @ X310 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_136])])])]) ).
thf(c_0_142,plain,
! [X3: mworld] :
( ( v3 @ mactual )
| ( v3 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_41])]),c_0_139]) ).
thf(c_0_143,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(split_conjunct,[status(thm)],[c_0_140]) ).
thf(c_0_144,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ( v4 @ mactual )
| ( v1 @ X5 )
| ( v4 @ X7 )
| ~ ( v3 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ X3 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X6 @ X7 ) ),
inference(split_conjunct,[status(thm)],[c_0_141]) ).
thf(c_0_145,plain,
v3 @ mactual,
inference(spm,[status(thm)],[c_0_142,c_0_41]) ).
thf(c_0_146,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v3 @ mactual )
| ~ ( v4 @ X3 ) ),
inference(spm,[status(thm)],[c_0_143,c_0_41]) ).
thf(c_0_147,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_148,plain,
! [X5: mworld,X7: mworld,X6: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v1 @ X3 )
| ( v4 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ mactual @ X7 )
| ~ ( mrel @ X6 @ X5 )
| ~ ( mrel @ X7 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_144,c_0_145])]) ).
thf(c_0_149,plain,
( ( v2 @ mactual )
| ( v1 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( v4 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_146,c_0_97]),c_0_53])]) ).
thf(c_0_150,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_147])])])]) ).
thf(c_0_151,plain,
! [X3: mworld,X6: mworld,X5: mworld] :
( ( v4 @ mactual )
| ( v4 @ X3 )
| ( v1 @ 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_148,c_0_57]),c_0_41])]) ).
thf(c_0_152,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X3 @ X5 )
| ~ ( v3 @ mactual )
| ~ ( v2 @ X5 ) ),
inference(spm,[status(thm)],[c_0_90,c_0_149]) ).
thf(c_0_153,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_154,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_150]) ).
thf(c_0_155,plain,
! [X5: mworld,X3: mworld] :
( ( v4 @ mactual )
| ( v1 @ 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_151,c_0_57]),c_0_41])]) ).
thf(c_0_156,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ mactual )
| ~ ( v3 @ mactual )
| ~ ( v2 @ X3 ) ),
inference(spm,[status(thm)],[c_0_152,c_0_41]) ).
thf(c_0_157,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v1 @ mactual )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v3 @ X6 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_119,c_0_145])]) ).
thf(c_0_158,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_153])])])]) ).
thf(c_0_159,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_154,c_0_104]) ).
thf(c_0_160,plain,
! [X3: mworld] :
( ( v4 @ esk1_0 )
| ( v4 @ mactual )
| ( v1 @ X3 )
| ~ ( mrel @ esk1_0 @ X3 ) ),
inference(spm,[status(thm)],[c_0_155,c_0_41]) ).
thf(c_0_161,plain,
( ( v1 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( v3 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_156,c_0_149]),c_0_41])]) ).
thf(c_0_162,plain,
! [X3: mworld,X5: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual )
| ~ ( v3 @ X5 ) ),
inference(spm,[status(thm)],[c_0_157,c_0_41]) ).
thf(c_0_163,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_158]) ).
thf(c_0_164,plain,
! [X3: mworld,X5: mworld] :
( ( v1 @ mactual )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( v4 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159,c_0_57]),c_0_41])]) ).
thf(c_0_165,plain,
( ( v1 @ esk1_0 )
| ( v4 @ mactual )
| ( v4 @ esk1_0 ) ),
inference(spm,[status(thm)],[c_0_160,c_0_41]) ).
thf(c_0_166,plain,
( ( v1 @ mactual )
| ~ ( v4 @ mactual ) ),
inference(spm,[status(thm)],[c_0_161,c_0_104]) ).
thf(c_0_167,plain,
! [X3: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_162,c_0_145]),c_0_41])]) ).
thf(c_0_168,plain,
( ~ ( v3 @ mactual )
| ~ ( v4 @ mactual )
| ! [X169: mworld] :
( ( mrel @ mactual @ X169 )
=> ~ ( v4 @ X169 ) )
| ! [X171: mworld] :
( ( mrel @ mactual @ X171 )
=> ! [X170: mworld] :
( ( mrel @ X171 @ X170 )
=> ( v4 @ X170 ) ) ) ),
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)],[persat44,c_0_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_169,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_163,c_0_104]) ).
thf(c_0_170,plain,
! [X3: mworld] :
( ( v1 @ esk1_0 )
| ( v4 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_165]),c_0_41])]),c_0_166]),c_0_167]) ).
thf(c_0_171,plain,
! [X363: mworld,X364: mworld,X365: mworld] :
( ~ ( v3 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X363 )
| ~ ( v4 @ X363 )
| ~ ( mrel @ mactual @ X364 )
| ~ ( mrel @ X364 @ X365 )
| ( v4 @ X365 ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_168])])])]) ).
thf(c_0_172,plain,
! [X5: mworld,X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(spm,[status(thm)],[c_0_169,c_0_41]) ).
thf(c_0_173,plain,
( ( v1 @ esk1_0 )
| ( v1 @ mactual ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166,c_0_170]),c_0_41])]) ).
thf(c_0_174,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ X6 )
| ~ ( v3 @ mactual )
| ~ ( v4 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ X5 @ X6 ) ),
inference(split_conjunct,[status(thm)],[c_0_171]) ).
thf(c_0_175,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_176,plain,
! [X3: mworld] :
( ( v1 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_173]),c_0_53])]) ).
thf(c_0_177,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v4 @ mactual )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v4 @ X6 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_174,c_0_145])]) ).
thf(c_0_178,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_175])])])]) ).
thf(c_0_179,plain,
v1 @ mactual,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_176,c_0_173]),c_0_53])]) ).
thf(c_0_180,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 )
| ~ ( v1 @ mactual ) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_167]),c_0_41])]),c_0_167]) ).
thf(c_0_181,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_29]),c_0_32]),c_0_30]),c_0_31])]) ).
thf(c_0_182,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_178]) ).
thf(c_0_183,plain,
! [X3: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167,c_0_179])]) ).
thf(c_0_184,plain,
! [X6: mworld,X5: mworld,X3: mworld] :
( ( v4 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X5 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_180,c_0_179])]) ).
thf(c_0_185,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_181])])])]) ).
thf(c_0_186,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld,X8: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( mrel @ X3 @ X7 )
| ~ ( mrel @ X5 @ X8 )
| ~ ( v2 @ X8 ) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_182,c_0_145])]),c_0_183]),c_0_184]) ).
thf(c_0_187,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_185]) ).
thf(c_0_188,plain,
! [X3: mworld,X5: mworld,X6: mworld,X7: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( mrel @ esk1_0 @ X6 )
| ~ ( mrel @ X3 @ X7 )
| ~ ( v2 @ X7 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_57]),c_0_41])]) ).
thf(c_0_189,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_187,c_0_41]) ).
thf(c_0_190,plain,
! [X3: mworld,X5: mworld,X6: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ esk1_0 @ X5 )
| ~ ( mrel @ mactual @ X6 )
| ~ ( v2 @ X6 ) ),
inference(spm,[status(thm)],[c_0_188,c_0_41]) ).
thf(c_0_191,plain,
! [X5: mworld,X3: mworld] :
( ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v1 @ X5 )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_189,c_0_145])]) ).
thf(c_0_192,plain,
! [X3: mworld,X5: mworld] :
( ~ ( mrel @ esk1_0 @ X3 )
| ~ ( mrel @ mactual @ X5 )
| ~ ( v2 @ X5 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_57]),c_0_41])]) ).
thf(c_0_193,plain,
! [X3: mworld] :
( ( v2 @ mactual )
| ~ ( mrel @ mactual @ X3 )
| ~ ( v1 @ X3 ) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_179]),c_0_41])]) ).
thf(c_0_194,plain,
! [X3: mworld] :
( ~ ( mrel @ mactual @ X3 )
| ~ ( v2 @ X3 ) ),
inference(spm,[status(thm)],[c_0_192,c_0_41]) ).
thf(c_0_195,plain,
v2 @ mactual,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_193,c_0_179]),c_0_41])]) ).
thf(c_0_196,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_194,c_0_195]),c_0_41])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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.08/0.17 % Computer : n002.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 17:29:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.24 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.mh9iaRe9zE/E---3.1_1600899.p
% 0.20/0.31 % Version: 3.5.1-ho
% 0.20/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.20/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.20/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.20/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.20/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.20/0.31 % Starting post_as_ho1 with 300s (1) cores
% 0.20/0.31 % almost_fo_3_lam with pid 1600936 completed with status 0
% 0.20/0.31 % Result found by almost_fo_3_lam
% 0.20/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.20/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.20/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.20/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.20/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.20/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.31 % No SInE strategy applied
% 0.20/0.31 % Search class: HGHNF-FFMF00-SHSSMFNN
% 0.20/0.31 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.20/0.31 % Starting SubtermCWHack with 28s (1) cores
% 0.20/0.31 % SubtermCWHack with pid 1600945 completed with status 0
% 0.20/0.31 % Result found by SubtermCWHack
% 0.20/0.31 % partial match(1): HSMSSMSSMLMNHSN
% 0.20/0.31 % Preprocessing class: HSLSSMSSMLMNHSN.
% 0.20/0.31 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/0.31 % Starting ho_unfolding_3 with 1500s (5) cores
% 0.20/0.31 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 0.20/0.31 % Starting almost_fo_3_lam with 300s (1) cores
% 0.20/0.31 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/0.31 % No SInE strategy applied
% 0.20/0.31 % Search class: HGHNF-FFMF00-SHSSMFNN
% 0.20/0.31 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.20/0.31 % Starting SubtermCWHack with 28s (1) cores
% 0.20/0.31 % Preprocessing time : 0.002 s
% 0.20/0.31
% 0.20/0.31 % Proof found!
% 0.20/0.31 % SZS status ContradictoryAxioms
% 0.20/0.31 % SZS output start CNFRefutation
% See solution above
% 0.20/0.31 % Parsed axioms : 77
% 0.20/0.31 % Removed by relevancy pruning/SinE : 0
% 0.20/0.31 % Initial clauses : 70
% 0.20/0.31 % Removed in clause preprocessing : 17
% 0.20/0.31 % Initial clauses in saturation : 53
% 0.20/0.31 % Processed clauses : 496
% 0.20/0.31 % ...of these trivial : 2
% 0.20/0.31 % ...subsumed : 206
% 0.20/0.31 % ...remaining for further processing : 288
% 0.20/0.31 % Other redundant clauses eliminated : 0
% 0.20/0.31 % Clauses deleted for lack of memory : 0
% 0.20/0.31 % Backward-subsumed : 175
% 0.20/0.31 % Backward-rewritten : 88
% 0.20/0.31 % Generated clauses : 931
% 0.20/0.31 % ...of the previous two non-redundant : 776
% 0.20/0.31 % ...aggressively subsumed : 0
% 0.20/0.31 % Contextual simplify-reflections : 44
% 0.20/0.31 % Paramodulations : 931
% 0.20/0.31 % Factorizations : 0
% 0.20/0.31 % NegExts : 0
% 0.20/0.31 % Equation resolutions : 0
% 0.20/0.31 % Disequality decompositions : 0
% 0.20/0.31 % Total rewrite steps : 407
% 0.20/0.31 % ...of those cached : 398
% 0.20/0.31 % Propositional unsat checks : 0
% 0.20/0.31 % Propositional check models : 0
% 0.20/0.31 % Propositional check unsatisfiable : 0
% 0.20/0.31 % Propositional clauses : 0
% 0.20/0.31 % Propositional clauses after purity: 0
% 0.20/0.31 % Propositional unsat core size : 0
% 0.20/0.31 % Propositional preprocessing time : 0.000
% 0.20/0.31 % Propositional encoding time : 0.000
% 0.20/0.31 % Propositional solver time : 0.000
% 0.20/0.31 % Success case prop preproc time : 0.000
% 0.20/0.31 % Success case prop encoding time : 0.000
% 0.20/0.31 % Success case prop solver time : 0.000
% 0.20/0.31 % Current number of processed clauses : 25
% 0.20/0.31 % Positive orientable unit clauses : 8
% 0.20/0.31 % Positive unorientable unit clauses: 0
% 0.20/0.31 % Negative unit clauses : 1
% 0.20/0.31 % Non-unit-clauses : 16
% 0.20/0.31 % Current number of unprocessed clauses: 53
% 0.20/0.31 % ...number of literals in the above : 402
% 0.20/0.31 % Current number of archived formulas : 0
% 0.20/0.31 % Current number of archived clauses : 263
% 0.20/0.31 % Clause-clause subsumption calls (NU) : 3445
% 0.20/0.31 % Rec. Clause-clause subsumption calls : 1153
% 0.20/0.31 % Non-unit clause-clause subsumptions : 423
% 0.20/0.31 % Unit Clause-clause subsumption calls : 61
% 0.20/0.31 % Rewrite failures with RHS unbound : 0
% 0.20/0.31 % BW rewrite match attempts : 7
% 0.20/0.31 % BW rewrite match successes : 6
% 0.20/0.31 % Condensation attempts : 0
% 0.20/0.31 % Condensation successes : 0
% 0.20/0.31 % Termbank termtop insertions : 41393
% 0.20/0.31 % Search garbage collected termcells : 8636
% 0.20/0.31
% 0.20/0.31 % -------------------------------------------------
% 0.20/0.31 % User time : 0.044 s
% 0.20/0.31 % System time : 0.007 s
% 0.20/0.31 % Total time : 0.051 s
% 0.20/0.31 % Maximum resident set size: 4920 pages
% 0.20/0.31
% 0.20/0.31 % -------------------------------------------------
% 0.20/0.31 % User time : 0.045 s
% 0.20/0.31 % System time : 0.010 s
% 0.20/0.31 % Total time : 0.055 s
% 0.20/0.31 % Maximum resident set size: 4864 pages
% 0.20/0.31 % E exiting
%------------------------------------------------------------------------------