%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SET575^7 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/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:21:57 AM UTC 2026
% Result : Theorem 0.22s 0.33s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET575^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n006.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 13:37:24 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p
% 0.22/0.33 % Version: 3.5.1-ho
% 0.22/0.33 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.33 % Starting post_as_ho3 with 300s (1) cores
% 0.22/0.33 % Starting new_ho_12 with 300s (1) cores
% 0.22/0.33 % Starting new_bool_2 with 300s (1) cores
% 0.22/0.33 % new_bool_2 with pid 718343 completed with status 0
% 0.22/0.33 % Result found by new_bool_2
% 0.22/0.33 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.33 % Starting post_as_ho3 with 300s (1) cores
% 0.22/0.33 % Starting new_ho_12 with 300s (1) cores
% 0.22/0.33 % Starting new_bool_2 with 300s (1) cores
% 0.22/0.33 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.22/0.33 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.22/0.33 % Search class: HGHNF-FFMS33-SHSSMFNN
% 0.22/0.33 % partial match(2): HGHNF-FFMS11-SHSSMFNN
% 0.22/0.33 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.33 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.33 % SubtermCWHack with pid 718345 completed with status 0
% 0.22/0.33 % Result found by SubtermCWHack
% 0.22/0.33 % Preprocessing class: HSMSSMSSMLLNHSN.
% 0.22/0.33 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.22/0.33 % Starting new_ho_10_cnf2 with 1500s (5) cores
% 0.22/0.33 % Starting post_as_ho3 with 300s (1) cores
% 0.22/0.33 % Starting new_ho_12 with 300s (1) cores
% 0.22/0.33 % Starting new_bool_2 with 300s (1) cores
% 0.22/0.33 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.22/0.33 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.22/0.33 % Search class: HGHNF-FFMS33-SHSSMFNN
% 0.22/0.33 % partial match(2): HGHNF-FFMS11-SHSSMFNN
% 0.22/0.33 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.22/0.33 % Starting SubtermCWHack with 28s (1) cores
% 0.22/0.33 % Preprocessing time : 0.001 s
% 0.22/0.33
% 0.22/0.33 % Proof found!
% 0.22/0.33 % SZS status Theorem
% 0.22/0.33 % SZS output start CNFRefutation
% 0.22/0.33 thf(decl_sort1, type, mu: $tType).
% 0.22/0.33 thf(decl_25, type, mnot: ($i > $o) > $i > $o).
% 0.22/0.33 thf(decl_26, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 0.22/0.33 thf(decl_31, type, mand: ($i > $o) > ($i > $o) > $i > $o).
% 0.22/0.33 thf(decl_32, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.22/0.33 thf(decl_37, type, exists_in_world: mu > $i > $o).
% 0.22/0.33 thf(decl_38, type, mforall_ind: (mu > $i > $o) > $i > $o).
% 0.22/0.33 thf(decl_39, type, mexists_ind: (mu > $i > $o) > $i > $o).
% 0.22/0.33 thf(decl_51, type, mvalid: ($i > $o) > $o).
% 0.22/0.33 thf(decl_55, type, rel_s4: $i > $i > $o).
% 0.22/0.33 thf(decl_56, type, mbox_s4: ($i > $o) > $i > $o).
% 0.22/0.33 thf(decl_58, type, member: mu > mu > $i > $o).
% 0.22/0.33 thf(decl_59, type, intersect: mu > mu > $i > $o).
% 0.22/0.33 thf(decl_60, type, epred1_3: mu > $i > mu > $o).
% 0.22/0.33 thf(decl_61, type, esk1_0: $i).
% 0.22/0.33 thf(decl_62, type, esk2_0: $i).
% 0.22/0.33 thf(decl_63, type, esk3_0: mu).
% 0.22/0.33 thf(decl_64, type, esk4_0: $i).
% 0.22/0.33 thf(decl_65, type, esk5_0: mu).
% 0.22/0.33 thf(decl_66, type, esk6_0: $i).
% 0.22/0.33 thf(decl_67, type, esk7_1: mu > $i).
% 0.22/0.33 thf(decl_68, type, esk8_1: mu > $i).
% 0.22/0.33 thf(decl_71, type, esk11_4: mu > $i > mu > $i > $i).
% 0.22/0.33 thf(decl_72, type, esk12_4: mu > $i > mu > $i > mu).
% 0.22/0.33 thf(decl_73, type, esk13_5: mu > $i > mu > $i > mu > $i).
% 0.22/0.33 thf(decl_74, type, esk14_5: mu > $i > mu > $i > mu > $i).
% 0.22/0.33 thf(mand, axiom, ((mand)=(^[X4:$i > $o, X5:$i > $o]:(mnot @ (mor @ (mnot @ X4) @ (mnot @ X5))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mand)).
% 0.22/0.33 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X3:$i]:(~((X4 @ X3))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mnot)).
% 0.22/0.33 thf(mor, axiom, ((mor)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))|((X5 @ X3)))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mor)).
% 0.22/0.33 thf(mexists_ind, axiom, ((mexists_ind)=(^[X13:mu > $i > $o]:(mnot @ (mforall_ind @ (^[X14:mu]:(mnot @ (X13 @ X14))))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mexists_ind)).
% 0.22/0.33 thf(mforall_ind, axiom, ((mforall_ind)=(^[X11:mu > $i > $o, X3:$i]:(![X12:mu]:((((exists_in_world @ X12 @ X3))=>((X11 @ X12 @ X3))))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mforall_ind)).
% 0.22/0.33 thf(mimplies, axiom, ((mimplies)=(^[X4:$i > $o, X5:$i > $o]:(mor @ (mnot @ X4) @ X5))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mimplies)).
% 0.22/0.33 thf(mbox_s4, axiom, ((mbox_s4)=(^[X4:$i > $o, X3:$i]:(![X7:$i]:(((~((rel_s4 @ X3 @ X7)))|((X4 @ X7))))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mbox_s4)).
% 0.22/0.33 thf(mvalid, axiom, ((mvalid)=(^[X4:$i > $o]:(![X3:$i]:((X4 @ X3))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', mvalid)).
% 0.22/0.33 thf(prove_th15, conjecture, (mvalid @ (mbox_s4 @ (mforall_ind @ (^[X20:mu]:(mbox_s4 @ (mforall_ind @ (^[X21:mu]:(mbox_s4 @ (mimplies @ (mbox_s4 @ (intersect @ X20 @ X21)) @ (mexists_ind @ (^[X22:mu]:(mand @ (mbox_s4 @ (member @ X22 @ X20)) @ (mbox_s4 @ (member @ X22 @ X21)))))))))))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', prove_th15)).
% 0.22/0.33 thf(intersect_defn, axiom, (mvalid @ (mbox_s4 @ (mforall_ind @ (^[X20:mu]:(mbox_s4 @ (mforall_ind @ (^[X21:mu]:(mand @ (mbox_s4 @ (mimplies @ (mbox_s4 @ (intersect @ X20 @ X21)) @ (mexists_ind @ (^[X22:mu]:(mand @ (mbox_s4 @ (member @ X22 @ X20)) @ (mbox_s4 @ (member @ X22 @ X21))))))) @ (mbox_s4 @ (mimplies @ (mexists_ind @ (^[X22:mu]:(mand @ (mbox_s4 @ (member @ X22 @ X20)) @ (mbox_s4 @ (member @ X22 @ X21))))) @ (mbox_s4 @ (intersect @ X20 @ X21)))))))))))), file('/export/starexec/sandbox/tmp/tmp.z7X53Xul76/E---3.1_718327.p', intersect_defn)).
% 0.22/0.33 thf(c_0_10, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~((Z0 @ Z2))))|((~((Z1 @ Z2)))))))))), inference(fof_simplification,[status(thm)],[mand])).
% 0.22/0.33 thf(c_0_11, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 0.22/0.33 thf(c_0_12, plain, ((mor)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor])).
% 0.22/0.33 thf(c_0_13, plain, ((mexists_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X28:mu]:((((exists_in_world @ X28 @ Z1))=>((~((Z0 @ X28 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[mexists_ind])).
% 0.22/0.33 thf(c_0_14, plain, ((mforall_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(![X12:mu]:((((exists_in_world @ X12 @ Z1))=>((Z0 @ X12 @ Z1))))))), inference(fof_simplification,[status(thm)],[mforall_ind])).
% 0.22/0.33 thf(c_0_15, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 0.22/0.33 thf(c_0_16, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~((Z0 @ Z2))))|((~((Z1 @ Z2)))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_10, c_0_11]), c_0_12])).
% 0.22/0.33 thf(c_0_17, plain, ((mexists_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X28:mu]:((((exists_in_world @ X28 @ Z1))=>((~((Z0 @ X28 @ Z1))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_13, c_0_14]), c_0_11])).
% 0.22/0.33 thf(c_0_18, 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_15, c_0_11]), c_0_12])).
% 0.22/0.33 thf(c_0_19, plain, ((mbox_s4)=(^[Z0:$i > $o, Z1:$i]:(![X7:$i]:(((~((rel_s4 @ Z1 @ X7)))|((Z0 @ X7))))))), inference(fof_simplification,[status(thm)],[mbox_s4])).
% 0.22/0.33 thf(c_0_20, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 0.22/0.33 thf(c_0_21, plain, ![X59:mu, X58:$i, X57:mu]:(((epred1_3 @ X57 @ X58 @ X59)<=>~((~(![X51:$i]:((~(rel_s4 @ X58 @ X51)|(~(![X47:$i]:((~(rel_s4 @ X51 @ X47)|(intersect @ X59 @ X57 @ X47))))|~(![X50:mu]:(((exists_in_world @ X50 @ X51)=>~(~((~(![X48:$i]:((~(rel_s4 @ X51 @ X48)|(member @ X50 @ X59 @ X48))))|~(![X49:$i]:((~(rel_s4 @ X51 @ X49)|(member @ X50 @ X57 @ X49))))))))))))))|~(![X56:$i]:((~(rel_s4 @ X58 @ X56)|(~(~(![X54:mu]:(((exists_in_world @ X54 @ X56)=>~(~((~(![X52:$i]:((~(rel_s4 @ X56 @ X52)|(member @ X54 @ X59 @ X52))))|~(![X53:$i]:((~(rel_s4 @ X56 @ X53)|(member @ X54 @ X57 @ X53)))))))))))|![X55:$i]:((~(rel_s4 @ X56 @ X55)|(intersect @ X59 @ X57 @ X55))))))))))), introduced(definition)).
% 0.22/0.33 thf(c_0_22, negated_conjecture, ~((mvalid @ (mbox_s4 @ (mforall_ind @ (^[X20:mu]:(mbox_s4 @ (mforall_ind @ (^[X21:mu]:(mbox_s4 @ (mimplies @ (mbox_s4 @ (intersect @ X20 @ X21)) @ (mexists_ind @ (^[X22:mu]:(mand @ (mbox_s4 @ (member @ X22 @ X20)) @ (mbox_s4 @ (member @ X22 @ X21))))))))))))))), inference(assume_negation,[status(cth)],[prove_th15])).
% 0.22/0.33 thf(c_0_23, plain, ![X61:$i, X60:$i]:((~(rel_s4 @ X61 @ X60)|![X59:mu]:(((exists_in_world @ X59 @ X60)=>![X58:$i]:((~(rel_s4 @ X60 @ X58)|![X57:mu]:(((exists_in_world @ X57 @ X58)=>(epred1_3 @ X57 @ X58 @ X59))))))))), inference(apply_def,[status(thm)],[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)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[intersect_defn]), c_0_14]), c_0_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20])]), c_0_21])).
% 0.22/0.33 thf(c_0_24, negated_conjecture, ~(![X38:$i, X37:$i]:((~(rel_s4 @ X38 @ X37)|![X36:mu]:(((exists_in_world @ X36 @ X37)=>![X35:$i]:((~(rel_s4 @ X37 @ X35)|![X34:mu]:(((exists_in_world @ X34 @ X35)=>![X33:$i]:((~(rel_s4 @ X35 @ X33)|(~(![X29:$i]:((~(rel_s4 @ X33 @ X29)|(intersect @ X36 @ X34 @ X29))))|~(![X32:mu]:(((exists_in_world @ X32 @ X33)=>~(~((~(![X30:$i]:((~(rel_s4 @ X33 @ X30)|(member @ X32 @ X36 @ X30))))|~(![X31:$i]:((~(rel_s4 @ X33 @ X31)|(member @ X32 @ X34 @ X31)))))))))))))))))))))), 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)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_22]), c_0_14]), c_0_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20])])).
% 0.22/0.33 thf(c_0_25, plain, ![X80:$i, X81:$i, X82:mu, X83:$i, X84:mu]:((~(rel_s4 @ X80 @ X81)|(~(exists_in_world @ X82 @ X81)|(~(rel_s4 @ X81 @ X83)|(~(exists_in_world @ X84 @ X83)|(epred1_3 @ X84 @ X83 @ X82)))))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_23])])])).
% 0.22/0.33 thf(c_0_26, negated_conjecture, ![X68:$i, X69:mu]:(((rel_s4 @ esk1_0 @ esk2_0)&((exists_in_world @ esk3_0 @ esk2_0)&((rel_s4 @ esk2_0 @ esk4_0)&((exists_in_world @ esk5_0 @ esk4_0)&((rel_s4 @ esk4_0 @ esk6_0)&((~(rel_s4 @ esk6_0 @ X68)|(intersect @ esk3_0 @ esk5_0 @ X68))&((((rel_s4 @ esk6_0 @ (esk8_1 @ X69))|(rel_s4 @ esk6_0 @ (esk7_1 @ X69))|~(exists_in_world @ X69 @ esk6_0))&(~(member @ X69 @ esk5_0 @ (esk8_1 @ X69))|(rel_s4 @ esk6_0 @ (esk7_1 @ X69))|~(exists_in_world @ X69 @ esk6_0)))&(((rel_s4 @ esk6_0 @ (esk8_1 @ X69))|~(member @ X69 @ esk3_0 @ (esk7_1 @ X69))|~(exists_in_world @ X69 @ esk6_0))&(~(member @ X69 @ esk5_0 @ (esk8_1 @ X69))|~(member @ X69 @ esk3_0 @ (esk7_1 @ X69))|~(exists_in_world @ X69 @ esk6_0))))))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])])])])).
% 0.22/0.33 thf(c_0_27, plain, ![X59:mu, X58:$i, X57:mu]:(((epred1_3 @ X57 @ X58 @ X59)=>~((~(![X51:$i]:((~(rel_s4 @ X58 @ X51)|(~(![X47:$i]:((~(rel_s4 @ X51 @ X47)|(intersect @ X59 @ X57 @ X47))))|~(![X50:mu]:(((exists_in_world @ X50 @ X51)=>~(~((~(![X48:$i]:((~(rel_s4 @ X51 @ X48)|(member @ X50 @ X59 @ X48))))|~(![X49:$i]:((~(rel_s4 @ X51 @ X49)|(member @ X50 @ X57 @ X49))))))))))))))|~(![X56:$i]:((~(rel_s4 @ X58 @ X56)|(~(~(![X54:mu]:(((exists_in_world @ X54 @ X56)=>~(~((~(![X52:$i]:((~(rel_s4 @ X56 @ X52)|(member @ X54 @ X59 @ X52))))|~(![X53:$i]:((~(rel_s4 @ X56 @ X53)|(member @ X54 @ X57 @ X53)))))))))))|![X55:$i]:((~(rel_s4 @ X56 @ X55)|(intersect @ X59 @ X57 @ X55))))))))))), inference(split_equiv,[status(thm)],[c_0_21])).
% 0.22/0.33 thf(c_0_28, plain, ![X3:$i, X7:$i, X10:mu, X12:mu, X16:$i]:(((epred1_3 @ X12 @ X16 @ X10)|~((rel_s4 @ X3 @ X7))|~((exists_in_world @ X10 @ X7))|~((rel_s4 @ X7 @ X16))|~((exists_in_world @ X12 @ X16)))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.22/0.33 thf(c_0_29, negated_conjecture, (rel_s4 @ esk2_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_30, plain, ![X90:mu, X91:$i, X92:mu, X93:$i, X96:$i, X97:$i, X98:$i, X99:mu, X102:$i]:((((((exists_in_world @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X93)|(rel_s4 @ X93 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90))&((~(rel_s4 @ X93 @ X96)|(member @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X90 @ X96)|(rel_s4 @ X93 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90))&(~(rel_s4 @ X93 @ X97)|(member @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X92 @ X97)|(rel_s4 @ X93 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90))))&(((exists_in_world @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X93)|~(intersect @ X90 @ X92 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90))&((~(rel_s4 @ X93 @ X96)|(member @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X90 @ X96)|~(intersect @ X90 @ X92 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90))&(~(rel_s4 @ X93 @ X97)|(member @ (esk12_4 @ X90 @ X91 @ X92 @ X93) @ X92 @ X97)|~(intersect @ X90 @ X92 @ (esk11_4 @ X90 @ X91 @ X92 @ X93))|~(rel_s4 @ X91 @ X93)|~(epred1_3 @ X92 @ X91 @ X90)))))&((((rel_s4 @ X98 @ (esk14_5 @ X90 @ X91 @ X92 @ X98 @ X99))|(rel_s4 @ X98 @ (esk13_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(exists_in_world @ X99 @ X98)|(~(rel_s4 @ X98 @ X102)|(intersect @ X90 @ X92 @ X102))|~(rel_s4 @ X91 @ X98)|~(epred1_3 @ X92 @ X91 @ X90))&(~(member @ X99 @ X92 @ (esk14_5 @ X90 @ X91 @ X92 @ X98 @ X99))|(rel_s4 @ X98 @ (esk13_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(exists_in_world @ X99 @ X98)|(~(rel_s4 @ X98 @ X102)|(intersect @ X90 @ X92 @ X102))|~(rel_s4 @ X91 @ X98)|~(epred1_3 @ X92 @ X91 @ X90)))&(((rel_s4 @ X98 @ (esk14_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(member @ X99 @ X90 @ (esk13_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(exists_in_world @ X99 @ X98)|(~(rel_s4 @ X98 @ X102)|(intersect @ X90 @ X92 @ X102))|~(rel_s4 @ X91 @ X98)|~(epred1_3 @ X92 @ X91 @ X90))&(~(member @ X99 @ X92 @ (esk14_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(member @ X99 @ X90 @ (esk13_5 @ X90 @ X91 @ X92 @ X98 @ X99))|~(exists_in_world @ X99 @ X98)|(~(rel_s4 @ X98 @ X102)|(intersect @ X90 @ X92 @ X102))|~(rel_s4 @ X91 @ X98)|~(epred1_3 @ X92 @ X91 @ X90)))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_27])])])])])).
% 0.22/0.33 thf(c_0_31, negated_conjecture, ![X3:$i, X10:mu, X12:mu]:(((epred1_3 @ X10 @ esk4_0 @ X12)|~((rel_s4 @ X3 @ esk2_0))|~((exists_in_world @ X10 @ esk4_0))|~((exists_in_world @ X12 @ esk2_0)))), inference(spm,[status(thm)],[c_0_28, c_0_29])).
% 0.22/0.33 thf(c_0_32, negated_conjecture, (rel_s4 @ esk1_0 @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_33, plain, ![X7:$i, X3:$i, X16:$i, X12:mu, X10:mu]:(((member @ (esk12_4 @ X10 @ X16 @ X12 @ X3) @ X10 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ X16 @ X12 @ X3))|~((rel_s4 @ X3 @ X7))|~((rel_s4 @ X16 @ X3))|~((epred1_3 @ X12 @ X16 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_34, negated_conjecture, ![X10:mu, X12:mu]:(((epred1_3 @ X10 @ esk4_0 @ X12)|~((exists_in_world @ X10 @ esk4_0))|~((exists_in_world @ X12 @ esk2_0)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 0.22/0.33 thf(c_0_35, negated_conjecture, ![X3:$i, X12:mu, X10:mu, X7:$i]:(((member @ (esk12_4 @ X10 @ esk4_0 @ X12 @ X3) @ X10 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ esk4_0 @ X12 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((exists_in_world @ X12 @ esk4_0))|~((exists_in_world @ X10 @ esk2_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 0.22/0.33 thf(c_0_36, negated_conjecture, (exists_in_world @ esk5_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_37, plain, ![X7:$i, X3:$i, X16:$i, X12:mu, X10:mu]:(((member @ (esk12_4 @ X10 @ X16 @ X12 @ X3) @ X12 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ X16 @ X12 @ X3))|~((rel_s4 @ X3 @ X7))|~((rel_s4 @ X16 @ X3))|~((epred1_3 @ X12 @ X16 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_38, plain, ![X7:$i, X3:$i, X16:$i, X12:mu, X10:mu]:(((member @ (esk12_4 @ X10 @ X16 @ X12 @ X3) @ X12 @ X7)|~((rel_s4 @ X3 @ X7))|~((intersect @ X10 @ X12 @ (esk11_4 @ X10 @ X16 @ X12 @ X3)))|~((rel_s4 @ X16 @ X3))|~((epred1_3 @ X12 @ X16 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_39, negated_conjecture, ![X3:$i]:(((intersect @ esk3_0 @ esk5_0 @ X3)|~((rel_s4 @ esk6_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_40, negated_conjecture, ![X3:$i, X10:mu, X7:$i]:(((member @ (esk12_4 @ X10 @ esk4_0 @ esk5_0 @ X3) @ X10 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ esk4_0 @ esk5_0 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((exists_in_world @ X10 @ esk2_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.22/0.33 thf(c_0_41, negated_conjecture, (exists_in_world @ esk3_0 @ esk2_0), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_42, negated_conjecture, ![X3:$i, X12:mu, X10:mu, X7:$i]:(((member @ (esk12_4 @ X10 @ esk4_0 @ X12 @ X3) @ X12 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ esk4_0 @ X12 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((exists_in_world @ X12 @ esk4_0))|~((exists_in_world @ X10 @ esk2_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_37, c_0_34])).
% 0.22/0.33 thf(c_0_43, plain, ![X7:$i, X3:$i, X16:$i, X12:mu, X10:mu]:(((member @ (esk12_4 @ X10 @ X16 @ X12 @ X3) @ X10 @ X7)|~((rel_s4 @ X3 @ X7))|~((intersect @ X10 @ X12 @ (esk11_4 @ X10 @ X16 @ X12 @ X3)))|~((rel_s4 @ X16 @ X3))|~((epred1_3 @ X12 @ X16 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_44, negated_conjecture, ![X10:mu]:(((rel_s4 @ esk6_0 @ (esk7_1 @ X10))|~((member @ X10 @ esk5_0 @ (esk8_1 @ X10)))|~((exists_in_world @ X10 @ esk6_0)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_45, negated_conjecture, ![X3:$i, X7:$i, X16:$i]:(((member @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk5_0 @ X16)|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7))|~((rel_s4 @ X7 @ X16)))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 0.22/0.33 thf(c_0_46, plain, ![X3:$i, X7:$i, X12:mu, X10:mu]:(((exists_in_world @ (esk12_4 @ X10 @ X3 @ X12 @ X7) @ X7)|~((intersect @ X10 @ X12 @ (esk11_4 @ X10 @ X3 @ X12 @ X7)))|~((rel_s4 @ X3 @ X7))|~((epred1_3 @ X12 @ X3 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_47, negated_conjecture, ![X3:$i, X7:$i]:(((member @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ X3) @ esk3_0 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 0.22/0.33 thf(c_0_48, negated_conjecture, (rel_s4 @ esk4_0 @ esk6_0), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_49, negated_conjecture, ![X3:$i, X10:mu, X7:$i]:(((member @ (esk12_4 @ X10 @ esk4_0 @ esk5_0 @ X3) @ esk5_0 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ X10 @ esk4_0 @ esk5_0 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((exists_in_world @ X10 @ esk2_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_42, c_0_36])).
% 0.22/0.33 thf(c_0_50, negated_conjecture, ![X10:mu]:((~((member @ X10 @ esk5_0 @ (esk8_1 @ X10)))|~((member @ X10 @ esk3_0 @ (esk7_1 @ X10)))|~((exists_in_world @ X10 @ esk6_0)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_51, negated_conjecture, ![X3:$i, X7:$i, X16:$i]:(((member @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk3_0 @ X16)|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7))|~((rel_s4 @ X7 @ X16)))), inference(spm,[status(thm)],[c_0_43, c_0_39])).
% 0.22/0.33 thf(c_0_52, negated_conjecture, ![X10:mu]:(((rel_s4 @ esk6_0 @ (esk8_1 @ X10))|~((member @ X10 @ esk3_0 @ (esk7_1 @ X10)))|~((exists_in_world @ X10 @ esk6_0)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_53, negated_conjecture, ![X3:$i, X7:$i]:(((rel_s4 @ esk6_0 @ (esk7_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((rel_s4 @ X7 @ (esk8_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7))))|~((exists_in_world @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk6_0))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_44, c_0_45])).
% 0.22/0.33 thf(c_0_54, negated_conjecture, ![X10:mu]:(((rel_s4 @ esk6_0 @ (esk8_1 @ X10))|(rel_s4 @ esk6_0 @ (esk7_1 @ X10))|~((exists_in_world @ X10 @ esk6_0)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.22/0.33 thf(c_0_55, negated_conjecture, ![X3:$i, X7:$i]:(((exists_in_world @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ X7)|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_46, c_0_39])).
% 0.22/0.33 thf(c_0_56, negated_conjecture, ![X3:$i]:(((member @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk3_0 @ X3)|(rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((rel_s4 @ esk6_0 @ X3)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.22/0.33 thf(c_0_57, negated_conjecture, ![X3:$i, X7:$i]:(((member @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ X3) @ esk5_0 @ X7)|(rel_s4 @ X3 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ X3))|~((rel_s4 @ esk4_0 @ X3))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_49, c_0_41])).
% 0.22/0.33 thf(c_0_58, negated_conjecture, ![X3:$i, X7:$i]:((~((member @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk5_0 @ (esk8_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7))))|~((rel_s4 @ X7 @ (esk7_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7))))|~((exists_in_world @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk6_0))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 0.22/0.33 thf(c_0_59, negated_conjecture, ![X3:$i, X7:$i]:(((rel_s4 @ esk6_0 @ (esk8_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((rel_s4 @ X7 @ (esk7_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7))))|~((exists_in_world @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ X7) @ esk6_0))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ X7)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ X7)))), inference(spm,[status(thm)],[c_0_52, c_0_51])).
% 0.22/0.33 thf(c_0_60, negated_conjecture, ![X3:$i]:(((rel_s4 @ esk6_0 @ (esk7_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ esk6_0)))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ esk6_0)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ esk6_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_55])).
% 0.22/0.33 thf(c_0_61, negated_conjecture, ((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((member @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk5_0 @ (esk8_1 @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))))|~((exists_in_world @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk6_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_56]), c_0_44])).
% 0.22/0.33 thf(c_0_62, negated_conjecture, ![X3:$i]:(((member @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk5_0 @ X3)|(rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((rel_s4 @ esk6_0 @ X3)))), inference(spm,[status(thm)],[c_0_57, c_0_48])).
% 0.22/0.33 thf(c_0_63, negated_conjecture, ((rel_s4 @ esk6_0 @ (esk8_1 @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0)))|(rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((exists_in_world @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk6_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_56]), c_0_54])).
% 0.22/0.33 thf(c_0_64, negated_conjecture, ![X7:$i, X3:$i]:((~((rel_s4 @ X3 @ (esk7_1 @ (esk12_4 @ esk3_0 @ X7 @ esk5_0 @ X3))))|~((rel_s4 @ X3 @ (esk8_1 @ (esk12_4 @ esk3_0 @ X7 @ esk5_0 @ X3))))|~((exists_in_world @ (esk12_4 @ esk3_0 @ X7 @ esk5_0 @ X3) @ esk6_0))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X7 @ esk5_0 @ X3)))|~((epred1_3 @ esk5_0 @ X7 @ esk3_0))|~((rel_s4 @ X7 @ X3)))), inference(spm,[status(thm)],[c_0_58, c_0_45])).
% 0.22/0.33 thf(c_0_65, negated_conjecture, ![X3:$i]:(((rel_s4 @ esk6_0 @ (esk8_1 @ (esk12_4 @ esk3_0 @ X3 @ esk5_0 @ esk6_0)))|~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ esk6_0)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ esk6_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_55])).
% 0.22/0.33 thf(c_0_66, negated_conjecture, ((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((exists_in_world @ (esk12_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0) @ esk6_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63])).
% 0.22/0.33 thf(c_0_67, plain, ![X3:$i, X7:$i, X12:mu, X10:mu]:(((exists_in_world @ (esk12_4 @ X10 @ X3 @ X12 @ X7) @ X7)|(rel_s4 @ X7 @ (esk11_4 @ X10 @ X3 @ X12 @ X7))|~((rel_s4 @ X3 @ X7))|~((epred1_3 @ X12 @ X3 @ X10)))), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.33 thf(c_0_68, negated_conjecture, ![X3:$i]:((~((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ X3 @ esk5_0 @ esk6_0)))|~((epred1_3 @ esk5_0 @ X3 @ esk3_0))|~((rel_s4 @ X3 @ esk6_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_65]), c_0_55]), c_0_60])).
% 0.22/0.33 thf(c_0_69, plain, ((rel_s4 @ esk6_0 @ (esk11_4 @ esk3_0 @ esk4_0 @ esk5_0 @ esk6_0))|~((epred1_3 @ esk5_0 @ esk4_0 @ esk3_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_48])])).
% 0.22/0.33 thf(c_0_70, plain, ~((epred1_3 @ esk5_0 @ esk4_0 @ esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_48])])).
% 0.22/0.33 thf(c_0_71, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_34]), c_0_36]), c_0_41])]), ['proof']).
% 0.22/0.33 % SZS output end CNFRefutation
% 0.22/0.33 % Parsed axioms : 77
% 0.22/0.33 % Removed by relevancy pruning/SinE : 64
% 0.22/0.33 % Initial clauses : 25
% 0.22/0.33 % Removed in clause preprocessing : 0
% 0.22/0.33 % Initial clauses in saturation : 25
% 0.22/0.33 % Processed clauses : 581
% 0.22/0.33 % ...of these trivial : 0
% 0.22/0.33 % ...subsumed : 11
% 0.22/0.33 % ...remaining for further processing : 570
% 0.22/0.33 % Other redundant clauses eliminated : 0
% 0.22/0.33 % Clauses deleted for lack of memory : 0
% 0.22/0.33 % Backward-subsumed : 39
% 0.22/0.33 % Backward-rewritten : 0
% 0.22/0.33 % Generated clauses : 2230
% 0.22/0.33 % ...of the previous two non-redundant : 2223
% 0.22/0.33 % ...aggressively subsumed : 0
% 0.22/0.33 % Contextual simplify-reflections : 17
% 0.22/0.33 % Paramodulations : 2230
% 0.22/0.33 % Factorizations : 0
% 0.22/0.33 % NegExts : 0
% 0.22/0.33 % Equation resolutions : 0
% 0.22/0.33 % Disequality decompositions : 0
% 0.22/0.33 % Total rewrite steps : 112
% 0.22/0.33 % ...of those cached : 106
% 0.22/0.33 % Propositional unsat checks : 0
% 0.22/0.33 % Propositional check models : 0
% 0.22/0.33 % Propositional check unsatisfiable : 0
% 0.22/0.33 % Propositional clauses : 0
% 0.22/0.33 % Propositional clauses after purity: 0
% 0.22/0.33 % Propositional unsat core size : 0
% 0.22/0.33 % Propositional preprocessing time : 0.000
% 0.22/0.33 % Propositional encoding time : 0.000
% 0.22/0.33 % Propositional solver time : 0.000
% 0.22/0.33 % Success case prop preproc time : 0.000
% 0.22/0.33 % Success case prop encoding time : 0.000
% 0.22/0.33 % Success case prop solver time : 0.000
% 0.22/0.33 % Current number of processed clauses : 531
% 0.22/0.33 % Positive orientable unit clauses : 12
% 0.22/0.33 % Positive unorientable unit clauses: 0
% 0.22/0.33 % Negative unit clauses : 1
% 0.22/0.33 % Non-unit-clauses : 518
% 0.22/0.33 % Current number of unprocessed clauses: 1619
% 0.22/0.33 % ...number of literals in the above : 11341
% 0.22/0.33 % Current number of archived formulas : 0
% 0.22/0.33 % Current number of archived clauses : 39
% 0.22/0.33 % Clause-clause subsumption calls (NU) : 32211
% 0.22/0.33 % Rec. Clause-clause subsumption calls : 4191
% 0.22/0.33 % Non-unit clause-clause subsumptions : 62
% 0.22/0.33 % Unit Clause-clause subsumption calls : 78
% 0.22/0.33 % Rewrite failures with RHS unbound : 0
% 0.22/0.33 % BW rewrite match attempts : 0
% 0.22/0.33 % BW rewrite match successes : 0
% 0.22/0.33 % Condensation attempts : 0
% 0.22/0.33 % Condensation successes : 0
% 0.22/0.33 % Termbank termtop insertions : 101329
% 0.22/0.33 % Search garbage collected termcells : 2698
% 0.22/0.33
% 0.22/0.33 % -------------------------------------------------
% 0.22/0.33 % User time : 0.071 s
% 0.22/0.33 % System time : 0.011 s
% 0.22/0.33 % Total time : 0.082 s
% 0.22/0.33 % Maximum resident set size: 3964 pages
% 0.22/0.33
% 0.22/0.33 % -------------------------------------------------
% 0.22/0.33 % User time : 0.073 s
% 0.22/0.33 % System time : 0.015 s
% 0.22/0.33 % Total time : 0.088 s
% 0.22/0.33 % Maximum resident set size: 4864 pages
% 0.22/0.33 % E exiting
%------------------------------------------------------------------------------