%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : NLP004^7 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:16:00 AM UTC 2026
% Result : Theorem 0.21s 0.35s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP004^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 % Computer : n001.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Tue Sep 29 11:40:50 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.24 Running higher-order theorem proving
% 0.21/0.26 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.fejzxbdnyM/E---3.1_1138313.p
% 0.21/0.35 % Version: 3.5.1-ho
% 0.21/0.35 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.21/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.35 % Starting almost_fo_3 with 1500s (5) cores
% 0.21/0.35 % Starting sh10 with 300s (1) cores
% 0.21/0.35 % Starting new_ho_16 with 300s (1) cores
% 0.21/0.35 % Starting post_as_ho11 with 300s (1) cores
% 0.21/0.35 % new_ho_16 with pid 1138328 completed with status 0
% 0.21/0.35 % Result found by new_ho_16
% 0.21/0.35 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.21/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.35 % Starting almost_fo_3 with 1500s (5) cores
% 0.21/0.35 % Starting sh10 with 300s (1) cores
% 0.21/0.35 % Starting new_ho_16 with 300s (1) cores
% 0.21/0.35 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 0.21/0.35 % SinE strategy is LambdaDef
% 0.21/0.35 % Search class: HGHNF-FFMF11-SHSSMFNN
% 0.21/0.35 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.35 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.35 % SubtermCWHack with pid 1138330 completed with status 0
% 0.21/0.35 % Result found by SubtermCWHack
% 0.21/0.35 % Preprocessing class: HSLSSMSSMLLNHSN.
% 0.21/0.35 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.35 % Starting almost_fo_3 with 1500s (5) cores
% 0.21/0.35 % Starting sh10 with 300s (1) cores
% 0.21/0.35 % Starting new_ho_16 with 300s (1) cores
% 0.21/0.35 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = LambdaDef)
% 0.21/0.35 % SinE strategy is LambdaDef
% 0.21/0.35 % Search class: HGHNF-FFMF11-SHSSMFNN
% 0.21/0.35 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.35 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.35 % Preprocessing time : 0.003 s
% 0.21/0.35
% 0.21/0.35 % Proof found!
% 0.21/0.35 % SZS status Theorem
% 0.21/0.35 % SZS output start CNFRefutation
% 0.21/0.35 thf(decl_sort1, type, mu: $tType).
% 0.21/0.35 thf(decl_23, type, qmltpeq: mu > mu > $i > $o).
% 0.21/0.35 thf(decl_25, type, mnot: ($i > $o) > $i > $o).
% 0.21/0.35 thf(decl_26, type, mor: ($i > $o) > ($i > $o) > $i > $o).
% 0.21/0.35 thf(decl_31, type, mand: ($i > $o) > ($i > $o) > $i > $o).
% 0.21/0.35 thf(decl_32, type, mimplies: ($i > $o) > ($i > $o) > $i > $o).
% 0.21/0.35 thf(decl_37, type, exists_in_world: mu > $i > $o).
% 0.21/0.35 thf(decl_38, type, mforall_ind: (mu > $i > $o) > $i > $o).
% 0.21/0.35 thf(decl_39, type, mexists_ind: (mu > $i > $o) > $i > $o).
% 0.21/0.35 thf(decl_51, type, mvalid: ($i > $o) > $o).
% 0.21/0.35 thf(decl_58, type, young: mu > $i > $o).
% 0.21/0.35 thf(decl_59, type, man: mu > $i > $o).
% 0.21/0.35 thf(decl_60, type, fellow: mu > $i > $o).
% 0.21/0.35 thf(decl_61, type, in: mu > mu > $i > $o).
% 0.21/0.35 thf(decl_62, type, down: mu > mu > $i > $o).
% 0.21/0.35 thf(decl_63, type, barrel: mu > mu > $i > $o).
% 0.21/0.35 thf(decl_64, type, old: mu > $i > $o).
% 0.21/0.35 thf(decl_65, type, dirty: mu > $i > $o).
% 0.21/0.35 thf(decl_66, type, white: mu > $i > $o).
% 0.21/0.35 thf(decl_67, type, car: mu > $i > $o).
% 0.21/0.35 thf(decl_68, type, chevy: mu > $i > $o).
% 0.21/0.35 thf(decl_69, type, lonely: mu > $i > $o).
% 0.21/0.35 thf(decl_70, type, way: mu > $i > $o).
% 0.21/0.35 thf(decl_71, type, street: mu > $i > $o).
% 0.21/0.35 thf(decl_72, type, event: mu > $i > $o).
% 0.21/0.35 thf(decl_73, type, city: mu > $i > $o).
% 0.21/0.35 thf(decl_74, type, hollywood: mu > $i > $o).
% 0.21/0.35 thf(decl_75, type, front: mu > $i > $o).
% 0.21/0.35 thf(decl_76, type, furniture: mu > $i > $o).
% 0.21/0.35 thf(decl_77, type, seat: mu > $i > $o).
% 0.21/0.35 thf(decl_78, type, epred1_11: $i > mu > mu > mu > mu > mu > mu > mu > mu > mu > mu > $o).
% 0.21/0.35 thf(decl_79, type, epred2_1: $i > $o).
% 0.21/0.35 thf(decl_80, type, epred3_11: $i > mu > mu > mu > mu > mu > mu > mu > mu > mu > mu > $o).
% 0.21/0.35 thf(decl_81, type, epred4_1: $i > $o).
% 0.21/0.35 thf(decl_82, type, esk1_0: $i).
% 0.21/0.35 thf(decl_83, type, esk2_1: $i > mu).
% 0.21/0.35 thf(decl_84, type, esk3_1: $i > mu).
% 0.21/0.35 thf(decl_85, type, esk4_1: $i > mu).
% 0.21/0.35 thf(decl_86, type, esk5_1: $i > mu).
% 0.21/0.35 thf(decl_87, type, esk6_1: $i > mu).
% 0.21/0.35 thf(decl_88, type, esk7_1: $i > mu).
% 0.21/0.35 thf(decl_89, type, esk8_1: $i > mu).
% 0.21/0.35 thf(decl_90, type, esk9_1: $i > mu).
% 0.21/0.35 thf(decl_91, type, esk10_1: $i > mu).
% 0.21/0.35 thf(decl_92, type, esk11_1: $i > mu).
% 0.21/0.35 thf(decl_93, type, esk12_1: $i > mu).
% 0.21/0.35 thf(decl_94, type, esk13_1: $i > mu).
% 0.21/0.35 thf(decl_95, type, esk14_1: $i > mu).
% 0.21/0.35 thf(decl_96, type, esk15_1: $i > mu).
% 0.21/0.35 thf(decl_97, type, esk16_1: $i > mu).
% 0.21/0.35 thf(decl_98, type, esk17_1: $i > mu).
% 0.21/0.35 thf(decl_99, type, esk18_1: $i > mu).
% 0.21/0.35 thf(decl_100, type, esk19_1: $i > mu).
% 0.21/0.35 thf(decl_101, type, esk20_1: $i > mu).
% 0.21/0.35 thf(decl_102, type, esk21_1: $i > mu).
% 0.21/0.35 thf(mexists_ind, axiom, ((mexists_ind)=(^[X13:mu > $i > $o]:(mnot @ (mforall_ind @ (^[X14:mu]:(mnot @ (X13 @ X14))))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mexists_ind)).
% 0.21/0.35 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/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mforall_ind)).
% 0.21/0.35 thf(mnot, axiom, ((mnot)=(^[X4:$i > $o, X3:$i]:(~((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mnot)).
% 0.21/0.35 thf(mimplies, axiom, ((mimplies)=(^[X4:$i > $o, X5:$i > $o]:(mor @ (mnot @ X4) @ X5))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mimplies)).
% 0.21/0.35 thf(mor, axiom, ((mor)=(^[X4:$i > $o, X5:$i > $o, X3:$i]:((((X4 @ X3))|((X5 @ X3)))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mor)).
% 0.21/0.35 thf(mand, axiom, ((mand)=(^[X4:$i > $o, X5:$i > $o]:(mnot @ (mor @ (mnot @ X4) @ (mnot @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mand)).
% 0.21/0.35 thf(co1, conjecture, (mvalid @ (mand @ (mimplies @ (mexists_ind @ (^[X29:mu]:(mexists_ind @ (^[X30:mu]:(mexists_ind @ (^[X31:mu]:(mexists_ind @ (^[X32:mu]:(mexists_ind @ (^[X33:mu]:(mexists_ind @ (^[X25:mu]:(mexists_ind @ (^[X34:mu]:(mexists_ind @ (^[X35:mu]:(mexists_ind @ (^[X36:mu]:(mexists_ind @ (^[X37:mu]:(mand @ (seat @ X29) @ (mand @ (furniture @ X29) @ (mand @ (front @ X29) @ (mand @ (seat @ X30) @ (mand @ (furniture @ X30) @ (mand @ (front @ X30) @ (mand @ (hollywood @ X31) @ (mand @ (city @ X31) @ (mand @ (event @ X32) @ (mand @ (street @ X33) @ (mand @ (way @ X33) @ (mand @ (lonely @ X33) @ (mand @ (chevy @ X25) @ (mand @ (car @ X25) @ (mand @ (white @ X25) @ (mand @ (dirty @ X25) @ (mand @ (old @ X25) @ (mand @ (barrel @ X32 @ X25) @ (mand @ (down @ X32 @ X33) @ (mand @ (in @ X32 @ X31) @ (mand @ (mnot @ (qmltpeq @ X34 @ X35)) @ (mand @ (fellow @ X34) @ (mand @ (man @ X34) @ (mand @ (young @ X34) @ (mand @ (fellow @ X35) @ (mand @ (man @ X35) @ (mand @ (young @ X35) @ (mand @ (qmltpeq @ X34 @ X36) @ (mand @ (in @ X36 @ X29) @ (mand @ (qmltpeq @ X35 @ X37) @ (in @ X37 @ X30))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mexists_ind @ (^[X38:mu]:(mexists_ind @ (^[X39:mu]:(mexists_ind @ (^[X40:mu]:(mexists_ind @ (^[X41:mu]:(mexists_ind @ (^[X42:mu]:(mexists_ind @ (^[X43:mu]:(mexists_ind @ (^[X44:mu]:(mexists_ind @ (^[X45:mu]:(mexists_ind @ (^[X46:mu]:(mexists_ind @ (^[X47:mu]:(mand @ (seat @ X38) @ (mand @ (furniture @ X38) @ (mand @ (front @ X38) @ (mand @ (seat @ X39) @ (mand @ (furniture @ X39) @ (mand @ (front @ X39) @ (mand @ (hollywood @ X40) @ (mand @ (city @ X40) @ (mand @ (event @ X41) @ (mand @ (chevy @ X42) @ (mand @ (car @ X42) @ (mand @ (white @ X42) @ (mand @ (dirty @ X42) @ (mand @ (old @ X42) @ (mand @ (street @ X43) @ (mand @ (way @ X43) @ (mand @ (lonely @ X43) @ (mand @ (barrel @ X41 @ X42) @ (mand @ (down @ X41 @ X43) @ (mand @ (in @ X41 @ X40) @ (mand @ (mnot @ (qmltpeq @ X44 @ X45)) @ (mand @ (fellow @ X44) @ (mand @ (man @ X44) @ (mand @ (young @ X44) @ (mand @ (fellow @ X45) @ (mand @ (man @ X45) @ (mand @ (young @ X45) @ (mand @ (qmltpeq @ X44 @ X46) @ (mand @ (in @ X46 @ X38) @ (mand @ (qmltpeq @ X45 @ X47) @ (in @ X47 @ X39)))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mimplies @ (mexists_ind @ (^[X48:mu]:(mexists_ind @ (^[X49:mu]:(mexists_ind @ (^[X50:mu]:(mexists_ind @ (^[X51:mu]:(mexists_ind @ (^[X52:mu]:(mexists_ind @ (^[X53:mu]:(mexists_ind @ (^[X54:mu]:(mexists_ind @ (^[X55:mu]:(mexists_ind @ (^[X56:mu]:(mexists_ind @ (^[X57:mu]:(mand @ (seat @ X48) @ (mand @ (furniture @ X48) @ (mand @ (front @ X48) @ (mand @ (seat @ X49) @ (mand @ (furniture @ X49) @ (mand @ (front @ X49) @ (mand @ (hollywood @ X50) @ (mand @ (city @ X50) @ (mand @ (event @ X51) @ (mand @ (chevy @ X52) @ (mand @ (car @ X52) @ (mand @ (white @ X52) @ (mand @ (dirty @ X52) @ (mand @ (old @ X52) @ (mand @ (street @ X53) @ (mand @ (way @ X53) @ (mand @ (lonely @ X53) @ (mand @ (barrel @ X51 @ X52) @ (mand @ (down @ X51 @ X53) @ (mand @ (in @ X51 @ X50) @ (mand @ (mnot @ (qmltpeq @ X54 @ X55)) @ (mand @ (fellow @ X54) @ (mand @ (man @ X54) @ (mand @ (young @ X54) @ (mand @ (fellow @ X55) @ (mand @ (man @ X55) @ (mand @ (young @ X55) @ (mand @ (qmltpeq @ X54 @ X56) @ (mand @ (in @ X56 @ X48) @ (mand @ (qmltpeq @ X55 @ X57) @ (in @ X57 @ X49))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mexists_ind @ (^[X58:mu]:(mexists_ind @ (^[X59:mu]:(mexists_ind @ (^[X60:mu]:(mexists_ind @ (^[X61:mu]:(mexists_ind @ (^[X62:mu]:(mexists_ind @ (^[X63:mu]:(mexists_ind @ (^[X64:mu]:(mexists_ind @ (^[X65:mu]:(mexists_ind @ (^[X66:mu]:(mexists_ind @ (^[X67:mu]:(mand @ (seat @ X58) @ (mand @ (furniture @ X58) @ (mand @ (front @ X58) @ (mand @ (seat @ X59) @ (mand @ (furniture @ X59) @ (mand @ (front @ X59) @ (mand @ (hollywood @ X60) @ (mand @ (city @ X60) @ (mand @ (event @ X61) @ (mand @ (street @ X62) @ (mand @ (way @ X62) @ (mand @ (lonely @ X62) @ (mand @ (chevy @ X63) @ (mand @ (car @ X63) @ (mand @ (white @ X63) @ (mand @ (dirty @ X63) @ (mand @ (old @ X63) @ (mand @ (barrel @ X61 @ X63) @ (mand @ (down @ X61 @ X62) @ (mand @ (in @ X61 @ X60) @ (mand @ (mnot @ (qmltpeq @ X64 @ X65)) @ (mand @ (fellow @ X64) @ (mand @ (man @ X64) @ (mand @ (young @ X64) @ (mand @ (fellow @ X65) @ (mand @ (man @ X65) @ (mand @ (young @ X65) @ (mand @ (qmltpeq @ X64 @ X66) @ (mand @ (in @ X66 @ X58) @ (mand @ (qmltpeq @ X65 @ X67) @ (in @ X67 @ X59)))))))))))))))))))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', co1)).
% 0.21/0.35 thf(mvalid, axiom, ((mvalid)=(^[X4:$i > $o]:(![X3:$i]:((X4 @ X3))))), file('/export/starexec/sandbox2/tmp/tmp.fejzxbdnyM/E---3.1_1138313.p', mvalid)).
% 0.21/0.35 thf(c_0_8, plain, ![X82:mu, X86:mu, X87:mu, X85:mu, X84:mu, X83:mu, X88:mu, X89:mu, X90:mu, X91:mu, X112:$i]:(((epred1_11 @ X112 @ X91 @ X90 @ X83 @ X89 @ X84 @ X85 @ X86 @ X87 @ X88 @ X82)<=>~(~((~(seat @ X91 @ X112)|~(~((~(furniture @ X91 @ X112)|~(~((~(front @ X91 @ X112)|~(~((~(seat @ X90 @ X112)|~(~((~(furniture @ X90 @ X112)|~(~((~(front @ X90 @ X112)|~(~((~(hollywood @ X89 @ X112)|~(~((~(city @ X89 @ X112)|~(~((~(event @ X88 @ X112)|~(~((~(chevy @ X87 @ X112)|~(~((~(car @ X87 @ X112)|~(~((~(white @ X87 @ X112)|~(~((~(dirty @ X87 @ X112)|~(~((~(old @ X87 @ X112)|~(~((~(street @ X86 @ X112)|~(~((~(way @ X86 @ X112)|~(~((~(lonely @ X86 @ X112)|~(~((~(barrel @ X88 @ X87 @ X112)|~(~((~(down @ X88 @ X86 @ X112)|~(~((~(in @ X88 @ X89 @ X112)|~(~(((qmltpeq @ X85 @ X84 @ X112)|~(~((~(fellow @ X85 @ X112)|~(~((~(man @ X85 @ X112)|~(~((~(young @ X85 @ X112)|~(~((~(fellow @ X84 @ X112)|~(~((~(man @ X84 @ X112)|~(~((~(young @ X84 @ X112)|~(~((~(qmltpeq @ X85 @ X83 @ X112)|~(~((~(in @ X83 @ X91 @ X112)|~(~((~(qmltpeq @ X84 @ X82 @ X112)|~(in @ X82 @ X90 @ X112))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.21/0.35 thf(c_0_9, plain, ![X112:$i]:(((epred2_1 @ X112)<=>~((~(~(![X81:mu]:(((exists_in_world @ X81 @ X112)=>~(~(![X80:mu]:(((exists_in_world @ X80 @ X112)=>~(~(![X79:mu]:(((exists_in_world @ X79 @ X112)=>~(~(![X78:mu]:(((exists_in_world @ X78 @ X112)=>~(~(![X77:mu]:(((exists_in_world @ X77 @ X112)=>~(~(![X76:mu]:(((exists_in_world @ X76 @ X112)=>~(~(![X75:mu]:(((exists_in_world @ X75 @ X112)=>~(~(![X74:mu]:(((exists_in_world @ X74 @ X112)=>~(~(![X73:mu]:(((exists_in_world @ X73 @ X112)=>~(~(![X72:mu]:(((exists_in_world @ X72 @ X112)=>~(~((~(seat @ X81 @ X112)|~(~((~(furniture @ X81 @ X112)|~(~((~(front @ X81 @ X112)|~(~((~(seat @ X80 @ X112)|~(~((~(furniture @ X80 @ X112)|~(~((~(front @ X80 @ X112)|~(~((~(hollywood @ X79 @ X112)|~(~((~(city @ X79 @ X112)|~(~((~(event @ X78 @ X112)|~(~((~(street @ X77 @ X112)|~(~((~(way @ X77 @ X112)|~(~((~(lonely @ X77 @ X112)|~(~((~(chevy @ X76 @ X112)|~(~((~(car @ X76 @ X112)|~(~((~(white @ X76 @ X112)|~(~((~(dirty @ X76 @ X112)|~(~((~(old @ X76 @ X112)|~(~((~(barrel @ X78 @ X76 @ X112)|~(~((~(down @ X78 @ X77 @ X112)|~(~((~(in @ X78 @ X79 @ X112)|~(~(((qmltpeq @ X75 @ X74 @ X112)|~(~((~(fellow @ X75 @ X112)|~(~((~(man @ X75 @ X112)|~(~((~(young @ X75 @ X112)|~(~((~(fellow @ X74 @ X112)|~(~((~(man @ X74 @ X112)|~(~((~(young @ X74 @ X112)|~(~((~(qmltpeq @ X75 @ X73 @ X112)|~(~((~(in @ X73 @ X81 @ X112)|~(~((~(qmltpeq @ X74 @ X72 @ X112)|~(in @ X72 @ X80 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|~(![X91:mu]:(((exists_in_world @ X91 @ X112)=>~(~(![X90:mu]:(((exists_in_world @ X90 @ X112)=>~(~(![X89:mu]:(((exists_in_world @ X89 @ X112)=>~(~(![X88:mu]:(((exists_in_world @ X88 @ X112)=>~(~(![X87:mu]:(((exists_in_world @ X87 @ X112)=>~(~(![X86:mu]:(((exists_in_world @ X86 @ X112)=>~(~(![X85:mu]:(((exists_in_world @ X85 @ X112)=>~(~(![X84:mu]:(((exists_in_world @ X84 @ X112)=>~(~(![X83:mu]:(((exists_in_world @ X83 @ X112)=>~(~(![X82:mu]:(((exists_in_world @ X82 @ X112)=>~(~((~(seat @ X91 @ X112)|~(~((~(furniture @ X91 @ X112)|~(~((~(front @ X91 @ X112)|~(~((~(seat @ X90 @ X112)|~(~((~(furniture @ X90 @ X112)|~(~((~(front @ X90 @ X112)|~(~((~(hollywood @ X89 @ X112)|~(~((~(city @ X89 @ X112)|~(~((~(event @ X88 @ X112)|~(~((~(chevy @ X87 @ X112)|~(~((~(car @ X87 @ X112)|~(~((~(white @ X87 @ X112)|~(~((~(dirty @ X87 @ X112)|~(~((~(old @ X87 @ X112)|~(~((~(street @ X86 @ X112)|~(~((~(way @ X86 @ X112)|~(~((~(lonely @ X86 @ X112)|~(~((~(barrel @ X88 @ X87 @ X112)|~(~((~(down @ X88 @ X86 @ X112)|~(~((~(in @ X88 @ X89 @ X112)|~(~(((qmltpeq @ X85 @ X84 @ X112)|~(~((~(fellow @ X85 @ X112)|~(~((~(man @ X85 @ X112)|~(~((~(young @ X85 @ X112)|~(~((~(fellow @ X84 @ X112)|~(~((~(man @ X84 @ X112)|~(~((~(young @ X84 @ X112)|~(~((~(qmltpeq @ X85 @ X83 @ X112)|~(~((~(in @ X83 @ X91 @ X112)|~(~((~(qmltpeq @ X84 @ X82 @ X112)|~(in @ X82 @ X90 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.21/0.35 thf(c_0_10, plain, ![X82:mu, X86:mu, X87:mu, X85:mu, X84:mu, X83:mu, X88:mu, X89:mu, X90:mu, X91:mu, X112:$i]:(((epred1_11 @ X112 @ X91 @ X90 @ X83 @ X89 @ X84 @ X85 @ X86 @ X87 @ X88 @ X82)=>~(~((~(seat @ X91 @ X112)|~(~((~(furniture @ X91 @ X112)|~(~((~(front @ X91 @ X112)|~(~((~(seat @ X90 @ X112)|~(~((~(furniture @ X90 @ X112)|~(~((~(front @ X90 @ X112)|~(~((~(hollywood @ X89 @ X112)|~(~((~(city @ X89 @ X112)|~(~((~(event @ X88 @ X112)|~(~((~(chevy @ X87 @ X112)|~(~((~(car @ X87 @ X112)|~(~((~(white @ X87 @ X112)|~(~((~(dirty @ X87 @ X112)|~(~((~(old @ X87 @ X112)|~(~((~(street @ X86 @ X112)|~(~((~(way @ X86 @ X112)|~(~((~(lonely @ X86 @ X112)|~(~((~(barrel @ X88 @ X87 @ X112)|~(~((~(down @ X88 @ X86 @ X112)|~(~((~(in @ X88 @ X89 @ X112)|~(~(((qmltpeq @ X85 @ X84 @ X112)|~(~((~(fellow @ X85 @ X112)|~(~((~(man @ X85 @ X112)|~(~((~(young @ X85 @ X112)|~(~((~(fellow @ X84 @ X112)|~(~((~(man @ X84 @ X112)|~(~((~(young @ X84 @ X112)|~(~((~(qmltpeq @ X85 @ X83 @ X112)|~(~((~(in @ X83 @ X91 @ X112)|~(~((~(qmltpeq @ X84 @ X82 @ X112)|~(in @ X82 @ X90 @ X112))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_8])).
% 0.21/0.35 thf(c_0_11, plain, ![X112:$i]:(((epred2_1 @ X112)=>~((~(~(![X81:mu]:(((exists_in_world @ X81 @ X112)=>~(~(![X80:mu]:(((exists_in_world @ X80 @ X112)=>~(~(![X79:mu]:(((exists_in_world @ X79 @ X112)=>~(~(![X78:mu]:(((exists_in_world @ X78 @ X112)=>~(~(![X77:mu]:(((exists_in_world @ X77 @ X112)=>~(~(![X76:mu]:(((exists_in_world @ X76 @ X112)=>~(~(![X75:mu]:(((exists_in_world @ X75 @ X112)=>~(~(![X74:mu]:(((exists_in_world @ X74 @ X112)=>~(~(![X73:mu]:(((exists_in_world @ X73 @ X112)=>~(~(![X72:mu]:(((exists_in_world @ X72 @ X112)=>~(~((~(seat @ X81 @ X112)|~(~((~(furniture @ X81 @ X112)|~(~((~(front @ X81 @ X112)|~(~((~(seat @ X80 @ X112)|~(~((~(furniture @ X80 @ X112)|~(~((~(front @ X80 @ X112)|~(~((~(hollywood @ X79 @ X112)|~(~((~(city @ X79 @ X112)|~(~((~(event @ X78 @ X112)|~(~((~(street @ X77 @ X112)|~(~((~(way @ X77 @ X112)|~(~((~(lonely @ X77 @ X112)|~(~((~(chevy @ X76 @ X112)|~(~((~(car @ X76 @ X112)|~(~((~(white @ X76 @ X112)|~(~((~(dirty @ X76 @ X112)|~(~((~(old @ X76 @ X112)|~(~((~(barrel @ X78 @ X76 @ X112)|~(~((~(down @ X78 @ X77 @ X112)|~(~((~(in @ X78 @ X79 @ X112)|~(~(((qmltpeq @ X75 @ X74 @ X112)|~(~((~(fellow @ X75 @ X112)|~(~((~(man @ X75 @ X112)|~(~((~(young @ X75 @ X112)|~(~((~(fellow @ X74 @ X112)|~(~((~(man @ X74 @ X112)|~(~((~(young @ X74 @ X112)|~(~((~(qmltpeq @ X75 @ X73 @ X112)|~(~((~(in @ X73 @ X81 @ X112)|~(~((~(qmltpeq @ X74 @ X72 @ X112)|~(in @ X72 @ X80 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|~(![X91:mu]:(((exists_in_world @ X91 @ X112)=>~(~(![X90:mu]:(((exists_in_world @ X90 @ X112)=>~(~(![X89:mu]:(((exists_in_world @ X89 @ X112)=>~(~(![X88:mu]:(((exists_in_world @ X88 @ X112)=>~(~(![X87:mu]:(((exists_in_world @ X87 @ X112)=>~(~(![X86:mu]:(((exists_in_world @ X86 @ X112)=>~(~(![X85:mu]:(((exists_in_world @ X85 @ X112)=>~(~(![X84:mu]:(((exists_in_world @ X84 @ X112)=>~(~(![X83:mu]:(((exists_in_world @ X83 @ X112)=>~(~(![X82:mu]:(((exists_in_world @ X82 @ X112)=>(epred1_11 @ X112 @ X91 @ X90 @ X83 @ X89 @ X84 @ X85 @ X86 @ X87 @ X88 @ X82)))))))))))))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_9]), c_0_8])).
% 0.21/0.35 thf(c_0_12, plain, ![X102:mu, X106:mu, X107:mu, X105:mu, X104:mu, X103:mu, X108:mu, X109:mu, X110:mu, X111:mu, X112:$i]:(((epred3_11 @ X112 @ X111 @ X110 @ X103 @ X109 @ X104 @ X105 @ X106 @ X107 @ X108 @ X102)<=>~(~((~(seat @ X111 @ X112)|~(~((~(furniture @ X111 @ X112)|~(~((~(front @ X111 @ X112)|~(~((~(seat @ X110 @ X112)|~(~((~(furniture @ X110 @ X112)|~(~((~(front @ X110 @ X112)|~(~((~(hollywood @ X109 @ X112)|~(~((~(city @ X109 @ X112)|~(~((~(event @ X108 @ X112)|~(~((~(street @ X107 @ X112)|~(~((~(way @ X107 @ X112)|~(~((~(lonely @ X107 @ X112)|~(~((~(chevy @ X106 @ X112)|~(~((~(car @ X106 @ X112)|~(~((~(white @ X106 @ X112)|~(~((~(dirty @ X106 @ X112)|~(~((~(old @ X106 @ X112)|~(~((~(barrel @ X108 @ X106 @ X112)|~(~((~(down @ X108 @ X107 @ X112)|~(~((~(in @ X108 @ X109 @ X112)|~(~(((qmltpeq @ X105 @ X104 @ X112)|~(~((~(fellow @ X105 @ X112)|~(~((~(man @ X105 @ X112)|~(~((~(young @ X105 @ X112)|~(~((~(fellow @ X104 @ X112)|~(~((~(man @ X104 @ X112)|~(~((~(young @ X104 @ X112)|~(~((~(qmltpeq @ X105 @ X103 @ X112)|~(~((~(in @ X103 @ X111 @ X112)|~(~((~(qmltpeq @ X104 @ X102 @ X112)|~(in @ X102 @ X110 @ X112))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.21/0.35 thf(c_0_13, plain, ![X112:$i]:(((epred4_1 @ X112)<=>~((~(~(![X101:mu]:(((exists_in_world @ X101 @ X112)=>~(~(![X100:mu]:(((exists_in_world @ X100 @ X112)=>~(~(![X99:mu]:(((exists_in_world @ X99 @ X112)=>~(~(![X98:mu]:(((exists_in_world @ X98 @ X112)=>~(~(![X97:mu]:(((exists_in_world @ X97 @ X112)=>~(~(![X96:mu]:(((exists_in_world @ X96 @ X112)=>~(~(![X95:mu]:(((exists_in_world @ X95 @ X112)=>~(~(![X94:mu]:(((exists_in_world @ X94 @ X112)=>~(~(![X93:mu]:(((exists_in_world @ X93 @ X112)=>~(~(![X92:mu]:(((exists_in_world @ X92 @ X112)=>~(~((~(seat @ X101 @ X112)|~(~((~(furniture @ X101 @ X112)|~(~((~(front @ X101 @ X112)|~(~((~(seat @ X100 @ X112)|~(~((~(furniture @ X100 @ X112)|~(~((~(front @ X100 @ X112)|~(~((~(hollywood @ X99 @ X112)|~(~((~(city @ X99 @ X112)|~(~((~(event @ X98 @ X112)|~(~((~(chevy @ X97 @ X112)|~(~((~(car @ X97 @ X112)|~(~((~(white @ X97 @ X112)|~(~((~(dirty @ X97 @ X112)|~(~((~(old @ X97 @ X112)|~(~((~(street @ X96 @ X112)|~(~((~(way @ X96 @ X112)|~(~((~(lonely @ X96 @ X112)|~(~((~(barrel @ X98 @ X97 @ X112)|~(~((~(down @ X98 @ X96 @ X112)|~(~((~(in @ X98 @ X99 @ X112)|~(~(((qmltpeq @ X95 @ X94 @ X112)|~(~((~(fellow @ X95 @ X112)|~(~((~(man @ X95 @ X112)|~(~((~(young @ X95 @ X112)|~(~((~(fellow @ X94 @ X112)|~(~((~(man @ X94 @ X112)|~(~((~(young @ X94 @ X112)|~(~((~(qmltpeq @ X95 @ X93 @ X112)|~(~((~(in @ X93 @ X101 @ X112)|~(~((~(qmltpeq @ X94 @ X92 @ X112)|~(in @ X92 @ X100 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|~(![X111:mu]:(((exists_in_world @ X111 @ X112)=>~(~(![X110:mu]:(((exists_in_world @ X110 @ X112)=>~(~(![X109:mu]:(((exists_in_world @ X109 @ X112)=>~(~(![X108:mu]:(((exists_in_world @ X108 @ X112)=>~(~(![X107:mu]:(((exists_in_world @ X107 @ X112)=>~(~(![X106:mu]:(((exists_in_world @ X106 @ X112)=>~(~(![X105:mu]:(((exists_in_world @ X105 @ X112)=>~(~(![X104:mu]:(((exists_in_world @ X104 @ X112)=>~(~(![X103:mu]:(((exists_in_world @ X103 @ X112)=>~(~(![X102:mu]:(((exists_in_world @ X102 @ X112)=>~(~((~(seat @ X111 @ X112)|~(~((~(furniture @ X111 @ X112)|~(~((~(front @ X111 @ X112)|~(~((~(seat @ X110 @ X112)|~(~((~(furniture @ X110 @ X112)|~(~((~(front @ X110 @ X112)|~(~((~(hollywood @ X109 @ X112)|~(~((~(city @ X109 @ X112)|~(~((~(event @ X108 @ X112)|~(~((~(street @ X107 @ X112)|~(~((~(way @ X107 @ X112)|~(~((~(lonely @ X107 @ X112)|~(~((~(chevy @ X106 @ X112)|~(~((~(car @ X106 @ X112)|~(~((~(white @ X106 @ X112)|~(~((~(dirty @ X106 @ X112)|~(~((~(old @ X106 @ X112)|~(~((~(barrel @ X108 @ X106 @ X112)|~(~((~(down @ X108 @ X107 @ X112)|~(~((~(in @ X108 @ X109 @ X112)|~(~(((qmltpeq @ X105 @ X104 @ X112)|~(~((~(fellow @ X105 @ X112)|~(~((~(man @ X105 @ X112)|~(~((~(young @ X105 @ X112)|~(~((~(fellow @ X104 @ X112)|~(~((~(man @ X104 @ X112)|~(~((~(young @ X104 @ X112)|~(~((~(qmltpeq @ X105 @ X103 @ X112)|~(~((~(in @ X103 @ X111 @ X112)|~(~((~(qmltpeq @ X104 @ X102 @ X112)|~(in @ X102 @ X110 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 0.21/0.35 thf(c_0_14, plain, ![X114:mu, X115:mu, X116:mu, X117:mu, X118:mu, X119:mu, X120:mu, X121:mu, X122:mu, X123:mu, X124:$i]:((~(epred1_11 @ X124 @ X123 @ X122 @ X119 @ X121 @ X118 @ X117 @ X115 @ X116 @ X120 @ X114)|(~(seat @ X123 @ X124)|(~(furniture @ X123 @ X124)|(~(front @ X123 @ X124)|(~(seat @ X122 @ X124)|(~(furniture @ X122 @ X124)|(~(front @ X122 @ X124)|(~(hollywood @ X121 @ X124)|(~(city @ X121 @ X124)|(~(event @ X120 @ X124)|(~(chevy @ X116 @ X124)|(~(car @ X116 @ X124)|(~(white @ X116 @ X124)|(~(dirty @ X116 @ X124)|(~(old @ X116 @ X124)|(~(street @ X115 @ X124)|(~(way @ X115 @ X124)|(~(lonely @ X115 @ X124)|(~(barrel @ X120 @ X116 @ X124)|(~(down @ X120 @ X115 @ X124)|(~(in @ X120 @ X121 @ X124)|((qmltpeq @ X117 @ X118 @ X124)|(~(fellow @ X117 @ X124)|(~(man @ X117 @ X124)|(~(young @ X117 @ X124)|(~(fellow @ X118 @ X124)|(~(man @ X118 @ X124)|(~(young @ X118 @ X124)|(~(qmltpeq @ X117 @ X119 @ X124)|(~(in @ X119 @ X123 @ X124)|(~(qmltpeq @ X118 @ X114 @ X124)|~(in @ X114 @ X122 @ X124))))))))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])).
% 0.21/0.35 thf(c_0_15, plain, ![X125:$i, X136:mu, X137:mu, X138:mu, X139:mu, X140:mu, X141:mu, X142:mu, X143:mu, X144:mu, X145:mu]:(((((exists_in_world @ (esk2_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk3_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk4_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk5_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk6_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk8_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk9_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk10_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((exists_in_world @ (esk11_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((seat @ (esk2_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((furniture @ (esk2_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((front @ (esk2_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((seat @ (esk3_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((furniture @ (esk3_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((front @ (esk3_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((hollywood @ (esk4_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((city @ (esk4_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((event @ (esk5_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((street @ (esk6_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((way @ (esk6_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((lonely @ (esk6_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((chevy @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((car @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((white @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((dirty @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((old @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((barrel @ (esk5_1 @ X125) @ (esk7_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((down @ (esk5_1 @ X125) @ (esk6_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((in @ (esk5_1 @ X125) @ (esk4_1 @ X125) @ X125)|~(epred2_1 @ X125))&((~(qmltpeq @ (esk8_1 @ X125) @ (esk9_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((fellow @ (esk8_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((man @ (esk8_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((young @ (esk8_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((fellow @ (esk9_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((man @ (esk9_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((young @ (esk9_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((qmltpeq @ (esk8_1 @ X125) @ (esk10_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((in @ (esk10_1 @ X125) @ (esk2_1 @ X125) @ X125)|~(epred2_1 @ X125))&(((qmltpeq @ (esk9_1 @ X125) @ (esk11_1 @ X125) @ X125)|~(epred2_1 @ X125))&((in @ (esk11_1 @ X125) @ (esk3_1 @ X125) @ X125)|~(epred2_1 @ X125))))))))))))))))))))))))))))))))))))))))))&(~(exists_in_world @ X136 @ X125)|(~(exists_in_world @ X137 @ X125)|(~(exists_in_world @ X138 @ X125)|(~(exists_in_world @ X139 @ X125)|(~(exists_in_world @ X140 @ X125)|(~(exists_in_world @ X141 @ X125)|(~(exists_in_world @ X142 @ X125)|(~(exists_in_world @ X143 @ X125)|(~(exists_in_world @ X144 @ X125)|(~(exists_in_world @ X145 @ X125)|(epred1_11 @ X125 @ X136 @ X137 @ X144 @ X138 @ X143 @ X142 @ X141 @ X140 @ X139 @ X145))))))))))|~(epred2_1 @ X125)))), 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_11])])])])])])).
% 0.21/0.35 thf(c_0_16, plain, ![X102:mu, X106:mu, X107:mu, X105:mu, X104:mu, X103:mu, X108:mu, X109:mu, X110:mu, X111:mu, X112:$i]:(((epred3_11 @ X112 @ X111 @ X110 @ X103 @ X109 @ X104 @ X105 @ X106 @ X107 @ X108 @ X102)=>~(~((~(seat @ X111 @ X112)|~(~((~(furniture @ X111 @ X112)|~(~((~(front @ X111 @ X112)|~(~((~(seat @ X110 @ X112)|~(~((~(furniture @ X110 @ X112)|~(~((~(front @ X110 @ X112)|~(~((~(hollywood @ X109 @ X112)|~(~((~(city @ X109 @ X112)|~(~((~(event @ X108 @ X112)|~(~((~(street @ X107 @ X112)|~(~((~(way @ X107 @ X112)|~(~((~(lonely @ X107 @ X112)|~(~((~(chevy @ X106 @ X112)|~(~((~(car @ X106 @ X112)|~(~((~(white @ X106 @ X112)|~(~((~(dirty @ X106 @ X112)|~(~((~(old @ X106 @ X112)|~(~((~(barrel @ X108 @ X106 @ X112)|~(~((~(down @ X108 @ X107 @ X112)|~(~((~(in @ X108 @ X109 @ X112)|~(~(((qmltpeq @ X105 @ X104 @ X112)|~(~((~(fellow @ X105 @ X112)|~(~((~(man @ X105 @ X112)|~(~((~(young @ X105 @ X112)|~(~((~(fellow @ X104 @ X112)|~(~((~(man @ X104 @ X112)|~(~((~(young @ X104 @ X112)|~(~((~(qmltpeq @ X105 @ X103 @ X112)|~(~((~(in @ X103 @ X111 @ X112)|~(~((~(qmltpeq @ X104 @ X102 @ X112)|~(in @ X102 @ X110 @ X112))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_12])).
% 0.21/0.35 thf(c_0_17, plain, ![X112:$i]:(((epred4_1 @ X112)=>~((~(~(![X101:mu]:(((exists_in_world @ X101 @ X112)=>~(~(![X100:mu]:(((exists_in_world @ X100 @ X112)=>~(~(![X99:mu]:(((exists_in_world @ X99 @ X112)=>~(~(![X98:mu]:(((exists_in_world @ X98 @ X112)=>~(~(![X97:mu]:(((exists_in_world @ X97 @ X112)=>~(~(![X96:mu]:(((exists_in_world @ X96 @ X112)=>~(~(![X95:mu]:(((exists_in_world @ X95 @ X112)=>~(~(![X94:mu]:(((exists_in_world @ X94 @ X112)=>~(~(![X93:mu]:(((exists_in_world @ X93 @ X112)=>~(~(![X92:mu]:(((exists_in_world @ X92 @ X112)=>~(~((~(seat @ X101 @ X112)|~(~((~(furniture @ X101 @ X112)|~(~((~(front @ X101 @ X112)|~(~((~(seat @ X100 @ X112)|~(~((~(furniture @ X100 @ X112)|~(~((~(front @ X100 @ X112)|~(~((~(hollywood @ X99 @ X112)|~(~((~(city @ X99 @ X112)|~(~((~(event @ X98 @ X112)|~(~((~(chevy @ X97 @ X112)|~(~((~(car @ X97 @ X112)|~(~((~(white @ X97 @ X112)|~(~((~(dirty @ X97 @ X112)|~(~((~(old @ X97 @ X112)|~(~((~(street @ X96 @ X112)|~(~((~(way @ X96 @ X112)|~(~((~(lonely @ X96 @ X112)|~(~((~(barrel @ X98 @ X97 @ X112)|~(~((~(down @ X98 @ X96 @ X112)|~(~((~(in @ X98 @ X99 @ X112)|~(~(((qmltpeq @ X95 @ X94 @ X112)|~(~((~(fellow @ X95 @ X112)|~(~((~(man @ X95 @ X112)|~(~((~(young @ X95 @ X112)|~(~((~(fellow @ X94 @ X112)|~(~((~(man @ X94 @ X112)|~(~((~(young @ X94 @ X112)|~(~((~(qmltpeq @ X95 @ X93 @ X112)|~(~((~(in @ X93 @ X101 @ X112)|~(~((~(qmltpeq @ X94 @ X92 @ X112)|~(in @ X92 @ X100 @ X112)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|~(![X111:mu]:(((exists_in_world @ X111 @ X112)=>~(~(![X110:mu]:(((exists_in_world @ X110 @ X112)=>~(~(![X109:mu]:(((exists_in_world @ X109 @ X112)=>~(~(![X108:mu]:(((exists_in_world @ X108 @ X112)=>~(~(![X107:mu]:(((exists_in_world @ X107 @ X112)=>~(~(![X106:mu]:(((exists_in_world @ X106 @ X112)=>~(~(![X105:mu]:(((exists_in_world @ X105 @ X112)=>~(~(![X104:mu]:(((exists_in_world @ X104 @ X112)=>~(~(![X103:mu]:(((exists_in_world @ X103 @ X112)=>~(~(![X102:mu]:(((exists_in_world @ X102 @ X112)=>(epred3_11 @ X112 @ X111 @ X110 @ X103 @ X109 @ X104 @ X105 @ X106 @ X107 @ X108 @ X102)))))))))))))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_13]), c_0_12])).
% 0.21/0.35 thf(c_0_18, plain, ![X19:mu, X20:mu, X14:mu, X23:mu, X22:mu, X24:mu, X25:mu, X21:mu, X12:mu, X10:mu, X3:$i]:(((qmltpeq @ X21 @ X20 @ X3)|~((epred1_11 @ X3 @ X10 @ X12 @ X14 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25))|~((seat @ X10 @ X3))|~((furniture @ X10 @ X3))|~((front @ X10 @ X3))|~((seat @ X12 @ X3))|~((furniture @ X12 @ X3))|~((front @ X12 @ X3))|~((hollywood @ X19 @ X3))|~((city @ X19 @ X3))|~((event @ X24 @ X3))|~((chevy @ X23 @ X3))|~((car @ X23 @ X3))|~((white @ X23 @ X3))|~((dirty @ X23 @ X3))|~((old @ X23 @ X3))|~((street @ X22 @ X3))|~((way @ X22 @ X3))|~((lonely @ X22 @ X3))|~((barrel @ X24 @ X23 @ X3))|~((down @ X24 @ X22 @ X3))|~((in @ X24 @ X19 @ X3))|~((fellow @ X21 @ X3))|~((man @ X21 @ X3))|~((young @ X21 @ X3))|~((fellow @ X20 @ X3))|~((man @ X20 @ X3))|~((young @ X20 @ X3))|~((qmltpeq @ X21 @ X14 @ X3))|~((in @ X14 @ X10 @ X3))|~((qmltpeq @ X20 @ X25 @ X3))|~((in @ X25 @ X12 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.21/0.35 thf(c_0_19, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X21:mu, X22:mu, X23:mu, X24:mu, X25:mu, X10:mu, X3:$i]:(((epred1_11 @ X3 @ X10 @ X12 @ X24 @ X14 @ X23 @ X22 @ X21 @ X20 @ X19 @ X25)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X23 @ X3))|~((exists_in_world @ X24 @ X3))|~((exists_in_world @ X25 @ X3))|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_20, plain, ![X146:mu, X147:mu, X148:mu, X149:mu, X150:mu, X151:mu, X152:mu, X153:mu, X154:mu, X155:mu, X156:$i]:((~(epred3_11 @ X156 @ X155 @ X154 @ X151 @ X153 @ X150 @ X149 @ X147 @ X148 @ X152 @ X146)|(~(seat @ X155 @ X156)|(~(furniture @ X155 @ X156)|(~(front @ X155 @ X156)|(~(seat @ X154 @ X156)|(~(furniture @ X154 @ X156)|(~(front @ X154 @ X156)|(~(hollywood @ X153 @ X156)|(~(city @ X153 @ X156)|(~(event @ X152 @ X156)|(~(street @ X148 @ X156)|(~(way @ X148 @ X156)|(~(lonely @ X148 @ X156)|(~(chevy @ X147 @ X156)|(~(car @ X147 @ X156)|(~(white @ X147 @ X156)|(~(dirty @ X147 @ X156)|(~(old @ X147 @ X156)|(~(barrel @ X152 @ X147 @ X156)|(~(down @ X152 @ X148 @ X156)|(~(in @ X152 @ X153 @ X156)|((qmltpeq @ X149 @ X150 @ X156)|(~(fellow @ X149 @ X156)|(~(man @ X149 @ X156)|(~(young @ X149 @ X156)|(~(fellow @ X150 @ X156)|(~(man @ X150 @ X156)|(~(young @ X150 @ X156)|(~(qmltpeq @ X149 @ X151 @ X156)|(~(in @ X151 @ X155 @ X156)|(~(qmltpeq @ X150 @ X146 @ X156)|~(in @ X146 @ X154 @ X156))))))))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])])).
% 0.21/0.35 thf(c_0_21, plain, ![X157:$i, X168:mu, X169:mu, X170:mu, X171:mu, X172:mu, X173:mu, X174:mu, X175:mu, X176:mu, X177:mu]:(((((exists_in_world @ (esk12_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk13_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk14_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk15_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk17_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk18_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk19_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk20_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((exists_in_world @ (esk21_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((seat @ (esk12_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((furniture @ (esk12_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((front @ (esk12_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((seat @ (esk13_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((furniture @ (esk13_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((front @ (esk13_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((hollywood @ (esk14_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((city @ (esk14_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((event @ (esk15_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((chevy @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((car @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((white @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((dirty @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((old @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((street @ (esk17_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((way @ (esk17_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((lonely @ (esk17_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((barrel @ (esk15_1 @ X157) @ (esk16_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((down @ (esk15_1 @ X157) @ (esk17_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((in @ (esk15_1 @ X157) @ (esk14_1 @ X157) @ X157)|~(epred4_1 @ X157))&((~(qmltpeq @ (esk18_1 @ X157) @ (esk19_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((fellow @ (esk18_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((man @ (esk18_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((young @ (esk18_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((fellow @ (esk19_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((man @ (esk19_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((young @ (esk19_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((qmltpeq @ (esk18_1 @ X157) @ (esk20_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((in @ (esk20_1 @ X157) @ (esk12_1 @ X157) @ X157)|~(epred4_1 @ X157))&(((qmltpeq @ (esk19_1 @ X157) @ (esk21_1 @ X157) @ X157)|~(epred4_1 @ X157))&((in @ (esk21_1 @ X157) @ (esk13_1 @ X157) @ X157)|~(epred4_1 @ X157))))))))))))))))))))))))))))))))))))))))))&(~(exists_in_world @ X168 @ X157)|(~(exists_in_world @ X169 @ X157)|(~(exists_in_world @ X170 @ X157)|(~(exists_in_world @ X171 @ X157)|(~(exists_in_world @ X172 @ X157)|(~(exists_in_world @ X173 @ X157)|(~(exists_in_world @ X174 @ X157)|(~(exists_in_world @ X175 @ X157)|(~(exists_in_world @ X176 @ X157)|(~(exists_in_world @ X177 @ X157)|(epred3_11 @ X157 @ X168 @ X169 @ X176 @ X170 @ X175 @ X174 @ X173 @ X172 @ X171 @ X177))))))))))|~(epred4_1 @ X157)))), 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_17])])])])])])).
% 0.21/0.35 thf(c_0_22, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X22:mu, X21:mu, X25:mu, X24:mu, X23:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ X12 @ X3)|~((qmltpeq @ X10 @ X14 @ X3))|~((qmltpeq @ X12 @ X19 @ X3))|~((in @ X19 @ X20 @ X3))|~((in @ X21 @ X22 @ X3))|~((in @ X14 @ X23 @ X3))|~((down @ X21 @ X24 @ X3))|~((barrel @ X21 @ X25 @ X3))|~((young @ X10 @ X3))|~((young @ X12 @ X3))|~((man @ X10 @ X3))|~((man @ X12 @ X3))|~((fellow @ X10 @ X3))|~((fellow @ X12 @ X3))|~((old @ X25 @ X3))|~((dirty @ X25 @ X3))|~((white @ X25 @ X3))|~((car @ X25 @ X3))|~((chevy @ X25 @ X3))|~((lonely @ X24 @ X3))|~((way @ X24 @ X3))|~((street @ X24 @ X3))|~((event @ X21 @ X3))|~((city @ X22 @ X3))|~((hollywood @ X22 @ X3))|~((front @ X20 @ X3))|~((front @ X23 @ X3))|~((furniture @ X20 @ X3))|~((furniture @ X23 @ X3))|~((seat @ X20 @ X3))|~((seat @ X23 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X24 @ X3))|~((exists_in_world @ X25 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X23 @ X3))|~((epred2_1 @ X3)))), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 0.21/0.35 thf(c_0_23, plain, ![X3:$i]:(((in @ (esk11_1 @ X3) @ (esk3_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_24, plain, ![X3:$i]:(((exists_in_world @ (esk3_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_25, plain, ![X3:$i]:(((exists_in_world @ (esk11_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_26, plain, ![X3:$i]:(((seat @ (esk3_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_27, plain, ![X3:$i]:(((furniture @ (esk3_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_28, plain, ![X3:$i]:(((front @ (esk3_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_29, plain, ![X19:mu, X20:mu, X14:mu, X23:mu, X22:mu, X24:mu, X25:mu, X21:mu, X12:mu, X10:mu, X3:$i]:(((qmltpeq @ X21 @ X20 @ X3)|~((epred3_11 @ X3 @ X10 @ X12 @ X14 @ X19 @ X20 @ X21 @ X22 @ X23 @ X24 @ X25))|~((seat @ X10 @ X3))|~((furniture @ X10 @ X3))|~((front @ X10 @ X3))|~((seat @ X12 @ X3))|~((furniture @ X12 @ X3))|~((front @ X12 @ X3))|~((hollywood @ X19 @ X3))|~((city @ X19 @ X3))|~((event @ X24 @ X3))|~((street @ X23 @ X3))|~((way @ X23 @ X3))|~((lonely @ X23 @ X3))|~((chevy @ X22 @ X3))|~((car @ X22 @ X3))|~((white @ X22 @ X3))|~((dirty @ X22 @ X3))|~((old @ X22 @ X3))|~((barrel @ X24 @ X22 @ X3))|~((down @ X24 @ X23 @ X3))|~((in @ X24 @ X19 @ X3))|~((fellow @ X21 @ X3))|~((man @ X21 @ X3))|~((young @ X21 @ X3))|~((fellow @ X20 @ X3))|~((man @ X20 @ X3))|~((young @ X20 @ X3))|~((qmltpeq @ X21 @ X14 @ X3))|~((in @ X14 @ X10 @ X3))|~((qmltpeq @ X20 @ X25 @ X3))|~((in @ X25 @ X12 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.35 thf(c_0_30, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X21:mu, X22:mu, X23:mu, X24:mu, X25:mu, X10:mu, X3:$i]:(((epred3_11 @ X3 @ X10 @ X12 @ X24 @ X14 @ X23 @ X22 @ X21 @ X20 @ X19 @ X25)|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X23 @ X3))|~((exists_in_world @ X24 @ X3))|~((exists_in_world @ X25 @ X3))|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_31, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X23:mu, X22:mu, X21:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ X12 @ X3)|~((qmltpeq @ X12 @ (esk11_1 @ X3) @ X3))|~((qmltpeq @ X10 @ X14 @ X3))|~((in @ X19 @ X20 @ X3))|~((in @ X14 @ X21 @ X3))|~((down @ X19 @ X22 @ X3))|~((barrel @ X19 @ X23 @ X3))|~((young @ X10 @ X3))|~((young @ X12 @ X3))|~((man @ X10 @ X3))|~((man @ X12 @ X3))|~((fellow @ X10 @ X3))|~((fellow @ X12 @ X3))|~((old @ X23 @ X3))|~((dirty @ X23 @ X3))|~((white @ X23 @ X3))|~((car @ X23 @ X3))|~((chevy @ X23 @ X3))|~((lonely @ X22 @ X3))|~((way @ X22 @ X3))|~((street @ X22 @ X3))|~((event @ X19 @ X3))|~((city @ X20 @ X3))|~((hollywood @ X20 @ X3))|~((front @ X21 @ X3))|~((furniture @ X21 @ X3))|~((seat @ X21 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X23 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X21 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24]), c_0_25]), c_0_26]), c_0_27]), c_0_28])).
% 0.21/0.35 thf(c_0_32, plain, ![X3:$i]:(((qmltpeq @ (esk9_1 @ X3) @ (esk11_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_33, plain, ![X3:$i]:(((exists_in_world @ (esk9_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_34, plain, ![X3:$i]:(((fellow @ (esk9_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_35, plain, ![X3:$i]:(((man @ (esk9_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_36, plain, ![X3:$i]:(((young @ (esk9_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_37, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X22:mu, X21:mu, X25:mu, X24:mu, X23:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ X12 @ X3)|~((qmltpeq @ X10 @ X14 @ X3))|~((qmltpeq @ X12 @ X19 @ X3))|~((in @ X19 @ X20 @ X3))|~((in @ X21 @ X22 @ X3))|~((in @ X14 @ X23 @ X3))|~((down @ X21 @ X24 @ X3))|~((barrel @ X21 @ X25 @ X3))|~((young @ X10 @ X3))|~((young @ X12 @ X3))|~((man @ X10 @ X3))|~((man @ X12 @ X3))|~((fellow @ X10 @ X3))|~((fellow @ X12 @ X3))|~((old @ X25 @ X3))|~((dirty @ X25 @ X3))|~((white @ X25 @ X3))|~((car @ X25 @ X3))|~((chevy @ X25 @ X3))|~((lonely @ X24 @ X3))|~((way @ X24 @ X3))|~((street @ X24 @ X3))|~((event @ X21 @ X3))|~((city @ X22 @ X3))|~((hollywood @ X22 @ X3))|~((front @ X20 @ X3))|~((front @ X23 @ X3))|~((furniture @ X20 @ X3))|~((furniture @ X23 @ X3))|~((seat @ X20 @ X3))|~((seat @ X23 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X25 @ X3))|~((exists_in_world @ X24 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X23 @ X3))|~((epred4_1 @ X3)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.21/0.35 thf(c_0_38, plain, ![X3:$i]:(((in @ (esk21_1 @ X3) @ (esk13_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_39, plain, ![X3:$i]:(((exists_in_world @ (esk13_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_40, plain, ![X3:$i]:(((exists_in_world @ (esk21_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_41, plain, ![X3:$i]:(((seat @ (esk13_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_42, plain, ![X3:$i]:(((furniture @ (esk13_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_43, plain, ![X3:$i]:(((front @ (esk13_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_44, plain, ![X12:mu, X14:mu, X19:mu, X22:mu, X21:mu, X20:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk9_1 @ X3) @ X3)|~((qmltpeq @ X10 @ X12 @ X3))|~((in @ X14 @ X19 @ X3))|~((in @ X12 @ X20 @ X3))|~((down @ X14 @ X21 @ X3))|~((barrel @ X14 @ X22 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X22 @ X3))|~((dirty @ X22 @ X3))|~((white @ X22 @ X3))|~((car @ X22 @ X3))|~((chevy @ X22 @ X3))|~((lonely @ X21 @ X3))|~((way @ X21 @ X3))|~((street @ X21 @ X3))|~((event @ X14 @ X3))|~((city @ X19 @ X3))|~((hollywood @ X19 @ X3))|~((front @ X20 @ X3))|~((furniture @ X20 @ X3))|~((seat @ X20 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33]), c_0_34]), c_0_35]), c_0_36])).
% 0.21/0.35 thf(c_0_45, plain, ![X3:$i]:(((in @ (esk5_1 @ X3) @ (esk4_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_46, plain, ![X3:$i]:(((exists_in_world @ (esk4_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_47, plain, ![X3:$i]:(((exists_in_world @ (esk5_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_48, plain, ![X3:$i]:(((hollywood @ (esk4_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_49, plain, ![X3:$i]:(((city @ (esk4_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_50, plain, ![X3:$i]:(((event @ (esk5_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_51, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X23:mu, X22:mu, X21:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ X12 @ X3)|~((qmltpeq @ X12 @ (esk21_1 @ X3) @ X3))|~((qmltpeq @ X10 @ X14 @ X3))|~((in @ X19 @ X20 @ X3))|~((in @ X14 @ X21 @ X3))|~((down @ X19 @ X22 @ X3))|~((barrel @ X19 @ X23 @ X3))|~((young @ X10 @ X3))|~((young @ X12 @ X3))|~((man @ X10 @ X3))|~((man @ X12 @ X3))|~((fellow @ X10 @ X3))|~((fellow @ X12 @ X3))|~((old @ X23 @ X3))|~((dirty @ X23 @ X3))|~((white @ X23 @ X3))|~((car @ X23 @ X3))|~((chevy @ X23 @ X3))|~((lonely @ X22 @ X3))|~((way @ X22 @ X3))|~((street @ X22 @ X3))|~((event @ X19 @ X3))|~((city @ X20 @ X3))|~((hollywood @ X20 @ X3))|~((front @ X21 @ X3))|~((furniture @ X21 @ X3))|~((seat @ X21 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X23 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((exists_in_world @ X21 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40]), c_0_41]), c_0_42]), c_0_43])).
% 0.21/0.35 thf(c_0_52, plain, ![X3:$i]:(((qmltpeq @ (esk19_1 @ X3) @ (esk21_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_53, plain, ![X3:$i]:(((exists_in_world @ (esk19_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_54, plain, ![X3:$i]:(((fellow @ (esk19_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_55, plain, ![X3:$i]:(((man @ (esk19_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_56, plain, ![X3:$i]:(((young @ (esk19_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_57, plain, ((mexists_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X69:mu]:((((exists_in_world @ X69 @ Z1))=>((~((Z0 @ X69 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[mexists_ind])).
% 0.21/0.35 thf(c_0_58, 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.21/0.35 thf(c_0_59, plain, ((mnot)=(^[Z0:$i > $o, Z1:$i]:(~((Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[mnot])).
% 0.21/0.35 thf(c_0_60, plain, ((mimplies)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((~((Z0 @ Z2))))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mimplies])).
% 0.21/0.35 thf(c_0_61, plain, ((mor)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:((((Z0 @ Z2))|((Z1 @ Z2)))))), inference(fof_simplification,[status(thm)],[mor])).
% 0.21/0.35 thf(c_0_62, plain, ((mand)=(^[Z0:$i > $o, Z1:$i > $o, Z2:$i]:(~(((((~((Z0 @ Z2))))|((~((Z1 @ Z2)))))))))), inference(fof_simplification,[status(thm)],[mand])).
% 0.21/0.35 thf(c_0_63, plain, ![X12:mu, X14:mu, X19:mu, X20:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk9_1 @ X3) @ X3)|~((down @ (esk5_1 @ X3) @ X12 @ X3))|~((barrel @ (esk5_1 @ X3) @ X14 @ X3))|~((qmltpeq @ X10 @ X19 @ X3))|~((in @ X19 @ X20 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X14 @ X3))|~((dirty @ X14 @ X3))|~((white @ X14 @ X3))|~((car @ X14 @ X3))|~((chevy @ X14 @ X3))|~((lonely @ X12 @ X3))|~((way @ X12 @ X3))|~((street @ X12 @ X3))|~((front @ X20 @ X3))|~((furniture @ X20 @ X3))|~((seat @ X20 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X20 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_45]), c_0_46]), c_0_47]), c_0_48]), c_0_49]), c_0_50])).
% 0.21/0.35 thf(c_0_64, plain, ![X3:$i]:(((down @ (esk5_1 @ X3) @ (esk6_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_65, plain, ![X3:$i]:(((exists_in_world @ (esk6_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_66, plain, ![X3:$i]:(((street @ (esk6_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_67, plain, ![X3:$i]:(((way @ (esk6_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_68, plain, ![X3:$i]:(((lonely @ (esk6_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_69, plain, ![X12:mu, X14:mu, X19:mu, X22:mu, X21:mu, X20:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk19_1 @ X3) @ X3)|~((qmltpeq @ X10 @ X12 @ X3))|~((in @ X14 @ X19 @ X3))|~((in @ X12 @ X20 @ X3))|~((down @ X14 @ X21 @ X3))|~((barrel @ X14 @ X22 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X22 @ X3))|~((dirty @ X22 @ X3))|~((white @ X22 @ X3))|~((car @ X22 @ X3))|~((chevy @ X22 @ X3))|~((lonely @ X21 @ X3))|~((way @ X21 @ X3))|~((street @ X21 @ X3))|~((event @ X14 @ X3))|~((city @ X19 @ X3))|~((hollywood @ X19 @ X3))|~((front @ X20 @ X3))|~((furniture @ X20 @ X3))|~((seat @ X20 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X22 @ X3))|~((exists_in_world @ X21 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X20 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56])).
% 0.21/0.35 thf(c_0_70, plain, ![X3:$i]:(((in @ (esk15_1 @ X3) @ (esk14_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_71, plain, ![X3:$i]:(((exists_in_world @ (esk14_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_72, plain, ![X3:$i]:(((exists_in_world @ (esk15_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_73, plain, ![X3:$i]:(((hollywood @ (esk14_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_74, plain, ![X3:$i]:(((city @ (esk14_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_75, plain, ![X3:$i]:(((event @ (esk15_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_76, negated_conjecture, ~((mvalid @ (mand @ (mimplies @ (mexists_ind @ (^[X29:mu]:(mexists_ind @ (^[X30:mu]:(mexists_ind @ (^[X31:mu]:(mexists_ind @ (^[X32:mu]:(mexists_ind @ (^[X33:mu]:(mexists_ind @ (^[X25:mu]:(mexists_ind @ (^[X34:mu]:(mexists_ind @ (^[X35:mu]:(mexists_ind @ (^[X36:mu]:(mexists_ind @ (^[X37:mu]:(mand @ (seat @ X29) @ (mand @ (furniture @ X29) @ (mand @ (front @ X29) @ (mand @ (seat @ X30) @ (mand @ (furniture @ X30) @ (mand @ (front @ X30) @ (mand @ (hollywood @ X31) @ (mand @ (city @ X31) @ (mand @ (event @ X32) @ (mand @ (street @ X33) @ (mand @ (way @ X33) @ (mand @ (lonely @ X33) @ (mand @ (chevy @ X25) @ (mand @ (car @ X25) @ (mand @ (white @ X25) @ (mand @ (dirty @ X25) @ (mand @ (old @ X25) @ (mand @ (barrel @ X32 @ X25) @ (mand @ (down @ X32 @ X33) @ (mand @ (in @ X32 @ X31) @ (mand @ (mnot @ (qmltpeq @ X34 @ X35)) @ (mand @ (fellow @ X34) @ (mand @ (man @ X34) @ (mand @ (young @ X34) @ (mand @ (fellow @ X35) @ (mand @ (man @ X35) @ (mand @ (young @ X35) @ (mand @ (qmltpeq @ X34 @ X36) @ (mand @ (in @ X36 @ X29) @ (mand @ (qmltpeq @ X35 @ X37) @ (in @ X37 @ X30))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mexists_ind @ (^[X38:mu]:(mexists_ind @ (^[X39:mu]:(mexists_ind @ (^[X40:mu]:(mexists_ind @ (^[X41:mu]:(mexists_ind @ (^[X42:mu]:(mexists_ind @ (^[X43:mu]:(mexists_ind @ (^[X44:mu]:(mexists_ind @ (^[X45:mu]:(mexists_ind @ (^[X46:mu]:(mexists_ind @ (^[X47:mu]:(mand @ (seat @ X38) @ (mand @ (furniture @ X38) @ (mand @ (front @ X38) @ (mand @ (seat @ X39) @ (mand @ (furniture @ X39) @ (mand @ (front @ X39) @ (mand @ (hollywood @ X40) @ (mand @ (city @ X40) @ (mand @ (event @ X41) @ (mand @ (chevy @ X42) @ (mand @ (car @ X42) @ (mand @ (white @ X42) @ (mand @ (dirty @ X42) @ (mand @ (old @ X42) @ (mand @ (street @ X43) @ (mand @ (way @ X43) @ (mand @ (lonely @ X43) @ (mand @ (barrel @ X41 @ X42) @ (mand @ (down @ X41 @ X43) @ (mand @ (in @ X41 @ X40) @ (mand @ (mnot @ (qmltpeq @ X44 @ X45)) @ (mand @ (fellow @ X44) @ (mand @ (man @ X44) @ (mand @ (young @ X44) @ (mand @ (fellow @ X45) @ (mand @ (man @ X45) @ (mand @ (young @ X45) @ (mand @ (qmltpeq @ X44 @ X46) @ (mand @ (in @ X46 @ X38) @ (mand @ (qmltpeq @ X45 @ X47) @ (in @ X47 @ X39)))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mimplies @ (mexists_ind @ (^[X48:mu]:(mexists_ind @ (^[X49:mu]:(mexists_ind @ (^[X50:mu]:(mexists_ind @ (^[X51:mu]:(mexists_ind @ (^[X52:mu]:(mexists_ind @ (^[X53:mu]:(mexists_ind @ (^[X54:mu]:(mexists_ind @ (^[X55:mu]:(mexists_ind @ (^[X56:mu]:(mexists_ind @ (^[X57:mu]:(mand @ (seat @ X48) @ (mand @ (furniture @ X48) @ (mand @ (front @ X48) @ (mand @ (seat @ X49) @ (mand @ (furniture @ X49) @ (mand @ (front @ X49) @ (mand @ (hollywood @ X50) @ (mand @ (city @ X50) @ (mand @ (event @ X51) @ (mand @ (chevy @ X52) @ (mand @ (car @ X52) @ (mand @ (white @ X52) @ (mand @ (dirty @ X52) @ (mand @ (old @ X52) @ (mand @ (street @ X53) @ (mand @ (way @ X53) @ (mand @ (lonely @ X53) @ (mand @ (barrel @ X51 @ X52) @ (mand @ (down @ X51 @ X53) @ (mand @ (in @ X51 @ X50) @ (mand @ (mnot @ (qmltpeq @ X54 @ X55)) @ (mand @ (fellow @ X54) @ (mand @ (man @ X54) @ (mand @ (young @ X54) @ (mand @ (fellow @ X55) @ (mand @ (man @ X55) @ (mand @ (young @ X55) @ (mand @ (qmltpeq @ X54 @ X56) @ (mand @ (in @ X56 @ X48) @ (mand @ (qmltpeq @ X55 @ X57) @ (in @ X57 @ X49))))))))))))))))))))))))))))))))))))))))))))))))))) @ (mexists_ind @ (^[X58:mu]:(mexists_ind @ (^[X59:mu]:(mexists_ind @ (^[X60:mu]:(mexists_ind @ (^[X61:mu]:(mexists_ind @ (^[X62:mu]:(mexists_ind @ (^[X63:mu]:(mexists_ind @ (^[X64:mu]:(mexists_ind @ (^[X65:mu]:(mexists_ind @ (^[X66:mu]:(mexists_ind @ (^[X67:mu]:(mand @ (seat @ X58) @ (mand @ (furniture @ X58) @ (mand @ (front @ X58) @ (mand @ (seat @ X59) @ (mand @ (furniture @ X59) @ (mand @ (front @ X59) @ (mand @ (hollywood @ X60) @ (mand @ (city @ X60) @ (mand @ (event @ X61) @ (mand @ (street @ X62) @ (mand @ (way @ X62) @ (mand @ (lonely @ X62) @ (mand @ (chevy @ X63) @ (mand @ (car @ X63) @ (mand @ (white @ X63) @ (mand @ (dirty @ X63) @ (mand @ (old @ X63) @ (mand @ (barrel @ X61 @ X63) @ (mand @ (down @ X61 @ X62) @ (mand @ (in @ X61 @ X60) @ (mand @ (mnot @ (qmltpeq @ X64 @ X65)) @ (mand @ (fellow @ X64) @ (mand @ (man @ X64) @ (mand @ (young @ X64) @ (mand @ (fellow @ X65) @ (mand @ (man @ X65) @ (mand @ (young @ X65) @ (mand @ (qmltpeq @ X64 @ X66) @ (mand @ (in @ X66 @ X58) @ (mand @ (qmltpeq @ X65 @ X67) @ (in @ X67 @ X59))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[co1])).
% 0.21/0.35 thf(c_0_77, plain, ((mexists_ind)=(^[Z0:mu > $i > $o, Z1:$i]:(~((![X69:mu]:((((exists_in_world @ X69 @ Z1))=>((~((Z0 @ X69 @ Z1))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_57, c_0_58]), c_0_59])).
% 0.21/0.35 thf(c_0_78, plain, ((mvalid)=(^[Z0:$i > $o]:(![X3:$i]:((Z0 @ X3))))), inference(fof_simplification,[status(thm)],[mvalid])).
% 0.21/0.35 thf(c_0_79, 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_60, c_0_61]), c_0_59])).
% 0.21/0.35 thf(c_0_80, 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_62, c_0_61]), c_0_59])).
% 0.21/0.35 thf(c_0_81, plain, ![X12:mu, X14:mu, X19:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk9_1 @ X3) @ X3)|~((barrel @ (esk5_1 @ X3) @ X12 @ X3))|~((qmltpeq @ X10 @ X14 @ X3))|~((in @ X14 @ X19 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X12 @ X3))|~((dirty @ X12 @ X3))|~((white @ X12 @ X3))|~((car @ X12 @ X3))|~((chevy @ X12 @ X3))|~((front @ X19 @ X3))|~((furniture @ X19 @ X3))|~((seat @ X19 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X19 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_65]), c_0_66]), c_0_67]), c_0_68])).
% 0.21/0.35 thf(c_0_82, plain, ![X3:$i]:(((barrel @ (esk5_1 @ X3) @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_83, plain, ![X3:$i]:(((exists_in_world @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_84, plain, ![X3:$i]:(((chevy @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_85, plain, ![X3:$i]:(((car @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_86, plain, ![X3:$i]:(((white @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_87, plain, ![X3:$i]:(((dirty @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_88, plain, ![X3:$i]:(((old @ (esk7_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_89, plain, ![X12:mu, X19:mu, X14:mu, X20:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk19_1 @ X3) @ X3)|~((down @ (esk15_1 @ X3) @ X12 @ X3))|~((barrel @ (esk15_1 @ X3) @ X14 @ X3))|~((qmltpeq @ X10 @ X19 @ X3))|~((in @ X19 @ X20 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X14 @ X3))|~((dirty @ X14 @ X3))|~((white @ X14 @ X3))|~((car @ X14 @ X3))|~((chevy @ X14 @ X3))|~((lonely @ X12 @ X3))|~((way @ X12 @ X3))|~((street @ X12 @ X3))|~((front @ X20 @ X3))|~((furniture @ X20 @ X3))|~((seat @ X20 @ X3))|~((exists_in_world @ X19 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X20 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_70]), c_0_71]), c_0_72]), c_0_73]), c_0_74]), c_0_75])).
% 0.21/0.35 thf(c_0_90, plain, ![X3:$i]:(((down @ (esk15_1 @ X3) @ (esk17_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_91, plain, ![X3:$i]:(((exists_in_world @ (esk17_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_92, plain, ![X3:$i]:(((street @ (esk17_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_93, plain, ![X3:$i]:(((way @ (esk17_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_94, plain, ![X3:$i]:(((lonely @ (esk17_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_95, negated_conjecture, ~(![X112:$i]:(~(((epred2_1 @ X112)|(epred4_1 @ X112))))), inference(apply_def,[status(thm)],[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(fof_simplification,[status(thm)],[c_0_76]), c_0_77]), c_0_78]), c_0_79]), c_0_80]), c_0_59])]), c_0_9]), c_0_13])).
% 0.21/0.35 thf(c_0_96, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk9_1 @ X3) @ X3)|~((qmltpeq @ X10 @ X12 @ X3))|~((in @ X12 @ X14 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((front @ X14 @ X3))|~((furniture @ X14 @ X3))|~((seat @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X14 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_82]), c_0_83]), c_0_84]), c_0_85]), c_0_86]), c_0_87]), c_0_88])).
% 0.21/0.35 thf(c_0_97, plain, ![X3:$i]:(((in @ (esk10_1 @ X3) @ (esk2_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_98, plain, ![X3:$i]:(((exists_in_world @ (esk2_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_99, plain, ![X3:$i]:(((exists_in_world @ (esk10_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_100, plain, ![X3:$i]:(((seat @ (esk2_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_101, plain, ![X3:$i]:(((furniture @ (esk2_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_102, plain, ![X3:$i]:(((front @ (esk2_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_103, plain, ![X12:mu, X14:mu, X19:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk19_1 @ X3) @ X3)|~((barrel @ (esk15_1 @ X3) @ X12 @ X3))|~((qmltpeq @ X10 @ X14 @ X3))|~((in @ X14 @ X19 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((old @ X12 @ X3))|~((dirty @ X12 @ X3))|~((white @ X12 @ X3))|~((car @ X12 @ X3))|~((chevy @ X12 @ X3))|~((front @ X19 @ X3))|~((furniture @ X19 @ X3))|~((seat @ X19 @ X3))|~((exists_in_world @ X14 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X19 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_90]), c_0_91]), c_0_92]), c_0_93]), c_0_94])).
% 0.21/0.35 thf(c_0_104, plain, ![X3:$i]:(((barrel @ (esk15_1 @ X3) @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_105, plain, ![X3:$i]:(((exists_in_world @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_106, plain, ![X3:$i]:(((chevy @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_107, plain, ![X3:$i]:(((car @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_108, plain, ![X3:$i]:(((white @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_109, plain, ![X3:$i]:(((dirty @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_110, plain, ![X3:$i]:(((old @ (esk16_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_111, negated_conjecture, ((epred2_1 @ esk1_0)|(epred4_1 @ esk1_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_95])])])).
% 0.21/0.35 thf(c_0_112, plain, ![X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk9_1 @ X3) @ X3)|~((qmltpeq @ X10 @ (esk10_1 @ X3) @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((exists_in_world @ X10 @ X3))|~((epred2_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_98]), c_0_99]), c_0_100]), c_0_101]), c_0_102])).
% 0.21/0.35 thf(c_0_113, plain, ![X3:$i]:(((qmltpeq @ (esk8_1 @ X3) @ (esk10_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_114, plain, ![X3:$i]:(((exists_in_world @ (esk8_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_115, plain, ![X3:$i]:(((fellow @ (esk8_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_116, plain, ![X3:$i]:(((man @ (esk8_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_117, plain, ![X3:$i]:(((young @ (esk8_1 @ X3) @ X3)|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_118, plain, ![X3:$i]:((~((qmltpeq @ (esk8_1 @ X3) @ (esk9_1 @ X3) @ X3))|~((epred2_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.21/0.35 thf(c_0_119, plain, ![X12:mu, X14:mu, X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk19_1 @ X3) @ X3)|~((qmltpeq @ X10 @ X12 @ X3))|~((in @ X12 @ X14 @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((front @ X14 @ X3))|~((furniture @ X14 @ X3))|~((seat @ X14 @ X3))|~((exists_in_world @ X12 @ X3))|~((exists_in_world @ X10 @ X3))|~((exists_in_world @ X14 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_104]), c_0_105]), c_0_106]), c_0_107]), c_0_108]), c_0_109]), c_0_110])).
% 0.21/0.35 thf(c_0_120, plain, ![X3:$i]:(((in @ (esk20_1 @ X3) @ (esk12_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_121, plain, ![X3:$i]:(((exists_in_world @ (esk12_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_122, plain, ![X3:$i]:(((exists_in_world @ (esk20_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_123, plain, ![X3:$i]:(((seat @ (esk12_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_124, plain, ![X3:$i]:(((furniture @ (esk12_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_125, plain, ![X3:$i]:(((front @ (esk12_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_126, negated_conjecture, ((epred2_1 @ esk1_0)|(epred4_1 @ esk1_0)), inference(split_conjunct,[status(thm)],[c_0_111])).
% 0.21/0.35 thf(c_0_127, plain, ![X3:$i]:(~((epred2_1 @ X3))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_113]), c_0_114]), c_0_115]), c_0_116]), c_0_117]), c_0_118])).
% 0.21/0.35 thf(c_0_128, plain, ![X10:mu, X3:$i]:(((qmltpeq @ X10 @ (esk19_1 @ X3) @ X3)|~((qmltpeq @ X10 @ (esk20_1 @ X3) @ X3))|~((young @ X10 @ X3))|~((man @ X10 @ X3))|~((fellow @ X10 @ X3))|~((exists_in_world @ X10 @ X3))|~((epred4_1 @ X3)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_120]), c_0_121]), c_0_122]), c_0_123]), c_0_124]), c_0_125])).
% 0.21/0.35 thf(c_0_129, plain, ![X3:$i]:(((qmltpeq @ (esk18_1 @ X3) @ (esk20_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_130, plain, ![X3:$i]:(((exists_in_world @ (esk18_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_131, plain, ![X3:$i]:(((fellow @ (esk18_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_132, plain, ![X3:$i]:(((man @ (esk18_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_133, plain, ![X3:$i]:(((young @ (esk18_1 @ X3) @ X3)|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_134, plain, ![X3:$i]:((~((qmltpeq @ (esk18_1 @ X3) @ (esk19_1 @ X3) @ X3))|~((epred4_1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.35 thf(c_0_135, negated_conjecture, (epred4_1 @ esk1_0), inference(sr,[status(thm)],[c_0_126, c_0_127])).
% 0.21/0.35 thf(c_0_136, plain, ![X3:$i]:(~((epred4_1 @ X3))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_130]), c_0_131]), c_0_132]), c_0_133]), c_0_134])).
% 0.21/0.35 thf(c_0_137, negated_conjecture, ($false), inference(sr,[status(thm)],[c_0_135, c_0_136]), ['proof']).
% 0.21/0.35 % SZS output end CNFRefutation
% 0.21/0.35 % Parsed axioms : 119
% 0.21/0.35 % Removed by relevancy pruning/SinE : 86
% 0.21/0.35 % Initial clauses : 87
% 0.21/0.35 % Removed in clause preprocessing : 0
% 0.21/0.35 % Initial clauses in saturation : 87
% 0.21/0.35 % Processed clauses : 114
% 0.21/0.35 % ...of these trivial : 0
% 0.21/0.35 % ...subsumed : 0
% 0.21/0.35 % ...remaining for further processing : 114
% 0.21/0.35 % Other redundant clauses eliminated : 0
% 0.21/0.35 % Clauses deleted for lack of memory : 0
% 0.21/0.35 % Backward-subsumed : 108
% 0.21/0.35 % Backward-rewritten : 0
% 0.21/0.35 % Generated clauses : 46
% 0.21/0.35 % ...of the previous two non-redundant : 45
% 0.21/0.35 % ...aggressively subsumed : 0
% 0.21/0.35 % Contextual simplify-reflections : 104
% 0.21/0.35 % Paramodulations : 44
% 0.21/0.35 % Factorizations : 0
% 0.21/0.35 % NegExts : 0
% 0.21/0.35 % Equation resolutions : 0
% 0.21/0.35 % Disequality decompositions : 0
% 0.21/0.35 % Total rewrite steps : 0
% 0.21/0.35 % ...of those cached : 0
% 0.21/0.35 % Propositional unsat checks : 0
% 0.21/0.35 % Propositional check models : 0
% 0.21/0.35 % Propositional check unsatisfiable : 0
% 0.21/0.35 % Propositional clauses : 0
% 0.21/0.35 % Propositional clauses after purity: 0
% 0.21/0.35 % Propositional unsat core size : 0
% 0.21/0.35 % Propositional preprocessing time : 0.000
% 0.21/0.35 % Propositional encoding time : 0.000
% 0.21/0.35 % Propositional solver time : 0.000
% 0.21/0.35 % Success case prop preproc time : 0.000
% 0.21/0.35 % Success case prop encoding time : 0.000
% 0.21/0.35 % Success case prop solver time : 0.000
% 0.21/0.35 % Current number of processed clauses : 4
% 0.21/0.35 % Positive orientable unit clauses : 0
% 0.21/0.35 % Positive unorientable unit clauses: 0
% 0.21/0.35 % Negative unit clauses : 2
% 0.21/0.35 % Non-unit-clauses : 2
% 0.21/0.35 % Current number of unprocessed clauses: 6
% 0.21/0.35 % ...number of literals in the above : 214
% 0.21/0.35 % Current number of archived formulas : 0
% 0.21/0.35 % Current number of archived clauses : 110
% 0.21/0.35 % Clause-clause subsumption calls (NU) : 15985
% 0.21/0.35 % Rec. Clause-clause subsumption calls : 1673
% 0.21/0.35 % Non-unit clause-clause subsumptions : 114
% 0.21/0.35 % Unit Clause-clause subsumption calls : 152
% 0.21/0.35 % Rewrite failures with RHS unbound : 0
% 0.21/0.35 % BW rewrite match attempts : 0
% 0.21/0.35 % BW rewrite match successes : 0
% 0.21/0.35 % Condensation attempts : 0
% 0.21/0.35 % Condensation successes : 0
% 0.21/0.35 % Termbank termtop insertions : 60629
% 0.21/0.35 % Search garbage collected termcells : 23137
% 0.21/0.35
% 0.21/0.35 % -------------------------------------------------
% 0.21/0.35 % User time : 0.051 s
% 0.21/0.35 % System time : 0.010 s
% 0.21/0.35 % Total time : 0.061 s
% 0.21/0.35 % Maximum resident set size: 6896 pages
% 0.21/0.35
% 0.21/0.35 % -------------------------------------------------
% 0.21/0.35 % User time : 0.055 s
% 0.21/0.35 % System time : 0.016 s
% 0.21/0.35 % Total time : 0.071 s
% 0.21/0.35 % Maximum resident set size: 5120 pages
% 0.21/0.35 % E exiting
%------------------------------------------------------------------------------