%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ091^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:21:01 AM UTC 2026
% Result : Theorem 0.08s 0.25s
% Output : Refutation 0.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ091^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n013.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 13:21:36 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.25 % (2091400)Will run a generic schedule for satisfiability detection.
% 0.08/0.25 % (2091413)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1473202289_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.25 % Detected minimum model sizes of [1]
% 0.08/0.25 % Detected maximum model sizes of [11]
% 0.08/0.25 % TRYING [1]
% 0.08/0.25 % TRYING [2]
% 0.08/0.25 % TRYING [3]
% 0.08/0.25 % TRYING [4]
% 0.08/0.25 % TRYING [5]
% 0.08/0.25 % TRYING [6]
% 0.08/0.25 % TRYING [7]
% 0.08/0.25 % TRYING [8]
% 0.08/0.25 % TRYING [9]
% 0.08/0.25 % TRYING [10]
% 0.08/0.25 % (2091414)% WARNING: option uhcvi not known.
% 0.08/0.25 % TRYING [11]
% 0.08/0.25 % (2091413) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2091400-2091413"...
% 0.08/0.25 % (2091413)...printing done.
% 0.08/0.25 % (2091413)Refutation found. Thanks to Tanya!
% 0.08/0.25 % SZS status Theorem for theBenchmark
% 0.08/0.25 % SZS output start Proof for theBenchmark
% 0.08/0.25 tff(func_def_0, type, cIN_BED_BEFORE_FOUR: $o).
% 0.08/0.25 tff(func_def_1, type, cRISES_AT_FIVE: $o).
% 0.08/0.25 tff(func_def_2, type, cLOGICIAN: $o).
% 0.08/0.25 tff(func_def_3, type, cEARNEST: $o).
% 0.08/0.25 tff(func_def_4, type, cGAMBLER: $o).
% 0.08/0.25 tff(func_def_5, type, cLIKELY_LOSE_MONEY: $o).
% 0.08/0.25 tff(func_def_6, type, cLIVELY: $o).
% 0.08/0.25 tff(func_def_7, type, cRAVENOUS: $o).
% 0.08/0.25 tff(func_def_8, type, cBETTER_TAKE_TO_CAB_DRIVING: $o).
% 0.08/0.25 tff(func_def_9, type, cEATS_PORKCHOPS: $o).
% 0.08/0.25 tff(func_def_10, type, cHAS_LOST_MONEY: $o).
% 0.08/0.25 tff(pred_def_4, type, sP3: $o > $o).
% 0.08/0.25 tff(pred_def_8, type, sP7: $o > $o).
% 0.08/0.25 tff(pred_def_10, type, sP9: $o > $o).
% 0.08/0.25 tff(pred_def_12, type, sP11: $o > $o).
% 0.08/0.25 tff(pred_def_17, type, sP16: $o > $o).
% 0.08/0.25 tff(pred_def_19, type, sP18: $o > $o).
% 0.08/0.25 tff(pred_def_26, type, sP25: $o > $o).
% 0.08/0.25 tff(pred_def_28, type, sP27: $o > $o).
% 0.08/0.25 tff(pred_def_30, type, sP29: $o > $o).
% 0.08/0.25 tff(pred_def_39, type, sP38: $o > $o).
% 0.08/0.25 tff(pred_def_42, type, sP41: $o > $o).
% 0.08/0.25 tff(pred_def_44, type, sP43: $o > $o).
% 0.08/0.25 tff(pred_def_50, type, sP49: $o > $o).
% 0.08/0.25 tff(pred_def_52, type, sP51: $o > $o).
% 0.08/0.25 tff(f1,conjecture,(
% 0.08/0.25 (((~cLIKELY_LOSE_MONEY & ~cLIVELY & cRAVENOUS) => cGAMBLER) & ((~cRAVENOUS & cIN_BED_BEFORE_FOUR & cGAMBLER) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cEATS_PORKCHOPS & cHAS_LOST_MONEY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cLIKELY_LOSE_MONEY & ~cLIVELY & cGAMBLER) => ~cIN_BED_BEFORE_FOUR) & ((cEARNEST & cRAVENOUS) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((cEARNEST & cLOGICIAN & cLIVELY) => ~cLIKELY_LOSE_MONEY) & ((~cRAVENOUS & ~cGAMBLER) => cLIVELY) & ((~cHAS_LOST_MONEY & cGAMBLER & ~cLIVELY & cEARNEST) => ~cLIKELY_LOSE_MONEY) & ((cLIKELY_LOSE_MONEY & cLOGICIAN) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cHAS_LOST_MONEY & cRAVENOUS) => cEATS_PORKCHOPS) & ((cIN_BED_BEFORE_FOUR & cLIVELY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cEATS_PORKCHOPS & ~cGAMBLER) => cRAVENOUS) & ((cLIKELY_LOSE_MONEY & cHAS_LOST_MONEY & ~cLIVELY) => cRISES_AT_FIVE) & ((~cRAVENOUS & cGAMBLER) => cLIKELY_LOSE_MONEY) & ((cEATS_PORKCHOPS & cLOGICIAN) => cLIKELY_LOSE_MONEY)) => ((cLOGICIAN & cEARNEST) => (~cIN_BED_BEFORE_FOUR & cRISES_AT_FIVE))),
% 0.08/0.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cPORKCHOP1)).
% 0.08/0.26 tff(f2,negated_conjecture,(
% 0.08/0.26 ~((((~cLIKELY_LOSE_MONEY & ~cLIVELY & cRAVENOUS) => cGAMBLER) & ((~cRAVENOUS & cIN_BED_BEFORE_FOUR & cGAMBLER) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cEATS_PORKCHOPS & cHAS_LOST_MONEY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cLIKELY_LOSE_MONEY & ~cLIVELY & cGAMBLER) => ~cIN_BED_BEFORE_FOUR) & ((cEARNEST & cRAVENOUS) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((cEARNEST & cLOGICIAN & cLIVELY) => ~cLIKELY_LOSE_MONEY) & ((~cRAVENOUS & ~cGAMBLER) => cLIVELY) & ((~cHAS_LOST_MONEY & cGAMBLER & ~cLIVELY & cEARNEST) => ~cLIKELY_LOSE_MONEY) & ((cLIKELY_LOSE_MONEY & cLOGICIAN) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cHAS_LOST_MONEY & cRAVENOUS) => cEATS_PORKCHOPS) & ((cIN_BED_BEFORE_FOUR & cLIVELY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cEATS_PORKCHOPS & ~cGAMBLER) => cRAVENOUS) & ((cLIKELY_LOSE_MONEY & cHAS_LOST_MONEY & ~cLIVELY) => cRISES_AT_FIVE) & ((~cRAVENOUS & cGAMBLER) => cLIKELY_LOSE_MONEY) & ((cEATS_PORKCHOPS & cLOGICIAN) => cLIKELY_LOSE_MONEY)) => ((cLOGICIAN & cEARNEST) => (~cIN_BED_BEFORE_FOUR & cRISES_AT_FIVE)))),
% 0.08/0.26 inference(negated_conjecture,[status(cth)],[f1])).
% 0.08/0.26 tff(f3,plain,(
% 0.08/0.26 ~((((~cLIKELY_LOSE_MONEY & ~cLIVELY & cRAVENOUS) => cGAMBLER) & ((~cRAVENOUS & cIN_BED_BEFORE_FOUR & cGAMBLER) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cEATS_PORKCHOPS & cHAS_LOST_MONEY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cLIKELY_LOSE_MONEY & ~cLIVELY & cGAMBLER) => ~cIN_BED_BEFORE_FOUR) & ((cEARNEST & cRAVENOUS) => ~cBETTER_TAKE_TO_CAB_DRIVING) & ((cEARNEST & cLOGICIAN & cLIVELY) => ~cLIKELY_LOSE_MONEY) & ((~cRAVENOUS & ~cGAMBLER) => cLIVELY) & ((~cHAS_LOST_MONEY & cGAMBLER & ~cLIVELY & cEARNEST) => ~cLIKELY_LOSE_MONEY) & ((cLIKELY_LOSE_MONEY & cLOGICIAN) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cRISES_AT_FIVE & ~cHAS_LOST_MONEY & cRAVENOUS) => cEATS_PORKCHOPS) & ((cIN_BED_BEFORE_FOUR & cLIVELY) => cBETTER_TAKE_TO_CAB_DRIVING) & ((~cEATS_PORKCHOPS & ~cGAMBLER) => cRAVENOUS) & ((cLIKELY_LOSE_MONEY & cHAS_LOST_MONEY & ~cLIVELY) => cRISES_AT_FIVE) & ((~cRAVENOUS & cGAMBLER) => cLIKELY_LOSE_MONEY) & ((cEATS_PORKCHOPS & cLOGICIAN) => cLIKELY_LOSE_MONEY)) => ((cLOGICIAN & cEARNEST) => (~cIN_BED_BEFORE_FOUR & cRISES_AT_FIVE)))),
% 0.08/0.26 inference(rectify,[],[f2])).
% 0.08/0.26 tff(f4,plain,(
% 0.08/0.26 ~((((~ (cLIKELY_LOSE_MONEY = $true) & ~ (cLIVELY = $true) & (cRAVENOUS = $true)) => (cGAMBLER = $true)) & ((~ (cRAVENOUS = $true) & (cIN_BED_BEFORE_FOUR = $true) & (cGAMBLER = $true)) => ~ (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & ((~ (cRISES_AT_FIVE = $true) & ~ (cEATS_PORKCHOPS = $true) & (cHAS_LOST_MONEY = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & ((~ (cLIKELY_LOSE_MONEY = $true) & ~ (cLIVELY = $true) & (cGAMBLER = $true)) => ~ (cIN_BED_BEFORE_FOUR = $true)) & (((cEARNEST = $true) & (cRAVENOUS = $true)) => ~ (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & (((cEARNEST = $true) & (cLOGICIAN = $true) & (cLIVELY = $true)) => ~ (cLIKELY_LOSE_MONEY = $true)) & ((~ (cRAVENOUS = $true) & ~ (cGAMBLER = $true)) => (cLIVELY = $true)) & ((~ (cHAS_LOST_MONEY = $true) & (cGAMBLER = $true) & ~ (cLIVELY = $true) & (cEARNEST = $true)) => ~ (cLIKELY_LOSE_MONEY = $true)) & (((cLIKELY_LOSE_MONEY = $true) & (cLOGICIAN = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & ((~ (cRISES_AT_FIVE = $true) & ~ (cHAS_LOST_MONEY = $true) & (cRAVENOUS = $true)) => (cEATS_PORKCHOPS = $true)) & (((cIN_BED_BEFORE_FOUR = $true) & (cLIVELY = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & ((~ (cEATS_PORKCHOPS = $true) & ~ (cGAMBLER = $true)) => (cRAVENOUS = $true)) & (((cLIKELY_LOSE_MONEY = $true) & (cHAS_LOST_MONEY = $true) & ~ (cLIVELY = $true)) => (cRISES_AT_FIVE = $true)) & ((~ (cRAVENOUS = $true) & (cGAMBLER = $true)) => (cLIKELY_LOSE_MONEY = $true)) & (((cEATS_PORKCHOPS = $true) & (cLOGICIAN = $true)) => (cLIKELY_LOSE_MONEY = $true))) => (((cLOGICIAN = $true) & (cEARNEST = $true)) => (~ (cIN_BED_BEFORE_FOUR = $true) & (cRISES_AT_FIVE = $true))))),
% 0.08/0.26 inference(fool_elimination,[],[f3])).
% 0.08/0.26 tff(f5,plain,(
% 0.08/0.26 ~(((((cLIKELY_LOSE_MONEY != $true) & (cLIVELY != $true) & (cRAVENOUS = $true)) => (cGAMBLER = $true)) & (((cRAVENOUS != $true) & (cIN_BED_BEFORE_FOUR = $true) & (cGAMBLER = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING != $true)) & (((cRISES_AT_FIVE != $true) & (cEATS_PORKCHOPS != $true) & (cHAS_LOST_MONEY = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & (((cLIKELY_LOSE_MONEY != $true) & (cLIVELY != $true) & (cGAMBLER = $true)) => (cIN_BED_BEFORE_FOUR != $true)) & (((cEARNEST = $true) & (cRAVENOUS = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING != $true)) & (((cEARNEST = $true) & (cLOGICIAN = $true) & (cLIVELY = $true)) => (cLIKELY_LOSE_MONEY != $true)) & (((cRAVENOUS != $true) & (cGAMBLER != $true)) => (cLIVELY = $true)) & (((cHAS_LOST_MONEY != $true) & (cGAMBLER = $true) & (cLIVELY != $true) & (cEARNEST = $true)) => (cLIKELY_LOSE_MONEY != $true)) & (((cLIKELY_LOSE_MONEY = $true) & (cLOGICIAN = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & (((cRISES_AT_FIVE != $true) & (cHAS_LOST_MONEY != $true) & (cRAVENOUS = $true)) => (cEATS_PORKCHOPS = $true)) & (((cIN_BED_BEFORE_FOUR = $true) & (cLIVELY = $true)) => (cBETTER_TAKE_TO_CAB_DRIVING = $true)) & (((cEATS_PORKCHOPS != $true) & (cGAMBLER != $true)) => (cRAVENOUS = $true)) & (((cLIKELY_LOSE_MONEY = $true) & (cHAS_LOST_MONEY = $true) & (cLIVELY != $true)) => (cRISES_AT_FIVE = $true)) & (((cRAVENOUS != $true) & (cGAMBLER = $true)) => (cLIKELY_LOSE_MONEY = $true)) & (((cEATS_PORKCHOPS = $true) & (cLOGICIAN = $true)) => (cLIKELY_LOSE_MONEY = $true))) => (((cLOGICIAN = $true) & (cEARNEST = $true)) => ((cIN_BED_BEFORE_FOUR != $true) & (cRISES_AT_FIVE = $true))))),
% 0.08/0.26 inference(flattening,[],[f4])).
% 0.08/0.26 tff(f6,plain,(
% 0.08/0.26 (((cIN_BED_BEFORE_FOUR = $true) | (cRISES_AT_FIVE != $true)) & ((cLOGICIAN = $true) & (cEARNEST = $true))) & (((cGAMBLER = $true) | ((cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cRAVENOUS != $true))) & ((cBETTER_TAKE_TO_CAB_DRIVING != $true) | ((cRAVENOUS = $true) | (cIN_BED_BEFORE_FOUR != $true) | (cGAMBLER != $true))) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | ((cRISES_AT_FIVE = $true) | (cEATS_PORKCHOPS = $true) | (cHAS_LOST_MONEY != $true))) & ((cIN_BED_BEFORE_FOUR != $true) | ((cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cGAMBLER != $true))) & ((cBETTER_TAKE_TO_CAB_DRIVING != $true) | ((cEARNEST != $true) | (cRAVENOUS != $true))) & ((cLIKELY_LOSE_MONEY != $true) | ((cEARNEST != $true) | (cLOGICIAN != $true) | (cLIVELY != $true))) & ((cLIVELY = $true) | ((cRAVENOUS = $true) | (cGAMBLER = $true))) & ((cLIKELY_LOSE_MONEY != $true) | ((cHAS_LOST_MONEY = $true) | (cGAMBLER != $true) | (cLIVELY = $true) | (cEARNEST != $true))) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | ((cLIKELY_LOSE_MONEY != $true) | (cLOGICIAN != $true))) & ((cEATS_PORKCHOPS = $true) | ((cRISES_AT_FIVE = $true) | (cHAS_LOST_MONEY = $true) | (cRAVENOUS != $true))) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | ((cIN_BED_BEFORE_FOUR != $true) | (cLIVELY != $true))) & ((cRAVENOUS = $true) | ((cEATS_PORKCHOPS = $true) | (cGAMBLER = $true))) & ((cRISES_AT_FIVE = $true) | ((cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY != $true) | (cLIVELY = $true))) & ((cLIKELY_LOSE_MONEY = $true) | ((cRAVENOUS = $true) | (cGAMBLER != $true))) & ((cLIKELY_LOSE_MONEY = $true) | ((cEATS_PORKCHOPS != $true) | (cLOGICIAN != $true))))),
% 0.08/0.26 inference(ennf_transformation,[],[f5])).
% 0.08/0.26 tff(f7,plain,(
% 0.08/0.26 ((cIN_BED_BEFORE_FOUR = $true) | (cRISES_AT_FIVE != $true)) & (cLOGICIAN = $true) & (cEARNEST = $true) & ((cGAMBLER = $true) | (cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cRAVENOUS != $true)) & ((cBETTER_TAKE_TO_CAB_DRIVING != $true) | (cRAVENOUS = $true) | (cIN_BED_BEFORE_FOUR != $true) | (cGAMBLER != $true)) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cRISES_AT_FIVE = $true) | (cEATS_PORKCHOPS = $true) | (cHAS_LOST_MONEY != $true)) & ((cIN_BED_BEFORE_FOUR != $true) | (cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cGAMBLER != $true)) & ((cBETTER_TAKE_TO_CAB_DRIVING != $true) | (cEARNEST != $true) | (cRAVENOUS != $true)) & ((cLIKELY_LOSE_MONEY != $true) | (cEARNEST != $true) | (cLOGICIAN != $true) | (cLIVELY != $true)) & ((cLIVELY = $true) | (cRAVENOUS = $true) | (cGAMBLER = $true)) & ((cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY = $true) | (cGAMBLER != $true) | (cLIVELY = $true) | (cEARNEST != $true)) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cLIKELY_LOSE_MONEY != $true) | (cLOGICIAN != $true)) & ((cEATS_PORKCHOPS = $true) | (cRISES_AT_FIVE = $true) | (cHAS_LOST_MONEY = $true) | (cRAVENOUS != $true)) & ((cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cIN_BED_BEFORE_FOUR != $true) | (cLIVELY != $true)) & ((cRAVENOUS = $true) | (cEATS_PORKCHOPS = $true) | (cGAMBLER = $true)) & ((cRISES_AT_FIVE = $true) | (cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY != $true) | (cLIVELY = $true)) & ((cLIKELY_LOSE_MONEY = $true) | (cRAVENOUS = $true) | (cGAMBLER != $true)) & ((cLIKELY_LOSE_MONEY = $true) | (cEATS_PORKCHOPS != $true) | (cLOGICIAN != $true))),
% 0.08/0.26 inference(flattening,[],[f6])).
% 0.08/0.26 tff(f8,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY = $true) | (cEATS_PORKCHOPS != $true) | (cLOGICIAN != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f9,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY = $true) | (cRAVENOUS = $true) | (cGAMBLER != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f10,plain,(
% 0.08/0.26 (cRISES_AT_FIVE = $true) | (cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY != $true) | (cLIVELY = $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f11,plain,(
% 0.08/0.26 (cRAVENOUS = $true) | (cEATS_PORKCHOPS = $true) | (cGAMBLER = $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f12,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cIN_BED_BEFORE_FOUR != $true) | (cLIVELY != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f13,plain,(
% 0.08/0.26 (cEATS_PORKCHOPS = $true) | (cRISES_AT_FIVE = $true) | (cHAS_LOST_MONEY = $true) | (cRAVENOUS != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f14,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cLIKELY_LOSE_MONEY != $true) | (cLOGICIAN != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f15,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY = $true) | (cGAMBLER != $true) | (cLIVELY = $true) | (cEARNEST != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f16,plain,(
% 0.08/0.26 (cLIVELY = $true) | (cRAVENOUS = $true) | (cGAMBLER = $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f17,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY != $true) | (cEARNEST != $true) | (cLOGICIAN != $true) | (cLIVELY != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f18,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING != $true) | (cEARNEST != $true) | (cRAVENOUS != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f19,plain,(
% 0.08/0.26 (cIN_BED_BEFORE_FOUR != $true) | (cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cGAMBLER != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f20,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cRISES_AT_FIVE = $true) | (cEATS_PORKCHOPS = $true) | (cHAS_LOST_MONEY != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f21,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING != $true) | (cRAVENOUS = $true) | (cIN_BED_BEFORE_FOUR != $true) | (cGAMBLER != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f22,plain,(
% 0.08/0.26 (cGAMBLER = $true) | (cLIKELY_LOSE_MONEY = $true) | (cLIVELY = $true) | (cRAVENOUS != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f23,plain,(
% 0.08/0.26 (cEARNEST = $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f24,plain,(
% 0.08/0.26 (cLOGICIAN = $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f25,plain,(
% 0.08/0.26 (cIN_BED_BEFORE_FOUR = $true) | (cRISES_AT_FIVE != $true)),
% 0.08/0.26 inference(cnf_transformation,[],[f7])).
% 0.08/0.26 tff(f26,definition,(
% 0.08/0.26 ($true != $false)),
% 0.08/0.26 introduced(theory,[fool_distinctness_axiom])).
% 0.08/0.26 tff(f27,definition,(
% 0.08/0.26 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.08/0.26 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.08/0.26 tff(f28,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING != $true) | ($true != $true) | (cRAVENOUS != $true)),
% 0.08/0.26 inference(definition_unfolding,[],[f18,f23])).
% 0.08/0.26 tff(f29,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY != $true) | ($true != $true) | ($true != $true) | (cLIVELY != $true)),
% 0.08/0.26 inference(definition_unfolding,[],[f17,f23,f24])).
% 0.08/0.26 tff(f30,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY != $true) | (cHAS_LOST_MONEY = $true) | (cGAMBLER != $true) | (cLIVELY = $true) | ($true != $true)),
% 0.08/0.26 inference(definition_unfolding,[],[f15,f23])).
% 0.08/0.26 tff(f31,plain,(
% 0.08/0.26 (cBETTER_TAKE_TO_CAB_DRIVING = $true) | (cLIKELY_LOSE_MONEY != $true) | ($true != $true)),
% 0.08/0.26 inference(definition_unfolding,[],[f14,f24])).
% 0.08/0.26 tff(f32,plain,(
% 0.08/0.26 (cLIKELY_LOSE_MONEY = $true) | (cEATS_PORKCHOPS != $true) | ($true != $true)),
% 0.08/0.26 inference(definition_unfolding,[],[f8,f24])).
% 0.08/0.26 tff(f158,plain,(
% 0.08/0.26 $false),
% 0.08/0.26 inference(finite_model_not_found_(exhaustively_excluded_all_possible_domain_size_assignments),[],[f27,f26,f25,f22,f21,f20,f19,f28,f29,f16,f30,f31,f13,f12,f11,f10,f9,f32])).
% 0.08/0.26 % SZS output end Proof for theBenchmark
% 0.08/0.26 % (2091413)------------------------------
% 0.08/0.26 % (2091413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.26 % (2091413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.26 % (2091413)CaDiCaL version: 2.1.3
% 0.08/0.26 % (2091413)Termination reason: Refutation
% 0.08/0.26 % (2091413)Time elapsed: 0.006 s
% 0.08/0.26 % (2091413)Peak memory usage: 11 MB
% 0.08/0.26 % (2091413)Instructions burned: 20 (million)
% 0.08/0.26 % (2091400)Success in time 0.041 s
% 0.08/0.26 % Vampire exiting
%------------------------------------------------------------------------------