%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SYN391^4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:41:04 AM UTC 2026
% Result : Theorem 0.12s 0.28s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN391^4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.18 % Computer : n006.cluster.edu
% 0.12/0.18 % Model : x86_64 x86_64
% 0.12/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.18 % Memory : 8046.5625MB
% 0.12/0.18 % OS : Linux 6.8.0-71-generic
% 0.12/0.18 % CPULimit : 300
% 0.12/0.18 % WCLimit : 300
% 0.12/0.18 % DateTime : Tue Sep 29 16:15:39 UTC 2026
% 0.12/0.18 % CPUTime :
% 0.12/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running higher-order theorem proving
% 0.12/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.SqKfsABsil/E---3.1_927003.p
% 0.12/0.28 % Version: 3.5.1-ho
% 0.12/0.28 % Preprocessing class: HSMSSMSSMLSNHSN.
% 0.12/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.12/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.12/0.28 % Starting post_as_ho3 with 300s (1) cores
% 0.12/0.28 % Starting post_as_ho11 with 300s (1) cores
% 0.12/0.28 % Starting full_lambda_8 with 300s (1) cores
% 0.12/0.28 % post_as_ho3 with pid 927030 completed with status 0
% 0.12/0.28 % Result found by post_as_ho3
% 0.12/0.28 % Preprocessing class: HSMSSMSSMLSNHSN.
% 0.12/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.12/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.12/0.28 % Starting post_as_ho3 with 300s (1) cores
% 0.12/0.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.12/0.28 % No SInE strategy applied
% 0.12/0.28 % Search class: HGHNF-FFSF22-SHSSMFNN
% 0.12/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.12/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.12/0.28 % SubtermCWHack with pid 927033 completed with status 0
% 0.12/0.28 % Result found by SubtermCWHack
% 0.12/0.28 % Preprocessing class: HSMSSMSSMLSNHSN.
% 0.12/0.28 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.12/0.28 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.12/0.28 % Starting post_as_ho3 with 300s (1) cores
% 0.12/0.28 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.12/0.28 % No SInE strategy applied
% 0.12/0.28 % Search class: HGHNF-FFSF22-SHSSMFNN
% 0.12/0.28 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.12/0.28 % Starting SubtermCWHack with 28s (1) cores
% 0.12/0.28 % Preprocessing time : 0.001 s
% 0.12/0.28
% 0.12/0.28 % Proof found!
% 0.12/0.28 % SZS status Theorem
% 0.12/0.28 % SZS output start CNFRefutation
% 0.12/0.28 thf(decl_23, type, irel: $i > $i > $o).
% 0.12/0.28 thf(decl_24, type, mnot: ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_25, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_26, type, mand: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_27, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_28, type, mbox_s4: ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_29, type, iatom: ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_30, type, inot: ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_33, type, iand: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_34, type, ior: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_35, type, iimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.12/0.28 thf(decl_39, type, ivalid: ($i > $o) > $o).
% 0.12/0.28 thf(decl_43, type, p1: $i > $o).
% 0.12/0.28 thf(decl_44, type, p2: $i > $o).
% 0.12/0.28 thf(decl_45, type, epred1_1: $i > $o).
% 0.12/0.28 thf(decl_46, type, esk1_0: $i).
% 0.12/0.28 thf(decl_47, type, esk2_0: $i).
% 0.12/0.28 thf(decl_48, type, esk3_2: $i > $i > $i).
% 0.12/0.28 thf(decl_49, type, esk4_2: $i > $i > $i).
% 0.12/0.28 thf(decl_50, type, esk5_2: $i > $i > $i).
% 0.12/0.28 thf(decl_51, type, esk6_2: $i > $i > $i).
% 0.12/0.28 thf(mimplies, axiom, ((mimplies)=(^[X10:$i > $o, X11:$i > $o]:(mor @ (mnot @ X10) @ X11))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', mimplies)).
% 0.12/0.28 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X5:$i]:(~((X4 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', mnot)).
% 0.12/0.28 thf(mor, axiom, ((mor)=(^[X6:$i > $o, X7:$i > $o, X5:$i]:((((X6 @ X5))|((X7 @ X5)))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', mor)).
% 0.12/0.28 thf(inot, axiom, ((inot)=(^[X12:$i > $o]:(mnot @ (mbox_s4 @ X12)))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', inot)).
% 0.12/0.28 thf(mbox_s4, axiom, ((mbox_s4)=(^[X12:$i > $o, X1:$i]:(![X2:$i]:((((irel @ X1 @ X2))=>((X12 @ X2))))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', mbox_s4)).
% 0.12/0.28 thf(iand, axiom, ((iand)=(^[X12:$i > $o, X14:$i > $o]:(mand @ X12 @ X14))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', iand)).
% 0.12/0.28 thf(mand, axiom, ((mand)=(^[X8:$i > $o, X9:$i > $o, X5:$i]:((((X8 @ X5))&((X9 @ X5)))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', mand)).
% 0.12/0.28 thf(ior, axiom, ((ior)=(^[X12:$i > $o, X14:$i > $o]:(mor @ (mbox_s4 @ X12) @ (mbox_s4 @ X14)))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', ior)).
% 0.12/0.28 thf(iimplies, axiom, ((iimplies)=(^[X12:$i > $o, X14:$i > $o]:(mimplies @ (mbox_s4 @ X12) @ (mbox_s4 @ X14)))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', iimplies)).
% 0.12/0.28 thf(pel9, conjecture, (ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2)))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', pel9)).
% 0.12/0.28 thf(iatom, axiom, ((iatom)=(^[X12:$i > $o]:(X12))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', iatom)).
% 0.12/0.28 thf(ivalid, axiom, ((ivalid)=(^[X15:$i > $o]:(![X13:$i]:((X15 @ X13))))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', ivalid)).
% 0.12/0.28 thf(refl_axiom, axiom, ![X1:$i]:((irel @ X1 @ X1)), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', refl_axiom)).
% 0.12/0.28 thf(trans_axiom, axiom, ![X1:$i, X2:$i, X3:$i]:((((irel @ X1 @ X2)&(irel @ X2 @ X3))=>(irel @ X1 @ X3))), file('/export/starexec/sandbox2/tmp/tmp.SqKfsABsil/E---3.1_927003.p', trans_axiom)).
% 0.12/0.28 thf(c_0_14, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 0.12/0.28 thf(c_0_15, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 0.12/0.28 thf(c_0_16, plain, ((mor)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor])).
% 0.12/0.28 thf(c_0_17, plain, ((inot)=(^[Z0:$i > $o, Z1:$i]:(~((![X20:$i]:((((irel @ Z1 @ X20))=>((Z0 @ X20))))))))), inference(fof_simplification,[status(thm)],[inot])).
% 0.12/0.28 thf(c_0_18, plain, ((mbox_s4)=(^[Z0:$i > $o, Z1:$i]:(![X2:$i]:((((irel @ Z1 @ X2))=>((Z0 @ X2))))))), inference(fof_simplification,[status(thm)],[mbox_s4])).
% 0.12/0.28 thf(c_0_19, plain, ((iand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[iand])).
% 0.12/0.28 thf(c_0_20, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mand])).
% 0.12/0.28 thf(c_0_21, plain, ((ior)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((![X22:$i]:((((irel @ Z2 @ X22))=>((Z0 @ X22))))))|((![X23:$i]:((((irel @ Z2 @ X23))=>((Z1 @ X23)))))))))), inference(fof_simplification,[status(thm)],[ior])).
% 0.12/0.28 thf(c_0_22, plain, ((iimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((![X24:$i]:((((irel @ Z2 @ X24))=>((Z0 @ X24))))))))|((![X25:$i]:((((irel @ Z2 @ X25))=>((Z1 @ X25)))))))))), inference(fof_simplification,[status(thm)],[iimplies])).
% 0.12/0.28 thf(c_0_23, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_14, c_0_15]), c_0_16])).
% 0.12/0.28 thf(c_0_24, negated_conjecture, ~((ivalid @ (iimplies @ (iand @ (ior @ (iatom @ p1) @ (iatom @ p2)) @ (iand @ (ior @ (inot @ (iatom @ p1)) @ (iatom @ p2)) @ (ior @ (iatom @ p1) @ (inot @ (iatom @ p2))))) @ (inot @ (ior @ (inot @ (iatom @ p1)) @ (inot @ (iatom @ p2))))))), inference(assume_negation,[status(cth)],[pel9])).
% 0.12/0.28 thf(c_0_25, plain, ((iatom)=(^[Z0:$i > $o]:(Z0))), inference(fof_simplification,[status(thm)],[iatom])).
% 0.12/0.28 thf(c_0_26, plain, ((inot)=(^[Z0:$i > $o, Z1:$i]:(~((![X20:$i]:((((irel @ Z1 @ X20))=>((Z0 @ X20))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_17, c_0_15]), c_0_18])).
% 0.12/0.28 thf(c_0_27, plain, ((iand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))&((Z1 @ Z2)))))), inference(apply_def,[status(thm)],[c_0_19, c_0_20])).
% 0.12/0.28 thf(c_0_28, plain, ((ior)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((![X22:$i]:((((irel @ Z2 @ X22))=>((Z0 @ X22))))))|((![X23:$i]:((((irel @ Z2 @ X23))=>((Z1 @ X23)))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_21, c_0_16]), c_0_18])).
% 0.12/0.28 thf(c_0_29, plain, ((iimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((![X24:$i]:((((irel @ Z2 @ X24))=>((Z0 @ X24))))))))|((![X25:$i]:((((irel @ Z2 @ X25))=>((Z1 @ X25)))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_22, c_0_23]), c_0_18])).
% 0.12/0.28 thf(c_0_30, plain, ((ivalid)=(^[Z0:$i > $o]:(![X13:$i]:((Z0 @ X13))))), inference(fof_simplification,[status(thm)],[ivalid])).
% 0.12/0.28 thf(c_0_31, plain, ![X50:$i]:(((epred1_1 @ X50)<=>((![X37:$i]:(((irel @ X50 @ X37)=>(p1 @ X37)))|![X38:$i]:(((irel @ X50 @ X38)=>(p2 @ X38))))&((![X40:$i]:(((irel @ X50 @ X40)=>~(![X39:$i]:(((irel @ X40 @ X39)=>(p1 @ X39))))))|![X41:$i]:(((irel @ X50 @ X41)=>(p2 @ X41))))&(![X43:$i]:(((irel @ X50 @ X43)=>(p1 @ X43)))|![X44:$i]:(((irel @ X50 @ X44)=>~(![X42:$i]:(((irel @ X44 @ X42)=>(p2 @ X42))))))))))), introduced(definition)).
% 0.12/0.28 thf(c_0_32, negated_conjecture, ~(![X52:$i]:((~(![X50:$i]:(((irel @ X52 @ X50)=>(epred1_1 @ X50))))|![X51:$i]:(((irel @ X52 @ X51)=>~(![X49:$i]:(((irel @ X51 @ X49)=>(![X47:$i]:(((irel @ X49 @ X47)=>~(![X45:$i]:(((irel @ X47 @ X45)=>(p1 @ X45))))))|![X48:$i]:(((irel @ X49 @ X48)=>~(![X46:$i]:(((irel @ X48 @ X46)=>(p2 @ X46))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_24, c_0_25]), c_0_26]), c_0_27]), c_0_28]), c_0_29]), c_0_30]), c_0_31])).
% 0.12/0.28 thf(c_0_33, negated_conjecture, ![X58:$i, X60:$i, X61:$i, X63:$i]:(((~(irel @ esk1_0 @ X58)|(epred1_1 @ X58))&((irel @ esk1_0 @ esk2_0)&((((irel @ X63 @ (esk4_2 @ X60 @ X63))|~(irel @ X60 @ X63)|((irel @ X61 @ (esk3_2 @ X60 @ X61))|~(irel @ X60 @ X61))|~(irel @ esk2_0 @ X60))&(~(p2 @ (esk4_2 @ X60 @ X63))|~(irel @ X60 @ X63)|((irel @ X61 @ (esk3_2 @ X60 @ X61))|~(irel @ X60 @ X61))|~(irel @ esk2_0 @ X60)))&(((irel @ X63 @ (esk4_2 @ X60 @ X63))|~(irel @ X60 @ X63)|(~(p1 @ (esk3_2 @ X60 @ X61))|~(irel @ X60 @ X61))|~(irel @ esk2_0 @ X60))&(~(p2 @ (esk4_2 @ X60 @ X63))|~(irel @ X60 @ X63)|(~(p1 @ (esk3_2 @ X60 @ X61))|~(irel @ X60 @ X61))|~(irel @ esk2_0 @ X60))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])])])])])).
% 0.12/0.28 thf(c_0_34, plain, ![X53:$i]:((irel @ X53 @ X53)), inference(variable_rename,[status(thm)],[refl_axiom])).
% 0.12/0.28 thf(c_0_35, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((irel @ X1 @ (esk4_2 @ X2 @ X1))|(irel @ X3 @ (esk3_2 @ X2 @ X3))|~((irel @ X2 @ X1))|~((irel @ X2 @ X3))|~((irel @ esk2_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_36, plain, ![X1:$i]:((irel @ X1 @ X1)), inference(split_conjunct,[status(thm)],[c_0_34])).
% 0.12/0.28 thf(c_0_37, plain, ![X50:$i]:(((epred1_1 @ X50)=>((![X37:$i]:(((irel @ X50 @ X37)=>(p1 @ X37)))|![X38:$i]:(((irel @ X50 @ X38)=>(p2 @ X38))))&((![X40:$i]:(((irel @ X50 @ X40)=>~(![X39:$i]:(((irel @ X40 @ X39)=>(p1 @ X39))))))|![X41:$i]:(((irel @ X50 @ X41)=>(p2 @ X41))))&(![X43:$i]:(((irel @ X50 @ X43)=>(p1 @ X43)))|![X44:$i]:(((irel @ X50 @ X44)=>~(![X42:$i]:(((irel @ X44 @ X42)=>(p2 @ X42))))))))))), inference(split_equiv,[status(thm)],[c_0_31])).
% 0.12/0.28 thf(c_0_38, negated_conjecture, ![X1:$i, X2:$i]:(((irel @ X1 @ (esk3_2 @ esk2_0 @ X1))|(irel @ X2 @ (esk4_2 @ esk2_0 @ X2))|~((irel @ esk2_0 @ X1))|~((irel @ esk2_0 @ X2)))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.12/0.28 thf(c_0_39, plain, ![X65:$i, X66:$i, X67:$i, X68:$i, X70:$i, X71:$i, X72:$i]:(((~(irel @ X65 @ X66)|(p1 @ X66)|(~(irel @ X65 @ X67)|(p2 @ X67))|~(epred1_1 @ X65))&((((irel @ X68 @ (esk5_2 @ X65 @ X68))|~(irel @ X65 @ X68)|(~(irel @ X65 @ X70)|(p2 @ X70))|~(epred1_1 @ X65))&(~(p1 @ (esk5_2 @ X65 @ X68))|~(irel @ X65 @ X68)|(~(irel @ X65 @ X70)|(p2 @ X70))|~(epred1_1 @ X65)))&(((irel @ X72 @ (esk6_2 @ X65 @ X72))|~(irel @ X65 @ X72)|(~(irel @ X65 @ X71)|(p1 @ X71))|~(epred1_1 @ X65))&(~(p2 @ (esk6_2 @ X65 @ X72))|~(irel @ X65 @ X72)|(~(irel @ X65 @ X71)|(p1 @ X71))|~(epred1_1 @ X65)))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])])])])).
% 0.12/0.28 thf(c_0_40, negated_conjecture, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(irel @ X1 @ (esk4_2 @ esk2_0 @ X1))|~((irel @ esk2_0 @ X1)))), inference(spm,[status(thm)],[c_0_38, c_0_36])).
% 0.12/0.28 thf(c_0_41, plain, ![X3:$i, X2:$i, X1:$i]:(((p1 @ X2)|(p2 @ X3)|~((irel @ X1 @ X2))|~((irel @ X1 @ X3))|~((epred1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.12/0.28 thf(c_0_42, negated_conjecture, ((irel @ esk2_0 @ (esk4_2 @ esk2_0 @ esk2_0))|(irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_40, c_0_36])).
% 0.12/0.28 thf(c_0_43, plain, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|(p1 @ X1)|~((irel @ esk2_0 @ X1))|~((epred1_1 @ esk2_0)))), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 0.12/0.28 thf(c_0_44, negated_conjecture, ![X1:$i]:(((epred1_1 @ X1)|~((irel @ esk1_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_45, negated_conjecture, (irel @ esk1_0 @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_46, plain, ![X1:$i, X3:$i, X2:$i]:(((irel @ X1 @ (esk5_2 @ X2 @ X1))|(p2 @ X3)|~((irel @ X2 @ X1))|~((irel @ X2 @ X3))|~((epred1_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.12/0.28 thf(c_0_47, negated_conjecture, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|(p1 @ X1)|~((irel @ esk2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_45])])).
% 0.12/0.28 thf(c_0_48, plain, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|(irel @ X1 @ (esk5_2 @ esk2_0 @ X1))|~((irel @ esk2_0 @ X1))|~((epred1_1 @ esk2_0)))), inference(spm,[status(thm)],[c_0_46, c_0_42])).
% 0.12/0.28 thf(c_0_49, plain, ![X3:$i, X2:$i, X1:$i]:(((p2 @ X3)|~((p1 @ (esk5_2 @ X1 @ X2)))|~((irel @ X1 @ X2))|~((irel @ X1 @ X3))|~((epred1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.12/0.28 thf(c_0_50, negated_conjecture, ((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p1 @ (esk5_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|~((epred1_1 @ esk2_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_36])])).
% 0.12/0.28 thf(c_0_51, plain, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|(p2 @ X1)|~((irel @ esk2_0 @ X1))|~((epred1_1 @ esk2_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_50]), c_0_36])])).
% 0.12/0.28 thf(c_0_52, negated_conjecture, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))|(p2 @ X1)|~((irel @ esk2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_44]), c_0_45])])).
% 0.12/0.28 thf(c_0_53, plain, ![X1:$i, X2:$i]:(((p1 @ X1)|(p2 @ X2)|~((irel @ X2 @ X1))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_41, c_0_36])).
% 0.12/0.28 thf(c_0_54, plain, ![X1:$i, X2:$i]:(((irel @ X1 @ (esk5_2 @ X2 @ X1))|(p2 @ X2)|~((irel @ X2 @ X1))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_46, c_0_36])).
% 0.12/0.28 thf(c_0_55, negated_conjecture, ![X3:$i, X2:$i, X1:$i]:(((irel @ X3 @ (esk3_2 @ X1 @ X3))|~((p2 @ (esk4_2 @ X1 @ X2)))|~((irel @ X1 @ X2))|~((irel @ X1 @ X3))|~((irel @ esk2_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_56, negated_conjecture, ((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(p2 @ (esk4_2 @ esk2_0 @ esk2_0))), inference(spm,[status(thm)],[c_0_52, c_0_42])).
% 0.12/0.28 thf(c_0_57, plain, ![X2:$i, X1:$i]:(((p1 @ (esk5_2 @ X1 @ X2))|(p2 @ X1)|(p2 @ X2)|~((irel @ X1 @ X2))|~((epred1_1 @ X2))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 0.12/0.28 thf(c_0_58, plain, ![X54:$i, X55:$i, X56:$i]:((~(irel @ X54 @ X55)|~(irel @ X55 @ X56)|(irel @ X54 @ X56))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[trans_axiom])])])).
% 0.12/0.28 thf(c_0_59, negated_conjecture, ![X1:$i]:(((irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0))|(irel @ X1 @ (esk3_2 @ esk2_0 @ X1))|~((irel @ esk2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_55, c_0_56]), c_0_36])])).
% 0.12/0.28 thf(c_0_60, plain, ![X3:$i, X2:$i, X1:$i]:(((p2 @ X1)|(p2 @ X2)|(p2 @ X3)|~((irel @ X2 @ X3))|~((irel @ X2 @ X1))|~((epred1_1 @ X2))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_49, c_0_57])).
% 0.12/0.28 thf(c_0_61, plain, ![X1:$i, X2:$i, X3:$i]:(((irel @ X1 @ X3)|~((irel @ X1 @ X2))|~((irel @ X2 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.12/0.28 thf(c_0_62, negated_conjecture, (irel @ esk2_0 @ (esk3_2 @ esk2_0 @ esk2_0)), inference(spm,[status(thm)],[c_0_59, c_0_36])).
% 0.12/0.28 thf(c_0_63, plain, ![X1:$i, X2:$i]:(((p2 @ X1)|(p2 @ X2)|~((irel @ X1 @ X2))|~((epred1_1 @ X1))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_60, c_0_36])).
% 0.12/0.28 thf(c_0_64, negated_conjecture, ![X1:$i]:(((irel @ X1 @ (esk3_2 @ esk2_0 @ esk2_0))|~((irel @ X1 @ esk2_0)))), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 0.12/0.28 thf(c_0_65, plain, ![X3:$i, X2:$i, X1:$i]:(((p1 @ X3)|~((p2 @ (esk6_2 @ X1 @ X2)))|~((irel @ X1 @ X2))|~((irel @ X1 @ X3))|~((epred1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.12/0.28 thf(c_0_66, plain, ![X1:$i]:(((p2 @ X1)|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_63, c_0_36])).
% 0.12/0.28 thf(c_0_67, negated_conjecture, ![X1:$i, X2:$i]:(((irel @ X1 @ (esk3_2 @ esk2_0 @ esk2_0))|~((irel @ X2 @ esk2_0))|~((irel @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_61, c_0_64])).
% 0.12/0.28 thf(c_0_68, plain, ![X1:$i, X3:$i, X2:$i]:(((p1 @ X1)|~((epred1_1 @ (esk6_2 @ X2 @ X3)))|~((irel @ X2 @ X1))|~((irel @ X2 @ X3))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 0.12/0.28 thf(c_0_69, plain, ![X1:$i, X3:$i, X2:$i]:(((irel @ X1 @ (esk6_2 @ X2 @ X1))|(p1 @ X3)|~((irel @ X2 @ X1))|~((irel @ X2 @ X3))|~((epred1_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_39])).
% 0.12/0.28 thf(c_0_70, negated_conjecture, ![X1:$i]:(((irel @ X1 @ (esk3_2 @ esk2_0 @ esk2_0))|~((irel @ X1 @ esk1_0)))), inference(spm,[status(thm)],[c_0_67, c_0_45])).
% 0.12/0.28 thf(c_0_71, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((p1 @ X1)|~((irel @ esk1_0 @ (esk6_2 @ X2 @ X3)))|~((irel @ X2 @ X1))|~((irel @ X2 @ X3))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_68, c_0_44])).
% 0.12/0.28 thf(c_0_72, plain, ![X1:$i, X2:$i]:(((p1 @ (esk3_2 @ esk2_0 @ esk2_0))|(irel @ X1 @ (esk6_2 @ X2 @ X1))|~((irel @ X2 @ esk1_0))|~((irel @ X2 @ X1))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 0.12/0.28 thf(c_0_73, negated_conjecture, ![X1:$i, X2:$i]:(((p1 @ (esk3_2 @ esk2_0 @ esk2_0))|(p1 @ X1)|~((irel @ X2 @ esk1_0))|~((irel @ X2 @ X1))|~((epred1_1 @ X2)))), inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 0.12/0.28 thf(c_0_74, negated_conjecture, ![X1:$i]:(((p1 @ (esk3_2 @ esk2_0 @ esk2_0))|~((irel @ X1 @ esk1_0))|~((epred1_1 @ X1)))), inference(spm,[status(thm)],[c_0_73, c_0_70])).
% 0.12/0.28 thf(c_0_75, negated_conjecture, ![X1:$i]:(((p1 @ (esk3_2 @ esk2_0 @ esk2_0))|~((irel @ X1 @ esk1_0))|~((irel @ esk1_0 @ X1)))), inference(spm,[status(thm)],[c_0_74, c_0_44])).
% 0.12/0.28 thf(c_0_76, negated_conjecture, ![X3:$i, X2:$i, X1:$i]:((~((p2 @ (esk4_2 @ X1 @ X2)))|~((irel @ X1 @ X2))|~((p1 @ (esk3_2 @ X1 @ X3)))|~((irel @ X1 @ X3))|~((irel @ esk2_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_77, negated_conjecture, (p1 @ (esk3_2 @ esk2_0 @ esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_36]), c_0_36])])).
% 0.12/0.28 thf(c_0_78, negated_conjecture, ![X1:$i]:((~((p2 @ (esk4_2 @ esk2_0 @ X1)))|~((irel @ esk2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_36])])).
% 0.12/0.28 thf(c_0_79, negated_conjecture, ![X1:$i, X3:$i, X2:$i]:(((irel @ X1 @ (esk4_2 @ X2 @ X1))|~((irel @ X2 @ X1))|~((p1 @ (esk3_2 @ X2 @ X3)))|~((irel @ X2 @ X3))|~((irel @ esk2_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 0.12/0.28 thf(c_0_80, plain, ![X1:$i]:((~((epred1_1 @ (esk4_2 @ esk2_0 @ X1)))|~((irel @ esk2_0 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_66])).
% 0.12/0.28 thf(c_0_81, negated_conjecture, ![X1:$i]:(((irel @ X1 @ (esk4_2 @ esk2_0 @ X1))|~((irel @ esk2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_77]), c_0_36])])).
% 0.12/0.28 thf(c_0_82, negated_conjecture, ![X1:$i]:((~((irel @ esk1_0 @ (esk4_2 @ esk2_0 @ X1)))|~((irel @ esk2_0 @ X1)))), inference(spm,[status(thm)],[c_0_80, c_0_44])).
% 0.12/0.28 thf(c_0_83, negated_conjecture, ![X1:$i, X2:$i]:(((irel @ X1 @ (esk4_2 @ esk2_0 @ X2))|~((irel @ esk2_0 @ X2))|~((irel @ X1 @ X2)))), inference(spm,[status(thm)],[c_0_61, c_0_81])).
% 0.12/0.28 thf(c_0_84, negated_conjecture, ![X1:$i]:((~((irel @ esk2_0 @ X1))|~((irel @ esk1_0 @ X1)))), inference(spm,[status(thm)],[c_0_82, c_0_83])).
% 0.12/0.28 thf(c_0_85, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_70]), c_0_62]), c_0_36])]), ['proof']).
% 0.12/0.28 % SZS output end CNFRefutation
% 0.12/0.28 % Parsed axioms : 44
% 0.12/0.28 % Removed by relevancy pruning/SinE : 0
% 0.12/0.28 % Initial clauses : 35
% 0.12/0.28 % Removed in clause preprocessing : 22
% 0.12/0.28 % Initial clauses in saturation : 13
% 0.12/0.28 % Processed clauses : 162
% 0.12/0.28 % ...of these trivial : 4
% 0.12/0.28 % ...subsumed : 27
% 0.12/0.28 % ...remaining for further processing : 131
% 0.12/0.28 % Other redundant clauses eliminated : 0
% 0.12/0.28 % Clauses deleted for lack of memory : 0
% 0.12/0.28 % Backward-subsumed : 64
% 0.12/0.28 % Backward-rewritten : 26
% 0.12/0.28 % Generated clauses : 471
% 0.12/0.28 % ...of the previous two non-redundant : 440
% 0.12/0.28 % ...aggressively subsumed : 0
% 0.12/0.28 % Contextual simplify-reflections : 1
% 0.12/0.28 % Paramodulations : 471
% 0.12/0.28 % Factorizations : 0
% 0.12/0.28 % NegExts : 0
% 0.12/0.28 % Equation resolutions : 0
% 0.12/0.28 % Disequality decompositions : 0
% 0.12/0.28 % Total rewrite steps : 143
% 0.12/0.28 % ...of those cached : 135
% 0.12/0.28 % Propositional unsat checks : 0
% 0.12/0.28 % Propositional check models : 0
% 0.12/0.28 % Propositional check unsatisfiable : 0
% 0.12/0.28 % Propositional clauses : 0
% 0.12/0.28 % Propositional clauses after purity: 0
% 0.12/0.28 % Propositional unsat core size : 0
% 0.12/0.28 % Propositional preprocessing time : 0.000
% 0.12/0.28 % Propositional encoding time : 0.000
% 0.12/0.28 % Propositional solver time : 0.000
% 0.12/0.28 % Success case prop preproc time : 0.000
% 0.12/0.28 % Success case prop encoding time : 0.000
% 0.12/0.28 % Success case prop solver time : 0.000
% 0.12/0.28 % Current number of processed clauses : 41
% 0.12/0.28 % Positive orientable unit clauses : 7
% 0.12/0.28 % Positive unorientable unit clauses: 0
% 0.12/0.28 % Negative unit clauses : 1
% 0.12/0.28 % Non-unit-clauses : 33
% 0.12/0.28 % Current number of unprocessed clauses: 66
% 0.12/0.28 % ...number of literals in the above : 360
% 0.12/0.28 % Current number of archived formulas : 0
% 0.12/0.28 % Current number of archived clauses : 90
% 0.12/0.28 % Clause-clause subsumption calls (NU) : 1754
% 0.12/0.28 % Rec. Clause-clause subsumption calls : 750
% 0.12/0.28 % Non-unit clause-clause subsumptions : 87
% 0.12/0.28 % Unit Clause-clause subsumption calls : 40
% 0.12/0.28 % Rewrite failures with RHS unbound : 0
% 0.12/0.28 % BW rewrite match attempts : 6
% 0.12/0.28 % BW rewrite match successes : 5
% 0.12/0.28 % Condensation attempts : 0
% 0.12/0.28 % Condensation successes : 0
% 0.12/0.28 % Termbank termtop insertions : 12797
% 0.12/0.28 % Search garbage collected termcells : 1068
% 0.12/0.28
% 0.12/0.28 % -------------------------------------------------
% 0.12/0.28 % User time : 0.024 s
% 0.12/0.28 % System time : 0.003 s
% 0.12/0.28 % Total time : 0.026 s
% 0.12/0.28 % Maximum resident set size: 3664 pages
% 0.12/0.28
% 0.12/0.28 % -------------------------------------------------
% 0.12/0.28 % User time : 0.026 s
% 0.12/0.28 % System time : 0.007 s
% 0.12/0.28 % Total time : 0.033 s
% 0.12/0.28 % Maximum resident set size: 4864 pages
% 0.12/0.28 % E exiting
%------------------------------------------------------------------------------