%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYN047+1 : TPTP v9.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:07:02 PM UTC 2025 % Result : Theorem 3.52s 3.74s % Output : Proof 3.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYN047+1 : TPTP v9.2.0. Released v2.0.0. % 0.03/0.14 % Command : duper %s % 0.13/0.35 % Computer : n007.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 15:29:08 EDT 2025 % 0.13/0.36 % CPUTime : % 3.52/3.74 SZS status Theorem for theBenchmark.p % 3.52/3.74 SZS output start Proof for theBenchmark.p % 3.52/3.74 Clause #0 (by assumption #[]): Eq (Not (Iff (And p (q → r) → s) (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)))) True % 3.52/3.74 Clause #1 (by clausification #[0]): Eq (Iff (And p (q → r) → s) (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s))) False % 3.52/3.74 Clause #2 (by clausification #[1]): Or (Eq (And p (q → r) → s) False) (Eq (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)) False) % 3.52/3.74 Clause #3 (by clausification #[1]): Or (Eq (And p (q → r) → s) True) (Eq (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)) True) % 3.52/3.74 Clause #4 (by clausification #[2]): Or (Eq (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)) False) (Eq (And p (q → r)) True) % 3.52/3.74 Clause #5 (by clausification #[2]): Or (Eq (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)) False) (Eq s False) % 3.52/3.74 Clause #6 (by clausification #[4]): Or (Eq (And p (q → r)) True) (Or (Eq (Or (Or (Not p) q) s) False) (Eq (Or (Or (Not p) (Not r)) s) False)) % 3.52/3.74 Clause #7 (by clausification #[6]): Or (Eq (Or (Or (Not p) q) s) False) (Or (Eq (Or (Or (Not p) (Not r)) s) False) (Eq (q → r) True)) % 3.52/3.74 Clause #8 (by clausification #[6]): Or (Eq (Or (Or (Not p) q) s) False) (Or (Eq (Or (Or (Not p) (Not r)) s) False) (Eq p True)) % 3.52/3.74 Clause #10 (by clausification #[7]): Or (Eq (Or (Or (Not p) (Not r)) s) False) (Or (Eq (q → r) True) (Eq (Or (Not p) q) False)) % 3.52/3.74 Clause #21 (by clausification #[10]): Or (Eq (q → r) True) (Or (Eq (Or (Not p) q) False) (Eq (Or (Not p) (Not r)) False)) % 3.52/3.74 Clause #24 (by clausification #[21]): Or (Eq (Or (Not p) q) False) (Or (Eq (Or (Not p) (Not r)) False) (Or (Eq q False) (Eq r True))) % 3.52/3.74 Clause #25 (by clausification #[24]): Or (Eq (Or (Not p) (Not r)) False) (Or (Eq q False) (Or (Eq r True) (Eq q False))) % 3.52/3.74 Clause #27 (by clausification #[25]): Or (Eq q False) (Or (Eq r True) (Or (Eq q False) (Eq (Not r) False))) % 3.52/3.74 Clause #29 (by clausification #[27]): Or (Eq q False) (Or (Eq r True) (Or (Eq q False) (Eq r True))) % 3.52/3.74 Clause #30 (by eliminate duplicate literals #[29]): Or (Eq q False) (Eq r True) % 3.52/3.74 Clause #31 (by clausification #[3]): Or (Eq (And (Or (Or (Not p) q) s) (Or (Or (Not p) (Not r)) s)) True) (Or (Eq (And p (q → r)) False) (Eq s True)) % 3.52/3.74 Clause #32 (by clausification #[31]): Or (Eq (And p (q → r)) False) (Or (Eq s True) (Eq (Or (Or (Not p) (Not r)) s) True)) % 3.52/3.74 Clause #33 (by clausification #[31]): Or (Eq (And p (q → r)) False) (Or (Eq s True) (Eq (Or (Or (Not p) q) s) True)) % 3.52/3.74 Clause #34 (by clausification #[32]): Or (Eq s True) (Or (Eq (Or (Or (Not p) (Not r)) s) True) (Or (Eq p False) (Eq (q → r) False))) % 3.52/3.74 Clause #35 (by clausification #[34]): Or (Eq s True) (Or (Eq p False) (Or (Eq (q → r) False) (Or (Eq (Or (Not p) (Not r)) True) (Eq s True)))) % 3.52/3.74 Clause #37 (by clausification #[35]): Or (Eq s True) (Or (Eq p False) (Or (Eq (Or (Not p) (Not r)) True) (Or (Eq s True) (Eq r False)))) % 3.52/3.74 Clause #50 (by clausification #[37]): Or (Eq s True) (Or (Eq p False) (Or (Eq s True) (Or (Eq r False) (Or (Eq (Not p) True) (Eq (Not r) True))))) % 3.52/3.74 Clause #51 (by clausification #[50]): Or (Eq s True) (Or (Eq p False) (Or (Eq s True) (Or (Eq r False) (Or (Eq (Not r) True) (Eq p False))))) % 3.52/3.74 Clause #52 (by clausification #[51]): Or (Eq s True) (Or (Eq p False) (Or (Eq s True) (Or (Eq r False) (Or (Eq p False) (Eq r False))))) % 3.52/3.74 Clause #53 (by eliminate duplicate literals #[52]): Or (Eq s True) (Or (Eq p False) (Eq r False)) % 3.52/3.74 Clause #54 (by clausification #[33]): Or (Eq s True) (Or (Eq (Or (Or (Not p) q) s) True) (Or (Eq p False) (Eq (q → r) False))) % 3.52/3.74 Clause #55 (by clausification #[54]): Or (Eq s True) (Or (Eq p False) (Or (Eq (q → r) False) (Or (Eq (Or (Not p) q) True) (Eq s True)))) % 3.52/3.74 Clause #56 (by clausification #[55]): Or (Eq s True) (Or (Eq p False) (Or (Eq (Or (Not p) q) True) (Or (Eq s True) (Eq q True)))) % 3.52/3.74 Clause #58 (by clausification #[56]): Or (Eq s True) (Or (Eq p False) (Or (Eq s True) (Or (Eq q True) (Or (Eq (Not p) True) (Eq q True))))) % 3.52/3.74 Clause #59 (by clausification #[58]): Or (Eq s True) (Or (Eq p False) (Or (Eq s True) (Or (Eq q True) (Or (Eq q True) (Eq p False))))) % 3.52/3.74 Clause #60 (by eliminate duplicate literals #[59]): Or (Eq s True) (Or (Eq p False) (Eq q True)) % 3.52/3.75 Clause #61 (by clausification #[5]): Or (Eq s False) (Or (Eq (Or (Or (Not p) q) s) False) (Eq (Or (Or (Not p) (Not r)) s) False)) % 3.52/3.75 Clause #62 (by clausification #[61]): Or (Eq s False) (Or (Eq (Or (Or (Not p) (Not r)) s) False) (Eq s False)) % 3.52/3.75 Clause #64 (by clausification #[62]): Or (Eq s False) (Or (Eq s False) (Eq s False)) % 3.52/3.75 Clause #66 (by eliminate duplicate literals #[64]): Eq s False % 3.52/3.75 Clause #67 (by backward demodulation #[66, 53]): Or (Eq False True) (Or (Eq p False) (Eq r False)) % 3.52/3.75 Clause #68 (by backward demodulation #[66, 60]): Or (Eq False True) (Or (Eq p False) (Eq q True)) % 3.52/3.75 Clause #69 (by clausification #[68]): Or (Eq p False) (Eq q True) % 3.52/3.75 Clause #70 (by clausification #[67]): Or (Eq p False) (Eq r False) % 3.52/3.75 Clause #84 (by clausification #[8]): Or (Eq (Or (Or (Not p) (Not r)) s) False) (Or (Eq p True) (Eq (Or (Not p) q) False)) % 3.52/3.75 Clause #105 (by clausification #[84]): Or (Eq p True) (Or (Eq (Or (Not p) q) False) (Eq (Or (Not p) (Not r)) False)) % 3.52/3.75 Clause #116 (by clausification #[105]): Or (Eq p True) (Or (Eq (Or (Not p) (Not r)) False) (Eq (Not p) False)) % 3.52/3.75 Clause #123 (by clausification #[116]): Or (Eq p True) (Or (Eq (Not p) False) (Eq (Not p) False)) % 3.52/3.75 Clause #127 (by clausification #[123]): Or (Eq p True) (Or (Eq (Not p) False) (Eq p True)) % 3.52/3.75 Clause #128 (by clausification #[127]): Or (Eq p True) (Or (Eq p True) (Eq p True)) % 3.52/3.75 Clause #129 (by eliminate duplicate literals #[128]): Eq p True % 3.52/3.75 Clause #130 (by backward demodulation #[129, 69]): Or (Eq True False) (Eq q True) % 3.52/3.75 Clause #131 (by backward demodulation #[129, 70]): Or (Eq True False) (Eq r False) % 3.52/3.75 Clause #134 (by clausification #[131]): Eq r False % 3.52/3.75 Clause #135 (by clausification #[130]): Eq q True % 3.52/3.75 Clause #136 (by backward demodulation #[135, 30]): Or (Eq True False) (Eq r True) % 3.52/3.75 Clause #137 (by clausification #[136]): Eq r True % 3.52/3.75 Clause #138 (by superposition #[137, 134]): Eq True False % 3.52/3.75 Clause #139 (by clausification #[138]): False % 3.52/3.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------