%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO175^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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 08:08:41 PM UTC 2025 % Result : Theorem 3.71s 3.86s % Output : Proof 3.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO175^5 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 13:42:38 EDT 2025 % 0.13/0.34 % CPUTime : % 3.71/3.86 SZS status Theorem for theBenchmark.p % 3.71/3.86 SZS output start Proof for theBenchmark.p % 3.71/3.86 Clause #0 (by assumption #[]): Eq % 3.71/3.86 (Not % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (∀ (Xx : a), % 3.71/3.86 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.86 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists fun Xw => cVEG_EATS Xz Xw) → cMEAT_EATS Xx Xz)) % 3.71/3.86 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.86 (cSMALLER cSNAIL cBIRD)) % 3.71/3.86 (cSMALLER cBIRD cFOX)) % 3.71/3.86 (cSMALLER cFOX cWOLF)) % 3.71/3.86 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.86 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.86 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.86 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.86 (Exists fun Xy => cVEG_EATS cCATERPILLAR Xy)) % 3.71/3.86 (Exists fun Xy => cVEG_EATS cSNAIL Xy) → % 3.71/3.86 Exists fun Xx => Exists fun Xy => And (cMEAT_EATS Xx Xy) (cVEG_EATS Xy cGRAIN))) % 3.71/3.86 True % 3.71/3.86 Clause #1 (by betaEtaReduce #[0]): Eq % 3.71/3.86 (Not % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (∀ (Xx : a), % 3.71/3.86 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.86 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.86 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.86 (cSMALLER cSNAIL cBIRD)) % 3.71/3.86 (cSMALLER cBIRD cFOX)) % 3.71/3.86 (cSMALLER cFOX cWOLF)) % 3.71/3.86 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.86 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.86 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.86 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.86 (Exists (cVEG_EATS cCATERPILLAR))) % 3.71/3.86 (Exists (cVEG_EATS cSNAIL)) → % 3.71/3.86 Exists fun Xx => Exists fun Xy => And (cMEAT_EATS Xx Xy) (cVEG_EATS Xy cGRAIN))) % 3.71/3.86 True % 3.71/3.86 Clause #2 (by clausification #[1]): Eq % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (∀ (Xx : a), % 3.71/3.86 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.86 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.86 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.86 (cSMALLER cSNAIL cBIRD)) % 3.71/3.86 (cSMALLER cBIRD cFOX)) % 3.71/3.86 (cSMALLER cFOX cWOLF)) % 3.71/3.86 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.86 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.86 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.86 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.86 (Exists (cVEG_EATS cCATERPILLAR))) % 3.71/3.86 (Exists (cVEG_EATS cSNAIL)) → % 3.71/3.86 Exists fun Xx => Exists fun Xy => And (cMEAT_EATS Xx Xy) (cVEG_EATS Xy cGRAIN)) % 3.71/3.86 False % 3.71/3.86 Clause #3 (by clausification #[2]): Eq % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (And % 3.71/3.86 (∀ (Xx : a), % 3.71/3.86 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.86 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.86 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.86 (cSMALLER cSNAIL cBIRD)) % 3.71/3.86 (cSMALLER cBIRD cFOX)) % 3.71/3.86 (cSMALLER cFOX cWOLF)) % 3.71/3.86 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.86 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.86 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.86 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.86 (Exists (cVEG_EATS cCATERPILLAR))) % 3.71/3.86 (Exists (cVEG_EATS cSNAIL))) % 3.71/3.86 True % 3.71/3.86 Clause #4 (by clausification #[2]): Eq (Exists fun Xx => Exists fun Xy => And (cMEAT_EATS Xx Xy) (cVEG_EATS Xy cGRAIN)) False % 3.71/3.86 Clause #5 (by clausification #[3]): Eq (Exists (cVEG_EATS cSNAIL)) True % 3.71/3.87 Clause #6 (by clausification #[3]): Eq % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (∀ (Xx : a), % 3.71/3.87 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.87 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.87 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.87 (cSMALLER cSNAIL cBIRD)) % 3.71/3.87 (cSMALLER cBIRD cFOX)) % 3.71/3.87 (cSMALLER cFOX cWOLF)) % 3.71/3.87 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.87 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.87 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.87 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.87 (Exists (cVEG_EATS cCATERPILLAR))) % 3.71/3.87 True % 3.71/3.87 Clause #7 (by clausification #[5]): ∀ (a : p), Eq (cVEG_EATS cSNAIL (skS.0 0 a)) True % 3.71/3.87 Clause #8 (by clausification #[4]): ∀ (a_1 : a), Eq (Exists fun Xy => And (cMEAT_EATS a_1 Xy) (cVEG_EATS Xy cGRAIN)) False % 3.71/3.87 Clause #9 (by clausification #[8]): ∀ (a_1 a : a), Eq (And (cMEAT_EATS a_1 a) (cVEG_EATS a cGRAIN)) False % 3.71/3.87 Clause #10 (by clausification #[9]): ∀ (a_1 a : a), Or (Eq (cMEAT_EATS a_1 a) False) (Eq (cVEG_EATS a cGRAIN) False) % 3.71/3.87 Clause #12 (by clausification #[6]): Eq % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (And % 3.71/3.87 (∀ (Xx : a), % 3.71/3.87 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.87 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.87 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.87 (cSMALLER cSNAIL cBIRD)) % 3.71/3.87 (cSMALLER cBIRD cFOX)) % 3.71/3.87 (cSMALLER cFOX cWOLF)) % 3.71/3.87 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.87 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.87 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.87 (Not (cMEAT_EATS cBIRD cSNAIL))) % 3.71/3.87 True % 3.71/3.87 Clause #14 (by clausification #[12]): Eq (Not (cMEAT_EATS cBIRD cSNAIL)) True % 3.71/3.87 Clause #15 (by clausification #[12]): Eq % 3.71/3.87 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (∀ (Xx : a), % 3.71/3.88 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.88 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.88 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.88 (cSMALLER cSNAIL cBIRD)) % 3.71/3.88 (cSMALLER cBIRD cFOX)) % 3.71/3.88 (cSMALLER cFOX cWOLF)) % 3.71/3.88 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.88 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.88 (cMEAT_EATS cBIRD cCATERPILLAR)) % 3.71/3.88 True % 3.71/3.88 Clause #16 (by clausification #[14]): Eq (cMEAT_EATS cBIRD cSNAIL) False % 3.71/3.88 Clause #18 (by clausification #[15]): Eq % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (∀ (Xx : a), % 3.71/3.88 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.88 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.88 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.88 (cSMALLER cSNAIL cBIRD)) % 3.71/3.88 (cSMALLER cBIRD cFOX)) % 3.71/3.88 (cSMALLER cFOX cWOLF)) % 3.71/3.88 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.88 (Not (cVEG_EATS cWOLF cGRAIN))) % 3.71/3.88 True % 3.71/3.88 Clause #20 (by clausification #[18]): Eq (Not (cVEG_EATS cWOLF cGRAIN)) True % 3.71/3.88 Clause #21 (by clausification #[18]): Eq % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (∀ (Xx : a), % 3.71/3.88 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.88 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.88 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.88 (cSMALLER cSNAIL cBIRD)) % 3.71/3.88 (cSMALLER cBIRD cFOX)) % 3.71/3.88 (cSMALLER cFOX cWOLF)) % 3.71/3.88 (Not (cMEAT_EATS cWOLF cFOX))) % 3.71/3.88 True % 3.71/3.88 Clause #22 (by clausification #[20]): Eq (cVEG_EATS cWOLF cGRAIN) False % 3.71/3.88 Clause #24 (by clausification #[21]): Eq (Not (cMEAT_EATS cWOLF cFOX)) True % 3.71/3.88 Clause #25 (by clausification #[21]): Eq % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (And % 3.71/3.88 (∀ (Xx : a), % 3.71/3.88 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.88 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.90 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.90 (cSMALLER cSNAIL cBIRD)) % 3.71/3.90 (cSMALLER cBIRD cFOX)) % 3.71/3.90 (cSMALLER cFOX cWOLF)) % 3.71/3.90 True % 3.71/3.90 Clause #26 (by clausification #[24]): Eq (cMEAT_EATS cWOLF cFOX) False % 3.71/3.90 Clause #27 (by clausification #[25]): Eq (cSMALLER cFOX cWOLF) True % 3.71/3.90 Clause #28 (by clausification #[25]): Eq % 3.71/3.90 (And % 3.71/3.90 (And % 3.71/3.90 (And % 3.71/3.90 (∀ (Xx : a), % 3.71/3.90 Or (∀ (Xy : p), cVEG_EATS Xx Xy) % 3.71/3.90 (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.90 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.90 (cSMALLER cSNAIL cBIRD)) % 3.71/3.90 (cSMALLER cBIRD cFOX)) % 3.71/3.90 True % 3.71/3.90 Clause #29 (by clausification #[28]): Eq (cSMALLER cBIRD cFOX) True % 3.71/3.90 Clause #30 (by clausification #[28]): Eq % 3.71/3.90 (And % 3.71/3.90 (And % 3.71/3.90 (∀ (Xx : a), % 3.71/3.90 Or (∀ (Xy : p), cVEG_EATS Xx Xy) (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.90 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.90 (cSMALLER cSNAIL cBIRD)) % 3.71/3.90 True % 3.71/3.90 Clause #31 (by clausification #[30]): Eq (cSMALLER cSNAIL cBIRD) True % 3.71/3.90 Clause #32 (by clausification #[30]): Eq % 3.71/3.90 (And % 3.71/3.90 (∀ (Xx : a), % 3.71/3.90 Or (∀ (Xy : p), cVEG_EATS Xx Xy) (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.90 (cSMALLER cCATERPILLAR cBIRD)) % 3.71/3.90 True % 3.71/3.90 Clause #34 (by clausification #[32]): Eq % 3.71/3.90 (∀ (Xx : a), % 3.71/3.90 Or (∀ (Xy : p), cVEG_EATS Xx Xy) (∀ (Xz : a), And (cSMALLER Xz Xx) (Exists (cVEG_EATS Xz)) → cMEAT_EATS Xx Xz)) % 3.71/3.90 True % 3.71/3.90 Clause #35 (by clausification #[34]): ∀ (a_1 : a), % 3.71/3.90 Eq (Or (∀ (Xy : p), cVEG_EATS a_1 Xy) (∀ (Xz : a), And (cSMALLER Xz a_1) (Exists (cVEG_EATS Xz)) → cMEAT_EATS a_1 Xz)) % 3.71/3.90 True % 3.71/3.90 Clause #36 (by clausification #[35]): ∀ (a_1 : a), % 3.71/3.90 Or (Eq (∀ (Xy : p), cVEG_EATS a_1 Xy) True) % 3.71/3.90 (Eq (∀ (Xz : a), And (cSMALLER Xz a_1) (Exists (cVEG_EATS Xz)) → cMEAT_EATS a_1 Xz) True) % 3.71/3.90 Clause #37 (by clausification #[36]): ∀ (a_1 : a) (a_2 : p), % 3.71/3.90 Or (Eq (∀ (Xz : a), And (cSMALLER Xz a_1) (Exists (cVEG_EATS Xz)) → cMEAT_EATS a_1 Xz) True) % 3.71/3.90 (Eq (cVEG_EATS a_1 a_2) True) % 3.71/3.90 Clause #38 (by clausification #[37]): ∀ (a_1 : a) (a_2 : p) (a : a), % 3.71/3.90 Or (Eq (cVEG_EATS a_1 a_2) True) (Eq (And (cSMALLER a a_1) (Exists (cVEG_EATS a)) → cMEAT_EATS a_1 a) True) % 3.71/3.90 Clause #39 (by clausification #[38]): ∀ (a_1 : a) (a_2 : p) (a : a), % 3.71/3.90 Or (Eq (cVEG_EATS a_1 a_2) True) % 3.71/3.90 (Or (Eq (And (cSMALLER a a_1) (Exists (cVEG_EATS a))) False) (Eq (cMEAT_EATS a_1 a) True)) % 3.71/3.90 Clause #40 (by clausification #[39]): ∀ (a_1 : a) (a_2 : p) (a : a), % 3.71/3.90 Or (Eq (cVEG_EATS a_1 a_2) True) % 3.71/3.90 (Or (Eq (cMEAT_EATS a_1 a) True) (Or (Eq (cSMALLER a a_1) False) (Eq (Exists (cVEG_EATS a)) False))) % 3.71/3.90 Clause #41 (by clausification #[40]): ∀ (a_1 : a) (a_2 : p) (a : a) (a_3 : p), % 3.71/3.90 Or (Eq (cVEG_EATS a_1 a_2) True) % 3.71/3.90 (Or (Eq (cMEAT_EATS a_1 a) True) (Or (Eq (cSMALLER a a_1) False) (Eq (cVEG_EATS a a_3) False))) % 3.71/3.90 Clause #42 (by superposition #[41, 27]): ∀ (a a_1 : p), % 3.71/3.90 Or (Eq (cVEG_EATS cWOLF a) True) % 3.71/3.90 (Or (Eq (cMEAT_EATS cWOLF cFOX) True) (Or (Eq (cVEG_EATS cFOX a_1) False) (Eq False True))) % 3.71/3.90 Clause #43 (by superposition #[41, 29]): ∀ (a a_1 : p), % 3.71/3.90 Or (Eq (cVEG_EATS cFOX a) True) % 3.71/3.90 (Or (Eq (cMEAT_EATS cFOX cBIRD) True) (Or (Eq (cVEG_EATS cBIRD a_1) False) (Eq False True))) % 3.71/3.90 Clause #44 (by superposition #[41, 31]): ∀ (a a_1 : p), % 3.71/3.90 Or (Eq (cVEG_EATS cBIRD a) True) % 3.71/3.90 (Or (Eq (cMEAT_EATS cBIRD cSNAIL) True) (Or (Eq (cVEG_EATS cSNAIL a_1) False) (Eq False True))) % 3.71/3.90 Clause #46 (by clausification #[43]): ∀ (a a_1 : p), Or (Eq (cVEG_EATS cFOX a) True) (Or (Eq (cMEAT_EATS cFOX cBIRD) True) (Eq (cVEG_EATS cBIRD a_1) False)) % 3.71/3.90 Clause #48 (by clausification #[44]): ∀ (a a_1 : p), % 3.71/3.90 Or (Eq (cVEG_EATS cBIRD a) True) (Or (Eq (cMEAT_EATS cBIRD cSNAIL) True) (Eq (cVEG_EATS cSNAIL a_1) False)) % 3.71/3.90 Clause #49 (by superposition #[48, 7]): ∀ (a : p), Or (Eq (cVEG_EATS cBIRD a) True) (Or (Eq (cMEAT_EATS cBIRD cSNAIL) True) (Eq False True)) % 3.71/3.90 Clause #50 (by clausification #[49]): ∀ (a : p), Or (Eq (cVEG_EATS cBIRD a) True) (Eq (cMEAT_EATS cBIRD cSNAIL) True) % 3.71/3.90 Clause #52 (by superposition #[50, 16]): ∀ (a : p), Or (Eq (cVEG_EATS cBIRD a) True) (Eq True False) % 3.71/3.90 Clause #54 (by clausification #[42]): ∀ (a a_1 : p), Or (Eq (cVEG_EATS cWOLF a) True) (Or (Eq (cMEAT_EATS cWOLF cFOX) True) (Eq (cVEG_EATS cFOX a_1) False)) % 3.71/3.90 Clause #55 (by clausification #[52]): ∀ (a : p), Eq (cVEG_EATS cBIRD a) True % 3.71/3.90 Clause #56 (by superposition #[55, 46]): ∀ (a : p), Or (Eq (cVEG_EATS cFOX a) True) (Or (Eq (cMEAT_EATS cFOX cBIRD) True) (Eq True False)) % 3.71/3.90 Clause #57 (by clausification #[56]): ∀ (a : p), Or (Eq (cVEG_EATS cFOX a) True) (Eq (cMEAT_EATS cFOX cBIRD) True) % 3.71/3.90 Clause #59 (by superposition #[57, 10]): ∀ (a : p), Or (Eq (cVEG_EATS cFOX a) True) (Or (Eq True False) (Eq (cVEG_EATS cBIRD cGRAIN) False)) % 3.71/3.90 Clause #60 (by clausification #[59]): ∀ (a : p), Or (Eq (cVEG_EATS cFOX a) True) (Eq (cVEG_EATS cBIRD cGRAIN) False) % 3.71/3.90 Clause #61 (by forward demodulation #[60, 55]): ∀ (a : p), Or (Eq (cVEG_EATS cFOX a) True) (Eq True False) % 3.71/3.90 Clause #62 (by clausification #[61]): ∀ (a : p), Eq (cVEG_EATS cFOX a) True % 3.71/3.90 Clause #63 (by superposition #[62, 54]): ∀ (a : p), Or (Eq (cVEG_EATS cWOLF a) True) (Or (Eq (cMEAT_EATS cWOLF cFOX) True) (Eq True False)) % 3.71/3.90 Clause #64 (by clausification #[63]): ∀ (a : p), Or (Eq (cVEG_EATS cWOLF a) True) (Eq (cMEAT_EATS cWOLF cFOX) True) % 3.71/3.90 Clause #65 (by superposition #[64, 26]): ∀ (a : p), Or (Eq (cVEG_EATS cWOLF a) True) (Eq True False) % 3.71/3.90 Clause #67 (by clausification #[65]): ∀ (a : p), Eq (cVEG_EATS cWOLF a) True % 3.71/3.90 Clause #68 (by superposition #[67, 22]): Eq True False % 3.71/3.90 Clause #71 (by clausification #[68]): False % 3.71/3.90 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------