%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ047+1 : TPTP v9.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:16 PM UTC 2025 % Result : Theorem 5.46s 5.70s % Output : Proof 5.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ047+1 : TPTP v9.2.0. Released v2.5.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n021.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 : Thu Oct 2 20:52:38 EDT 2025 % 0.13/0.34 % CPUTime : % 5.46/5.70 SZS status Theorem for theBenchmark.p % 5.46/5.70 SZS output start Proof for theBenchmark.p % 5.46/5.70 Clause #0 (by assumption #[]): Eq % 5.46/5.70 (Not % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And (p south south south south start) % 5.46/5.70 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.46/5.70 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.46/5.70 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.46/5.70 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.46/5.70 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.46/5.70 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.46/5.70 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.46/5.70 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.46/5.70 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.46/5.70 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.46/5.70 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.46/5.70 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.46/5.70 (∀ (U1 : Iota), p south south north south U1 → p north south north north (take_cabbage U1))) % 5.46/5.70 (∀ (V1 : Iota), p north south north north V1 → p south south north south (take_cabbage V1)) → % 5.46/5.70 Exists fun Z => p north north north north Z)) % 5.46/5.70 True % 5.46/5.70 Clause #1 (by betaEtaReduce #[0]): Eq % 5.46/5.70 (Not % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And % 5.46/5.70 (And (p south south south south start) % 5.46/5.70 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.46/5.70 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.46/5.70 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.46/5.70 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.46/5.70 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.46/5.70 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.46/5.70 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.46/5.70 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.46/5.70 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.46/5.70 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.46/5.70 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.46/5.70 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.46/5.70 (∀ (U1 : Iota), p south south north south U1 → p north south north north (take_cabbage U1))) % 5.46/5.70 (∀ (V1 : Iota), p north south north north V1 → p south south north south (take_cabbage V1)) → % 5.56/5.72 Exists (p north north north north))) % 5.56/5.72 True % 5.56/5.72 Clause #2 (by clausification #[1]): Eq % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And (p south south south south start) % 5.56/5.72 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.72 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.72 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.72 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.72 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.72 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.72 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.72 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.72 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.72 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.72 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.56/5.72 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.56/5.72 (∀ (U1 : Iota), p south south north south U1 → p north south north north (take_cabbage U1))) % 5.56/5.72 (∀ (V1 : Iota), p north south north north V1 → p south south north south (take_cabbage V1)) → % 5.56/5.72 Exists (p north north north north)) % 5.56/5.72 False % 5.56/5.72 Clause #3 (by clausification #[2]): Eq % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And % 5.56/5.72 (And (p south south south south start) % 5.56/5.72 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.72 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.72 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.72 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.72 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.72 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.72 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.72 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.72 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.72 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.72 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.56/5.72 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.56/5.72 (∀ (U1 : Iota), p south south north south U1 → p north south north north (take_cabbage U1))) % 5.56/5.72 (∀ (V1 : Iota), p north south north north V1 → p south south north south (take_cabbage V1))) % 5.56/5.72 True % 5.56/5.72 Clause #4 (by clausification #[2]): Eq (Exists (p north north north north)) False % 5.56/5.72 Clause #6 (by clausification #[3]): Eq % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And (p south south south south start) % 5.56/5.73 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.73 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.73 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.73 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.73 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.73 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.73 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.73 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.73 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.73 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.73 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.56/5.73 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.56/5.73 (∀ (U1 : Iota), p south south north south U1 → p north south north north (take_cabbage U1))) % 5.56/5.73 True % 5.56/5.73 Clause #9 (by clausification #[4]): ∀ (a : Iota), Eq (p north north north north a) False % 5.56/5.73 Clause #11 (by clausification #[6]): Eq % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And (p south south south south start) % 5.56/5.73 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.73 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.73 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.73 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.73 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.73 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.73 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.73 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.73 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.73 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.73 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.56/5.73 (∀ (T9 : Iota), p north north south north T9 → p south north south south (take_cabbage T9))) % 5.56/5.73 True % 5.56/5.73 Clause #15 (by clausification #[11]): Eq % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And % 5.56/5.73 (And (p south south south south start) % 5.56/5.73 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.73 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.73 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.73 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.75 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.75 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.75 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.75 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.75 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.75 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.75 (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8))) % 5.56/5.75 True % 5.56/5.75 Clause #18 (by clausification #[15]): Eq (∀ (T8 : Iota), p south north south south T8 → p north north south north (take_cabbage T8)) True % 5.56/5.75 Clause #19 (by clausification #[15]): Eq % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And (p south south south south start) % 5.56/5.75 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.75 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.75 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.75 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.75 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.75 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.75 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.75 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.75 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.75 (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V))) % 5.56/5.75 True % 5.56/5.75 Clause #20 (by clausification #[18]): ∀ (a : Iota), Eq (p south north south south a → p north north south north (take_cabbage a)) True % 5.56/5.75 Clause #21 (by clausification #[20]): ∀ (a : Iota), Or (Eq (p south north south south a) False) (Eq (p north north south north (take_cabbage a)) True) % 5.56/5.75 Clause #22 (by clausification #[19]): Eq (∀ (X1 Y1 V : Iota), p north X1 north Y1 V → p south X1 south Y1 (take_goat V)) True % 5.56/5.75 Clause #23 (by clausification #[19]): Eq % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And % 5.56/5.75 (And (p south south south south start) % 5.56/5.75 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.75 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.75 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.75 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.75 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.75 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.75 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.75 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.75 (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U))) % 5.56/5.75 True % 5.56/5.75 Clause #24 (by clausification #[22]): ∀ (a : Iota), Eq (∀ (Y1 V : Iota), p north a north Y1 V → p south a south Y1 (take_goat V)) True % 5.56/5.75 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), Eq (∀ (V : Iota), p north a north a_1 V → p south a south a_1 (take_goat V)) True % 5.56/5.75 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), Eq (p north a north a_1 a_2 → p south a south a_1 (take_goat a_2)) True % 5.56/5.77 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota), Or (Eq (p north a north a_1 a_2) False) (Eq (p south a south a_1 (take_goat a_2)) True) % 5.56/5.77 Clause #28 (by clausification #[23]): Eq (∀ (X Y U : Iota), p south X south Y U → p north X north Y (take_goat U)) True % 5.56/5.77 Clause #29 (by clausification #[23]): Eq % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And (p south south south south start) % 5.56/5.77 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.77 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.77 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.77 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.77 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.77 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.77 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.77 (∀ (T7 : Iota), p north north north south T7 → p south south north south (take_wolf T7))) % 5.56/5.77 True % 5.56/5.77 Clause #30 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (Y U : Iota), p south a south Y U → p north a north Y (take_goat U)) True % 5.56/5.77 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), Eq (∀ (U : Iota), p south a south a_1 U → p north a north a_1 (take_goat U)) True % 5.56/5.77 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), Eq (p south a south a_1 a_2 → p north a north a_1 (take_goat a_2)) True % 5.56/5.77 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), Or (Eq (p south a south a_1 a_2) False) (Eq (p north a north a_1 (take_goat a_2)) True) % 5.56/5.77 Clause #35 (by clausification #[29]): Eq % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And (p south south south south start) % 5.56/5.77 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.77 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.77 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.77 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.77 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.77 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.77 (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6))) % 5.56/5.77 True % 5.56/5.77 Clause #38 (by clausification #[35]): Eq (∀ (T6 : Iota), p south south north south T6 → p north north north south (take_wolf T6)) True % 5.56/5.77 Clause #39 (by clausification #[35]): Eq % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And (p south south south south start) % 5.56/5.77 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.77 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.77 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.77 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.77 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.77 (∀ (T5 : Iota), p north north south north T5 → p south south south north (take_wolf T5))) % 5.56/5.77 True % 5.56/5.77 Clause #40 (by clausification #[38]): ∀ (a : Iota), Eq (p south south north south a → p north north north south (take_wolf a)) True % 5.56/5.77 Clause #41 (by clausification #[40]): ∀ (a : Iota), Or (Eq (p south south north south a) False) (Eq (p north north north south (take_wolf a)) True) % 5.56/5.77 Clause #43 (by clausification #[39]): Eq % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And % 5.56/5.77 (And (p south south south south start) % 5.56/5.78 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.78 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.78 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.78 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.78 (∀ (T4 : Iota), p south south south north T4 → p north north south north (take_wolf T4))) % 5.56/5.78 True % 5.56/5.78 Clause #47 (by clausification #[43]): Eq % 5.56/5.78 (And % 5.56/5.78 (And % 5.56/5.78 (And % 5.56/5.78 (And (p south south south south start) % 5.56/5.78 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.78 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.78 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.78 (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3))) % 5.56/5.78 True % 5.56/5.78 Clause #50 (by clausification #[47]): Eq (∀ (T3 : Iota), p north south north south T3 → p south south north south (go_alone T3)) True % 5.56/5.78 Clause #51 (by clausification #[47]): Eq % 5.56/5.78 (And % 5.56/5.78 (And % 5.56/5.78 (And (p south south south south start) % 5.56/5.78 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.78 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.78 (∀ (T2 : Iota), p south south north south T2 → p north south north south (go_alone T2))) % 5.56/5.78 True % 5.56/5.78 Clause #52 (by clausification #[50]): ∀ (a : Iota), Eq (p north south north south a → p south south north south (go_alone a)) True % 5.56/5.78 Clause #53 (by clausification #[52]): ∀ (a : Iota), Or (Eq (p north south north south a) False) (Eq (p south south north south (go_alone a)) True) % 5.56/5.78 Clause #55 (by clausification #[51]): Eq % 5.56/5.78 (And % 5.56/5.78 (And (p south south south south start) % 5.56/5.78 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.78 (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1))) % 5.56/5.78 True % 5.56/5.78 Clause #58 (by clausification #[55]): Eq (∀ (T1 : Iota), p north north south north T1 → p south north south north (go_alone T1)) True % 5.56/5.78 Clause #59 (by clausification #[55]): Eq % 5.56/5.78 (And (p south south south south start) % 5.56/5.78 (∀ (T : Iota), p south north south north T → p north north south north (go_alone T))) % 5.56/5.78 True % 5.56/5.78 Clause #60 (by clausification #[58]): ∀ (a : Iota), Eq (p north north south north a → p south north south north (go_alone a)) True % 5.56/5.78 Clause #61 (by clausification #[60]): ∀ (a : Iota), Or (Eq (p north north south north a) False) (Eq (p south north south north (go_alone a)) True) % 5.56/5.78 Clause #63 (by clausification #[59]): Eq (p south south south south start) True % 5.56/5.78 Clause #66 (by superposition #[63, 33]): Or (Eq True False) (Eq (p north south north south (take_goat start)) True) % 5.56/5.78 Clause #67 (by clausification #[66]): Eq (p north south north south (take_goat start)) True % 5.56/5.78 Clause #68 (by superposition #[67, 53]): Or (Eq True False) (Eq (p south south north south (go_alone (take_goat start))) True) % 5.56/5.78 Clause #70 (by clausification #[68]): Eq (p south south north south (go_alone (take_goat start))) True % 5.56/5.78 Clause #72 (by superposition #[70, 41]): Or (Eq True False) (Eq (p north north north south (take_wolf (go_alone (take_goat start)))) True) % 5.56/5.78 Clause #79 (by clausification #[72]): Eq (p north north north south (take_wolf (go_alone (take_goat start)))) True % 5.56/5.78 Clause #81 (by superposition #[79, 27]): Or (Eq True False) (Eq (p south north south south (take_goat (take_wolf (go_alone (take_goat start))))) True) % 5.56/5.78 Clause #105 (by clausification #[81]): Eq (p south north south south (take_goat (take_wolf (go_alone (take_goat start))))) True % 5.56/5.78 Clause #106 (by superposition #[105, 21]): Or (Eq True False) % 5.56/5.78 (Eq (p north north south north (take_cabbage (take_goat (take_wolf (go_alone (take_goat start)))))) True) % 5.56/5.78 Clause #166 (by clausification #[106]): Eq (p north north south north (take_cabbage (take_goat (take_wolf (go_alone (take_goat start)))))) True % 5.56/5.79 Clause #169 (by superposition #[166, 61]): Or (Eq True False) % 5.56/5.79 (Eq (p south north south north (go_alone (take_cabbage (take_goat (take_wolf (go_alone (take_goat start))))))) True) % 5.56/5.79 Clause #170 (by clausification #[169]): Eq (p south north south north (go_alone (take_cabbage (take_goat (take_wolf (go_alone (take_goat start))))))) True % 5.56/5.79 Clause #172 (by superposition #[170, 33]): Or (Eq True False) % 5.56/5.79 (Eq % 5.56/5.79 (p north north north north % 5.56/5.79 (take_goat (go_alone (take_cabbage (take_goat (take_wolf (go_alone (take_goat start)))))))) % 5.56/5.79 True) % 5.56/5.79 Clause #319 (by clausification #[172]): Eq % 5.56/5.79 (p north north north north (take_goat (go_alone (take_cabbage (take_goat (take_wolf (go_alone (take_goat start)))))))) % 5.56/5.79 True % 5.56/5.79 Clause #320 (by superposition #[319, 9]): Eq True False % 5.56/5.79 Clause #322 (by clausification #[320]): False % 5.56/5.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------