%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : REL012-2 : TPTP v9.3.1. Released v4.0.0.
% 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 : n003.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 08:23:54 AM UTC 2026
% Result : Unsatisfiable 96.68s 21.06s
% Output : Refutation 82.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 17
% Syntax : Number of formulae : 335 ( 172 unt; 0 typ; 0 def)
% Number of atoms : 589 ( 588 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 3579 ( 367 ~; 254 |; 0 &;2958 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 12 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 351 ( 0 ^; 351 !; 0 ?; 351 :)
% Comments :
%------------------------------------------------------------------------------
thf(join_decl,type,
join: $i > $i > $i ).
thf(composition_decl,type,
composition: $i > $i > $i ).
thf(complement_decl,type,
complement: $i > $i ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(converse_decl,type,
converse: $i > $i ).
thf(one_decl,type,
one: $i ).
thf(meet_decl,type,
meet: $i > $i > $i ).
thf(zero_decl,type,
zero: $i ).
thf(top_decl,type,
top: $i ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ join ) )
= ( A @ ( B @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
thf(33,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ join ) )
= ( A @ ( B @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(34,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ join ) )
= ( A @ ( B @ join ) ) ),
inference(lifteq,[status(thm)],[33]) ).
thf(14,axiom,
! [A: $i] :
( top
= ( A @ complement @ ( A @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
thf(45,plain,
! [A: $i] :
( top
= ( A @ complement @ ( A @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(46,plain,
! [A: $i] :
( ( A @ complement @ ( A @ join ) )
= top ),
inference(lifteq,[status(thm)],[45]) ).
thf(12,axiom,
! [A: $i] :
( zero
= ( A @ complement @ ( A @ meet ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
thf(41,plain,
! [A: $i] :
( zero
= ( A @ complement @ ( A @ meet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(42,plain,
! [A: $i] :
( ( A @ complement @ ( A @ meet ) )
= zero ),
inference(lifteq,[status(thm)],[41]) ).
thf(10,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ meet ) )
= ( B @ complement @ ( A @ complement @ join ) @ complement ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ meet ) )
= ( B @ complement @ ( A @ complement @ join ) @ complement ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ meet ) )
= ( B @ complement @ ( A @ complement @ join ) @ complement ) ),
inference(lifteq,[status(thm)],[37]) ).
thf(895,plain,
! [A: $i] :
( ( A @ complement @ complement @ ( A @ complement @ join ) @ complement )
= zero ),
inference(rewrite,[status(thm)],[42,38]) ).
thf(896,plain,
( ( top @ complement )
= zero ),
inference(rewrite,[status(thm)],[895,46]) ).
thf(912,plain,
! [A: $i] :
( ( ( top @ complement )
!= ( A @ complement ) )
| ( ( zero @ ( A @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[896,46]) ).
thf(913,plain,
( ( zero @ ( top @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[912:[bind(A,$thf( top ))]]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ join ) @ ( A @ join ) )
= ( C @ ( B @ ( A @ join ) @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ join ) @ ( A @ join ) )
= ( C @ ( B @ ( A @ join ) @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ join ) @ join ) )
= ( C @ ( B @ join ) @ ( A @ join ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(1041,plain,
! [C: $i,B: $i,A: $i] :
( ( ( zero @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( C @ ( top @ join ) )
= ( C @ ( B @ join ) @ ( A @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[913,28]) ).
thf(1042,plain,
! [A: $i] :
( ( A @ ( zero @ join ) @ ( top @ join ) )
= ( A @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[1041:[bind(A,$thf( top )),bind(B,$thf( zero ))]]) ).
thf(1084,plain,
! [A: $i] :
( ( A @ ( zero @ join ) @ ( top @ join ) )
= ( A @ ( top @ join ) ) ),
inference(simp,[status(thm)],[1042]) ).
thf(1309,plain,
! [B: $i,A: $i] :
( ( ( A @ complement @ ( A @ join ) )
!= ( B @ ( zero @ join ) ) )
| ( ( top @ ( top @ join ) )
= ( B @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,1084]) ).
thf(1310,plain,
( ( zero @ complement @ ( top @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[1309:[bind(A,$thf( zero )),bind(B,$thf( zero @ complement ))]]) ).
thf(1426,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( top @ ( top @ join ) )
= ( A @ ( B @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[1310,34]) ).
thf(1427,plain,
( ( top @ ( zero @ complement @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[1426:[bind(A,$thf( top )),bind(B,$thf( zero @ complement ))]]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( A
= ( B @ ( A @ complement @ join ) @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
thf(25,plain,
! [B: $i,A: $i] :
( A
= ( B @ ( A @ complement @ join ) @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ complement @ join ) @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ),
inference(lifteq,[status(thm)],[25]) ).
thf(1829,plain,
! [B: $i,A: $i] :
( ( ( top @ ( zero @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( top @ ( top @ join ) @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[1427,26]) ).
thf(1830,plain,
( ( top @ ( top @ join ) @ complement @ ( top @ complement @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[1829:[bind(A,$thf( zero )),bind(B,$thf( top ))]]) ).
thf(1890,plain,
( ( top @ ( top @ join ) @ complement @ ( zero @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[1830,896]) ).
thf(1943,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( zero @ ( zero @ complement @ join ) ) )
| ( ( top @ ( top @ join ) @ complement @ ( A @ ( B @ join ) @ complement @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[34,1890]) ).
thf(1944,plain,
( ( top @ ( top @ join ) @ complement @ ( zero @ complement @ ( zero @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[1943:[bind(A,$thf( zero @ complement )),bind(B,$thf( zero ))]]) ).
thf(4149,plain,
( ( top @ ( top @ join ) @ complement @ ( top @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[1944,46]) ).
thf(4260,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( top @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( zero @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[4149,26]) ).
thf(4261,plain,
( ( zero @ complement @ ( top @ ( top @ join ) @ complement @ complement @ ( top @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[4260:[bind(A,$thf( top )),bind(B,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(1939,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( zero @ ( zero @ complement @ join ) @ complement @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1890,34]) ).
thf(1940,plain,
( ( zero @ ( zero @ complement @ join ) @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[1939:[bind(A,$thf( zero @ ( zero @ complement @ join ) @ complement )),bind(B,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ complement @ ( A @ join ) )
!= ( C @ ( B @ join ) ) )
| ( ( B @ ( C @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[46,34]) ).
thf(85,plain,
! [A: $i] :
( ( A @ ( A @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ complement ))]]) ).
thf(88,plain,
! [A: $i] :
( ( A @ ( A @ complement @ join ) )
= top ),
inference(simp,[status(thm)],[85]) ).
thf(3538,plain,
( ( top @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[1940,88]) ).
thf(3643,plain,
! [B: $i,A: $i] :
( ( ( top @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
!= ( B @ complement @ ( A @ complement @ join ) ) )
| ( ( B @ ( A @ complement @ join ) @ complement @ ( zero @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[3538,26]) ).
thf(3644,plain,
( ( top @ ( top @ ( top @ join ) @ complement @ join ) @ complement @ ( zero @ complement @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[3643:[bind(A,$thf( top @ ( top @ join ) )),bind(B,$thf( top ))]]) ).
thf(1892,plain,
! [A: $i] :
( ( ( A @ ( A @ complement @ join ) )
!= ( zero @ ( zero @ complement @ join ) ) )
| ( ( top @ ( top @ join ) @ complement @ ( top @ complement @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[88,1890]) ).
thf(1893,plain,
( ( top @ ( top @ join ) @ complement @ ( top @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[1892:[bind(A,$thf( zero ))]]) ).
thf(2071,plain,
( ( top @ ( top @ join ) @ complement @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[1893,896]) ).
thf(2129,plain,
! [A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( zero @ join ) )
!= ( A @ ( zero @ join ) ) )
| ( ( zero @ ( top @ join ) )
= ( A @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[2071,1084]) ).
thf(2130,plain,
( ( top @ ( top @ join ) @ complement @ ( top @ join ) )
= ( zero @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[2129:[bind(A,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(2717,plain,
( ( top @ ( top @ join ) @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[2130,913]) ).
thf(2770,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[2717,34]) ).
thf(2771,plain,
( ( top @ ( top @ ( top @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[2770:[bind(A,$thf( top )),bind(B,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(7137,plain,
( ( top @ complement @ ( zero @ complement @ join ) )
= ( top @ ( top @ join ) ) ),
inference(rewrite,[status(thm)],[3644,2771]) ).
thf(7243,plain,
( ( ( top @ complement )
!= ( top @ complement ) )
| ( ( zero @ ( zero @ complement @ join ) )
= ( top @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[896,7137]) ).
thf(7244,plain,
( ( zero @ ( zero @ complement @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[7243:[]]) ).
thf(7545,plain,
( ( top @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[7244,88]) ).
thf(18183,plain,
( ( zero @ complement @ ( top @ complement @ complement @ ( zero @ join ) @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[4261,896,7545]) ).
thf(18285,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ ( top @ complement @ complement @ ( zero @ join ) @ complement @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[18183,34]) ).
thf(18286,plain,
( ( top @ complement @ complement @ ( zero @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[18285:[bind(A,$thf( top @ complement @ complement @ ( zero @ join ) @ complement )),bind(B,$thf( zero @ complement ))]]) ).
thf(18636,plain,
( ( zero @ complement @ ( zero @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[18286,896]) ).
thf(3,axiom,
! [A: $i] :
( ( one @ ( A @ composition ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
thf(23,plain,
! [A: $i] :
( ( one @ ( A @ composition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(24,plain,
! [A: $i] :
( ( one @ ( A @ composition ) )
= A ),
inference(lifteq,[status(thm)],[23]) ).
thf(1,negated_conjecture,
( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_17) ).
thf(18,plain,
( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(19,plain,
( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ),
inference(polarity_switch,[status(thm)],[18]) ).
thf(20,plain,
( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ),
inference(lifteq,[status(thm)],[19]) ).
thf(57,plain,
! [A: $i] :
( ( ( one @ ( A @ composition ) )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( sk1 @ complement @ ( A @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[24,20]) ).
thf(61,plain,
! [A: $i] :
( ( ( sk2 @ converse )
!= one )
| ( A
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk1 @ complement @ ( A @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(64,plain,
( ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[61]) ).
thf(157,plain,
! [A: $i] :
( ( ( A @ ( A @ complement @ join ) )
!= ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[88,64]) ).
thf(159,plain,
! [A: $i] :
( ( A
!= ( sk1 @ complement ) )
| ( ( A @ complement )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[157]) ).
thf(169,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= ( sk1 @ complement @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[159]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ join ) @ converse )
= ( B @ converse @ ( A @ converse @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
thf(39,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ join ) @ converse )
= ( B @ converse @ ( A @ converse @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(144,plain,
! [A: $i] :
( ( ( A @ ( A @ complement @ join ) )
!= ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[88,20]) ).
thf(160,plain,
! [A: $i] :
( ( A
!= ( sk1 @ complement ) )
| ( ( A @ complement )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[144]) ).
thf(162,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= ( sk1 @ complement @ complement ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[160]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ converse @ converse )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
thf(29,plain,
! [A: $i] :
( ( A @ converse @ converse )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(30,plain,
! [A: $i] :
( ( A @ converse @ converse )
= A ),
inference(lifteq,[status(thm)],[29]) ).
thf(56,plain,
! [A: $i] :
( ( ( one @ ( A @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( A @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[24,20]) ).
thf(60,plain,
! [A: $i] :
( ( one != sk2 )
| ( A != sk1 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( A @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(63,plain,
( ( one != sk2 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( sk1 @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(66,plain,
! [A: $i] :
( ( ( A @ converse @ converse )
!= ( sk2 @ converse ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ ( sk1 @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[30,63]) ).
thf(69,plain,
! [A: $i] :
( ( ( A @ converse )
!= sk2 )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ ( sk1 @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(92,plain,
! [A: $i] :
( ( ( A @ complement @ ( A @ join ) )
!= ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[46,64]) ).
thf(97,plain,
! [A: $i] :
( ( ( A @ complement )
!= ( sk1 @ complement ) )
| ( A
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[92]) ).
thf(101,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement @ complement )
!= ( sk1 @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[97]) ).
thf(897,plain,
! [A: $i] :
( ( ( top @ complement )
!= ( A @ complement ) )
| ( ( A @ ( zero @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[896,88]) ).
thf(898,plain,
( ( top @ ( zero @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[897:[bind(A,$thf( top ))]]) ).
thf(979,plain,
! [C: $i,B: $i,A: $i] :
( ( ( top @ ( zero @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( C @ ( top @ join ) )
= ( C @ ( B @ join ) @ ( A @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[898,28]) ).
thf(980,plain,
! [A: $i] :
( ( A @ ( top @ join ) @ ( zero @ join ) )
= ( A @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[979:[bind(A,$thf( zero )),bind(B,$thf( top ))]]) ).
thf(1021,plain,
! [A: $i] :
( ( A @ ( top @ join ) @ ( zero @ join ) )
= ( A @ ( top @ join ) ) ),
inference(simp,[status(thm)],[980]) ).
thf(1221,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ join ) )
!= ( C @ ( top @ join ) ) )
| ( ( B @ ( A @ join ) @ ( zero @ join ) )
= ( C @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,1021]) ).
thf(1222,plain,
! [A: $i] :
( ( top @ ( A @ join ) @ ( zero @ join ) )
= ( A @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[1221:[bind(A,$thf( A )),bind(B,$thf( top )),bind(C,$thf( A ))]]) ).
thf(1215,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( top @ join ) @ ( zero @ join ) )
!= ( B @ ( C @ join ) ) )
| ( ( A @ ( top @ join ) )
= ( C @ ( B @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[1021,34]) ).
thf(1216,plain,
! [A: $i] :
( ( zero @ ( A @ ( top @ join ) @ join ) )
= ( A @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[1215:[bind(A,$thf( E )),bind(B,$thf( E @ ( top @ join ) )),bind(C,$thf( zero ))]]) ).
thf(1264,plain,
! [A: $i] :
( ( zero @ ( A @ ( top @ join ) @ join ) )
= ( A @ ( top @ join ) ) ),
inference(simp,[status(thm)],[1216]) ).
thf(19580,plain,
! [A: $i] :
( ( zero @ ( A @ join ) @ ( top @ join ) )
= ( A @ ( top @ join ) ) ),
inference(rewrite,[status(thm)],[1264,28]) ).
thf(19602,plain,
! [B: $i,A: $i] :
( ( ( A @ ( top @ join ) )
!= ( zero @ ( B @ join ) ) )
| ( ( top @ ( A @ join ) @ ( zero @ join ) @ ( top @ join ) )
= ( B @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[1222,19580]) ).
thf(19603,plain,
( ( top @ ( zero @ join ) @ ( zero @ join ) @ ( top @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[19602:[bind(A,$thf( zero )),bind(B,$thf( top ))]]) ).
thf(20557,plain,
( ( top @ ( zero @ join ) @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[19603,7545,1084]) ).
thf(20683,plain,
! [B: $i,A: $i] :
( ( ( top @ ( zero @ join ) @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[20557,34]) ).
thf(20684,plain,
( ( top @ ( top @ ( zero @ join ) @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[20683:[bind(A,$thf( top )),bind(B,$thf( top @ ( zero @ join ) ))]]) ).
thf(21012,plain,
( ( top @ ( top @ join ) @ ( zero @ join ) )
= top ),
inference(rewrite,[status(thm)],[20684,28]) ).
thf(21145,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ ( zero @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[21012,34]) ).
thf(21146,plain,
( ( zero @ ( top @ ( top @ join ) @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[21145:[bind(A,$thf( zero )),bind(B,$thf( top @ ( top @ join ) ))]]) ).
thf(21486,plain,
( ( zero @ ( top @ join ) @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[21146,28]) ).
thf(93,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( A @ ( B @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[34,64]) ).
thf(94,plain,
( ( ( sk2 @ converse )
!= one )
| ( ( sk2 @ ( sk1 @ composition ) @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(pattern_uni,[status(thm)],[93:[bind(A,$thf( sk2 @ ( sk1 @ composition ) @ complement )),bind(B,$thf( sk1 @ complement ))]]) ).
thf(7639,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement @ ( sk1 @ complement @ join ) )
!= ( top @ ( top @ join ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[7545,94]) ).
thf(7663,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= top )
| ( ( sk1 @ complement )
!= top )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7639]) ).
thf(7697,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= top )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7663]) ).
thf(7,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ composition ) @ converse )
= ( A @ converse @ ( B @ converse @ composition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ composition ) @ converse )
= ( A @ converse @ ( B @ converse @ composition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ composition ) @ converse )
= ( A @ converse @ ( B @ converse @ composition ) ) ),
inference(lifteq,[status(thm)],[31]) ).
thf(229,plain,
! [C: $i,B: $i,A: $i] :
( ( ( one @ ( A @ composition ) )
!= ( C @ ( B @ composition ) ) )
| ( ( A @ converse )
= ( B @ converse @ ( C @ converse @ composition ) ) ) ),
inference(paramod_ordered,[status(thm)],[24,32]) ).
thf(230,plain,
! [A: $i] :
( ( A @ converse @ ( one @ converse @ composition ) )
= ( A @ converse ) ),
inference(pattern_uni,[status(thm)],[229:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( one ))]]) ).
thf(390,plain,
! [B: $i,A: $i] :
( ( ( A @ converse @ converse )
!= ( B @ converse ) )
| ( ( A @ ( one @ converse @ composition ) )
= ( B @ converse ) ) ),
inference(paramod_ordered,[status(thm)],[30,230]) ).
thf(391,plain,
! [A: $i] :
( ( A @ ( one @ converse @ composition ) )
= ( A @ converse @ converse ) ),
inference(pattern_uni,[status(thm)],[390:[bind(A,$thf( C )),bind(B,$thf( C @ converse ))]]) ).
thf(425,plain,
! [A: $i] :
( ( A @ ( one @ converse @ composition ) )
= ( A @ converse @ converse ) ),
inference(simp,[status(thm)],[391]) ).
thf(434,plain,
! [A: $i] :
( ( A @ ( one @ converse @ composition ) )
= A ),
inference(rewrite,[status(thm)],[425,30]) ).
thf(442,plain,
! [B: $i,A: $i] :
( ( ( A @ ( one @ converse @ composition ) )
!= ( one @ ( B @ composition ) ) )
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[434,24]) ).
thf(443,plain,
( ( one @ converse )
= one ),
inference(pattern_uni,[status(thm)],[442:[bind(A,$thf( one )),bind(B,$thf( one @ converse ))]]) ).
thf(514,plain,
! [A: $i] :
( ( A @ ( one @ composition ) )
= A ),
inference(rewrite,[status(thm)],[434,443]) ).
thf(534,plain,
( ( ( one @ converse )
!= ( sk2 @ converse ) )
| ( one != one )
| ( ( sk2 @ ( sk1 @ composition ) @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[443,94]) ).
thf(535,plain,
( ( ( one @ converse )
!= ( sk2 @ converse ) )
| ( ( sk2 @ ( sk1 @ composition ) @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[534]) ).
thf(544,plain,
( ( one != sk2 )
| ( ( sk2 @ ( sk1 @ composition ) @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[535]) ).
thf(863,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( one != sk2 )
| ( ( A @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[514,544]) ).
thf(874,plain,
! [A: $i] :
( ( A != sk2 )
| ( one != sk1 )
| ( one != sk2 )
| ( ( A @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[863]) ).
thf(885,plain,
( ( one != sk1 )
| ( one != sk2 )
| ( ( sk2 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[874]) ).
thf(4263,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( top @ complement @ join ) )
!= ( B @ complement @ ( A @ complement @ join ) ) )
| ( ( B @ ( A @ complement @ join ) @ complement @ ( zero @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[4149,26]) ).
thf(4264,plain,
( ( top @ ( top @ join ) @ ( top @ complement @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[4263:[bind(A,$thf( top )),bind(B,$thf( top @ ( top @ join ) ))]]) ).
thf(4577,plain,
( ( top @ ( top @ join ) @ ( zero @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[4264,896]) ).
thf(4643,plain,
! [A: $i] :
( ( ( A @ ( top @ join ) @ ( zero @ join ) )
!= ( top @ ( top @ join ) @ ( zero @ join ) ) )
| ( ( A @ ( top @ join ) @ complement @ ( zero @ complement @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[1021,4577]) ).
thf(4644,plain,
( ( top @ ( top @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[4643:[bind(A,$thf( top ))]]) ).
thf(4998,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( zero @ complement @ join ) )
!= ( B @ complement @ ( A @ complement @ join ) ) )
| ( ( B @ ( A @ complement @ join ) @ complement @ ( top @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[4644,26]) ).
thf(4999,plain,
( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( top @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[4998:[bind(A,$thf( zero )),bind(B,$thf( top @ ( top @ join ) ))]]) ).
thf(5552,plain,
( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[4999,896]) ).
thf(5693,plain,
! [A: $i] :
( ( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
!= ( A @ ( zero @ join ) ) )
| ( ( zero @ ( top @ join ) )
= ( A @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[5552,1084]) ).
thf(5694,plain,
( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
= ( zero @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[5693:[bind(A,$thf( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement ))]]) ).
thf(6366,plain,
( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[5694,913]) ).
thf(6492,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[6366,34]) ).
thf(6493,plain,
( ( top @ ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[6492:[bind(A,$thf( top )),bind(B,$thf( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement ))]]) ).
thf(7558,plain,
( ( top @ ( top @ ( zero @ complement @ join ) @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[6493,7545]) ).
thf(7547,plain,
( ( top @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[1427,7545]) ).
thf(9056,plain,
( ( top @ ( top @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[7558,7547]) ).
thf(982,plain,
( ( ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) )
!= ( top @ ( zero @ join ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[898,64]) ).
thf(1011,plain,
( ( ( sk1 @ complement )
!= top )
| ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= zero )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[982]) ).
thf(1020,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= zero )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[1011]) ).
thf(13475,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= ( top @ complement ) )
| ( zero != zero )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[896,1020]) ).
thf(13476,plain,
( ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= ( top @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[13475]) ).
thf(13483,plain,
( ( ( sk2 @ ( sk1 @ composition ) )
!= top )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[13476]) ).
thf(13501,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( A != top )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[514,13483]) ).
thf(13511,plain,
( ( top != sk2 )
| ( one != sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[13501]) ).
thf(17,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modular_law_2_16) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(52,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ meet ) ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(3776,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ complement @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ complement @ join ) @ complement @ ( C @ complement @ ( B @ ( A @ composition ) @ complement @ join ) @ complement @ join ) )
= ( C @ complement @ ( B @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ complement @ join ) @ complement ) ),
inference(rewrite,[status(thm)],[52,38]) ).
thf(20577,plain,
! [A: $i] :
( ( ( top @ ( zero @ join ) @ ( top @ join ) )
!= ( A @ ( top @ join ) ) )
| ( ( top @ ( A @ join ) @ ( zero @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[20557,1222]) ).
thf(20578,plain,
( ( top @ ( top @ ( zero @ join ) @ join ) @ ( zero @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[20577:[bind(A,$thf( top @ ( zero @ join ) ))]]) ).
thf(22004,plain,
( ( top @ ( top @ join ) @ ( zero @ join ) @ ( zero @ join ) )
= top ),
inference(rewrite,[status(thm)],[20578,28]) ).
thf(18846,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ ( zero @ join ) @ complement @ ( zero @ complement @ join ) )
!= ( B @ complement @ ( A @ complement @ join ) ) )
| ( ( B @ ( A @ complement @ join ) @ complement @ ( top @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[18636,26]) ).
thf(18847,plain,
( ( zero @ complement @ ( zero @ join ) @ ( zero @ complement @ join ) @ complement @ ( top @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[18846:[bind(A,$thf( zero )),bind(B,$thf( zero @ complement @ ( zero @ join ) ))]]) ).
thf(4950,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( zero @ complement @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[4644,34]) ).
thf(4951,plain,
( ( zero @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[4950:[bind(A,$thf( zero @ complement )),bind(B,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(7546,plain,
( ( zero @ complement @ ( top @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[4951,7545]) ).
thf(8221,plain,
( ( zero @ complement @ ( zero @ join ) )
= top ),
inference(rewrite,[status(thm)],[7546,896]) ).
thf(19063,plain,
( ( top @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[18847,896,8221]) ).
thf(58,plain,
! [A: $i] :
( ( ( A @ complement @ ( A @ join ) )
!= ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[46,20]) ).
thf(62,plain,
! [A: $i] :
( ( ( A @ complement )
!= ( sk1 @ complement ) )
| ( A
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[58]) ).
thf(65,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ complement )
!= ( sk1 @ complement ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[62]) ).
thf(5461,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[65]) ).
thf(973,plain,
( ( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( top @ ( zero @ join ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[898,20]) ).
thf(998,plain,
( ( ( sk1 @ complement )
!= top )
| ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= zero )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[973]) ).
thf(1013,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= zero )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[998]) ).
thf(7560,plain,
( ( top @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[5552,7545]) ).
thf(9480,plain,
( ( top @ complement @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[7560,7547]) ).
thf(2,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ join ) @ composition ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
thf(21,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ join ) @ composition ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(22,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ join ) @ composition ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
inference(lifteq,[status(thm)],[21]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) ) )
| ( ( A @ ( B @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[34,20]) ).
thf(79,plain,
( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ),
inference(pattern_uni,[status(thm)],[78:[bind(A,$thf( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )),bind(B,$thf( sk1 @ complement ))]]) ).
thf(172,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,79]) ).
thf(183,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( sk2 @ converse ) )
| ( ( B @ ( A @ join ) )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(189,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk2 @ converse @ ( B @ composition ) @ ( sk2 @ converse @ ( A @ composition ) @ join ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[183]) ).
thf(7251,plain,
! [B: $i,A: $i] :
( ( ( top @ complement @ ( zero @ complement @ join ) )
!= ( B @ complement @ ( A @ complement @ join ) ) )
| ( ( B @ ( A @ complement @ join ) @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[7137,26]) ).
thf(7252,plain,
( ( top @ ( zero @ complement @ join ) @ complement @ ( top @ ( top @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[7251:[bind(A,$thf( zero )),bind(B,$thf( top ))]]) ).
thf(12281,plain,
( ( top @ complement @ ( top @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[7252,7545,7547]) ).
thf(90,plain,
! [A: $i] :
( ( ( A @ converse @ converse )
!= ( sk2 @ converse ) )
| ( A != one )
| ( ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[30,64]) ).
thf(100,plain,
( ( ( one @ converse )
!= sk2 )
| ( ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[90]) ).
thf(515,plain,
( ( one != sk2 )
| ( ( sk1 @ complement @ ( sk2 @ ( sk1 @ composition ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(rewrite,[status(thm)],[100,443]) ).
thf(746,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[514,515]) ).
thf(756,plain,
! [A: $i] :
( ( A != sk2 )
| ( one != sk1 )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[746]) ).
thf(766,plain,
( ( one != sk1 )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk2 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[756]) ).
thf(126,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,64]) ).
thf(130,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk2 )
| ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[126]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement @ ( sk2 @ ( B @ composition ) @ ( sk2 @ ( A @ composition ) @ join ) @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(12387,plain,
! [B: $i,A: $i] :
( ( ( top @ complement @ ( top @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( zero @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[12281,26]) ).
thf(12388,plain,
( ( zero @ complement @ ( top @ complement @ complement @ ( top @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[12387:[bind(A,$thf( top )),bind(B,$thf( top @ complement ))]]) ).
thf(13217,plain,
( ( zero @ complement @ ( top @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[12388,46]) ).
thf(13338,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ ( top @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( top @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[13217,26]) ).
thf(13339,plain,
( ( top @ complement @ ( zero @ complement @ complement @ ( top @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[13338:[bind(A,$thf( top )),bind(B,$thf( zero @ complement ))]]) ).
thf(13527,plain,
( ( zero @ ( zero @ complement @ complement @ ( zero @ join ) @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[13339,896]) ).
thf(13605,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( zero @ complement @ complement @ ( zero @ join ) @ complement @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[13527,34]) ).
thf(13606,plain,
( ( zero @ complement @ complement @ ( zero @ join ) @ complement @ ( zero @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[13605:[bind(A,$thf( zero @ complement @ complement @ ( zero @ join ) @ complement )),bind(B,$thf( zero ))]]) ).
thf(14348,plain,
! [A: $i] :
( ( ( zero @ complement @ complement @ ( zero @ join ) @ complement @ ( zero @ join ) )
!= ( A @ ( zero @ join ) ) )
| ( ( top @ ( top @ join ) )
= ( A @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[13606,1084]) ).
thf(14349,plain,
( ( zero @ complement @ complement @ ( zero @ join ) @ complement @ ( top @ join ) )
= ( top @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[14348:[bind(A,$thf( zero @ complement @ complement @ ( zero @ join ) @ complement ))]]) ).
thf(14573,plain,
( ( zero @ complement @ complement @ ( zero @ join ) @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[14349,7545]) ).
thf(14653,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ complement @ ( zero @ join ) @ complement @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[14573,34]) ).
thf(14654,plain,
( ( top @ ( zero @ complement @ complement @ ( zero @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[14653:[bind(A,$thf( top )),bind(B,$thf( zero @ complement @ complement @ ( zero @ join ) @ complement ))]]) ).
thf(657,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( C @ ( B @ composition ) ) )
| ( ( A @ converse )
= ( B @ converse @ ( C @ converse @ composition ) ) ) ),
inference(paramod_ordered,[status(thm)],[514,32]) ).
thf(658,plain,
! [A: $i] :
( ( one @ converse @ ( A @ converse @ composition ) )
= ( A @ converse ) ),
inference(pattern_uni,[status(thm)],[657:[bind(A,$thf( A )),bind(B,$thf( one )),bind(C,$thf( A ))]]) ).
thf(693,plain,
! [A: $i] :
( ( one @ ( A @ converse @ composition ) )
= ( A @ converse ) ),
inference(rewrite,[status(thm)],[658,443]) ).
thf(40,plain,
! [B: $i,A: $i] :
( ( B @ converse @ ( A @ converse @ join ) )
= ( B @ ( A @ join ) @ converse ) ),
inference(lifteq,[status(thm)],[39]) ).
thf(1114,plain,
! [B: $i,A: $i] :
( ( ( one @ converse )
!= ( A @ converse ) )
| ( ( B @ converse @ ( one @ join ) )
= ( B @ ( A @ join ) @ converse ) ) ),
inference(paramod_ordered,[status(thm)],[443,40]) ).
thf(1115,plain,
! [A: $i] :
( ( A @ converse @ ( one @ join ) )
= ( A @ ( one @ join ) @ converse ) ),
inference(pattern_uni,[status(thm)],[1114:[bind(A,$thf( one ))]]) ).
thf(1174,plain,
! [A: $i] :
( ( A @ converse @ ( one @ join ) )
= ( A @ ( one @ join ) @ converse ) ),
inference(simp,[status(thm)],[1115]) ).
thf(5466,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( A @ complement )
!= ( sk1 @ complement ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[514,65]) ).
thf(5507,plain,
! [A: $i] :
( ( A
!= ( sk2 @ converse ) )
| ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= one )
| ( A != sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5466]) ).
thf(5534,plain,
( ( ( sk2 @ converse )
!= sk1 )
| ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5507]) ).
thf(7563,plain,
( ( top @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[6366,7545]) ).
thf(9662,plain,
( ( top @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[7563,7547]) ).
thf(1112,plain,
! [B: $i,A: $i] :
( ( ( one @ converse )
!= ( B @ converse ) )
| ( ( one @ ( A @ converse @ join ) )
= ( B @ ( A @ join ) @ converse ) ) ),
inference(paramod_ordered,[status(thm)],[443,40]) ).
thf(1113,plain,
! [A: $i] :
( ( one @ ( A @ converse @ join ) )
= ( one @ ( A @ join ) @ converse ) ),
inference(pattern_uni,[status(thm)],[1112:[bind(A,$thf( A )),bind(B,$thf( one ))]]) ).
thf(15368,plain,
! [A: $i] :
( ( ( one @ converse )
!= ( A @ converse ) )
| ( ( one @ ( one @ join ) )
= ( one @ ( A @ join ) @ converse ) ) ),
inference(paramod_ordered,[status(thm)],[443,1113]) ).
thf(15369,plain,
( ( one @ ( one @ join ) @ converse )
= ( one @ ( one @ join ) ) ),
inference(pattern_uni,[status(thm)],[15368:[bind(A,$thf( one ))]]) ).
thf(20082,plain,
( ( top != top )
| ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= ( sk1 @ complement ) )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(eqfactor_ordered,[status(thm)],[7697]) ).
thf(20097,plain,
( ( ( sk2 @ ( sk1 @ composition ) )
!= sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[20082]) ).
thf(5653,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[5552,34]) ).
thf(5654,plain,
( ( zero @ ( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[5653:[bind(A,$thf( zero )),bind(B,$thf( top @ ( top @ join ) @ ( zero @ complement @ join ) @ complement ))]]) ).
thf(7550,plain,
( ( zero @ ( top @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[5654,7545]) ).
thf(8517,plain,
( ( zero @ ( top @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[7550,7547]) ).
thf(8586,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( top @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( zero @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[8517,26]) ).
thf(8587,plain,
( ( zero @ complement @ ( zero @ complement @ ( top @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[8586:[bind(A,$thf( top )),bind(B,$thf( zero ))]]) ).
thf(10635,plain,
( ( zero @ complement @ ( zero @ complement @ ( zero @ join ) @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[8587,896]) ).
thf(16,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',modular_law_1_15) ).
thf(49,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ meet ) ) ),
inference(lifteq,[status(thm)],[49]) ).
thf(3187,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ complement @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ complement @ join ) @ complement @ ( C @ complement @ ( B @ ( A @ composition ) @ complement @ join ) @ complement @ join ) )
= ( C @ complement @ ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( A @ composition ) @ complement @ join ) @ complement ) ),
inference(rewrite,[status(thm)],[50,38]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( ( sk2 @ converse @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,79]) ).
thf(185,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk2 )
| ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk2 @ converse @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk2 @ converse @ ( sk2 @ ( B @ composition ) @ ( sk2 @ ( A @ composition ) @ join ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(55,plain,
! [A: $i] :
( ( ( A @ converse @ converse )
!= ( sk2 @ converse ) )
| ( ( sk1 @ complement @ ( A @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[30,20]) ).
thf(59,plain,
! [A: $i] :
( ( ( A @ converse )
!= sk2 )
| ( ( sk1 @ complement @ ( A @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(13,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dedekind_law_14) ).
thf(43,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(44,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) @ ( C @ ( B @ ( A @ composition ) @ meet ) @ join ) )
= ( C @ ( A @ converse @ composition ) @ ( B @ meet ) @ ( B @ converse @ ( C @ composition ) @ ( A @ meet ) @ composition ) ) ),
inference(lifteq,[status(thm)],[43]) ).
thf(1488,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ converse @ composition ) @ complement @ ( B @ complement @ join ) @ complement @ ( B @ converse @ ( C @ composition ) @ complement @ ( A @ complement @ join ) @ complement @ composition ) @ ( C @ complement @ ( B @ ( A @ composition ) @ complement @ join ) @ complement @ join ) )
= ( C @ ( A @ converse @ composition ) @ complement @ ( B @ complement @ join ) @ complement @ ( B @ converse @ ( C @ composition ) @ complement @ ( A @ complement @ join ) @ complement @ composition ) ) ),
inference(rewrite,[status(thm)],[44,38]) ).
thf(173,plain,
! [A: $i] :
( ( ( A @ converse @ converse )
!= ( sk2 @ converse ) )
| ( ( A @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[30,79]) ).
thf(181,plain,
! [A: $i] :
( ( ( A @ converse )
!= sk2 )
| ( ( A @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[173]) ).
thf(7638,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( top @ ( top @ join ) ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[7545,79]) ).
thf(7641,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= top )
| ( ( sk1 @ complement )
!= top )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7638]) ).
thf(7685,plain,
( ( ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) )
!= top )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7641]) ).
thf(7551,plain,
( ( zero @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[1310,7545]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ composition ) @ ( A @ composition ) )
= ( C @ ( B @ ( A @ composition ) @ composition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
thf(35,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ composition ) @ ( A @ composition ) )
= ( C @ ( B @ ( A @ composition ) @ composition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(140,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ complement @ join ) )
!= ( C @ ( B @ join ) ) )
| ( ( D @ ( top @ composition ) )
= ( D @ ( C @ composition ) @ ( D @ ( B @ composition ) @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[88,22]) ).
thf(141,plain,
! [B: $i,A: $i] :
( ( A @ ( top @ composition ) )
= ( A @ ( B @ composition ) @ ( A @ ( B @ complement @ composition ) @ join ) ) ),
inference(pattern_uni,[status(thm)],[140:[bind(A,$thf( E )),bind(B,$thf( E @ complement )),bind(C,$thf( E ))]]) ).
thf(167,plain,
! [B: $i,A: $i] :
( ( A @ ( top @ composition ) )
= ( A @ ( B @ composition ) @ ( A @ ( B @ complement @ composition ) @ join ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(15636,plain,
! [A: $i] :
( ( ( one @ ( one @ join ) @ converse )
!= ( A @ converse ) )
| ( ( one @ ( one @ ( one @ join ) @ join ) )
= ( one @ ( A @ join ) @ converse ) ) ),
inference(paramod_ordered,[status(thm)],[15369,1113]) ).
thf(15637,plain,
( ( one @ ( one @ ( one @ join ) @ join ) @ converse )
= ( one @ ( one @ ( one @ join ) @ join ) ) ),
inference(pattern_uni,[status(thm)],[15636:[bind(A,$thf( one @ ( one @ join ) ))]]) ).
thf(15817,plain,
( ( one @ ( one @ join ) @ ( one @ join ) @ converse )
= ( one @ ( one @ join ) @ ( one @ join ) ) ),
inference(rewrite,[status(thm)],[15637,28]) ).
thf(15,axiom,
! [B: $i,A: $i] :
( ( B @ complement @ ( B @ ( A @ composition ) @ complement @ ( A @ converse @ composition ) @ join ) )
= ( B @ complement ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( B @ complement @ ( B @ ( A @ composition ) @ complement @ ( A @ converse @ composition ) @ join ) )
= ( B @ complement ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( B @ complement @ ( B @ ( A @ composition ) @ complement @ ( A @ converse @ composition ) @ join ) )
= ( B @ complement ) ),
inference(lifteq,[status(thm)],[47]) ).
thf(122,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( D @ ( C @ join ) ) )
| ( ( E @ ( A @ ( B @ join ) @ composition ) )
= ( E @ ( D @ composition ) @ ( E @ ( C @ composition ) @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,22]) ).
thf(123,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ join ) @ composition ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
inference(pattern_uni,[status(thm)],[122:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(137,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ join ) @ composition ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
inference(simp,[status(thm)],[123]) ).
thf(11770,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ composition ) @ ( C @ ( B @ composition ) @ join ) )
= ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) ) ),
inference(rewrite,[status(thm)],[137,22]) ).
thf(7555,plain,
( ( top @ complement @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[4644,7545]) ).
thf(8364,plain,
( ( zero @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[7555,896]) ).
thf(2111,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ join ) @ complement @ ( zero @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[2071,34]) ).
thf(2112,plain,
( ( zero @ ( top @ ( top @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[2111:[bind(A,$thf( zero )),bind(B,$thf( top @ ( top @ join ) @ complement ))]]) ).
thf(7554,plain,
( ( zero @ ( top @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[2112,7545]) ).
thf(7988,plain,
( ( zero @ ( zero @ join ) )
= zero ),
inference(rewrite,[status(thm)],[7554,896]) ).
thf(8446,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( zero @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( top @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[8364,26]) ).
thf(8447,plain,
( ( top @ complement @ ( zero @ complement @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[8446:[bind(A,$thf( zero )),bind(B,$thf( zero ))]]) ).
thf(10097,plain,
( ( zero @ ( zero @ complement @ ( zero @ complement @ join ) @ complement @ join ) )
= zero ),
inference(rewrite,[status(thm)],[8447,896]) ).
thf(10149,plain,
! [B: $i,A: $i] :
( ( ( zero @ ( zero @ complement @ ( zero @ complement @ join ) @ complement @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[10097,34]) ).
thf(10150,plain,
( ( zero @ complement @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
= zero ),
inference(pattern_uni,[status(thm)],[10149:[bind(A,$thf( zero @ complement @ ( zero @ complement @ join ) @ complement )),bind(B,$thf( zero ))]]) ).
thf(67,plain,
! [A: $i] :
( ( ( one @ ( A @ composition ) )
!= ( sk2 @ converse @ ( sk1 @ complement @ composition ) ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[24,63]) ).
thf(70,plain,
! [A: $i] :
( ( ( sk2 @ converse )
!= one )
| ( A
!= ( sk1 @ complement ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( A @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(72,plain,
( ( ( sk2 @ converse )
!= one )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(517,plain,
( ( ( one @ converse )
!= ( sk2 @ converse ) )
| ( one != one )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[443,72]) ).
thf(518,plain,
( ( ( one @ converse )
!= ( sk2 @ converse ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[517]) ).
thf(536,plain,
( ( one != sk2 )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[518]) ).
thf(549,plain,
( ( one != sk2 )
| ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[536]) ).
thf(8058,plain,
( ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( zero @ ( zero @ join ) ) )
| ( one != sk2 )
| ( ( sk1 @ complement )
!= zero ) ),
inference(paramod_ordered,[status(thm)],[7988,549]) ).
thf(8082,plain,
( ( ( sk1 @ complement )
!= zero )
| ( ( sk1 @ complement )
!= zero )
| ( one != sk2 )
| ( ( sk1 @ complement )
!= zero ) ),
inference(simp,[status(thm)],[8058]) ).
thf(8125,plain,
( ( one != sk2 )
| ( ( sk1 @ complement )
!= zero ) ),
inference(simp,[status(thm)],[8082]) ).
thf(8149,plain,
( ( ( top @ complement )
!= ( sk1 @ complement ) )
| ( one != sk2 )
| ( zero != zero ) ),
inference(paramod_ordered,[status(thm)],[896,8125]) ).
thf(8150,plain,
( ( ( top @ complement )
!= ( sk1 @ complement ) )
| ( one != sk2 ) ),
inference(simp,[status(thm)],[8149]) ).
thf(8151,plain,
( ( top != sk1 )
| ( one != sk2 ) ),
inference(simp,[status(thm)],[8150]) ).
thf(7637,plain,
( ( ( sk1 @ complement @ ( sk1 @ complement @ join ) )
!= ( top @ ( top @ join ) ) )
| ( one != sk2 )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[7545,549]) ).
thf(7647,plain,
( ( ( sk1 @ complement )
!= top )
| ( ( sk1 @ complement )
!= top )
| ( one != sk2 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7637]) ).
thf(7690,plain,
( ( one != sk2 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[7647]) ).
thf(118,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,20]) ).
thf(127,plain,
! [C: $i,B: $i,A: $i] :
( ( C != sk2 )
| ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= sk1 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( sk2 @ ( B @ composition ) @ ( sk2 @ ( A @ composition ) @ join ) @ complement @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk1 @ complement @ ( sk2 @ converse @ ( sk1 @ complement @ composition ) @ join ) ) )
| ( one != sk2 )
| ( ( A @ ( B @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[34,63]) ).
thf(75,plain,
( ( one != sk2 )
| ( ( sk2 @ converse @ ( sk1 @ complement @ composition ) @ ( sk1 @ complement @ join ) )
!= ( sk1 @ complement ) ) ),
inference(pattern_uni,[status(thm)],[74:[bind(A,$thf( sk2 @ converse @ ( sk1 @ complement @ composition ) )),bind(B,$thf( sk1 @ complement ))]]) ).
thf(5465,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( ( sk2 @ converse @ ( A @ complement @ composition ) @ complement )
!= ( sk1 @ complement ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[514,65]) ).
thf(5491,plain,
! [A: $i] :
( ( A != sk2 )
| ( one != sk1 )
| ( ( sk2 @ converse @ ( A @ complement @ composition ) )
!= sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5465]) ).
thf(5549,plain,
( ( one != sk1 )
| ( ( sk2 @ converse @ ( sk2 @ complement @ composition ) )
!= sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5491]) ).
thf(119,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,20]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( sk2 @ converse ) )
| ( ( B @ ( A @ join ) )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[119]) ).
thf(132,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( B @ composition ) @ ( sk2 @ converse @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[129]) ).
thf(9229,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( B @ composition ) @ join ) @ ( sk2 @ converse @ ( A @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(rewrite,[status(thm)],[132,28]) ).
thf(5463,plain,
! [A: $i] :
( ( ( one @ ( A @ composition ) )
!= ( sk2 @ converse @ ( sk2 @ ( sk1 @ composition ) @ complement @ composition ) ) )
| ( ( A @ complement )
!= ( sk1 @ complement ) )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[24,65]) ).
thf(5510,plain,
! [A: $i] :
( ( ( sk2 @ converse )
!= one )
| ( A
!= ( sk2 @ ( sk1 @ composition ) @ complement ) )
| ( A != sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5463]) ).
thf(5537,plain,
( ( ( sk2 @ converse )
!= one )
| ( ( sk2 @ ( sk1 @ composition ) @ complement )
!= sk1 )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[5510]) ).
thf(36,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ composition ) @ composition ) )
= ( C @ ( B @ composition ) @ ( A @ composition ) ) ),
inference(lifteq,[status(thm)],[35]) ).
thf(10463,plain,
! [A: $i] :
( ( ( zero @ complement @ ( zero @ complement @ join ) @ complement @ ( zero @ join ) )
!= ( A @ ( zero @ join ) ) )
| ( ( zero @ ( top @ join ) )
= ( A @ ( top @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[10150,1084]) ).
thf(10464,plain,
( ( zero @ complement @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
= ( zero @ ( top @ join ) ) ),
inference(pattern_uni,[status(thm)],[10463:[bind(A,$thf( zero @ complement @ ( zero @ complement @ join ) @ complement ))]]) ).
thf(12520,plain,
( ( zero @ complement @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
= top ),
inference(rewrite,[status(thm)],[10464,913]) ).
thf(120,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ complement @ ( A @ join ) )
!= ( C @ ( B @ join ) ) )
| ( ( D @ ( top @ composition ) )
= ( D @ ( C @ composition ) @ ( D @ ( B @ composition ) @ join ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,22]) ).
thf(121,plain,
! [B: $i,A: $i] :
( ( A @ ( top @ composition ) )
= ( A @ ( B @ complement @ composition ) @ ( A @ ( B @ composition ) @ join ) ) ),
inference(pattern_uni,[status(thm)],[120:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ complement ))]]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( A @ ( top @ composition ) )
= ( A @ ( B @ complement @ composition ) @ ( A @ ( B @ composition ) @ join ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(9149,plain,
! [B: $i,A: $i] :
( ( ( top @ ( top @ complement @ join ) )
!= ( B @ ( A @ complement @ join ) ) )
| ( ( top @ complement @ ( B @ complement @ ( A @ complement @ join ) @ complement @ join ) )
= A ) ),
inference(paramod_ordered,[status(thm)],[9056,26]) ).
thf(9150,plain,
( ( top @ complement @ ( top @ complement @ ( top @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[9149:[bind(A,$thf( top )),bind(B,$thf( top ))]]) ).
thf(11477,plain,
( ( zero @ ( zero @ ( zero @ join ) @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[9150,896]) ).
thf(7557,plain,
( ( top @ ( zero @ join ) @ complement @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[4577,7545]) ).
thf(8680,plain,
( ( top @ complement @ ( zero @ complement @ join ) )
= top ),
inference(rewrite,[status(thm)],[7557,898]) ).
thf(21964,plain,
! [A: $i] :
( ( ( A @ ( one @ composition ) )
!= ( sk2 @ ( sk1 @ composition ) ) )
| ( A != sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(paramod_ordered,[status(thm)],[514,20097]) ).
thf(21988,plain,
( ( sk2 != sk1 )
| ( one != sk1 )
| ( ( sk2 @ converse )
!= one )
| ( ( sk1 @ complement )
!= top ) ),
inference(simp,[status(thm)],[21964]) ).
thf(113,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ join ) @ composition ) )
!= ( sk2 @ converse @ ( sk1 @ complement @ composition ) ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[22,63]) ).
thf(128,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( sk2 @ converse ) )
| ( ( B @ ( A @ join ) )
!= ( sk1 @ complement ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( C @ ( B @ composition ) @ ( C @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk1 @ complement ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( B @ composition ) @ ( sk2 @ converse @ ( A @ composition ) @ join ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(8829,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ join ) )
!= ( sk1 @ complement ) )
| ( one != sk2 )
| ( ( sk1 @ complement @ ( sk2 @ converse @ ( B @ composition ) @ join ) @ ( sk2 @ converse @ ( A @ composition ) @ join ) )
!= ( sk1 @ complement ) ) ),
inference(rewrite,[status(thm)],[131,28]) ).
thf(12593,plain,
! [B: $i,A: $i] :
( ( ( zero @ complement @ ( zero @ complement @ join ) @ complement @ ( top @ join ) )
!= ( B @ ( A @ join ) ) )
| ( ( A @ ( B @ join ) )
= top ) ),
inference(paramod_ordered,[status(thm)],[12520,34]) ).
thf(12594,plain,
( ( top @ ( zero @ complement @ ( zero @ complement @ join ) @ complement @ join ) )
= top ),
inference(pattern_uni,[status(thm)],[12593:[bind(A,$thf( top )),bind(B,$thf( zero @ complement @ ( zero @ complement @ join ) @ complement ))]]) ).
thf(42494,plain,
$false,
inference(e,[status(thm)],[18636,169,39,162,69,101,21486,21012,88,7697,913,1222,898,24,885,37,25,9056,13511,3776,22004,19063,5461,20,46,1013,29,9480,189,12281,443,514,1020,766,133,14654,1021,693,21,33,1174,28,38,65,5534,7545,18183,9662,13527,515,15369,13483,20557,20097,41,10635,14573,45,64,32,34,3187,191,22,59,1488,27,13217,49,181,13606,8517,7685,7551,1113,35,19580,167,15817,48,63,11770,18,8364,7988,544,31,10097,10150,8151,43,7690,1084,7547,8221,896,40,26,139,23,75,5549,549,9229,30,51,5537,36,12520,136,79,94,47,11477,8680,21988,8125,8829,12594]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL012-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.13 % 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.24/0.56 % Computer : n003.cluster.edu
% 0.24/0.56 % Model : x86_64 x86_64
% 0.24/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.56 % Memory : 8046.5625MB
% 0.24/0.56 % OS : Linux 6.8.0-71-generic
% 0.24/0.56 % CPULimit : 300
% 0.24/0.56 % WCLimit : 300
% 0.24/0.56 % DateTime : Sat Sep 26 05:29:39 UTC 2026
% 0.24/0.57 % CPUTime :
% 0.24/0.57 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
% 1.47/1.44 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.97/1.76 % [INFO] Parsing done (314ms).
% 1.97/1.78 % [INFO] Running in sequential loop mode.
% 3.34/2.43 % [INFO] eprover registered as external prover.
% 3.34/2.44 % [INFO] Scanning for conjecture ...
% 3.53/2.58 % [INFO] Found a conjecture (or negated_conjecture) and 16 axioms. Running axiom selection ...
% 3.68/2.67 % [INFO] Axiom selection finished. Selected 16 axioms (removed 0 axioms).
% 3.90/2.73 % [INFO] Problem is propositional (TPTP CNF).
% 3.90/2.74 % [INFO] Type checking passed.
% 3.90/2.75 % [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 ...
% 96.68/21.05 % External prover 'e' found a proof!
% 96.68/21.05 % [INFO] Killing All external provers ...
% 96.68/21.06 % Time passed: 20273ms (effective reasoning time: 19261ms)
% 96.68/21.06 % Axioms used in derivation (16): maddux3_a_kind_of_de_Morgan_3, converse_idempotence_8, def_top_12, converse_cancellativity_11, composition_associativity_5, maddux2_join_associativity_2, composition_distributivity_7, maddux1_join_commutativity_1, modular_law_1_15, composition_identity_6, maddux4_definiton_of_meet_4, converse_additivity_9, dedekind_law_14, modular_law_2_16, def_zero_13, converse_multiplicativity_10
% 96.68/21.06 % No. of inferences in proof: 335
% 96.68/21.06 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 20273 ms resp. 19261 ms w/o parsing
% 82.72/21.21 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 82.72/21.21 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------