%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ091^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:58:20 PM UTC 2025 % Result : Theorem 3.74s 3.91s % Output : Proof 3.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PUZ091^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n006.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 20:45:08 EDT 2025 % 0.13/0.35 % CPUTime : % 3.74/3.91 SZS status Theorem for theBenchmark.p % 3.74/3.91 SZS output start Proof for theBenchmark.p % 3.74/3.91 Clause #0 (by assumption #[]): Eq % 3.74/3.91 (Not % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.91 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.91 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.91 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.91 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.91 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.91 (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS) → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cRAVENOUS (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → cGAMBLER) → % 3.74/3.91 And cEARNEST cLOGICIAN → And cRISES_AT_FIVE (Not cIN_BED_BEFORE_FOUR))) % 3.74/3.91 True % 3.74/3.91 Clause #1 (by clausification #[0]): Eq % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.91 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.91 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.91 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.91 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.91 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.91 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.91 (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS) → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.91 (And (And cRAVENOUS (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → cGAMBLER) → % 3.74/3.91 And cEARNEST cLOGICIAN → And cRISES_AT_FIVE (Not cIN_BED_BEFORE_FOUR)) % 3.74/3.91 False % 3.74/3.91 Clause #2 (by clausification #[1]): Eq % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And % 3.74/3.91 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.92 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.92 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.92 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.92 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.92 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.92 (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS) → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cRAVENOUS (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → cGAMBLER)) % 3.74/3.92 True % 3.74/3.92 Clause #3 (by clausification #[1]): Eq (And cEARNEST cLOGICIAN → And cRISES_AT_FIVE (Not cIN_BED_BEFORE_FOUR)) False % 3.74/3.92 Clause #4 (by clausification #[2]): Eq (And (And cRAVENOUS (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → cGAMBLER) True % 3.74/3.92 Clause #5 (by clausification #[2]): Eq % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And % 3.74/3.92 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.92 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.92 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.92 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.92 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.92 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.92 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.92 (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS) → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.92 True % 3.74/3.92 Clause #6 (by clausification #[4]): Or (Eq (And (And cRAVENOUS (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY)) False) (Eq cGAMBLER True) % 3.74/3.92 Clause #7 (by clausification #[6]): Or (Eq cGAMBLER True) (Or (Eq (And cRAVENOUS (Not cLIVELY)) False) (Eq (Not cLIKELY_LOSE_MONEY) False)) % 3.74/3.92 Clause #8 (by clausification #[7]): Or (Eq cGAMBLER True) (Or (Eq (Not cLIKELY_LOSE_MONEY) False) (Or (Eq cRAVENOUS False) (Eq (Not cLIVELY) False))) % 3.74/3.92 Clause #9 (by clausification #[8]): Or (Eq cGAMBLER True) (Or (Eq cRAVENOUS False) (Or (Eq (Not cLIVELY) False) (Eq cLIKELY_LOSE_MONEY True))) % 3.74/3.92 Clause #10 (by clausification #[9]): Or (Eq cGAMBLER True) (Or (Eq cRAVENOUS False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))) % 3.74/3.92 Clause #11 (by clausification #[3]): Eq (And cEARNEST cLOGICIAN) True % 3.74/3.92 Clause #12 (by clausification #[3]): Eq (And cRISES_AT_FIVE (Not cIN_BED_BEFORE_FOUR)) False % 3.74/3.92 Clause #13 (by clausification #[11]): Eq cLOGICIAN True % 3.74/3.92 Clause #14 (by clausification #[11]): Eq cEARNEST True % 3.74/3.92 Clause #15 (by clausification #[12]): Or (Eq cRISES_AT_FIVE False) (Eq (Not cIN_BED_BEFORE_FOUR) False) % 3.74/3.93 Clause #16 (by clausification #[15]): Or (Eq cRISES_AT_FIVE False) (Eq cIN_BED_BEFORE_FOUR True) % 3.74/3.93 Clause #17 (by clausification #[5]): Eq (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS) → Not cBETTER_TAKE_TO_CAB_DRIVING) True % 3.74/3.93 Clause #18 (by clausification #[5]): Eq % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.93 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.93 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.93 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.93 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.93 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.93 (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 True % 3.74/3.93 Clause #19 (by clausification #[17]): Or (Eq (And (And cGAMBLER cIN_BED_BEFORE_FOUR) (Not cRAVENOUS)) False) (Eq (Not cBETTER_TAKE_TO_CAB_DRIVING) True) % 3.74/3.93 Clause #20 (by clausification #[19]): Or (Eq (Not cBETTER_TAKE_TO_CAB_DRIVING) True) % 3.74/3.93 (Or (Eq (And cGAMBLER cIN_BED_BEFORE_FOUR) False) (Eq (Not cRAVENOUS) False)) % 3.74/3.93 Clause #21 (by clausification #[20]): Or (Eq (And cGAMBLER cIN_BED_BEFORE_FOUR) False) (Or (Eq (Not cRAVENOUS) False) (Eq cBETTER_TAKE_TO_CAB_DRIVING False)) % 3.74/3.93 Clause #22 (by clausification #[21]): Or (Eq (Not cRAVENOUS) False) % 3.74/3.93 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING False) (Or (Eq cGAMBLER False) (Eq cIN_BED_BEFORE_FOUR False))) % 3.74/3.93 Clause #23 (by clausification #[22]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING False) % 3.74/3.93 (Or (Eq cGAMBLER False) (Or (Eq cIN_BED_BEFORE_FOUR False) (Eq cRAVENOUS True))) % 3.74/3.93 Clause #24 (by clausification #[18]): Eq (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE) → cBETTER_TAKE_TO_CAB_DRIVING) True % 3.74/3.93 Clause #25 (by clausification #[18]): Eq % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And % 3.74/3.93 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.93 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.93 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.93 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.93 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.93 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.93 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.93 (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR)) % 3.74/3.93 True % 3.74/3.93 Clause #26 (by clausification #[24]): Or (Eq (And (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) (Not cRISES_AT_FIVE)) False) % 3.74/3.93 (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.93 Clause #27 (by clausification #[26]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.95 (Or (Eq (And cHAS_LOST_MONEY (Not cEATS_PORKCHOPS)) False) (Eq (Not cRISES_AT_FIVE) False)) % 3.74/3.95 Clause #28 (by clausification #[27]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.95 (Or (Eq (Not cRISES_AT_FIVE) False) (Or (Eq cHAS_LOST_MONEY False) (Eq (Not cEATS_PORKCHOPS) False))) % 3.74/3.95 Clause #29 (by clausification #[28]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.95 (Or (Eq cHAS_LOST_MONEY False) (Or (Eq (Not cEATS_PORKCHOPS) False) (Eq cRISES_AT_FIVE True))) % 3.74/3.95 Clause #30 (by clausification #[29]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.95 (Or (Eq cHAS_LOST_MONEY False) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True))) % 3.74/3.95 Clause #31 (by clausification #[25]): Eq (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY) → Not cIN_BED_BEFORE_FOUR) True % 3.74/3.95 Clause #32 (by clausification #[25]): Eq % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.95 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.95 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.95 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.95 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.95 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.95 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.95 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.95 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.95 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.95 (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.95 True % 3.74/3.95 Clause #33 (by clausification #[31]): Or (Eq (And (And cGAMBLER (Not cLIVELY)) (Not cLIKELY_LOSE_MONEY)) False) (Eq (Not cIN_BED_BEFORE_FOUR) True) % 3.74/3.95 Clause #34 (by clausification #[33]): Or (Eq (Not cIN_BED_BEFORE_FOUR) True) (Or (Eq (And cGAMBLER (Not cLIVELY)) False) (Eq (Not cLIKELY_LOSE_MONEY) False)) % 3.74/3.95 Clause #35 (by clausification #[34]): Or (Eq (And cGAMBLER (Not cLIVELY)) False) (Or (Eq (Not cLIKELY_LOSE_MONEY) False) (Eq cIN_BED_BEFORE_FOUR False)) % 3.74/3.95 Clause #36 (by clausification #[35]): Or (Eq (Not cLIKELY_LOSE_MONEY) False) % 3.74/3.95 (Or (Eq cIN_BED_BEFORE_FOUR False) (Or (Eq cGAMBLER False) (Eq (Not cLIVELY) False))) % 3.74/3.95 Clause #37 (by clausification #[36]): Or (Eq cIN_BED_BEFORE_FOUR False) (Or (Eq cGAMBLER False) (Or (Eq (Not cLIVELY) False) (Eq cLIKELY_LOSE_MONEY True))) % 3.74/3.95 Clause #38 (by clausification #[37]): Or (Eq cIN_BED_BEFORE_FOUR False) (Or (Eq cGAMBLER False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))) % 3.74/3.95 Clause #39 (by clausification #[32]): Eq (And cRAVENOUS cEARNEST → Not cBETTER_TAKE_TO_CAB_DRIVING) True % 3.74/3.95 Clause #40 (by clausification #[32]): Eq % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And % 3.74/3.95 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.95 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.95 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.95 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.95 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.95 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.95 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.95 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.95 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.95 (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY)) % 3.74/3.95 True % 3.74/3.95 Clause #41 (by clausification #[39]): Or (Eq (And cRAVENOUS cEARNEST) False) (Eq (Not cBETTER_TAKE_TO_CAB_DRIVING) True) % 3.74/3.95 Clause #42 (by clausification #[41]): Or (Eq (Not cBETTER_TAKE_TO_CAB_DRIVING) True) (Or (Eq cRAVENOUS False) (Eq cEARNEST False)) % 3.74/3.96 Clause #43 (by clausification #[42]): Or (Eq cRAVENOUS False) (Or (Eq cEARNEST False) (Eq cBETTER_TAKE_TO_CAB_DRIVING False)) % 3.74/3.96 Clause #44 (by clausification #[40]): Eq (And (And cLIVELY cLOGICIAN) cEARNEST → Not cLIKELY_LOSE_MONEY) True % 3.74/3.96 Clause #45 (by clausification #[40]): Eq % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.96 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.96 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.96 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.96 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.96 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.96 (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY)) % 3.74/3.96 True % 3.74/3.96 Clause #46 (by clausification #[44]): Or (Eq (And (And cLIVELY cLOGICIAN) cEARNEST) False) (Eq (Not cLIKELY_LOSE_MONEY) True) % 3.74/3.96 Clause #47 (by clausification #[46]): Or (Eq (Not cLIKELY_LOSE_MONEY) True) (Or (Eq (And cLIVELY cLOGICIAN) False) (Eq cEARNEST False)) % 3.74/3.96 Clause #48 (by clausification #[47]): Or (Eq (And cLIVELY cLOGICIAN) False) (Or (Eq cEARNEST False) (Eq cLIKELY_LOSE_MONEY False)) % 3.74/3.96 Clause #49 (by clausification #[48]): Or (Eq cEARNEST False) (Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq cLIVELY False) (Eq cLOGICIAN False))) % 3.74/3.96 Clause #50 (by forward demodulation #[49, 14]): Or (Eq True False) (Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq cLIVELY False) (Eq cLOGICIAN False))) % 3.74/3.96 Clause #51 (by clausification #[50]): Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq cLIVELY False) (Eq cLOGICIAN False)) % 3.74/3.96 Clause #52 (by clausification #[45]): Eq (And (Not cGAMBLER) (Not cRAVENOUS) → cLIVELY) True % 3.74/3.96 Clause #53 (by clausification #[45]): Eq % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.96 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.96 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.96 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.96 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.96 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY)) % 3.74/3.96 True % 3.74/3.96 Clause #54 (by clausification #[52]): Or (Eq (And (Not cGAMBLER) (Not cRAVENOUS)) False) (Eq cLIVELY True) % 3.74/3.96 Clause #55 (by clausification #[54]): Or (Eq cLIVELY True) (Or (Eq (Not cGAMBLER) False) (Eq (Not cRAVENOUS) False)) % 3.74/3.96 Clause #56 (by clausification #[55]): Or (Eq cLIVELY True) (Or (Eq (Not cRAVENOUS) False) (Eq cGAMBLER True)) % 3.74/3.96 Clause #57 (by clausification #[56]): Or (Eq cLIVELY True) (Or (Eq cGAMBLER True) (Eq cRAVENOUS True)) % 3.74/3.96 Clause #58 (by clausification #[53]): Eq (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY) → Not cLIKELY_LOSE_MONEY) True % 3.74/3.96 Clause #59 (by clausification #[53]): Eq % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And % 3.74/3.96 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) % 3.74/3.96 (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.96 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.96 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.96 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.96 (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.96 True % 3.74/3.96 Clause #60 (by clausification #[58]): Or (Eq (And (And (And cEARNEST (Not cLIVELY)) cGAMBLER) (Not cHAS_LOST_MONEY)) False) (Eq (Not cLIKELY_LOSE_MONEY) True) % 3.74/3.98 Clause #61 (by clausification #[60]): Or (Eq (Not cLIKELY_LOSE_MONEY) True) % 3.74/3.98 (Or (Eq (And (And cEARNEST (Not cLIVELY)) cGAMBLER) False) (Eq (Not cHAS_LOST_MONEY) False)) % 3.74/3.98 Clause #62 (by clausification #[61]): Or (Eq (And (And cEARNEST (Not cLIVELY)) cGAMBLER) False) % 3.74/3.98 (Or (Eq (Not cHAS_LOST_MONEY) False) (Eq cLIKELY_LOSE_MONEY False)) % 3.74/3.98 Clause #63 (by clausification #[62]): Or (Eq (Not cHAS_LOST_MONEY) False) % 3.74/3.98 (Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq (And cEARNEST (Not cLIVELY)) False) (Eq cGAMBLER False))) % 3.74/3.98 Clause #64 (by clausification #[63]): Or (Eq cLIKELY_LOSE_MONEY False) % 3.74/3.98 (Or (Eq (And cEARNEST (Not cLIVELY)) False) (Or (Eq cGAMBLER False) (Eq cHAS_LOST_MONEY True))) % 3.74/3.98 Clause #65 (by clausification #[64]): Or (Eq cLIKELY_LOSE_MONEY False) % 3.74/3.98 (Or (Eq cGAMBLER False) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Eq (Not cLIVELY) False)))) % 3.74/3.98 Clause #66 (by clausification #[65]): Or (Eq cLIKELY_LOSE_MONEY False) % 3.74/3.98 (Or (Eq cGAMBLER False) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Eq cLIVELY True)))) % 3.74/3.98 Clause #67 (by clausification #[59]): Eq (And cLOGICIAN cLIKELY_LOSE_MONEY → cBETTER_TAKE_TO_CAB_DRIVING) True % 3.74/3.98 Clause #68 (by clausification #[59]): Eq % 3.74/3.98 (And % 3.74/3.98 (And % 3.74/3.98 (And % 3.74/3.98 (And % 3.74/3.98 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.98 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.98 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.98 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.98 (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS)) % 3.74/3.98 True % 3.74/3.98 Clause #69 (by clausification #[67]): Or (Eq (And cLOGICIAN cLIKELY_LOSE_MONEY) False) (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.74/3.98 Clause #70 (by clausification #[69]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cLOGICIAN False) (Eq cLIKELY_LOSE_MONEY False)) % 3.74/3.98 Clause #71 (by superposition #[70, 13]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cLIKELY_LOSE_MONEY False) (Eq False True)) % 3.74/3.98 Clause #72 (by clausification #[71]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cLIKELY_LOSE_MONEY False) % 3.74/3.98 Clause #73 (by clausification #[68]): Eq (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE) → cEATS_PORKCHOPS) True % 3.74/3.98 Clause #74 (by clausification #[68]): Eq % 3.74/3.98 (And % 3.74/3.98 (And % 3.74/3.98 (And % 3.74/3.98 (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.98 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.98 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.98 (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING)) % 3.74/3.98 True % 3.74/3.98 Clause #75 (by clausification #[73]): Or (Eq (And (And cRAVENOUS (Not cHAS_LOST_MONEY)) (Not cRISES_AT_FIVE)) False) (Eq cEATS_PORKCHOPS True) % 3.74/3.98 Clause #76 (by clausification #[75]): Or (Eq cEATS_PORKCHOPS True) (Or (Eq (And cRAVENOUS (Not cHAS_LOST_MONEY)) False) (Eq (Not cRISES_AT_FIVE) False)) % 3.74/3.98 Clause #77 (by clausification #[76]): Or (Eq cEATS_PORKCHOPS True) % 3.74/3.98 (Or (Eq (Not cRISES_AT_FIVE) False) (Or (Eq cRAVENOUS False) (Eq (Not cHAS_LOST_MONEY) False))) % 3.74/3.98 Clause #78 (by clausification #[77]): Or (Eq cEATS_PORKCHOPS True) (Or (Eq cRAVENOUS False) (Or (Eq (Not cHAS_LOST_MONEY) False) (Eq cRISES_AT_FIVE True))) % 3.74/3.98 Clause #79 (by clausification #[78]): Or (Eq cEATS_PORKCHOPS True) (Or (Eq cRAVENOUS False) (Or (Eq cRISES_AT_FIVE True) (Eq cHAS_LOST_MONEY True))) % 3.74/3.98 Clause #80 (by clausification #[74]): Eq (And cLIVELY cIN_BED_BEFORE_FOUR → cBETTER_TAKE_TO_CAB_DRIVING) True % 3.74/3.98 Clause #81 (by clausification #[74]): Eq % 3.74/3.98 (And % 3.74/3.98 (And (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.74/3.98 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.74/3.98 (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS)) % 3.74/3.98 True % 3.74/3.98 Clause #82 (by clausification #[80]): Or (Eq (And cLIVELY cIN_BED_BEFORE_FOUR) False) (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.83/3.99 Clause #83 (by clausification #[82]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cLIVELY False) (Eq cIN_BED_BEFORE_FOUR False)) % 3.83/3.99 Clause #84 (by clausification #[81]): Eq (And (Not cGAMBLER) (Not cEATS_PORKCHOPS) → cRAVENOUS) True % 3.83/3.99 Clause #85 (by clausification #[81]): Eq % 3.83/3.99 (And (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) % 3.83/3.99 (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE)) % 3.83/3.99 True % 3.83/3.99 Clause #86 (by clausification #[84]): Or (Eq (And (Not cGAMBLER) (Not cEATS_PORKCHOPS)) False) (Eq cRAVENOUS True) % 3.83/3.99 Clause #87 (by clausification #[86]): Or (Eq cRAVENOUS True) (Or (Eq (Not cGAMBLER) False) (Eq (Not cEATS_PORKCHOPS) False)) % 3.83/3.99 Clause #88 (by clausification #[87]): Or (Eq cRAVENOUS True) (Or (Eq (Not cEATS_PORKCHOPS) False) (Eq cGAMBLER True)) % 3.83/3.99 Clause #89 (by clausification #[88]): Or (Eq cRAVENOUS True) (Or (Eq cGAMBLER True) (Eq cEATS_PORKCHOPS True)) % 3.83/3.99 Clause #90 (by clausification #[85]): Eq (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY → cRISES_AT_FIVE) True % 3.83/3.99 Clause #91 (by clausification #[85]): Eq (And (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY)) True % 3.83/3.99 Clause #92 (by clausification #[90]): Or (Eq (And (And (Not cLIVELY) cHAS_LOST_MONEY) cLIKELY_LOSE_MONEY) False) (Eq cRISES_AT_FIVE True) % 3.83/3.99 Clause #93 (by clausification #[92]): Or (Eq cRISES_AT_FIVE True) (Or (Eq (And (Not cLIVELY) cHAS_LOST_MONEY) False) (Eq cLIKELY_LOSE_MONEY False)) % 3.83/3.99 Clause #94 (by clausification #[93]): Or (Eq cRISES_AT_FIVE True) (Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq (Not cLIVELY) False) (Eq cHAS_LOST_MONEY False))) % 3.83/3.99 Clause #95 (by clausification #[94]): Or (Eq cRISES_AT_FIVE True) (Or (Eq cLIKELY_LOSE_MONEY False) (Or (Eq cHAS_LOST_MONEY False) (Eq cLIVELY True))) % 3.83/3.99 Clause #96 (by clausification #[91]): Eq (And cGAMBLER (Not cRAVENOUS) → cLIKELY_LOSE_MONEY) True % 3.83/3.99 Clause #97 (by clausification #[91]): Eq (And cLOGICIAN cEATS_PORKCHOPS → cLIKELY_LOSE_MONEY) True % 3.83/3.99 Clause #98 (by clausification #[96]): Or (Eq (And cGAMBLER (Not cRAVENOUS)) False) (Eq cLIKELY_LOSE_MONEY True) % 3.83/3.99 Clause #99 (by clausification #[98]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cGAMBLER False) (Eq (Not cRAVENOUS) False)) % 3.83/3.99 Clause #100 (by clausification #[99]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cGAMBLER False) (Eq cRAVENOUS True)) % 3.83/3.99 Clause #102 (by clausification #[97]): Or (Eq (And cLOGICIAN cEATS_PORKCHOPS) False) (Eq cLIKELY_LOSE_MONEY True) % 3.83/3.99 Clause #103 (by clausification #[102]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cLOGICIAN False) (Eq cEATS_PORKCHOPS False)) % 3.83/3.99 Clause #104 (by superposition #[103, 13]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEATS_PORKCHOPS False) (Eq False True)) % 3.83/3.99 Clause #105 (by clausification #[104]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cEATS_PORKCHOPS False) % 3.83/3.99 Clause #106 (by superposition #[105, 89]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cRAVENOUS True) (Or (Eq cGAMBLER True) (Eq False True))) % 3.83/3.99 Clause #107 (by clausification #[106]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cRAVENOUS True) (Eq cGAMBLER True)) % 3.83/3.99 Clause #108 (by superposition #[107, 100]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/3.99 (Or (Eq cRAVENOUS True) (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq True False) (Eq cRAVENOUS True)))) % 3.83/3.99 Clause #113 (by clausification #[108]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cRAVENOUS True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cRAVENOUS True))) % 3.83/3.99 Clause #114 (by eliminate duplicate literals #[113]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cRAVENOUS True) % 3.83/3.99 Clause #115 (by superposition #[114, 10]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/3.99 (Or (Eq cGAMBLER True) (Or (Eq True False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True)))) % 3.83/3.99 Clause #116 (by superposition #[114, 43]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq True False) (Or (Eq cEARNEST False) (Eq cBETTER_TAKE_TO_CAB_DRIVING False))) % 3.83/3.99 Clause #117 (by superposition #[114, 79]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/3.99 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq True False) (Or (Eq cRISES_AT_FIVE True) (Eq cHAS_LOST_MONEY True)))) % 3.83/4.01 Clause #118 (by clausification #[116]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEARNEST False) (Eq cBETTER_TAKE_TO_CAB_DRIVING False)) % 3.83/4.01 Clause #119 (by superposition #[118, 14]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING False) (Eq False True)) % 3.83/4.01 Clause #120 (by clausification #[119]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cBETTER_TAKE_TO_CAB_DRIVING False) % 3.83/4.01 Clause #121 (by clausification #[115]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cGAMBLER True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))) % 3.83/4.01 Clause #122 (by eliminate duplicate literals #[121]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cGAMBLER True) (Eq cLIVELY True)) % 3.83/4.01 Clause #123 (by clausification #[117]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cRISES_AT_FIVE True) (Eq cHAS_LOST_MONEY True))) % 3.83/4.01 Clause #124 (by superposition #[123, 16]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq True False) (Eq cIN_BED_BEFORE_FOUR True)))) % 3.83/4.01 Clause #125 (by clausification #[124]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cHAS_LOST_MONEY True) (Eq cIN_BED_BEFORE_FOUR True))) % 3.83/4.01 Clause #126 (by superposition #[125, 38]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) % 3.83/4.01 (Or (Eq cHAS_LOST_MONEY True) % 3.83/4.01 (Or (Eq True False) (Or (Eq cGAMBLER False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True)))))) % 3.83/4.01 Clause #127 (by clausification #[126]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) % 3.83/4.01 (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cGAMBLER False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))))) % 3.83/4.01 Clause #128 (by eliminate duplicate literals #[127]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cGAMBLER False) (Eq cLIVELY True)))) % 3.83/4.01 Clause #130 (by superposition #[128, 122]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) % 3.83/4.01 (Or (Eq cHAS_LOST_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq False True) (Eq cLIVELY True)))))) % 3.83/4.01 Clause #131 (by clausification #[130]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) % 3.83/4.01 (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIVELY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))))) % 3.83/4.01 Clause #132 (by eliminate duplicate literals #[131]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cHAS_LOST_MONEY True) (Eq cLIVELY True))) % 3.83/4.01 Clause #133 (by superposition #[132, 105]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIVELY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False)))) % 3.83/4.01 Clause #134 (by clausification #[133]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIVELY True) (Eq cLIKELY_LOSE_MONEY True))) % 3.83/4.01 Clause #135 (by eliminate duplicate literals #[134]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cHAS_LOST_MONEY True) (Eq cLIVELY True)) % 3.83/4.01 Clause #136 (by superposition #[135, 30]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) % 3.83/4.01 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.83/4.01 (Or (Eq True False) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True))))) % 3.83/4.01 Clause #137 (by clausification #[136]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) % 3.83/4.01 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True)))) % 3.83/4.01 Clause #138 (by superposition #[137, 16]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) % 3.83/4.01 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq True False) (Eq cIN_BED_BEFORE_FOUR True))))) % 3.83/4.01 Clause #139 (by clausification #[138]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) % 3.83/4.01 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cEATS_PORKCHOPS True) (Eq cIN_BED_BEFORE_FOUR True)))) % 3.83/4.01 Clause #140 (by superposition #[139, 38]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.83/4.01 (Or (Eq cLIVELY True) % 3.83/4.01 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.83/4.01 (Or (Eq cEATS_PORKCHOPS True) % 3.83/4.01 (Or (Eq True False) (Or (Eq cGAMBLER False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))))))) % 3.87/4.03 Clause #143 (by clausification #[140]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cGAMBLER False) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True)))))) % 3.87/4.03 Clause #144 (by eliminate duplicate literals #[143]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cEATS_PORKCHOPS True) (Eq cGAMBLER False)))) % 3.87/4.03 Clause #146 (by superposition #[144, 122]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq False True) (Eq cLIVELY True)))))) % 3.87/4.03 Clause #147 (by clausification #[146]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True))))) % 3.87/4.03 Clause #148 (by eliminate duplicate literals #[147]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cEATS_PORKCHOPS True))) % 3.87/4.03 Clause #149 (by superposition #[148, 105]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False)))) % 3.87/4.03 Clause #150 (by clausification #[149]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cLIVELY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cLIKELY_LOSE_MONEY True))) % 3.87/4.03 Clause #151 (by eliminate duplicate literals #[150]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cLIVELY True) (Eq cBETTER_TAKE_TO_CAB_DRIVING True)) % 3.87/4.03 Clause #153 (by superposition #[151, 120]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cLIVELY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False))) % 3.87/4.03 Clause #154 (by clausification #[153]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cLIVELY True) (Eq cLIKELY_LOSE_MONEY True)) % 3.87/4.03 Clause #155 (by eliminate duplicate literals #[154]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIVELY True) % 3.87/4.03 Clause #156 (by superposition #[155, 83]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq True False) (Eq cIN_BED_BEFORE_FOUR False))) % 3.87/4.03 Clause #157 (by clausification #[156]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cIN_BED_BEFORE_FOUR False)) % 3.87/4.03 Clause #158 (by superposition #[157, 125]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cHAS_LOST_MONEY True) (Eq False True))))) % 3.87/4.03 Clause #162 (by clausification #[158]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cEATS_PORKCHOPS True) (Eq cHAS_LOST_MONEY True)))) % 3.87/4.03 Clause #163 (by eliminate duplicate literals #[162]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cEATS_PORKCHOPS True) (Eq cHAS_LOST_MONEY True))) % 3.87/4.03 Clause #164 (by superposition #[163, 105]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False)))) % 3.87/4.03 Clause #165 (by clausification #[164]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cHAS_LOST_MONEY True) (Eq cLIKELY_LOSE_MONEY True))) % 3.87/4.03 Clause #166 (by eliminate duplicate literals #[165]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cHAS_LOST_MONEY True)) % 3.87/4.03 Clause #167 (by superposition #[166, 30]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq True False) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True))))) % 3.87/4.03 Clause #168 (by clausification #[167]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.87/4.03 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True)))) % 3.87/4.03 Clause #169 (by eliminate duplicate literals #[168]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cRISES_AT_FIVE True) (Eq cEATS_PORKCHOPS True))) % 3.89/4.05 Clause #170 (by superposition #[169, 16]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.89/4.05 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq True False) (Eq cIN_BED_BEFORE_FOUR True)))) % 3.89/4.05 Clause #171 (by clausification #[170]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cEATS_PORKCHOPS True) (Eq cIN_BED_BEFORE_FOUR True))) % 3.89/4.05 Clause #172 (by superposition #[171, 157]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.89/4.05 (Or (Eq cEATS_PORKCHOPS True) % 3.89/4.05 (Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq True False))))) % 3.89/4.05 Clause #173 (by clausification #[172]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.89/4.05 (Or (Eq cEATS_PORKCHOPS True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq cBETTER_TAKE_TO_CAB_DRIVING True)))) % 3.89/4.05 Clause #174 (by eliminate duplicate literals #[173]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cEATS_PORKCHOPS True)) % 3.89/4.05 Clause #175 (by superposition #[174, 105]): Or (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False))) % 3.89/4.05 Clause #176 (by clausification #[175]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq cLIKELY_LOSE_MONEY True)) % 3.89/4.05 Clause #177 (by eliminate duplicate literals #[176]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cBETTER_TAKE_TO_CAB_DRIVING True) % 3.89/4.05 Clause #179 (by superposition #[177, 120]): Or (Eq cLIKELY_LOSE_MONEY True) (Or (Eq cLIKELY_LOSE_MONEY True) (Eq True False)) % 3.89/4.05 Clause #180 (by clausification #[179]): Or (Eq cLIKELY_LOSE_MONEY True) (Eq cLIKELY_LOSE_MONEY True) % 3.89/4.05 Clause #181 (by eliminate duplicate literals #[180]): Eq cLIKELY_LOSE_MONEY True % 3.89/4.05 Clause #182 (by backward demodulation #[181, 51]): Or (Eq True False) (Or (Eq cLIVELY False) (Eq cLOGICIAN False)) % 3.89/4.05 Clause #183 (by backward demodulation #[181, 66]): Or (Eq True False) (Or (Eq cGAMBLER False) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Eq cLIVELY True)))) % 3.89/4.05 Clause #184 (by backward demodulation #[181, 72]): Or (Eq cBETTER_TAKE_TO_CAB_DRIVING True) (Eq True False) % 3.89/4.05 Clause #185 (by backward demodulation #[181, 95]): Or (Eq cRISES_AT_FIVE True) (Or (Eq True False) (Or (Eq cHAS_LOST_MONEY False) (Eq cLIVELY True))) % 3.89/4.05 Clause #195 (by clausification #[184]): Eq cBETTER_TAKE_TO_CAB_DRIVING True % 3.89/4.05 Clause #196 (by backward demodulation #[195, 23]): Or (Eq True False) (Or (Eq cGAMBLER False) (Or (Eq cIN_BED_BEFORE_FOUR False) (Eq cRAVENOUS True))) % 3.89/4.05 Clause #198 (by backward demodulation #[195, 43]): Or (Eq cRAVENOUS False) (Or (Eq cEARNEST False) (Eq True False)) % 3.89/4.05 Clause #200 (by clausification #[182]): Or (Eq cLIVELY False) (Eq cLOGICIAN False) % 3.89/4.05 Clause #201 (by clausification #[198]): Or (Eq cRAVENOUS False) (Eq cEARNEST False) % 3.89/4.05 Clause #202 (by clausification #[183]): Or (Eq cGAMBLER False) (Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Eq cLIVELY True))) % 3.89/4.05 Clause #203 (by superposition #[202, 57]): Or (Eq cHAS_LOST_MONEY True) % 3.89/4.05 (Or (Eq cEARNEST False) (Or (Eq cLIVELY True) (Or (Eq cLIVELY True) (Or (Eq False True) (Eq cRAVENOUS True))))) % 3.89/4.05 Clause #204 (by clausification #[196]): Or (Eq cGAMBLER False) (Or (Eq cIN_BED_BEFORE_FOUR False) (Eq cRAVENOUS True)) % 3.89/4.05 Clause #205 (by superposition #[204, 57]): Or (Eq cIN_BED_BEFORE_FOUR False) % 3.89/4.05 (Or (Eq cRAVENOUS True) (Or (Eq cLIVELY True) (Or (Eq False True) (Eq cRAVENOUS True)))) % 3.89/4.05 Clause #206 (by clausification #[185]): Or (Eq cRISES_AT_FIVE True) (Or (Eq cHAS_LOST_MONEY False) (Eq cLIVELY True)) % 3.89/4.05 Clause #207 (by clausification #[203]): Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Or (Eq cLIVELY True) (Or (Eq cLIVELY True) (Eq cRAVENOUS True)))) % 3.89/4.05 Clause #208 (by eliminate duplicate literals #[207]): Or (Eq cHAS_LOST_MONEY True) (Or (Eq cEARNEST False) (Or (Eq cLIVELY True) (Eq cRAVENOUS True))) % 3.89/4.05 Clause #209 (by superposition #[208, 14]): Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Eq False True))) % 3.89/4.06 Clause #210 (by clausification #[209]): Or (Eq cHAS_LOST_MONEY True) (Or (Eq cLIVELY True) (Eq cRAVENOUS True)) % 3.89/4.06 Clause #211 (by superposition #[210, 206]): Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Or (Eq cRISES_AT_FIVE True) (Or (Eq True False) (Eq cLIVELY True)))) % 3.89/4.06 Clause #212 (by clausification #[211]): Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Or (Eq cRISES_AT_FIVE True) (Eq cLIVELY True))) % 3.89/4.06 Clause #213 (by eliminate duplicate literals #[212]): Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Eq cRISES_AT_FIVE True)) % 3.89/4.06 Clause #214 (by superposition #[213, 16]): Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Or (Eq True False) (Eq cIN_BED_BEFORE_FOUR True))) % 3.89/4.06 Clause #215 (by clausification #[214]): Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Eq cIN_BED_BEFORE_FOUR True)) % 3.89/4.06 Clause #216 (by clausification #[205]): Or (Eq cIN_BED_BEFORE_FOUR False) (Or (Eq cRAVENOUS True) (Or (Eq cLIVELY True) (Eq cRAVENOUS True))) % 3.89/4.06 Clause #217 (by eliminate duplicate literals #[216]): Or (Eq cIN_BED_BEFORE_FOUR False) (Or (Eq cRAVENOUS True) (Eq cLIVELY True)) % 3.89/4.06 Clause #218 (by superposition #[217, 215]): Or (Eq cRAVENOUS True) (Or (Eq cLIVELY True) (Or (Eq cLIVELY True) (Or (Eq cRAVENOUS True) (Eq False True)))) % 3.89/4.06 Clause #219 (by clausification #[218]): Or (Eq cRAVENOUS True) (Or (Eq cLIVELY True) (Or (Eq cLIVELY True) (Eq cRAVENOUS True))) % 3.89/4.06 Clause #220 (by eliminate duplicate literals #[219]): Or (Eq cRAVENOUS True) (Eq cLIVELY True) % 3.89/4.06 Clause #221 (by superposition #[220, 200]): Or (Eq cRAVENOUS True) (Or (Eq True False) (Eq cLOGICIAN False)) % 3.89/4.06 Clause #222 (by clausification #[221]): Or (Eq cRAVENOUS True) (Eq cLOGICIAN False) % 3.89/4.06 Clause #223 (by superposition #[222, 13]): Or (Eq cRAVENOUS True) (Eq False True) % 3.89/4.06 Clause #224 (by clausification #[223]): Eq cRAVENOUS True % 3.89/4.06 Clause #227 (by backward demodulation #[224, 201]): Or (Eq True False) (Eq cEARNEST False) % 3.89/4.06 Clause #230 (by clausification #[227]): Eq cEARNEST False % 3.89/4.06 Clause #231 (by superposition #[230, 14]): Eq False True % 3.89/4.06 Clause #232 (by clausification #[231]): False % 3.89/4.06 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------