%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRP185-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:20:24 AM UTC 2026
% Result : Unsatisfiable 88.49s 21.23s
% Output : Refutation 85.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 19
% Syntax : Number of formulae : 178 ( 107 unt; 0 typ; 0 def)
% Number of atoms : 277 ( 276 equ; 0 cnn)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 1536 ( 162 ~; 99 |; 0 &;1275 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 9 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 266 ( 0 ^; 266 !; 0 ?; 266 :)
% Comments :
%------------------------------------------------------------------------------
thf(greatest_lower_bound_decl,type,
greatest_lower_bound: $i > $i > $i ).
thf(least_upper_bound_decl,type,
least_upper_bound: $i > $i > $i ).
thf(multiply_decl,type,
multiply: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(identity_decl,type,
identity: $i ).
thf(inverse_decl,type,
inverse: $i > $i ).
thf(16,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(52,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiply ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( A @ multiply ) ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(12,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',glb_absorbtion) ).
thf(43,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(44,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(lifteq,[status(thm)],[43]) ).
thf(15,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_glb) ).
thf(49,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(50,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) )
= ( A @ ( B @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(1048,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( A
= ( C @ ( D @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[44,50]) ).
thf(1049,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[1048:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ least_upper_bound ) ))]]) ).
thf(1068,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= A ),
inference(simp,[status(thm)],[1049]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lub_absorbtion) ).
thf(41,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(42,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
inference(lifteq,[status(thm)],[41]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetry_of_lub) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ least_upper_bound ) )
= ( A @ ( B @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(311,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( A
= ( C @ ( D @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,28]) ).
thf(312,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[311:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ greatest_lower_bound ) ))]]) ).
thf(381,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= A ),
inference(simp,[status(thm)],[312]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_gld) ).
thf(35,plain,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(36,plain,
! [A: $i] :
( ( A @ ( A @ greatest_lower_bound ) )
= A ),
inference(lifteq,[status(thm)],[35]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
thf(31,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(32,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) )
= A ),
inference(lifteq,[status(thm)],[31]) ).
thf(1,negated_conjecture,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_p22b) ).
thf(20,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(21,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(polarity_switch,[status(thm)],[20]) ).
thf(22,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[21]) ).
thf(80,plain,
! [A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) ) )
| ( ( A @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,22]) ).
thf(84,plain,
! [A: $i] :
( ( A
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( A @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[80]) ).
thf(88,plain,
( ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[84]) ).
thf(181,plain,
! [A: $i] :
( ( ( A @ ( A @ greatest_lower_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( A
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[36,88]) ).
thf(186,plain,
( ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[181]) ).
thf(194,plain,
( ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[186]) ).
thf(264,plain,
( ( identity != identity )
| ( ( b @ ( a @ multiply ) )
!= b )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[194]) ).
thf(294,plain,
( ( ( b @ ( a @ multiply ) )
!= b )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[264]) ).
thf(1117,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( b @ ( a @ multiply ) )
!= b )
| ( A != identity ) ),
inference(paramod_ordered,[status(thm)],[381,294]) ).
thf(1126,plain,
! [A: $i] :
( ( identity != identity )
| ( ( A @ ( identity @ greatest_lower_bound ) )
!= a )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[1117]) ).
thf(1162,plain,
! [A: $i] :
( ( ( A @ ( identity @ greatest_lower_bound ) )
!= a )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[1126]) ).
thf(1601,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( A != a )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[1068,1162]) ).
thf(1641,plain,
! [B: $i,A: $i] :
( ( a != B )
| ( ( A @ ( a @ least_upper_bound ) )
!= identity )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[1601]) ).
thf(1664,plain,
! [A: $i] :
( ( ( A @ ( a @ least_upper_bound ) )
!= identity )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(simp,[status(thm)],[1641]) ).
thf(2,axiom,
! [A: $i] :
( ( A @ inverse @ inverse )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p22b_2) ).
thf(23,plain,
! [A: $i] :
( ( A @ inverse @ inverse )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(24,plain,
! [A: $i] :
( ( A @ inverse @ inverse )
= A ),
inference(lifteq,[status(thm)],[23]) ).
thf(7,axiom,
( ( identity @ inverse )
= identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p22b_1) ).
thf(33,plain,
( ( identity @ inverse )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(34,plain,
( ( identity @ inverse )
= identity ),
inference(lifteq,[status(thm)],[33]) ).
thf(59,plain,
! [A: $i] :
( ( ( A @ inverse @ inverse )
!= ( identity @ inverse ) )
| ( A = identity ) ),
inference(paramod_ordered,[status(thm)],[24,34]) ).
thf(65,plain,
! [A: $i] :
( ( ( A @ inverse )
!= identity )
| ( A = identity ) ),
inference(simp,[status(thm)],[59]) ).
thf(17,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monotony_lub1) ).
thf(53,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(10,axiom,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_lub) ).
thf(39,plain,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(14,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_lub) ).
thf(47,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) )
= ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(48,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ least_upper_bound ) )
= ( C @ ( B @ least_upper_bound ) @ ( A @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(3,axiom,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_inverse) ).
thf(25,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(26,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) )
= identity ),
inference(lifteq,[status(thm)],[25]) ).
thf(78,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) ) )
| ( ( identity @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,22]) ).
thf(82,plain,
! [A: $i] :
( ( A
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( A @ inverse )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( identity @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(86,plain,
( ( ( identity @ ( b @ least_upper_bound ) @ inverse )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( identity @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[82]) ).
thf(1618,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( C @ ( A @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[28,1068]) ).
thf(1619,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[1618:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(4169,plain,
( ( ( identity @ ( b @ least_upper_bound ) @ inverse )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= identity ) ),
inference(rewrite,[status(thm)],[86,1619]) ).
thf(1091,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( C @ ( A @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[50,381]) ).
thf(1092,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[1091:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1691,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( C @ ( D @ greatest_lower_bound ) ) )
| ( ( C @ ( A @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[50,1092]) ).
thf(1692,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ greatest_lower_bound ) @ least_upper_bound ) )
= B ),
inference(pattern_uni,[status(thm)],[1691:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(18,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monotony_glb1) ).
thf(55,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(56,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(5,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ multiply ) @ inverse )
= ( A @ inverse @ ( B @ inverse @ multiply ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p22b_3) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ multiply ) @ inverse )
= ( A @ inverse @ ( B @ inverse @ multiply ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(30,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ multiply ) @ inverse )
= ( A @ inverse @ ( B @ inverse @ multiply ) ) ),
inference(lifteq,[status(thm)],[29]) ).
thf(416,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( C @ ( B @ multiply ) ) )
| ( ( A @ inverse )
= ( B @ inverse @ ( C @ inverse @ multiply ) ) ) ),
inference(paramod_ordered,[status(thm)],[32,30]) ).
thf(417,plain,
! [A: $i] :
( ( identity @ inverse @ ( A @ inverse @ multiply ) )
= ( A @ inverse ) ),
inference(pattern_uni,[status(thm)],[416:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(603,plain,
! [A: $i] :
( ( identity @ ( A @ inverse @ multiply ) )
= ( A @ inverse ) ),
inference(rewrite,[status(thm)],[417,34]) ).
thf(616,plain,
! [B: $i,A: $i] :
( ( ( A @ inverse @ inverse )
!= ( B @ inverse ) )
| ( ( identity @ ( A @ multiply ) )
= ( B @ inverse ) ) ),
inference(paramod_ordered,[status(thm)],[24,603]) ).
thf(617,plain,
! [A: $i] :
( ( identity @ ( A @ multiply ) )
= ( A @ inverse @ inverse ) ),
inference(pattern_uni,[status(thm)],[616:[bind(A,$thf( C )),bind(B,$thf( C @ inverse ))]]) ).
thf(657,plain,
! [A: $i] :
( ( identity @ ( A @ multiply ) )
= ( A @ inverse @ inverse ) ),
inference(simp,[status(thm)],[617]) ).
thf(720,plain,
! [A: $i] :
( ( identity @ ( A @ multiply ) )
= A ),
inference(rewrite,[status(thm)],[657,24]) ).
thf(40,plain,
! [A: $i] :
( ( A @ ( A @ least_upper_bound ) )
= A ),
inference(lifteq,[status(thm)],[39]) ).
thf(700,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ greatest_lower_bound ) ) )
| ( A
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[44,22]) ).
thf(709,plain,
! [A: $i] :
( ( ( A @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) ) )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[700]) ).
thf(715,plain,
! [A: $i] :
( ( A @ ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) ) ),
inference(simp,[status(thm)],[709]) ).
thf(19,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monotony_lub2) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(58,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ least_upper_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[57]) ).
thf(3147,plain,
! [A: $i] :
( ( A @ ( identity @ least_upper_bound ) @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[715,48,58]) ).
thf(3175,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
!= ( C @ ( identity @ least_upper_bound ) ) )
| ( ( A @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[42,3147]) ).
thf(3176,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[3175:[bind(A,$thf( identity )),bind(B,$thf( E )),bind(C,$thf( E @ ( identity @ greatest_lower_bound ) ))]]) ).
thf(54,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ least_upper_bound ) @ ( A @ multiply ) )
= ( C @ ( A @ multiply ) @ ( B @ ( A @ multiply ) @ least_upper_bound ) ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(3570,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ multiply ) @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[3176,32,54]) ).
thf(3611,plain,
! [A: $i] :
( ( ( A @ ( A @ least_upper_bound ) )
!= ( identity @ ( a @ multiply ) @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) )
| ( ( identity @ ( b @ least_upper_bound ) @ ( A @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,3570]) ).
thf(3642,plain,
! [A: $i] :
( ( A
!= ( identity @ ( a @ multiply ) ) )
| ( A
!= ( b @ ( a @ multiply ) ) )
| ( ( identity @ ( b @ least_upper_bound ) )
!= identity )
| ( A
!= ( b @ ( a @ multiply ) ) ) ),
inference(simp,[status(thm)],[3611]) ).
thf(3761,plain,
( ( ( identity @ ( a @ multiply ) )
!= ( b @ ( a @ multiply ) ) )
| ( ( identity @ ( b @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[3642]) ).
thf(4822,plain,
( ( ( b @ ( a @ multiply ) )
!= a )
| ( ( identity @ ( b @ least_upper_bound ) )
!= identity ) ),
inference(rewrite,[status(thm)],[3761,720]) ).
thf(4837,plain,
! [A: $i] :
( ( ( A @ ( A @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( b @ ( a @ multiply ) )
!= a )
| ( A != identity ) ),
inference(paramod_ordered,[status(thm)],[40,4822]) ).
thf(4851,plain,
( ( identity != identity )
| ( identity != b )
| ( ( b @ ( a @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[4837]) ).
thf(4883,plain,
( ( identity != b )
| ( ( b @ ( a @ multiply ) )
!= a ) ),
inference(simp,[status(thm)],[4851]) ).
thf(5144,plain,
! [A: $i] :
( ( ( identity @ ( A @ multiply ) )
!= ( b @ ( a @ multiply ) ) )
| ( identity != b )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[720,4883]) ).
thf(5156,plain,
( ( identity != b )
| ( a != a )
| ( identity != b ) ),
inference(simp,[status(thm)],[5144]) ).
thf(5161,plain,
identity != b,
inference(simp,[status(thm)],[5156]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monotony_glb2) ).
thf(37,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(13,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_glb) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) )
= ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(46,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ greatest_lower_bound ) )
= ( C @ ( B @ greatest_lower_bound ) @ ( A @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(694,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) @ ( C @ greatest_lower_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[28,44]) ).
thf(695,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[694:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1333,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ least_upper_bound ) @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( A
= ( C @ ( D @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[695,50]) ).
thf(1334,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= B ),
inference(pattern_uni,[status(thm)],[1333:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ least_upper_bound ) ))]]) ).
thf(1377,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ least_upper_bound ) @ greatest_lower_bound ) )
= B ),
inference(simp,[status(thm)],[1334]) ).
thf(2057,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( D @ ( C @ least_upper_bound ) ) )
| ( ( D @ ( A @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[28,1377]) ).
thf(2058,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ least_upper_bound ) @ greatest_lower_bound ) )
= B ),
inference(pattern_uni,[status(thm)],[2057:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ( ( A @ inverse @ inverse )
!= ( B @ inverse ) )
| ( ( B @ ( A @ multiply ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[24,26]) ).
thf(72,plain,
! [A: $i] :
( ( A @ inverse @ ( A @ multiply ) )
= identity ),
inference(pattern_uni,[status(thm)],[71:[bind(A,$thf( C )),bind(B,$thf( C @ inverse ))]]) ).
thf(75,plain,
! [A: $i] :
( ( A @ inverse @ ( A @ multiply ) )
= identity ),
inference(simp,[status(thm)],[72]) ).
thf(408,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) @ inverse )
!= ( C @ inverse ) )
| ( ( A @ inverse @ ( B @ inverse @ multiply ) @ inverse )
= C ) ),
inference(paramod_ordered,[status(thm)],[30,24]) ).
thf(409,plain,
! [B: $i,A: $i] :
( ( A @ inverse @ ( B @ inverse @ multiply ) @ inverse )
= ( B @ ( A @ multiply ) ) ),
inference(pattern_uni,[status(thm)],[408:[bind(A,$thf( D )),bind(B,$thf( E )),bind(C,$thf( E @ ( D @ multiply ) ))]]) ).
thf(457,plain,
! [B: $i,A: $i] :
( ( A @ inverse @ ( B @ inverse @ multiply ) @ inverse )
= ( B @ ( A @ multiply ) ) ),
inference(simp,[status(thm)],[409]) ).
thf(4971,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( C @ ( B @ multiply ) ) )
| ( A
= ( B @ inverse @ ( C @ inverse @ multiply ) @ inverse ) ) ),
inference(paramod_ordered,[status(thm)],[32,457]) ).
thf(4972,plain,
! [A: $i] :
( ( identity @ inverse @ ( A @ inverse @ multiply ) @ inverse )
= A ),
inference(pattern_uni,[status(thm)],[4971:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(5170,plain,
! [A: $i] :
( ( identity @ ( A @ inverse @ multiply ) @ inverse )
= A ),
inference(rewrite,[status(thm)],[4972,34]) ).
thf(5210,plain,
! [B: $i,A: $i] :
( ( ( identity @ ( A @ inverse @ multiply ) @ inverse )
!= ( B @ inverse ) )
| ( ( A @ ( B @ multiply ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[5170,75]) ).
thf(5211,plain,
! [A: $i] :
( ( A @ ( identity @ ( A @ inverse @ multiply ) @ multiply ) )
= identity ),
inference(pattern_uni,[status(thm)],[5210:[bind(A,$thf( E )),bind(B,$thf( identity @ ( E @ inverse @ multiply ) ))]]) ).
thf(5264,plain,
! [A: $i] :
( ( A @ ( identity @ ( A @ inverse @ multiply ) @ multiply ) )
= identity ),
inference(simp,[status(thm)],[5211]) ).
thf(5419,plain,
! [A: $i] :
( ( A @ ( identity @ multiply ) @ ( A @ inverse @ multiply ) )
= identity ),
inference(rewrite,[status(thm)],[5264,52]) ).
thf(5492,plain,
! [B: $i,A: $i] :
( ( ( A @ inverse @ ( A @ multiply ) )
!= ( B @ ( identity @ multiply ) ) )
| ( ( identity @ ( B @ inverse @ multiply ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[75,5419]) ).
thf(5493,plain,
( ( identity @ ( identity @ inverse @ inverse @ multiply ) )
= identity ),
inference(pattern_uni,[status(thm)],[5492:[bind(A,$thf( identity )),bind(B,$thf( identity @ inverse ))]]) ).
thf(5783,plain,
( ( identity @ inverse @ inverse )
= identity ),
inference(rewrite,[status(thm)],[5493,720]) ).
thf(3622,plain,
! [A: $i] :
( ( ( identity @ ( A @ multiply ) )
!= ( identity @ ( a @ multiply ) ) )
| ( ( identity @ ( b @ least_upper_bound ) @ ( A @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[720,3570]) ).
thf(3623,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( a @ ( b @ ( a @ multiply ) @ least_upper_bound ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[3622:[bind(A,$thf( a ))]]) ).
thf(3841,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[3623,48]) ).
thf(3842,plain,
( ( ( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= identity )
| ( ( b @ ( a @ multiply ) )
!= ( b @ ( a @ multiply ) ) ) ),
inference(simp,[status(thm)],[3841]) ).
thf(3984,plain,
( ( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) )
!= identity ),
inference(simp,[status(thm)],[3842]) ).
thf(5470,plain,
! [A: $i] :
( ( ( identity @ inverse )
!= ( A @ inverse ) )
| ( ( A @ ( identity @ multiply ) @ ( identity @ multiply ) )
= identity ) ),
inference(paramod_ordered,[status(thm)],[34,5419]) ).
thf(5471,plain,
( ( identity @ ( identity @ multiply ) @ ( identity @ multiply ) )
= identity ),
inference(pattern_uni,[status(thm)],[5470:[bind(A,$thf( identity ))]]) ).
thf(5630,plain,
( ( identity @ ( identity @ multiply ) )
= identity ),
inference(rewrite,[status(thm)],[5471,32]) ).
thf(79,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( b @ ( a @ multiply ) ) )
| ( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,22]) ).
thf(83,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ inverse )
!= a )
| ( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(87,plain,
( ( ( b @ inverse )
!= a )
| ( ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( a @ least_upper_bound ) @ multiply ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(4344,plain,
( ( ( b @ inverse )
!= a )
| ( ( identity @ ( b @ least_upper_bound ) @ ( identity @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ ( a @ multiply ) @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(rewrite,[status(thm)],[87,40,58]) ).
thf(38,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ greatest_lower_bound ) @ multiply ) )
= ( C @ ( B @ multiply ) @ ( C @ ( A @ multiply ) @ greatest_lower_bound ) ) ),
inference(lifteq,[status(thm)],[37]) ).
thf(272,plain,
! [A: $i] :
( ( ( A @ ( identity @ multiply ) )
!= ( b @ ( a @ multiply ) ) )
| ( ( identity @ ( A @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(paramod_ordered,[status(thm)],[32,194]) ).
thf(281,plain,
! [A: $i] :
( ( A != b )
| ( identity != a )
| ( identity != identity )
| ( A != b )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[272]) ).
thf(300,plain,
( ( identity != a )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity ) ),
inference(simp,[status(thm)],[281]) ).
thf(386,plain,
! [A: $i] :
( ( ( A @ ( A @ least_upper_bound ) )
!= ( identity @ ( a @ least_upper_bound ) ) )
| ( identity != a )
| ( A != identity ) ),
inference(paramod_ordered,[status(thm)],[40,300]) ).
thf(390,plain,
( ( identity != identity )
| ( identity != a )
| ( identity != a ) ),
inference(simp,[status(thm)],[386]) ).
thf(393,plain,
identity != a,
inference(simp,[status(thm)],[390]) ).
thf(90,plain,
! [A: $i] :
( ( ( A @ ( A @ inverse @ multiply ) )
!= ( b @ ( a @ multiply ) ) )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[26,88]) ).
thf(92,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ inverse )
!= a )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[90]) ).
thf(94,plain,
( ( ( b @ inverse )
!= a )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ ( identity @ least_upper_bound ) @ greatest_lower_bound ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(4599,plain,
( ( ( b @ inverse )
!= a )
| ( ( identity @ ( a @ least_upper_bound ) )
!= identity )
| ( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( identity @ greatest_lower_bound ) ) ) ),
inference(rewrite,[status(thm)],[94,40]) ).
thf(744,plain,
! [C: $i,B: $i,A: $i] :
( ( ( identity @ ( A @ multiply ) )
!= ( C @ ( B @ multiply ) ) )
| ( ( A @ inverse )
= ( B @ inverse @ ( C @ inverse @ multiply ) ) ) ),
inference(paramod_ordered,[status(thm)],[720,30]) ).
thf(745,plain,
! [A: $i] :
( ( A @ inverse @ ( identity @ inverse @ multiply ) )
= ( A @ inverse ) ),
inference(pattern_uni,[status(thm)],[744:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( identity ))]]) ).
thf(826,plain,
! [A: $i] :
( ( A @ inverse @ ( identity @ multiply ) )
= ( A @ inverse ) ),
inference(rewrite,[status(thm)],[745,34]) ).
thf(1187,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( C @ ( identity @ greatest_lower_bound ) ) )
| ( ( B @ ( A @ greatest_lower_bound ) )
!= a )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[50,1162]) ).
thf(1188,plain,
! [A: $i] :
( ( ( identity @ ( A @ greatest_lower_bound ) )
!= a )
| ( ( b @ ( a @ multiply ) )
!= b ) ),
inference(pattern_uni,[status(thm)],[1187:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(1093,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( C @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[50,381]) ).
thf(1094,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ greatest_lower_bound ) @ least_upper_bound ) )
= B ),
inference(pattern_uni,[status(thm)],[1093:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3861,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ least_upper_bound ) )
!= ( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) )
| ( ( A @ ( B @ least_upper_bound ) )
!= ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,3841]) ).
thf(3862,plain,
( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( b @ ( a @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) @ least_upper_bound ) ) ),
inference(pattern_uni,[status(thm)],[3861:[bind(A,$thf( b @ ( a @ multiply ) )),bind(B,$thf( identity @ ( b @ least_upper_bound ) @ ( a @ least_upper_bound ) ))]]) ).
thf(4715,plain,
( ( identity @ ( b @ ( a @ multiply ) @ least_upper_bound ) )
!= ( b @ ( a @ multiply ) @ ( identity @ ( b @ least_upper_bound ) @ least_upper_bound ) @ ( a @ least_upper_bound ) ) ),
inference(rewrite,[status(thm)],[3862,48]) ).
thf(5040,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiply ) )
!= ( identity @ ( C @ multiply ) ) )
| ( ( A @ inverse @ ( B @ inverse @ multiply ) @ inverse )
= C ) ),
inference(paramod_ordered,[status(thm)],[457,720]) ).
thf(5041,plain,
! [A: $i] :
( ( A @ inverse @ ( identity @ inverse @ multiply ) @ inverse )
= A ),
inference(pattern_uni,[status(thm)],[5040:[bind(A,$thf( A )),bind(B,$thf( identity )),bind(C,$thf( A ))]]) ).
thf(5290,plain,
! [A: $i] :
( ( A @ inverse @ ( identity @ multiply ) @ inverse )
= A ),
inference(rewrite,[status(thm)],[5041,34]) ).
thf(1036,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ greatest_lower_bound ) )
!= ( D @ ( C @ greatest_lower_bound ) ) )
| ( ( A @ ( B @ greatest_lower_bound ) @ ( C @ least_upper_bound ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[50,42]) ).
thf(1037,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ greatest_lower_bound ) @ ( A @ least_upper_bound ) )
= A ),
inference(pattern_uni,[status(thm)],[1036:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(401,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ inverse @ ( B @ inverse @ multiply ) )
!= ( C @ inverse @ ( C @ multiply ) ) )
| ( ( B @ ( A @ multiply ) @ inverse )
= identity ) ),
inference(paramod_ordered,[status(thm)],[30,75]) ).
thf(402,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) @ inverse )
= identity ),
inference(pattern_uni,[status(thm)],[401:[bind(A,$thf( E @ inverse )),bind(B,$thf( E )),bind(C,$thf( E @ inverse ))]]) ).
thf(454,plain,
! [A: $i] :
( ( A @ ( A @ inverse @ multiply ) @ inverse )
= identity ),
inference(simp,[status(thm)],[402]) ).
thf(59217,plain,
$false,
inference(e,[status(thm)],[52,1664,65,53,39,1162,194,48,4169,88,1068,1692,56,5161,42,24,37,25,20,46,57,29,2058,1377,5783,3984,381,5630,4344,1619,33,28,38,393,457,41,5419,3841,5170,3147,45,4599,32,34,44,826,27,54,4822,49,1092,695,35,50,1188,31,1094,43,40,26,4715,55,23,75,58,36,30,51,294,5290,720,3570,47,1037,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP185-4 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.16/0.41 % Computer : n009.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Fri Sep 25 14:36:16 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.87/0.98 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.22/1.19 % [INFO] Parsing done (203ms).
% 1.41/1.20 % [INFO] Running in sequential loop mode.
% 2.06/1.60 % [INFO] eprover registered as external prover.
% 2.06/1.61 % [INFO] Scanning for conjecture ...
% 2.23/1.70 % [INFO] Found a conjecture (or negated_conjecture) and 18 axioms. Running axiom selection ...
% 2.23/1.76 % [INFO] Axiom selection finished. Selected 18 axioms (removed 0 axioms).
% 2.23/1.78 % [INFO] Problem is propositional (TPTP CNF).
% 2.23/1.79 % [INFO] Type checking passed.
% 2.23/1.79 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 88.49/21.22 % External prover 'e' found a proof!
% 88.49/21.22 % [INFO] Killing All external provers ...
% 88.49/21.22 % Time passed: 20680ms (effective reasoning time: 20014ms)
% 88.49/21.22 % Axioms used in derivation (18): monotony_lub1, idempotence_of_lub, monotony_glb1, left_inverse, symmetry_of_glb, monotony_glb2, glb_absorbtion, idempotence_of_gld, associativity_of_glb, p22b_3, p22b_2, symmetry_of_lub, p22b_1, associativity, monotony_lub2, left_identity, associativity_of_lub, lub_absorbtion
% 88.49/21.22 % No. of inferences in proof: 178
% 88.49/21.23 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 20680 ms resp. 20014 ms w/o parsing
% 85.24/21.31 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 85.24/21.31 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------