↑ Up

Duper---1.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : ALG030+1 : TPTP v9.2.0. Released v2.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n028.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:43:55 PM UTC 2025

% Result   : Theorem 282.85s 283.01s
% Output   : Proof 283.36s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : ALG030+1 : TPTP v9.2.0. Released v2.7.0.
% 0.13/0.13  % Command    : duper %s
% 0.13/0.33  % Computer : n028.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.19/0.33  % CPULimit   : 300
% 0.19/0.33  % WCLimit    : 300
% 0.19/0.33  % DateTime   : Fri Oct  3 09:14:38 EDT 2025
% 0.19/0.34  % CPUTime    : 
% 282.85/283.01  SZS status Theorem for theBenchmark.p
% 282.85/283.01  SZS output start Proof for theBenchmark.p
% 282.85/283.01  Clause #0 (by assumption #[]): Eq (∀ (U : Iota), sorti1 U → ∀ (V : Iota), sorti1 V → sorti1 (op1 U V)) True
% 282.85/283.01  Clause #2 (by assumption #[]): Eq (Not (∀ (U : Iota), sorti1 U → ∀ (V : Iota), sorti1 V → Eq (op1 U V) (op1 V U))) True
% 282.85/283.01  Clause #3 (by assumption #[]): Eq (Not (Not (∀ (U : Iota), sorti2 U → ∀ (V : Iota), sorti2 V → Eq (op2 U V) (op2 V U)))) True
% 282.85/283.01  Clause #4 (by assumption #[]): Eq
% 282.85/283.01    (Not
% 282.85/283.01      (And (∀ (U : Iota), sorti1 U → sorti2 (h U)) (∀ (V : Iota), sorti2 V → sorti1 (j V)) →
% 282.85/283.01        Not
% 282.85/283.01          (And
% 282.85/283.01            (And
% 282.85/283.01              (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.01                (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.01              (∀ (X1 : Iota), sorti2 X1 → Eq (h (j X1)) X1))
% 282.85/283.01            (∀ (X2 : Iota), sorti1 X2 → Eq (j (h X2)) X2))))
% 282.85/283.01    True
% 282.85/283.01  Clause #9 (by clausification #[0]): ∀ (a : Iota), Eq (sorti1 a → ∀ (V : Iota), sorti1 V → sorti1 (op1 a V)) True
% 282.85/283.01  Clause #10 (by clausification #[9]): ∀ (a : Iota), Or (Eq (sorti1 a) False) (Eq (∀ (V : Iota), sorti1 V → sorti1 (op1 a V)) True)
% 282.85/283.01  Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Eq (sorti1 a_1 → sorti1 (op1 a a_1)) True)
% 282.85/283.01  Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Or (Eq (sorti1 a_1) False) (Eq (sorti1 (op1 a a_1)) True))
% 282.85/283.01  Clause #13 (by clausification #[2]): Eq (∀ (U : Iota), sorti1 U → ∀ (V : Iota), sorti1 V → Eq (op1 U V) (op1 V U)) False
% 282.85/283.01  Clause #14 (by clausification #[13]): ∀ (a : Iota), Eq (Not (sorti1 (skS.0 0 a) → ∀ (V : Iota), sorti1 V → Eq (op1 (skS.0 0 a) V) (op1 V (skS.0 0 a)))) True
% 282.85/283.01  Clause #15 (by clausification #[14]): ∀ (a : Iota), Eq (sorti1 (skS.0 0 a) → ∀ (V : Iota), sorti1 V → Eq (op1 (skS.0 0 a) V) (op1 V (skS.0 0 a))) False
% 282.85/283.01  Clause #16 (by clausification #[15]): ∀ (a : Iota), Eq (sorti1 (skS.0 0 a)) True
% 282.85/283.01  Clause #17 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (V : Iota), sorti1 V → Eq (op1 (skS.0 0 a) V) (op1 V (skS.0 0 a))) False
% 282.85/283.01  Clause #18 (by superposition #[16, 12]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (sorti1 a) False) (Eq (sorti1 (op1 (skS.0 0 a_1) a)) True))
% 282.85/283.01  Clause #19 (by clausification #[3]): Eq (Not (∀ (U : Iota), sorti2 U → ∀ (V : Iota), sorti2 V → Eq (op2 U V) (op2 V U))) False
% 282.85/283.01  Clause #20 (by clausification #[19]): Eq (∀ (U : Iota), sorti2 U → ∀ (V : Iota), sorti2 V → Eq (op2 U V) (op2 V U)) True
% 282.85/283.01  Clause #21 (by clausification #[20]): ∀ (a : Iota), Eq (sorti2 a → ∀ (V : Iota), sorti2 V → Eq (op2 a V) (op2 V a)) True
% 282.85/283.01  Clause #22 (by clausification #[21]): ∀ (a : Iota), Or (Eq (sorti2 a) False) (Eq (∀ (V : Iota), sorti2 V → Eq (op2 a V) (op2 V a)) True)
% 282.85/283.01  Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), Or (Eq (sorti2 a) False) (Eq (sorti2 a_1 → Eq (op2 a a_1) (op2 a_1 a)) True)
% 282.85/283.01  Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), Or (Eq (sorti2 a) False) (Or (Eq (sorti2 a_1) False) (Eq (Eq (op2 a a_1) (op2 a_1 a)) True))
% 282.85/283.01  Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), Or (Eq (sorti2 a) False) (Or (Eq (sorti2 a_1) False) (Eq (op2 a a_1) (op2 a_1 a)))
% 282.85/283.01  Clause #26 (by clausification #[18]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Eq (sorti1 (op1 (skS.0 0 a_1) a)) True)
% 282.85/283.01  Clause #28 (by clausification #[4]): Eq
% 282.85/283.01    (And (∀ (U : Iota), sorti1 U → sorti2 (h U)) (∀ (V : Iota), sorti2 V → sorti1 (j V)) →
% 282.85/283.01      Not
% 282.85/283.01        (And
% 282.85/283.01          (And
% 282.85/283.01            (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.01              (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.01            (∀ (X1 : Iota), sorti2 X1 → Eq (h (j X1)) X1))
% 282.85/283.01          (∀ (X2 : Iota), sorti1 X2 → Eq (j (h X2)) X2)))
% 282.85/283.01    False
% 282.85/283.01  Clause #29 (by clausification #[28]): Eq (And (∀ (U : Iota), sorti1 U → sorti2 (h U)) (∀ (V : Iota), sorti2 V → sorti1 (j V))) True
% 282.85/283.01  Clause #30 (by clausification #[28]): Eq
% 282.85/283.03    (Not
% 282.85/283.03      (And
% 282.85/283.03        (And
% 282.85/283.03          (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.03            (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.03          (∀ (X1 : Iota), sorti2 X1 → Eq (h (j X1)) X1))
% 282.85/283.03        (∀ (X2 : Iota), sorti1 X2 → Eq (j (h X2)) X2)))
% 282.85/283.03    False
% 282.85/283.03  Clause #32 (by clausification #[29]): Eq (∀ (U : Iota), sorti1 U → sorti2 (h U)) True
% 282.85/283.03  Clause #35 (by clausification #[32]): ∀ (a : Iota), Eq (sorti1 a → sorti2 (h a)) True
% 282.85/283.03  Clause #36 (by clausification #[35]): ∀ (a : Iota), Or (Eq (sorti1 a) False) (Eq (sorti2 (h a)) True)
% 282.85/283.03  Clause #37 (by superposition #[36, 16]): ∀ (a : Iota), Or (Eq (sorti2 (h (skS.0 0 a))) True) (Eq False True)
% 282.85/283.03  Clause #38 (by clausification #[37]): ∀ (a : Iota), Eq (sorti2 (h (skS.0 0 a))) True
% 282.85/283.03  Clause #40 (by superposition #[38, 25]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (sorti2 a) False) (Eq (op2 (h (skS.0 0 a_1)) a) (op2 a (h (skS.0 0 a_1)))))
% 282.85/283.03  Clause #54 (by clausification #[17]): ∀ (a a_1 : Iota),
% 282.85/283.03    Eq (Not (sorti1 (skS.0 1 a a_1) → Eq (op1 (skS.0 0 a) (skS.0 1 a a_1)) (op1 (skS.0 1 a a_1) (skS.0 0 a)))) True
% 282.85/283.03  Clause #55 (by clausification #[54]): ∀ (a a_1 : Iota),
% 282.85/283.03    Eq (sorti1 (skS.0 1 a a_1) → Eq (op1 (skS.0 0 a) (skS.0 1 a a_1)) (op1 (skS.0 1 a a_1) (skS.0 0 a))) False
% 282.85/283.03  Clause #56 (by clausification #[55]): ∀ (a a_1 : Iota), Eq (sorti1 (skS.0 1 a a_1)) True
% 282.85/283.03  Clause #57 (by clausification #[55]): ∀ (a a_1 : Iota), Eq (Eq (op1 (skS.0 0 a) (skS.0 1 a a_1)) (op1 (skS.0 1 a a_1) (skS.0 0 a))) False
% 282.85/283.03  Clause #58 (by superposition #[56, 12]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Or (Eq (sorti1 a) False) (Eq (sorti1 (op1 (skS.0 1 a_1 a_2) a)) True))
% 282.85/283.03  Clause #59 (by superposition #[56, 26]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (sorti1 (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) True)
% 282.85/283.03  Clause #60 (by superposition #[56, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (sorti2 (h (skS.0 1 a a_1))) True)
% 282.85/283.03  Clause #61 (by clausification #[60]): ∀ (a a_1 : Iota), Eq (sorti2 (h (skS.0 1 a a_1))) True
% 282.85/283.03  Clause #105 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), Or (Eq (sorti1 a) False) (Eq (sorti1 (op1 (skS.0 1 a_1 a_2) a)) True)
% 282.85/283.03  Clause #106 (by superposition #[105, 16]): ∀ (a a_1 a_2 : Iota), Or (Eq (sorti1 (op1 (skS.0 1 a a_1) (skS.0 0 a_2))) True) (Eq False True)
% 282.85/283.03  Clause #114 (by clausification #[30]): Eq
% 282.85/283.03    (And
% 282.85/283.03      (And
% 282.85/283.03        (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.03          (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.03        (∀ (X1 : Iota), sorti2 X1 → Eq (h (j X1)) X1))
% 282.85/283.03      (∀ (X2 : Iota), sorti1 X2 → Eq (j (h X2)) X2))
% 282.85/283.03    True
% 282.85/283.03  Clause #115 (by clausification #[114]): Eq (∀ (X2 : Iota), sorti1 X2 → Eq (j (h X2)) X2) True
% 282.85/283.03  Clause #116 (by clausification #[114]): Eq
% 282.85/283.03    (And
% 282.85/283.03      (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.03        (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.03      (∀ (X1 : Iota), sorti2 X1 → Eq (h (j X1)) X1))
% 282.85/283.03    True
% 282.85/283.03  Clause #117 (by clausification #[115]): ∀ (a : Iota), Eq (sorti1 a → Eq (j (h a)) a) True
% 282.85/283.03  Clause #118 (by clausification #[117]): ∀ (a : Iota), Or (Eq (sorti1 a) False) (Eq (Eq (j (h a)) a) True)
% 282.85/283.03  Clause #119 (by clausification #[118]): ∀ (a : Iota), Or (Eq (sorti1 a) False) (Eq (j (h a)) a)
% 282.85/283.03  Clause #142 (by clausification #[40]): ∀ (a a_1 : Iota), Or (Eq (sorti2 a) False) (Eq (op2 (h (skS.0 0 a_1)) a) (op2 a (h (skS.0 0 a_1))))
% 282.85/283.03  Clause #144 (by superposition #[142, 61]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.03    Or (Eq (op2 (h (skS.0 0 a)) (h (skS.0 1 a_1 a_2))) (op2 (h (skS.0 1 a_1 a_2)) (h (skS.0 0 a)))) (Eq False True)
% 282.85/283.03  Clause #155 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), Eq (sorti1 (op1 (skS.0 1 a a_1) (skS.0 0 a_2))) True
% 282.85/283.03  Clause #160 (by superposition #[155, 119]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.03    Or (Eq True False) (Eq (j (h (op1 (skS.0 1 a a_1) (skS.0 0 a_2)))) (op1 (skS.0 1 a a_1) (skS.0 0 a_2)))
% 282.85/283.06  Clause #185 (by clausification #[59]): ∀ (a a_1 a_2 : Iota), Eq (sorti1 (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) True
% 282.85/283.06  Clause #190 (by superposition #[185, 119]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.06    Or (Eq True False) (Eq (j (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2)))) (op1 (skS.0 0 a) (skS.0 1 a_1 a_2)))
% 282.85/283.06  Clause #256 (by clausification #[57]): ∀ (a a_1 : Iota), Ne (op1 (skS.0 0 a) (skS.0 1 a a_1)) (op1 (skS.0 1 a a_1) (skS.0 0 a))
% 282.85/283.06  Clause #773 (by clausification #[116]): Eq
% 282.85/283.06    (And (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X)))
% 282.85/283.06      (∀ (Y : Iota), sorti2 Y → ∀ (Z : Iota), sorti2 Z → Eq (j (op2 Y Z)) (op1 (j Y) (j Z))))
% 282.85/283.06    True
% 282.85/283.06  Clause #1434 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), Eq (op2 (h (skS.0 0 a)) (h (skS.0 1 a_1 a_2))) (op2 (h (skS.0 1 a_1 a_2)) (h (skS.0 0 a)))
% 282.85/283.06  Clause #1981 (by clausification #[160]): ∀ (a a_1 a_2 : Iota), Eq (j (h (op1 (skS.0 1 a a_1) (skS.0 0 a_2)))) (op1 (skS.0 1 a a_1) (skS.0 0 a_2))
% 282.85/283.06  Clause #2935 (by clausification #[190]): ∀ (a a_1 a_2 : Iota), Eq (j (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2)))) (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))
% 282.85/283.06  Clause #12629 (by clausification #[773]): Eq (∀ (W : Iota), sorti1 W → ∀ (X : Iota), sorti1 X → Eq (h (op1 W X)) (op2 (h W) (h X))) True
% 282.85/283.06  Clause #12775 (by clausification #[12629]): ∀ (a : Iota), Eq (sorti1 a → ∀ (X : Iota), sorti1 X → Eq (h (op1 a X)) (op2 (h a) (h X))) True
% 282.85/283.06  Clause #12776 (by clausification #[12775]): ∀ (a : Iota), Or (Eq (sorti1 a) False) (Eq (∀ (X : Iota), sorti1 X → Eq (h (op1 a X)) (op2 (h a) (h X))) True)
% 282.85/283.06  Clause #12777 (by clausification #[12776]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Eq (sorti1 a_1 → Eq (h (op1 a a_1)) (op2 (h a) (h a_1))) True)
% 282.85/283.06  Clause #12778 (by clausification #[12777]): ∀ (a a_1 : Iota),
% 282.85/283.06    Or (Eq (sorti1 a) False) (Or (Eq (sorti1 a_1) False) (Eq (Eq (h (op1 a a_1)) (op2 (h a) (h a_1))) True))
% 282.85/283.06  Clause #12779 (by clausification #[12778]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Or (Eq (sorti1 a_1) False) (Eq (h (op1 a a_1)) (op2 (h a) (h a_1))))
% 282.85/283.06  Clause #12780 (by superposition #[12779, 16]): ∀ (a a_1 : Iota),
% 282.85/283.06    Or (Eq (sorti1 a) False) (Or (Eq (h (op1 (skS.0 0 a_1) a)) (op2 (h (skS.0 0 a_1)) (h a))) (Eq False True))
% 282.85/283.06  Clause #12781 (by superposition #[12779, 56]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.06    Or (Eq (sorti1 a) False) (Or (Eq (h (op1 (skS.0 1 a_1 a_2) a)) (op2 (h (skS.0 1 a_1 a_2)) (h a))) (Eq False True))
% 282.85/283.06  Clause #12928 (by clausification #[12780]): ∀ (a a_1 : Iota), Or (Eq (sorti1 a) False) (Eq (h (op1 (skS.0 0 a_1) a)) (op2 (h (skS.0 0 a_1)) (h a)))
% 282.85/283.06  Clause #12930 (by superposition #[12928, 56]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.06    Or (Eq (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) (op2 (h (skS.0 0 a)) (h (skS.0 1 a_1 a_2)))) (Eq False True)
% 282.85/283.06  Clause #13220 (by clausification #[12781]): ∀ (a a_1 a_2 : Iota), Or (Eq (sorti1 a) False) (Eq (h (op1 (skS.0 1 a_1 a_2) a)) (op2 (h (skS.0 1 a_1 a_2)) (h a)))
% 282.85/283.06  Clause #13221 (by superposition #[13220, 16]): ∀ (a a_1 a_2 : Iota),
% 282.85/283.06    Or (Eq (h (op1 (skS.0 1 a a_1) (skS.0 0 a_2))) (op2 (h (skS.0 1 a a_1)) (h (skS.0 0 a_2)))) (Eq False True)
% 282.85/283.06  Clause #53462 (by clausification #[12930]): ∀ (a a_1 a_2 : Iota), Eq (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) (op2 (h (skS.0 0 a)) (h (skS.0 1 a_1 a_2)))
% 282.85/283.06  Clause #53463 (by backward demodulation #[53462, 1434]): ∀ (a a_1 a_2 : Iota), Eq (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) (op2 (h (skS.0 1 a_1 a_2)) (h (skS.0 0 a)))
% 282.85/283.06  Clause #53517 (by clausification #[13221]): ∀ (a a_1 a_2 : Iota), Eq (h (op1 (skS.0 1 a a_1) (skS.0 0 a_2))) (op2 (h (skS.0 1 a a_1)) (h (skS.0 0 a_2)))
% 282.85/283.06  Clause #53518 (by superposition #[53517, 53463]): ∀ (a a_1 a_2 : Iota), Eq (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2))) (h (op1 (skS.0 1 a_1 a_2) (skS.0 0 a)))
% 282.85/283.06  Clause #53520 (by superposition #[53518, 1981]): ∀ (a a_1 a_2 : Iota), Eq (j (h (op1 (skS.0 0 a) (skS.0 1 a_1 a_2)))) (op1 (skS.0 1 a_1 a_2) (skS.0 0 a))
% 282.85/283.06  Clause #53521 (by superposition #[53520, 2935]): ∀ (a a_1 a_2 : Iota), Eq (op1 (skS.0 1 a a_1) (skS.0 0 a_2)) (op1 (skS.0 0 a_2) (skS.0 1 a a_1))
% 282.85/283.06  Clause #53522 (by backward contextual literal cutting #[53521, 256]): False
% 283.36/283.59  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------