↑ Up

Duper---1.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : ALG001^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n025.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:53 PM UTC 2025

% Result   : Theorem 3.68s 3.89s
% Output   : Proof 3.77s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem    : ALG001^5 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.13  % Command    : duper %s
% 0.13/0.34  % Computer : n025.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 09:31:23 EDT 2025
% 0.13/0.34  % CPUTime    : 
% 3.68/3.89  SZS status Theorem for theBenchmark.p
% 3.68/3.89  SZS output start Proof for theBenchmark.p
% 3.68/3.89  Clause #0 (by assumption #[]): Eq
% 3.68/3.89    (Not
% 3.68/3.89      (∀ (Xh1 : g → b) (Xh2 : b → a) (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89        And (∀ (Xx Xy : g), Eq (Xh1 (Xf1 Xx Xy)) (Xf2 (Xh1 Xx) (Xh1 Xy)))
% 3.68/3.89            (∀ (Xx Xy : b), Eq (Xh2 (Xf2 Xx Xy)) (Xf3 (Xh2 Xx) (Xh2 Xy))) →
% 3.68/3.89          ∀ (Xx Xy : g), Eq (Xh2 (Xh1 (Xf1 Xx Xy))) (Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy)))))
% 3.68/3.89    True
% 3.68/3.89  Clause #1 (by clausification #[0]): Eq
% 3.68/3.89    (∀ (Xh1 : g → b) (Xh2 : b → a) (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89      And (∀ (Xx Xy : g), Eq (Xh1 (Xf1 Xx Xy)) (Xf2 (Xh1 Xx) (Xh1 Xy)))
% 3.68/3.89          (∀ (Xx Xy : b), Eq (Xh2 (Xf2 Xx Xy)) (Xf3 (Xh2 Xx) (Xh2 Xy))) →
% 3.68/3.89        ∀ (Xx Xy : g), Eq (Xh2 (Xh1 (Xf1 Xx Xy))) (Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy))))
% 3.68/3.89    False
% 3.68/3.89  Clause #2 (by clausification #[1]): ∀ (a_1 : g → b),
% 3.68/3.89    Eq
% 3.68/3.89      (Not
% 3.68/3.89        (∀ (Xh2 : b → a) (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89          And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (Xf1 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89              (∀ (Xx Xy : b), Eq (Xh2 (Xf2 Xx Xy)) (Xf3 (Xh2 Xx) (Xh2 Xy))) →
% 3.68/3.89            ∀ (Xx Xy : g), Eq (Xh2 (skS.0 0 a_1 (Xf1 Xx Xy))) (Xf3 (Xh2 (skS.0 0 a_1 Xx)) (Xh2 (skS.0 0 a_1 Xy)))))
% 3.68/3.89      True
% 3.68/3.89  Clause #3 (by clausification #[2]): ∀ (a_1 : g → b),
% 3.68/3.89    Eq
% 3.68/3.89      (∀ (Xh2 : b → a) (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89        And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (Xf1 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89            (∀ (Xx Xy : b), Eq (Xh2 (Xf2 Xx Xy)) (Xf3 (Xh2 Xx) (Xh2 Xy))) →
% 3.68/3.89          ∀ (Xx Xy : g), Eq (Xh2 (skS.0 0 a_1 (Xf1 Xx Xy))) (Xf3 (Xh2 (skS.0 0 a_1 Xx)) (Xh2 (skS.0 0 a_1 Xy))))
% 3.68/3.89      False
% 3.68/3.89  Clause #4 (by clausification #[3]): ∀ (a_1 : g → b) (a_2 : b → a),
% 3.68/3.89    Eq
% 3.68/3.89      (Not
% 3.68/3.89        (∀ (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89          And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (Xf1 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89              (∀ (Xx Xy : b), Eq (skS.0 1 a_1 a_2 (Xf2 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.89            ∀ (Xx Xy : g),
% 3.68/3.89              Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (Xf1 Xx Xy)))
% 3.68/3.89                (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy)))))
% 3.68/3.89      True
% 3.68/3.89  Clause #5 (by clausification #[4]): ∀ (a_1 : g → b) (a_2 : b → a),
% 3.68/3.89    Eq
% 3.68/3.89      (∀ (Xf1 : g → g → g) (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89        And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (Xf1 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89            (∀ (Xx Xy : b), Eq (skS.0 1 a_1 a_2 (Xf2 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.89          ∀ (Xx Xy : g),
% 3.68/3.89            Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (Xf1 Xx Xy)))
% 3.68/3.89              (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.68/3.89      False
% 3.68/3.89  Clause #6 (by clausification #[5]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g),
% 3.68/3.89    Eq
% 3.68/3.89      (Not
% 3.68/3.89        (∀ (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89          And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89              (∀ (Xx Xy : b), Eq (skS.0 1 a_1 a_2 (Xf2 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.89            ∀ (Xx Xy : g),
% 3.68/3.89              Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.89                (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy)))))
% 3.68/3.89      True
% 3.68/3.89  Clause #7 (by clausification #[6]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g),
% 3.68/3.89    Eq
% 3.68/3.89      (∀ (Xf2 : b → b → b) (Xf3 : a → a → a),
% 3.68/3.89        And (∀ (Xx Xy : g), Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (Xf2 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.89            (∀ (Xx Xy : b), Eq (skS.0 1 a_1 a_2 (Xf2 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.89          ∀ (Xx Xy : g),
% 3.68/3.89            Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.89              (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.68/3.89      False
% 3.68/3.89  Clause #8 (by clausification #[7]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b),
% 3.68/3.91    Eq
% 3.68/3.91      (Not
% 3.68/3.91        (∀ (Xf3 : a → a → a),
% 3.68/3.91          And
% 3.68/3.91              (∀ (Xx Xy : g),
% 3.68/3.91                Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.91              (∀ (Xx Xy : b),
% 3.68/3.91                Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.91            ∀ (Xx Xy : g),
% 3.68/3.91              Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.91                (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy)))))
% 3.68/3.91      True
% 3.68/3.91  Clause #9 (by clausification #[8]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b),
% 3.68/3.91    Eq
% 3.68/3.91      (∀ (Xf3 : a → a → a),
% 3.68/3.91        And
% 3.68/3.91            (∀ (Xx Xy : g),
% 3.68/3.91              Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.91            (∀ (Xx Xy : b),
% 3.68/3.91              Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy)) (Xf3 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.91          ∀ (Xx Xy : g),
% 3.68/3.91            Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.91              (Xf3 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.68/3.91      False
% 3.68/3.91  Clause #10 (by clausification #[9]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a),
% 3.68/3.91    Eq
% 3.68/3.91      (Not
% 3.68/3.91        (And
% 3.68/3.91            (∀ (Xx Xy : g),
% 3.68/3.91              Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.91            (∀ (Xx Xy : b),
% 3.68/3.91              Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy))
% 3.68/3.91                (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.91          ∀ (Xx Xy : g),
% 3.68/3.91            Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.91              (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy)))))
% 3.68/3.91      True
% 3.68/3.91  Clause #11 (by clausification #[10]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a),
% 3.68/3.91    Eq
% 3.68/3.91      (And
% 3.68/3.91          (∀ (Xx Xy : g),
% 3.68/3.91            Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.91          (∀ (Xx Xy : b),
% 3.68/3.91            Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy))
% 3.68/3.91              (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))) →
% 3.68/3.91        ∀ (Xx Xy : g),
% 3.68/3.91          Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.91            (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.68/3.91      False
% 3.68/3.91  Clause #12 (by clausification #[11]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a),
% 3.68/3.91    Eq
% 3.68/3.91      (And
% 3.68/3.91        (∀ (Xx Xy : g),
% 3.68/3.91          Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.68/3.91        (∀ (Xx Xy : b),
% 3.68/3.91          Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy))
% 3.68/3.91            (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy))))
% 3.68/3.91      True
% 3.68/3.91  Clause #13 (by clausification #[11]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a),
% 3.68/3.91    Eq
% 3.68/3.91      (∀ (Xx Xy : g),
% 3.68/3.91        Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)))
% 3.68/3.91          (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx)) (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.68/3.91      False
% 3.68/3.91  Clause #14 (by clausification #[12]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a),
% 3.68/3.91    Eq
% 3.68/3.91      (∀ (Xx Xy : b),
% 3.68/3.91        Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 Xx Xy))
% 3.68/3.91          (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 Xx) (skS.0 1 a_1 a_2 Xy)))
% 3.68/3.91      True
% 3.68/3.91  Clause #15 (by clausification #[12]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b),
% 3.68/3.91    Eq
% 3.68/3.91      (∀ (Xx Xy : g),
% 3.68/3.91        Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 Xx Xy)) (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 Xx) (skS.0 0 a_1 Xy)))
% 3.77/3.94      True
% 3.77/3.94  Clause #16 (by clausification #[14]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : b) (a_6 : a → a → a),
% 3.77/3.94    Eq
% 3.77/3.94      (∀ (Xy : b),
% 3.77/3.94        Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 a_5 Xy))
% 3.77/3.94          (skS.0 4 a_1 a_2 a_3 a_4 a_6 (skS.0 1 a_1 a_2 a_5) (skS.0 1 a_1 a_2 Xy)))
% 3.77/3.94      True
% 3.77/3.94  Clause #17 (by clausification #[16]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 a_6 : b) (a_7 : a → a → a),
% 3.77/3.94    Eq
% 3.77/3.94      (Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 a_5 a_6))
% 3.77/3.94        (skS.0 4 a_1 a_2 a_3 a_4 a_7 (skS.0 1 a_1 a_2 a_5) (skS.0 1 a_1 a_2 a_6)))
% 3.77/3.94      True
% 3.77/3.94  Clause #18 (by clausification #[17]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 a_6 : b) (a_7 : a → a → a),
% 3.77/3.94    Eq (skS.0 1 a_1 a_2 (skS.0 3 a_1 a_2 a_3 a_4 a_5 a_6))
% 3.77/3.94      (skS.0 4 a_1 a_2 a_3 a_4 a_7 (skS.0 1 a_1 a_2 a_5) (skS.0 1 a_1 a_2 a_6))
% 3.77/3.94  Clause #19 (by clausification #[15]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : g) (a_5 : b → b → b),
% 3.77/3.94    Eq
% 3.77/3.94      (∀ (Xy : g),
% 3.77/3.94        Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 a_4 Xy)) (skS.0 3 a_1 a_2 a_3 a_5 (skS.0 0 a_1 a_4) (skS.0 0 a_1 Xy)))
% 3.77/3.94      True
% 3.77/3.94  Clause #20 (by clausification #[19]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 a_5 : g) (a_6 : b → b → b),
% 3.77/3.94    Eq (Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 a_4 a_5)) (skS.0 3 a_1 a_2 a_3 a_6 (skS.0 0 a_1 a_4) (skS.0 0 a_1 a_5))) True
% 3.77/3.94  Clause #21 (by clausification #[20]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 a_5 : g) (a_6 : b → b → b),
% 3.77/3.94    Eq (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 a_4 a_5)) (skS.0 3 a_1 a_2 a_3 a_6 (skS.0 0 a_1 a_4) (skS.0 0 a_1 a_5))
% 3.77/3.94  Clause #22 (by clausification #[13]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 : g),
% 3.77/3.94    Eq
% 3.77/3.94      (Not
% 3.77/3.94        (∀ (Xy : g),
% 3.77/3.94          Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) Xy)))
% 3.77/3.94            (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6)))
% 3.77/3.94              (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy)))))
% 3.77/3.94      True
% 3.77/3.94  Clause #23 (by clausification #[22]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 : g),
% 3.77/3.94    Eq
% 3.77/3.94      (∀ (Xy : g),
% 3.77/3.94        Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) Xy)))
% 3.77/3.94          (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6)))
% 3.77/3.94            (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xy))))
% 3.77/3.94      False
% 3.77/3.94  Clause #24 (by clausification #[23]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 a_7 : g),
% 3.77/3.94    Eq
% 3.77/3.94      (Not
% 3.77/3.94        (Eq
% 3.77/3.94          (skS.0 1 a_1 a_2
% 3.77/3.94            (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94          (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6)))
% 3.77/3.94            (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))))
% 3.77/3.94      True
% 3.77/3.94  Clause #25 (by clausification #[24]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 a_7 : g),
% 3.77/3.94    Eq
% 3.77/3.94      (Eq
% 3.77/3.94        (skS.0 1 a_1 a_2
% 3.77/3.94          (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94        (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6)))
% 3.77/3.94          (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7)))))
% 3.77/3.94      False
% 3.77/3.94  Clause #26 (by clausification #[25]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 a_7 : g),
% 3.77/3.94    Ne
% 3.77/3.94      (skS.0 1 a_1 a_2
% 3.77/3.94        (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94      (skS.0 4 a_1 a_2 a_3 a_4 a_5 (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6)))
% 3.77/3.94        (skS.0 1 a_1 a_2 (skS.0 0 a_1 (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94  Clause #27 (by forward demodulation #[26, 18]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 a_7 : g),
% 3.77/3.94    Ne
% 3.77/3.94      (skS.0 1 a_1 a_2
% 3.77/3.94        (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94      (skS.0 1 a_1 a_2
% 3.77/3.94        (skS.0 3 a_1 a_2 a_3 a_4 (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6))
% 3.77/3.94          (skS.0 0 a_1 (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94  Clause #28 (by forward demodulation #[27, 21]): ∀ (a_1 : g → b) (a_2 : b → a) (a_3 : g → g → g) (a_4 : b → b → b) (a_5 : a → a → a) (a_6 a_7 : g),
% 3.77/3.94    Ne
% 3.77/3.94      (skS.0 1 a_1 a_2
% 3.77/3.94        (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94      (skS.0 1 a_1 a_2
% 3.77/3.94        (skS.0 0 a_1 (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_1 a_2 a_3 a_4 a_5 a_6 a_7))))
% 3.77/3.94  Clause #29 (by eliminate resolved literals #[28]): False
% 3.77/3.94  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------