%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : KLE013+1 : 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 : n011.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:42:58 AM UTC 2026
% Result : Theorem 105.72s 21.97s
% Output : Refutation 108.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 20
% Syntax : Number of formulae : 593 ( 204 unt; 0 typ; 3 def)
% Number of atoms : 1500 ( 929 equ; 0 cnn)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 5199 ( 661 ~; 543 |; 31 &;3934 @)
% ( 4 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 14 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 769 ( 1 ^; 760 !; 5 ?; 769 :)
% ( 0 !>; 0 ?*; 0 @-; 3 @+)
% Comments :
%------------------------------------------------------------------------------
thf(test_decl,type,
test: $i > $o ).
thf(one_decl,type,
one: $i ).
thf(addition_decl,type,
addition: $i > $i > $i ).
thf(multiplication_decl,type,
multiplication: $i > $i > $i ).
thf(c_decl,type,
c: $i > $i ).
thf(zero_decl,type,
zero: $i ).
thf(complement_decl,type,
complement: $i > $i > $o ).
thf(leq_decl,type,
leq: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( A @ test )
& ( B @ test ) )
=> ( one
= ( B @ c @ ( A @ c @ multiplication ) @ ( B @ ( A @ addition ) @ addition ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ( ( ( sk1 @ test )
& ( A @ test ) )
=> ( one
= ( A @ c @ ( sk1 @ c @ multiplication ) @ ( A @ ( sk1 @ addition ) @ addition ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( ^ [A: $i] :
@+[B: $i] : ( A @ ( B @ complement ) ) ) ) ).
thf(1,conjecture,
! [A: $i,B: $i] :
( ( ( A @ test )
& ( B @ test ) )
=> ( one
= ( B @ c @ ( A @ c @ multiplication ) @ ( B @ ( A @ addition ) @ addition ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i] :
( ( ( A @ test )
& ( B @ test ) )
=> ( one
= ( B @ c @ ( A @ c @ multiplication ) @ ( B @ ( A @ addition ) @ addition ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(19,plain,
~ ! [A: $i,B: $i] :
( ( ( A @ test )
& ( B @ test ) )
=> ( one
= ( B @ c @ ( A @ c @ multiplication ) @ ( B @ ( A @ addition ) @ addition ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(20,plain,
( ( one
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) ) )
& ( sk1 @ test )
& ( sk2 @ test ) ),
inference(cnf,[status(esa)],[19]) ).
thf(21,plain,
sk2 @ test,
inference(cnfConj,[status(thm)],[20]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( A @ test )
=> ( ( ( A @ c )
= B )
<=> ( B @ ( A @ complement ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_3) ).
thf(55,plain,
! [A: $i,B: $i] :
( ( A @ test )
=> ( ( ( B @ ( A @ complement ) )
=> ( ( A @ c )
= B ) )
& ( ( ( A @ c )
= B )
=> ( B @ ( A @ complement ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(56,plain,
! [A: $i] :
( ( A @ test )
=> ( ! [B: $i] :
( ( B @ ( A @ complement ) )
=> ( ( A @ c )
= B ) )
& ! [B: $i] :
( ( ( A @ c )
= B )
=> ( B @ ( A @ complement ) ) ) ) ),
inference(miniscope,[status(thm)],[55]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ( ( ( A @ c )
= C )
| ~ ( C @ ( A @ complement ) )
| ~ ( A @ test ) )
& ( ( B @ ( A @ complement ) )
| ( ( A @ c )
!= B )
| ~ ( A @ test ) ) ),
inference(cnf,[status(esa)],[56]) ).
thf(58,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ complement ) )
| ( ( A @ c )
!= B )
| ~ ( A @ test ) ),
inference(cnfConj,[status(thm)],[57]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ complement ) )
| ~ ( A @ test )
| ( ( A @ c )
!= B ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(61,plain,
! [A: $i] :
( ( A @ c @ ( A @ complement ) )
| ~ ( A @ test ) ),
inference(simp,[status(thm)],[60]) ).
thf(588,plain,
! [A: $i] :
( ( ( sk2 @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,61]) ).
thf(589,plain,
! [A: $i] :
( ( ( sk2 @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[588]) ).
thf(590,plain,
sk2 @ c @ ( sk2 @ complement ),
inference(pattern_uni,[status(thm)],[589:[bind(A,$thf( sk2 ))]]) ).
thf(9,axiom,
! [A: $i] :
( ( A @ test )
<=> ? [B: $i] : ( A @ ( B @ complement ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_1) ).
thf(43,plain,
! [A: $i] :
( ( ? [B: $i] : ( A @ ( B @ complement ) )
=> ( A @ test ) )
& ( ( A @ test )
=> ? [B: $i] : ( A @ ( B @ complement ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(44,plain,
( ! [A: $i] :
( ? [B: $i] : ( A @ ( B @ complement ) )
=> ( A @ test ) )
& ! [A: $i] :
( ( A @ test )
=> ? [B: $i] : ( A @ ( B @ complement ) ) ) ),
inference(miniscope,[status(thm)],[43]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ test )
| ~ ( B @ ( C @ complement ) ) )
& ( ( A @ ( A @ sk3 @ complement ) )
| ~ ( A @ test ) ) ),
inference(cnf,[status(esa)],[44]) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( A @ test )
| ~ ( A @ ( B @ complement ) ) ),
inference(cnfConj,[status(thm)],[45]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( A @ test )
| ~ ( A @ ( B @ complement ) ) ),
inference(simp,[status(thm)],[47]) ).
thf(597,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[590,48]) ).
thf(598,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[597]) ).
thf(599,plain,
sk2 @ c @ test,
inference(pattern_uni,[status(thm)],[598:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 ))]]) ).
thf(602,plain,
! [A: $i] :
( ( ( sk2 @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[599,61]) ).
thf(603,plain,
! [A: $i] :
( ( ( sk2 @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[602]) ).
thf(604,plain,
sk2 @ c @ c @ ( sk2 @ c @ complement ),
inference(pattern_uni,[status(thm)],[603:[bind(A,$thf( sk2 @ c ))]]) ).
thf(851,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[604,48]) ).
thf(852,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[851]) ).
thf(853,plain,
sk2 @ c @ c @ test,
inference(pattern_uni,[status(thm)],[852:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c ))]]) ).
thf(879,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[853,61]) ).
thf(880,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[879]) ).
thf(881,plain,
sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ),
inference(pattern_uni,[status(thm)],[880:[bind(A,$thf( sk2 @ c @ c ))]]) ).
thf(7234,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[881,48]) ).
thf(7235,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[7234]) ).
thf(7236,plain,
sk2 @ c @ c @ c @ test,
inference(pattern_uni,[status(thm)],[7235:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c ))]]) ).
thf(46,plain,
! [A: $i] :
( ( A @ ( A @ sk3 @ complement ) )
| ~ ( A @ test ) ),
inference(cnfConj,[status(thm)],[45]) ).
thf(7291,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7236,46]) ).
thf(7292,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[7291]) ).
thf(7293,plain,
sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[7292:[bind(A,$thf( sk2 @ c @ c @ c ))]]) ).
thf(13,axiom,
! [A: $i,B: $i] :
( ( A @ ( B @ complement ) )
<=> ( ( ( B @ ( A @ addition ) )
= one )
& ( ( A @ ( B @ multiplication ) )
= zero )
& ( ( B @ ( A @ multiplication ) )
= zero ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_2) ).
thf(64,plain,
! [A: $i,B: $i] :
( ( ( ( ( B @ ( A @ addition ) )
= one )
& ( ( A @ ( B @ multiplication ) )
= zero )
& ( ( B @ ( A @ multiplication ) )
= zero ) )
=> ( A @ ( B @ complement ) ) )
& ( ( A @ ( B @ complement ) )
=> ( ( ( B @ ( A @ addition ) )
= one )
& ( ( A @ ( B @ multiplication ) )
= zero )
& ( ( B @ ( A @ multiplication ) )
= zero ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(65,plain,
( ! [A: $i,B: $i] :
( ( ( ( B @ ( A @ addition ) )
= one )
& ( ( A @ ( B @ multiplication ) )
= zero )
& ( ( B @ ( A @ multiplication ) )
= zero ) )
=> ( A @ ( B @ complement ) ) )
& ! [A: $i,B: $i] :
( ( A @ ( B @ complement ) )
=> ( ( ( B @ ( A @ addition ) )
= one )
& ( ( A @ ( B @ multiplication ) )
= zero )
& ( ( B @ ( A @ multiplication ) )
= zero ) ) ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( D @ complement ) )
| ( ( D @ ( C @ addition ) )
!= one )
| ( ( C @ ( D @ multiplication ) )
!= zero )
| ( ( D @ ( C @ multiplication ) )
!= zero ) )
& ( ( ( B @ ( A @ addition ) )
= one )
| ~ ( A @ ( B @ complement ) ) )
& ( ( ( A @ ( B @ multiplication ) )
= zero )
| ~ ( A @ ( B @ complement ) ) )
& ( ( ( B @ ( A @ multiplication ) )
= zero )
| ~ ( A @ ( B @ complement ) ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(69,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
= one )
| ~ ( A @ ( B @ complement ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(73,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ complement ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(17402,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7293,73]) ).
thf(17403,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[17402]) ).
thf(17404,plain,
( ( sk2 @ c @ c @ c @ sk3 @ ( sk2 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[17403:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c @ sk3 ))]]) ).
thf(22,plain,
sk1 @ test,
inference(cnfConj,[status(thm)],[20]) ).
thf(440,plain,
! [A: $i] :
( ( ( sk1 @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,46]) ).
thf(441,plain,
! [A: $i] :
( ( ( sk1 @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[440]) ).
thf(442,plain,
sk1 @ ( sk1 @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[441:[bind(A,$thf( sk1 ))]]) ).
thf(1978,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[442,73]) ).
thf(1979,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1978]) ).
thf(1980,plain,
( ( sk1 @ sk3 @ ( sk1 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1979:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk3 ))]]) ).
thf(15,axiom,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_annihilation) ).
thf(79,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(80,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[79]) ).
thf(81,plain,
! [A: $i] :
( ( zero @ ( A @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[80]) ).
thf(23,plain,
( one
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) ) ),
inference(cnfConj,[status(thm)],[20]) ).
thf(24,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ),
inference(lifteq,[status(thm)],[23]) ).
thf(102,plain,
! [A: $i] :
( ( ( zero @ ( A @ multiplication ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[81,24]) ).
thf(104,plain,
! [A: $i] :
( ( ( sk2 @ c )
!= zero )
| ( A
!= ( sk1 @ c ) )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[102]) ).
thf(106,plain,
( ( ( sk2 @ c )
!= zero )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[104]) ).
thf(16,axiom,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
thf(82,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(83,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[82]) ).
thf(84,plain,
! [A: $i] :
( ( zero @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[83]) ).
thf(180,plain,
( ( ( sk2 @ c )
!= zero )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[106,84]) ).
thf(2223,plain,
( ( ( sk1 @ sk3 @ ( sk1 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[1980,180]) ).
thf(2224,plain,
( ( ( sk1 @ sk3 @ ( sk1 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2223]) ).
thf(2251,plain,
( ( ( sk1 @ sk3 )
!= sk2 )
| ( sk1 != sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2224]) ).
thf(2263,plain,
( ( ( sk1 @ sk3 )
!= sk2 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2251]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
thf(31,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(32,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ addition ) @ ( C @ addition ) )
= ( A @ ( B @ ( C @ addition ) @ addition ) ) ),
inference(cnf,[status(esa)],[31]) ).
thf(33,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ addition ) @ addition ) )
= ( A @ ( B @ addition ) @ ( C @ addition ) ) ),
inference(lifteq,[status(thm)],[32]) ).
thf(226,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[33,180]) ).
thf(231,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk2 )
| ( ( B @ ( C @ addition ) )
!= sk1 )
| ( ( sk2 @ c )
!= zero )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[226]) ).
thf(234,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= sk1 )
| ( ( sk2 @ c )
!= zero )
| ( ( sk2 @ ( A @ addition ) @ ( B @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[231]) ).
thf(591,plain,
! [A: $i] :
( ( ( sk1 @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,61]) ).
thf(592,plain,
! [A: $i] :
( ( ( sk1 @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[591]) ).
thf(593,plain,
sk1 @ c @ ( sk1 @ complement ),
inference(pattern_uni,[status(thm)],[592:[bind(A,$thf( sk1 ))]]) ).
thf(610,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[593,48]) ).
thf(611,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[610]) ).
thf(612,plain,
sk1 @ c @ test,
inference(pattern_uni,[status(thm)],[611:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 ))]]) ).
thf(615,plain,
! [A: $i] :
( ( ( sk1 @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[612,61]) ).
thf(616,plain,
! [A: $i] :
( ( ( sk1 @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[615]) ).
thf(617,plain,
sk1 @ c @ c @ ( sk1 @ c @ complement ),
inference(pattern_uni,[status(thm)],[616:[bind(A,$thf( sk1 @ c ))]]) ).
thf(928,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[617,48]) ).
thf(929,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[928]) ).
thf(930,plain,
sk1 @ c @ c @ test,
inference(pattern_uni,[status(thm)],[929:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c ))]]) ).
thf(980,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[930,61]) ).
thf(981,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[980]) ).
thf(982,plain,
sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ),
inference(pattern_uni,[status(thm)],[981:[bind(A,$thf( sk1 @ c @ c ))]]) ).
thf(7473,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[982,48]) ).
thf(7474,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[7473]) ).
thf(7475,plain,
sk1 @ c @ c @ c @ test,
inference(pattern_uni,[status(thm)],[7474:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c ))]]) ).
thf(7531,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7475,46]) ).
thf(7532,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[7531]) ).
thf(7533,plain,
sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[7532:[bind(A,$thf( sk1 @ c @ c @ c ))]]) ).
thf(17713,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7533,73]) ).
thf(17714,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[17713]) ).
thf(17715,plain,
( ( sk1 @ c @ c @ c @ sk3 @ ( sk1 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[17714:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c @ sk3 ))]]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
thf(52,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(cnf,[status(esa)],[52]) ).
thf(54,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) )
= ( A @ ( B @ addition ) ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(21325,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ sk3 @ ( sk1 @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[17715,54]) ).
thf(21326,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[21325:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c @ sk3 ))]]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
<=> ( ( B @ ( A @ addition ) )
= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order) ).
thf(88,plain,
! [A: $i,B: $i] :
( ( ( ( B @ ( A @ addition ) )
= B )
=> ( B @ ( A @ leq ) ) )
& ( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ addition ) )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(228,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( E @ ( F @ addition ) ) )
| ( ( D @ ( A @ ( B @ addition ) @ ( C @ addition ) @ addition ) )
= ( D @ ( E @ addition ) @ ( F @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[33,33]) ).
thf(229,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ ( C @ addition ) @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ ( C @ addition ) @ addition ) ) ),
inference(pattern_uni,[status(thm)],[228:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( G )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( H @ ( G @ addition ) ))]]) ).
thf(232,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ ( C @ addition ) @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ ( C @ addition ) @ addition ) ) ),
inference(simp,[status(thm)],[229]) ).
thf(18272,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ addition ) @ addition ) @ ( C @ addition ) )
= ( B @ ( A @ addition ) @ ( D @ addition ) @ ( C @ addition ) ) ),
inference(rewrite,[status(thm)],[232,33]) ).
thf(1935,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[593,73]) ).
thf(1936,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1935]) ).
thf(1937,plain,
( ( sk1 @ ( sk1 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1936:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 ))]]) ).
thf(2124,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ c @ addition ) )
!= ( zero @ ( A @ addition ) ) )
| ( one = A ) ),
inference(paramod_ordered,[status(thm)],[1937,84]) ).
thf(2177,plain,
! [A: $i] :
( ( sk1 != zero )
| ( ( sk1 @ c )
!= A )
| ( one = A ) ),
inference(simp,[status(thm)],[2124]) ).
thf(2189,plain,
( ( sk1 != zero )
| ( ( sk1 @ c )
= one ) ),
inference(simp,[status(thm)],[2177]) ).
thf(2150,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1937,54]) ).
thf(2151,plain,
( ( sk1 @ c @ ( sk1 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[2150:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 ))]]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
thf(40,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(41,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[40]) ).
thf(42,plain,
! [A: $i] :
( ( A @ ( one @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[41]) ).
thf(112,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( A @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[42,24]) ).
thf(116,plain,
! [A: $i] :
( ( A
!= ( sk2 @ c ) )
| ( ( sk1 @ c )
!= one )
| ( ( A @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[112]) ).
thf(119,plain,
( ( ( sk1 @ c )
!= one )
| ( ( sk2 @ c @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[116]) ).
thf(218,plain,
( ( ( sk1 @ c )
!= one )
| ( ( sk2 @ c @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[119,33]) ).
thf(1920,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[590,73]) ).
thf(1921,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1920]) ).
thf(1922,plain,
( ( sk2 @ ( sk2 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1921:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 ))]]) ).
thf(2009,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1922,54]) ).
thf(2010,plain,
( ( sk2 @ c @ ( sk2 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[2009:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 ))]]) ).
thf(18122,plain,
( ( ( sk1 @ c )
!= one )
| ( ( one @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[218,2010]) ).
thf(18170,plain,
( ( ( sk1 @ c @ ( sk1 @ addition ) )
!= ( one @ ( sk1 @ addition ) ) )
| ( ( sk1 @ c )
!= one )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[2151,18122]) ).
thf(18171,plain,
( ( ( sk1 @ c @ ( sk1 @ addition ) )
!= ( one @ ( sk1 @ addition ) ) )
| ( ( sk1 @ c )
!= one ) ),
inference(simp,[status(thm)],[18170]) ).
thf(18202,plain,
( ( ( sk1 @ c )
!= one )
| ( sk1 != sk1 )
| ( ( sk1 @ c )
!= one ) ),
inference(simp,[status(thm)],[18171]) ).
thf(18235,plain,
( ( sk1 @ c )
!= one ),
inference(simp,[status(thm)],[18202]) ).
thf(19804,plain,
sk1 != zero,
inference(simplifyReflect,[status(thm)],[2189,18235]) ).
thf(10,axiom,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
thf(49,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(50,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(cnf,[status(esa)],[49]) ).
thf(51,plain,
! [A: $i] :
( ( A @ ( A @ addition ) )
= A ),
inference(lifteq,[status(thm)],[50]) ).
thf(276,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( C @ ( D @ addition ) ) )
| ( ( B @ ( A @ addition ) )
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[51,33]) ).
thf(277,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[276:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(30193,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( one @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[2010,277]) ).
thf(30194,plain,
( ( sk2 @ c @ ( sk2 @ addition ) )
= ( one @ ( sk2 @ addition ) ) ),
inference(pattern_uni,[status(thm)],[30193:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ c ))]]) ).
thf(30609,plain,
( ( one @ ( sk2 @ addition ) )
= one ),
inference(rewrite,[status(thm)],[30194,2010]) ).
thf(30747,plain,
! [B: $i,A: $i] :
( ( ( one @ ( sk2 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[30609,54]) ).
thf(30748,plain,
( ( sk2 @ ( one @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[30747:[bind(A,$thf( sk2 )),bind(B,$thf( one ))]]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
= zero )
| ~ ( A @ ( B @ complement ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(71,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ complement ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(1010,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[593,71]) ).
thf(1011,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1010]) ).
thf(1012,plain,
( ( sk1 @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1011:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 ))]]) ).
thf(14,axiom,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
thf(76,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(77,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(cnf,[status(esa)],[76]) ).
thf(78,plain,
! [A: $i] :
( ( one @ ( A @ multiplication ) )
= A ),
inference(lifteq,[status(thm)],[77]) ).
thf(1079,plain,
! [A: $i] :
( ( ( sk1 @ ( sk1 @ c @ multiplication ) )
!= ( one @ ( A @ multiplication ) ) )
| ( zero = A ) ),
inference(paramod_ordered,[status(thm)],[1012,78]) ).
thf(1115,plain,
! [A: $i] :
( ( sk1 != one )
| ( ( sk1 @ c )
!= A )
| ( zero = A ) ),
inference(simp,[status(thm)],[1079]) ).
thf(1127,plain,
( ( sk1 != one )
| ( ( sk1 @ c )
= zero ) ),
inference(simp,[status(thm)],[1115]) ).
thf(3,axiom,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_annihilation) ).
thf(25,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(26,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(cnf,[status(esa)],[25]) ).
thf(27,plain,
! [A: $i] :
( ( A @ ( zero @ multiplication ) )
= zero ),
inference(lifteq,[status(thm)],[26]) ).
thf(103,plain,
! [A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[27,24]) ).
thf(105,plain,
! [A: $i] :
( ( A
!= ( sk2 @ c ) )
| ( ( sk1 @ c )
!= zero )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[103]) ).
thf(107,plain,
( ( ( sk1 @ c )
!= zero )
| ( ( zero @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[105]) ).
thf(181,plain,
( ( ( sk1 @ c )
!= zero )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[107,84]) ).
thf(1846,plain,
( ( ( sk1 @ c )
!= ( sk1 @ c ) )
| ( zero != zero )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk1 != one ) ),
inference(paramod_ordered,[status(thm)],[1127,181]) ).
thf(1847,plain,
( ( ( sk1 @ c )
!= ( sk1 @ c ) )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk1 != one ) ),
inference(simp,[status(thm)],[1846]) ).
thf(1848,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk1 != one ) ),
inference(pattern_uni,[status(thm)],[1847:[]]) ).
thf(31145,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= ( sk2 @ ( one @ addition ) ) )
| ( one != one )
| ( sk1 != one ) ),
inference(paramod_ordered,[status(thm)],[30748,1848]) ).
thf(31146,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= ( sk2 @ ( one @ addition ) ) )
| ( sk1 != one ) ),
inference(simp,[status(thm)],[31145]) ).
thf(31175,plain,
( ( sk2 != sk2 )
| ( sk1 != one )
| ( sk1 != one ) ),
inference(simp,[status(thm)],[31146]) ).
thf(31207,plain,
sk1 != one,
inference(simp,[status(thm)],[31175]) ).
thf(1051,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[617,71]) ).
thf(1052,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1051]) ).
thf(1053,plain,
( ( sk1 @ c @ ( sk1 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1052:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c ))]]) ).
thf(4,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
thf(28,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= ( C @ ( B @ ( A @ multiplication ) @ multiplication ) ) ),
inference(cnf,[status(esa)],[28]) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( A @ multiplication ) ) ),
inference(lifteq,[status(thm)],[29]) ).
thf(137,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ multiplication ) )
!= ( D @ ( C @ ( B @ multiplication ) @ multiplication ) ) )
| ( ( D @ ( C @ multiplication ) @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[27,30]) ).
thf(138,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( C @ ( B @ multiplication ) )
!= zero )
| ( ( D @ ( C @ multiplication ) @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[137]) ).
thf(147,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[138]) ).
thf(6451,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1053,147]) ).
thf(6452,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6451]) ).
thf(6453,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6452:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c )),bind(C,$thf( C ))]]) ).
thf(6522,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ c @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6453]) ).
thf(1013,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[590,71]) ).
thf(1014,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1013]) ).
thf(1015,plain,
( ( sk2 @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1014:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 ))]]) ).
thf(6406,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1015,147]) ).
thf(6407,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6406]) ).
thf(6408,plain,
! [A: $i] :
( ( A @ ( sk2 @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6407:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 )),bind(C,$thf( C ))]]) ).
thf(6505,plain,
! [A: $i] :
( ( A @ ( sk2 @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6408]) ).
thf(443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( zero @ ( C @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[54,84]) ).
thf(444,plain,
! [A: $i] :
( ( A @ ( zero @ addition ) )
= A ),
inference(pattern_uni,[status(thm)],[443:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(2149,plain,
! [A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( sk1 @ ( sk1 @ c @ addition ) ) )
| ( A = one ) ),
inference(paramod_ordered,[status(thm)],[444,1937]) ).
thf(2185,plain,
! [A: $i] :
( ( A != sk1 )
| ( ( sk1 @ c )
!= zero )
| ( A = one ) ),
inference(simp,[status(thm)],[2149]) ).
thf(2194,plain,
( ( ( sk1 @ c )
!= zero )
| ( sk1 = one ) ),
inference(simp,[status(thm)],[2185]) ).
thf(31220,plain,
( ( sk1 @ c )
!= zero ),
inference(simplifyReflect,[status(thm)],[2194,31207]) ).
thf(1966,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[617,73]) ).
thf(1967,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1966]) ).
thf(1968,plain,
( ( sk1 @ c @ ( sk1 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1967:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c ))]]) ).
thf(5226,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1968,54]) ).
thf(5227,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[5226:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c ))]]) ).
thf(437,plain,
! [A: $i] :
( ( ( sk2 @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[21,46]) ).
thf(438,plain,
! [A: $i] :
( ( ( sk2 @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[437]) ).
thf(439,plain,
sk2 @ ( sk2 @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[438:[bind(A,$thf( sk2 ))]]) ).
thf(1926,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[439,73]) ).
thf(1927,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1926]) ).
thf(1928,plain,
( ( sk2 @ sk3 @ ( sk2 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1927:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ sk3 ))]]) ).
thf(2081,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ sk3 @ ( sk2 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1928,54]) ).
thf(2082,plain,
( ( sk2 @ ( sk2 @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[2081:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ sk3 ))]]) ).
thf(7,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
thf(37,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(1027,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[439,71]) ).
thf(1028,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1027]) ).
thf(1029,plain,
( ( sk2 @ sk3 @ ( sk2 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1028:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ sk3 ))]]) ).
thf(6388,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ sk3 @ ( sk2 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1029,147]) ).
thf(6389,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ sk3 @ ( sk2 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6388]) ).
thf(6390,plain,
! [A: $i] :
( ( A @ ( sk2 @ sk3 @ multiplication ) @ ( sk2 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6389:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ sk3 )),bind(C,$thf( C ))]]) ).
thf(6552,plain,
! [A: $i] :
( ( A @ ( sk2 @ sk3 @ multiplication ) @ ( sk2 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6390]) ).
thf(882,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[853,46]) ).
thf(883,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[882]) ).
thf(884,plain,
sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[883:[bind(A,$thf( sk2 @ c @ c ))]]) ).
thf(7399,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[884,71]) ).
thf(7400,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7399]) ).
thf(7401,plain,
( ( sk2 @ c @ c @ sk3 @ ( sk2 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7400:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c @ c @ sk3 ))]]) ).
thf(7534,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7475,61]) ).
thf(7535,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[7534]) ).
thf(7536,plain,
sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ),
inference(pattern_uni,[status(thm)],[7535:[bind(A,$thf( sk1 @ c @ c @ c ))]]) ).
thf(17830,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7536,73]) ).
thf(17831,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[17830]) ).
thf(17832,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[17831:[bind(A,$thf( sk1 @ c @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c ))]]) ).
thf(22776,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[17832,54]) ).
thf(22777,plain,
( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[22776:[bind(A,$thf( sk1 @ c @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c ))]]) ).
thf(618,plain,
! [A: $i] :
( ( ( sk1 @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[612,46]) ).
thf(619,plain,
! [A: $i] :
( ( ( sk1 @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[618]) ).
thf(620,plain,
sk1 @ c @ ( sk1 @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[619:[bind(A,$thf( sk1 @ c ))]]) ).
thf(1774,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[620,71]) ).
thf(1775,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1774]) ).
thf(1776,plain,
( ( sk1 @ c @ sk3 @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1775:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 @ c @ sk3 ))]]) ).
thf(6312,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ sk3 @ ( sk1 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1776,147]) ).
thf(6313,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ sk3 @ ( sk1 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6312]) ).
thf(6314,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ sk3 @ multiplication ) @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6313:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 @ c @ sk3 )),bind(C,$thf( C ))]]) ).
thf(6519,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ sk3 @ multiplication ) @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6314]) ).
thf(7294,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7236,61]) ).
thf(7295,plain,
! [A: $i] :
( ( ( sk2 @ c @ c @ c @ test )
!= ( A @ test ) )
| ( A @ c @ ( A @ complement ) ) ),
inference(simp,[status(thm)],[7294]) ).
thf(7296,plain,
sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ),
inference(pattern_uni,[status(thm)],[7295:[bind(A,$thf( sk2 @ c @ c @ c ))]]) ).
thf(17529,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7296,73]) ).
thf(17530,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[17529]) ).
thf(17531,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[17530:[bind(A,$thf( sk2 @ c @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c ))]]) ).
thf(20275,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[17531,54]) ).
thf(20276,plain,
( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[20275:[bind(A,$thf( sk2 @ c @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c ))]]) ).
thf(89,plain,
( ! [A: $i,B: $i] :
( ( ( B @ ( A @ addition ) )
= B )
=> ( B @ ( A @ leq ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ leq ) )
=> ( ( B @ ( A @ addition ) )
= B ) ) ),
inference(miniscope,[status(thm)],[88]) ).
thf(90,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ leq ) )
| ( ( D @ ( C @ addition ) )
!= D ) )
& ( ( ( B @ ( A @ addition ) )
= B )
| ~ ( B @ ( A @ leq ) ) ) ),
inference(cnf,[status(esa)],[89]) ).
thf(91,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
= B )
| ~ ( B @ ( A @ leq ) ) ),
inference(cnfConj,[status(thm)],[90]) ).
thf(93,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
= B ) ),
inference(lifteq,[status(thm)],[91]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ multiplication ) )
= zero )
| ~ ( A @ ( B @ complement ) ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(72,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ complement ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(lifteq,[status(thm)],[68]) ).
thf(17586,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7296,72]) ).
thf(17587,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17586]) ).
thf(17588,plain,
( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17587:[bind(A,$thf( sk2 @ c @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c ))]]) ).
thf(274,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( B @ ( C @ ( D @ addition ) @ addition ) ) )
| ( A
= ( B @ ( C @ addition ) @ ( D @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[51,33]) ).
thf(275,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(pattern_uni,[status(thm)],[274:[bind(A,$thf( H @ ( G @ addition ) )),bind(B,$thf( H @ ( G @ addition ) )),bind(C,$thf( H )),bind(D,$thf( G ))]]) ).
thf(289,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ addition ) @ ( B @ addition ) @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ),
inference(simp,[status(thm)],[275]) ).
thf(219,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= one ),
inference(rewrite,[status(thm)],[24,33]) ).
thf(242,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[33,219]) ).
thf(259,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( B @ ( C @ addition ) )
!= sk2 )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[242]) ).
thf(261,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= sk2 )
| ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( A @ addition ) @ ( B @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[259]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ( ( A @ c )
= B )
| ~ ( B @ ( A @ complement ) )
| ~ ( A @ test ) ),
inference(cnfConj,[status(thm)],[57]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ complement ) )
| ~ ( A @ test )
| ( ( A @ c )
= B ) ),
inference(lifteq,[status(thm)],[59]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ complement ) )
| ~ ( A @ test )
| ( ( A @ c )
= B ) ),
inference(simp,[status(thm)],[62]) ).
thf(18247,plain,
! [B: $i,A: $i] :
( ( ( A @ c )
!= ( sk1 @ c ) )
| ( B != one )
| ~ ( B @ ( A @ complement ) )
| ~ ( A @ test ) ),
inference(paramod_ordered,[status(thm)],[63,18235]) ).
thf(18248,plain,
! [A: $i] :
( ( A != one )
| ~ ( A @ ( sk1 @ complement ) )
| ~ ( sk1 @ test ) ),
inference(pattern_uni,[status(thm)],[18247:[bind(A,$thf( sk1 ))]]) ).
thf(18256,plain,
( ~ ( one @ ( sk1 @ complement ) )
| ~ ( sk1 @ test ) ),
inference(simp,[status(thm)],[18248]) ).
thf(19735,plain,
( ~ ( one @ ( sk1 @ complement ) )
| ~ $true ),
inference(rewrite,[status(thm)],[18256,22]) ).
thf(19736,plain,
~ ( one @ ( sk1 @ complement ) ),
inference(simp,[status(thm)],[19735]) ).
thf(17457,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7293,72]) ).
thf(17458,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17457]) ).
thf(17459,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17458:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c @ sk3 ))]]) ).
thf(605,plain,
! [A: $i] :
( ( ( sk2 @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[599,46]) ).
thf(606,plain,
! [A: $i] :
( ( ( sk2 @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[605]) ).
thf(607,plain,
sk2 @ c @ ( sk2 @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[606:[bind(A,$thf( sk2 @ c ))]]) ).
thf(1401,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[607,72]) ).
thf(1402,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1401]) ).
thf(1403,plain,
( ( sk2 @ c @ ( sk2 @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1402:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ sk3 ))]]) ).
thf(6330,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1403,147]) ).
thf(6331,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6330]) ).
thf(6332,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ multiplication ) @ ( sk2 @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6331:[bind(A,$thf( sk2 @ c @ sk3 )),bind(B,$thf( sk2 @ c )),bind(C,$thf( C ))]]) ).
thf(6523,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ multiplication ) @ ( sk2 @ c @ sk3 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6332]) ).
thf(1971,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[620,73]) ).
thf(1972,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1971]) ).
thf(1973,plain,
( ( sk1 @ c @ sk3 @ ( sk1 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1972:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 @ c @ sk3 ))]]) ).
thf(5369,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ sk3 @ ( sk1 @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1973,54]) ).
thf(5370,plain,
( ( sk1 @ c @ ( sk1 @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[5369:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 @ c @ sk3 ))]]) ).
thf(1992,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ c @ addition ) )
!= ( zero @ ( A @ addition ) ) )
| ( one = A ) ),
inference(paramod_ordered,[status(thm)],[1922,84]) ).
thf(2037,plain,
! [A: $i] :
( ( sk2 != zero )
| ( ( sk2 @ c )
!= A )
| ( one = A ) ),
inference(simp,[status(thm)],[1992]) ).
thf(2053,plain,
( ( sk2 != zero )
| ( ( sk2 @ c )
= one ) ),
inference(simp,[status(thm)],[2037]) ).
thf(16685,plain,
( ( ( sk2 @ c )
!= ( sk2 @ c ) )
| ( one @ test )
| ( sk2 != zero ) ),
inference(paramod_ordered,[status(thm)],[2053,599]) ).
thf(16686,plain,
( ( one @ test )
| ( sk2 != zero ) ),
inference(pattern_uni,[status(thm)],[16685:[]]) ).
thf(19741,plain,
! [A: $i] :
( ( ( A @ ( A @ sk3 @ complement ) )
!= ( one @ ( sk1 @ complement ) ) )
| ~ $true
| ~ ( A @ test ) ),
inference(paramod_ordered,[status(thm)],[46,19736]) ).
thf(19742,plain,
! [A: $i] :
( ( ( A @ ( A @ sk3 @ complement ) )
!= ( one @ ( sk1 @ complement ) ) )
| ~ ( A @ test ) ),
inference(simp,[status(thm)],[19741]) ).
thf(19784,plain,
! [A: $i] :
( ( A != one )
| ( ( A @ sk3 )
!= sk1 )
| ~ ( A @ test ) ),
inference(simp,[status(thm)],[19742]) ).
thf(19800,plain,
( ( ( one @ sk3 )
!= sk1 )
| ~ ( one @ test ) ),
inference(simp,[status(thm)],[19784]) ).
thf(24448,plain,
( ( ( one @ test )
!= ( one @ test ) )
| ( ( one @ sk3 )
!= sk1 )
| ~ $true
| ( sk2 != zero ) ),
inference(paramod_ordered,[status(thm)],[16686,19800]) ).
thf(24449,plain,
( ( ( one @ test )
!= ( one @ test ) )
| ( ( one @ sk3 )
!= sk1 )
| ( sk2 != zero ) ),
inference(simp,[status(thm)],[24448]) ).
thf(24450,plain,
( ( ( one @ sk3 )
!= sk1 )
| ( sk2 != zero ) ),
inference(pattern_uni,[status(thm)],[24449:[]]) ).
thf(7460,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[982,73]) ).
thf(7461,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[7460]) ).
thf(7462,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[7461:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c ))]]) ).
thf(10112,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7462,54]) ).
thf(10113,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[10112:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c ))]]) ).
thf(92,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(cnfConj,[status(thm)],[90]) ).
thf(94,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(lifteq,[status(thm)],[92]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ leq ) )
| ( ( B @ ( A @ addition ) )
!= B ) ),
inference(simp,[status(thm)],[94]) ).
thf(30777,plain,
! [B: $i,A: $i] :
( ( ( one @ ( sk2 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( B @ ( A @ leq ) )
| ( one != B ) ),
inference(paramod_ordered,[status(thm)],[30609,95]) ).
thf(30778,plain,
( ( one @ ( sk2 @ leq ) )
| ( one != one ) ),
inference(pattern_uni,[status(thm)],[30777:[bind(A,$thf( sk2 )),bind(B,$thf( one ))]]) ).
thf(30902,plain,
one @ ( sk2 @ leq ),
inference(simp,[status(thm)],[30778]) ).
thf(2913,plain,
( ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= ( sk1 @ c @ ( sk1 @ addition ) ) )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[2151,219]) ).
thf(2914,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= ( sk1 @ c @ ( sk1 @ addition ) ) ),
inference(simp,[status(thm)],[2913]) ).
thf(2940,plain,
( ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) )
!= ( sk1 @ c ) )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[2914]) ).
thf(2954,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) )
!= ( sk1 @ c ) ),
inference(simp,[status(thm)],[2940]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
thf(85,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(1065,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[607,71]) ).
thf(1066,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1065]) ).
thf(1067,plain,
( ( sk2 @ c @ sk3 @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1066:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ sk3 ))]]) ).
thf(184,plain,
! [A: $i] :
( ( ( zero @ ( A @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( A @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[84,24]) ).
thf(188,plain,
! [A: $i] :
( ( sk2 != zero )
| ( A != sk1 )
| ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( A @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[184]) ).
thf(192,plain,
( ( sk2 != zero )
| ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk1 @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[188]) ).
thf(6285,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1012,147]) ).
thf(6286,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6285]) ).
thf(6287,plain,
! [A: $i] :
( ( A @ ( sk1 @ multiplication ) @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6286:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 )),bind(C,$thf( C ))]]) ).
thf(6509,plain,
! [A: $i] :
( ( A @ ( sk1 @ multiplication ) @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6287]) ).
thf(7430,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[884,72]) ).
thf(7431,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7430]) ).
thf(7432,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7431:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c @ c @ sk3 ))]]) ).
thf(1342,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[439,72]) ).
thf(1343,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1342]) ).
thf(1344,plain,
( ( sk2 @ ( sk2 @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1343:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ sk3 ))]]) ).
thf(6397,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1344,147]) ).
thf(6398,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk2 @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6397]) ).
thf(6399,plain,
! [A: $i] :
( ( A @ ( sk2 @ multiplication ) @ ( sk2 @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6398:[bind(A,$thf( sk2 @ sk3 )),bind(B,$thf( sk2 )),bind(C,$thf( C ))]]) ).
thf(6556,plain,
! [A: $i] :
( ( A @ ( sk2 @ multiplication ) @ ( sk2 @ sk3 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6399]) ).
thf(2246,plain,
! [A: $i] :
( ( ( sk1 @ sk3 @ ( sk1 @ addition ) )
!= ( A @ ( A @ addition ) ) )
| ( one = A ) ),
inference(paramod_ordered,[status(thm)],[1980,51]) ).
thf(2250,plain,
! [A: $i] :
( ( ( sk1 @ sk3 )
!= A )
| ( sk1 != A )
| ( one = A ) ),
inference(simp,[status(thm)],[2246]) ).
thf(2262,plain,
( ( ( sk1 @ sk3 )
!= sk1 )
| ( sk1 = one ) ),
inference(simp,[status(thm)],[2250]) ).
thf(31221,plain,
( ( sk1 @ sk3 )
!= sk1 ),
inference(simplifyReflect,[status(thm)],[2262,31207]) ).
thf(7501,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[982,72]) ).
thf(7502,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7501]) ).
thf(7503,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7502:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c ))]]) ).
thf(2227,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ sk3 @ ( sk1 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1980,54]) ).
thf(2228,plain,
( ( sk1 @ ( sk1 @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[2227:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk3 ))]]) ).
thf(17885,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7536,72]) ).
thf(17886,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17885]) ).
thf(17887,plain,
( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17886:[bind(A,$thf( sk1 @ c @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c ))]]) ).
thf(1981,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[607,73]) ).
thf(1982,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1981]) ).
thf(1983,plain,
( ( sk2 @ c @ sk3 @ ( sk2 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1982:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ sk3 ))]]) ).
thf(1062,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[442,71]) ).
thf(1063,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1062]) ).
thf(1064,plain,
( ( sk1 @ sk3 @ ( sk1 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1063:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk3 ))]]) ).
thf(17548,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7296,48]) ).
thf(17549,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[17548]) ).
thf(17550,plain,
sk2 @ c @ c @ c @ c @ test,
inference(pattern_uni,[status(thm)],[17549:[bind(A,$thf( sk2 @ c @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c ))]]) ).
thf(1398,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[442,72]) ).
thf(1399,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1398]) ).
thf(1400,plain,
( ( sk1 @ ( sk1 @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1399:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk3 ))]]) ).
thf(6433,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1400,147]) ).
thf(6434,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk1 @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6433]) ).
thf(6435,plain,
! [A: $i] :
( ( A @ ( sk1 @ multiplication ) @ ( sk1 @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6434:[bind(A,$thf( sk1 @ sk3 )),bind(B,$thf( sk1 )),bind(C,$thf( C ))]]) ).
thf(6518,plain,
! [A: $i] :
( ( A @ ( sk1 @ multiplication ) @ ( sk1 @ sk3 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6435]) ).
thf(1137,plain,
! [A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( sk2 @ ( sk2 @ c @ multiplication ) ) )
| ( A = zero ) ),
inference(paramod_ordered,[status(thm)],[42,1015]) ).
thf(1171,plain,
! [A: $i] :
( ( A != sk2 )
| ( ( sk2 @ c )
!= one )
| ( A = zero ) ),
inference(simp,[status(thm)],[1137]) ).
thf(1182,plain,
( ( ( sk2 @ c )
!= one )
| ( sk2 = zero ) ),
inference(simp,[status(thm)],[1171]) ).
thf(1322,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[590,72]) ).
thf(1323,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1322]) ).
thf(1324,plain,
( ( sk2 @ c @ ( sk2 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1323:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 ))]]) ).
thf(983,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[930,46]) ).
thf(984,plain,
! [A: $i] :
( ( ( sk1 @ c @ c @ test )
!= ( A @ test ) )
| ( A @ ( A @ sk3 @ complement ) ) ),
inference(simp,[status(thm)],[983]) ).
thf(985,plain,
sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ),
inference(pattern_uni,[status(thm)],[984:[bind(A,$thf( sk1 @ c @ c ))]]) ).
thf(7219,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[881,73]) ).
thf(7220,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[7219]) ).
thf(7221,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[7220:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c ))]]) ).
thf(7585,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[985,71]) ).
thf(7586,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7585]) ).
thf(7587,plain,
( ( sk1 @ c @ c @ sk3 @ ( sk1 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7586:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c @ c @ sk3 ))]]) ).
thf(133,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[30,24]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( sk2 @ c ) )
| ( ( B @ ( A @ multiplication ) )
!= ( sk1 @ c ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[133]) ).
thf(151,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= ( sk1 @ c ) )
| ( ( sk2 @ c @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[141]) ).
thf(7702,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= ( sk1 @ c ) )
| ( ( sk2 @ c @ ( B @ multiplication ) @ ( A @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[151,33]) ).
thf(17414,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7293,71]) ).
thf(17415,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17414]) ).
thf(17416,plain,
( ( sk2 @ c @ c @ c @ sk3 @ ( sk2 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17415:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c @ sk3 ))]]) ).
thf(1797,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[620,72]) ).
thf(1798,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1797]) ).
thf(1799,plain,
( ( sk1 @ c @ ( sk1 @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1798:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 @ c @ sk3 ))]]) ).
thf(6294,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ sk3 @ ( sk1 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1064,147]) ).
thf(6295,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ sk3 @ ( sk1 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6294]) ).
thf(6296,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk3 @ multiplication ) @ ( sk1 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6295:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ sk3 )),bind(C,$thf( C ))]]) ).
thf(6514,plain,
! [A: $i] :
( ( A @ ( sk1 @ sk3 @ multiplication ) @ ( sk1 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6296]) ).
thf(241,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ addition ) @ addition ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ) )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[33,219]) ).
thf(254,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) ) )
| ( ( B @ ( C @ addition ) )
!= sk1 )
| ( ( A @ ( B @ addition ) @ ( C @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[241]) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ addition ) )
!= sk1 )
| ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( A @ addition ) @ ( B @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[254]) ).
thf(1956,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[604,73]) ).
thf(1957,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[1956]) ).
thf(1958,plain,
( ( sk2 @ c @ ( sk2 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[1957:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c ))]]) ).
thf(5089,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1958,54]) ).
thf(5090,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[5089:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c ))]]) ).
thf(5832,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ sk3 @ ( sk2 @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[1983,54]) ).
thf(5833,plain,
( ( sk2 @ c @ ( sk2 @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[5832:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ sk3 ))]]) ).
thf(6,axiom,
! [A: $i] :
( ~ ( A @ test )
=> ( ( A @ c )
= zero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',test_4) ).
thf(34,plain,
! [A: $i] :
( ~ ( A @ test )
=> ( ( A @ c )
= zero ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(129,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( D @ ( one @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[30,42]) ).
thf(139,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ multiplication ) )
!= one )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= D ) ),
inference(simp,[status(thm)],[129]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ multiplication ) )
!= one )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= C ) ),
inference(simp,[status(thm)],[139]) ).
thf(1387,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[617,72]) ).
thf(1388,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1387]) ).
thf(1389,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1388:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c ))]]) ).
thf(7578,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[985,73]) ).
thf(7579,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[7578]) ).
thf(7580,plain,
( ( sk1 @ c @ c @ sk3 @ ( sk1 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[7579:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c @ c @ sk3 ))]]) ).
thf(10882,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ sk3 @ ( sk1 @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7580,54]) ).
thf(10883,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[10882:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c @ c @ sk3 ))]]) ).
thf(1200,plain,
! [A: $i] :
( ( ( sk2 @ sk3 @ ( sk2 @ multiplication ) )
!= ( one @ ( A @ multiplication ) ) )
| ( zero = A ) ),
inference(paramod_ordered,[status(thm)],[1029,78]) ).
thf(1229,plain,
! [A: $i] :
( ( ( sk2 @ sk3 )
!= one )
| ( sk2 != A )
| ( zero = A ) ),
inference(simp,[status(thm)],[1200]) ).
thf(1239,plain,
( ( ( sk2 @ sk3 )
!= one )
| ( sk2 = zero ) ),
inference(simp,[status(thm)],[1229]) ).
thf(3701,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[444,95]) ).
thf(3702,plain,
! [A: $i] :
( ( A @ ( zero @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[3701:[bind(A,$thf( A )),bind(B,$thf( zero )),bind(C,$thf( A ))]]) ).
thf(3719,plain,
! [A: $i] : ( A @ ( zero @ leq ) ),
inference(simp,[status(thm)],[3702]) ).
thf(2080,plain,
! [A: $i] :
( ( ( A @ ( zero @ addition ) )
!= ( sk2 @ sk3 @ ( sk2 @ addition ) ) )
| ( A = one ) ),
inference(paramod_ordered,[status(thm)],[444,1928]) ).
thf(2103,plain,
! [A: $i] :
( ( A
!= ( sk2 @ sk3 ) )
| ( sk2 != zero )
| ( A = one ) ),
inference(simp,[status(thm)],[2080]) ).
thf(2116,plain,
( ( sk2 != zero )
| ( ( sk2 @ sk3 )
= one ) ),
inference(simp,[status(thm)],[2103]) ).
thf(38,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[37]) ).
thf(39,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ addition ) @ multiplication ) )
= ( C @ ( B @ multiplication ) @ ( C @ ( A @ multiplication ) @ addition ) ) ),
inference(lifteq,[status(thm)],[38]) ).
thf(7468,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[982,71]) ).
thf(7469,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7468]) ).
thf(7470,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7469:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c ))]]) ).
thf(30334,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( one @ ( A @ addition ) )
= ( B @ ( A @ addition ) ) ) ),
inference(paramod_ordered,[status(thm)],[2151,277]) ).
thf(30335,plain,
( ( sk1 @ c @ ( sk1 @ addition ) )
= ( one @ ( sk1 @ addition ) ) ),
inference(pattern_uni,[status(thm)],[30334:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ c ))]]) ).
thf(31866,plain,
( ( one @ ( sk1 @ addition ) )
= one ),
inference(rewrite,[status(thm)],[30335,2151]) ).
thf(1138,plain,
! [A: $i] :
( ( ( sk2 @ ( sk2 @ c @ multiplication ) )
!= ( one @ ( A @ multiplication ) ) )
| ( zero = A ) ),
inference(paramod_ordered,[status(thm)],[1015,78]) ).
thf(1174,plain,
! [A: $i] :
( ( sk2 != one )
| ( ( sk2 @ c )
!= A )
| ( zero = A ) ),
inference(simp,[status(thm)],[1138]) ).
thf(1185,plain,
( ( sk2 != one )
| ( ( sk2 @ c )
= zero ) ),
inference(simp,[status(thm)],[1174]) ).
thf(3106,plain,
( ( ( sk2 @ c )
!= ( sk2 @ c ) )
| ( zero != zero )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk2 != one ) ),
inference(paramod_ordered,[status(thm)],[1185,180]) ).
thf(3107,plain,
( ( ( sk2 @ c )
!= ( sk2 @ c ) )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk2 != one ) ),
inference(simp,[status(thm)],[3106]) ).
thf(3108,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= one )
| ( sk2 != one ) ),
inference(pattern_uni,[status(thm)],[3107:[]]) ).
thf(31885,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= ( one @ ( sk1 @ addition ) ) )
| ( one != one )
| ( sk2 != one ) ),
inference(paramod_ordered,[status(thm)],[31866,3108]) ).
thf(31886,plain,
( ( ( sk2 @ ( sk1 @ addition ) )
!= ( one @ ( sk1 @ addition ) ) )
| ( sk2 != one ) ),
inference(simp,[status(thm)],[31885]) ).
thf(32099,plain,
( ( sk2 != one )
| ( sk1 != sk1 )
| ( sk2 != one ) ),
inference(simp,[status(thm)],[31886]) ).
thf(32145,plain,
sk2 != one,
inference(simp,[status(thm)],[32099]) ).
thf(17723,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7533,71]) ).
thf(17724,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17723]) ).
thf(17725,plain,
( ( sk1 @ c @ c @ c @ sk3 @ ( sk1 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17724:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c @ sk3 ))]]) ).
thf(2199,plain,
! [A: $i] :
( ( ( sk1 @ sk3 @ ( sk1 @ addition ) )
!= ( zero @ ( A @ addition ) ) )
| ( one = A ) ),
inference(paramod_ordered,[status(thm)],[1980,84]) ).
thf(2248,plain,
! [A: $i] :
( ( ( sk1 @ sk3 )
!= zero )
| ( sk1 != A )
| ( one = A ) ),
inference(simp,[status(thm)],[2199]) ).
thf(2260,plain,
( ( ( sk1 @ sk3 )
!= zero )
| ( sk1 = one ) ),
inference(simp,[status(thm)],[2248]) ).
thf(31218,plain,
( ( sk1 @ sk3 )
!= zero ),
inference(simplifyReflect,[status(thm)],[2260,31207]) ).
thf(185,plain,
! [A: $i] :
( ( ( zero @ ( A @ addition ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ ( sk1 @ addition ) @ addition ) ) )
| ( A != one ) ),
inference(paramod_ordered,[status(thm)],[84,24]) ).
thf(187,plain,
( ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) )
!= zero )
| ( ( sk2 @ ( sk1 @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[185]) ).
thf(6276,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ sk3 @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1067,147]) ).
thf(6277,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ sk3 @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6276]) ).
thf(6278,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ sk3 @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6277:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ sk3 )),bind(C,$thf( C ))]]) ).
thf(6504,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ sk3 @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6278]) ).
thf(18244,plain,
( ( ( sk2 @ c )
!= ( sk1 @ c ) )
| ( one != one )
| ( sk2 != zero ) ),
inference(paramod_ordered,[status(thm)],[2053,18235]) ).
thf(18245,plain,
( ( ( sk2 @ c )
!= ( sk1 @ c ) )
| ( sk2 != zero ) ),
inference(simp,[status(thm)],[18244]) ).
thf(18254,plain,
( ( sk2 != sk1 )
| ( sk2 != zero ) ),
inference(simp,[status(thm)],[18245]) ).
thf(2005,plain,
( ( ( sk2 @ ( sk2 @ c @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[1922,180]) ).
thf(2006,plain,
( ( ( sk2 @ ( sk2 @ c @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2005]) ).
thf(2039,plain,
( ( sk2 != sk2 )
| ( ( sk2 @ c )
!= sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2006]) ).
thf(2054,plain,
( ( ( sk2 @ c )
!= sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2039]) ).
thf(2568,plain,
( ( ( sk2 @ ( sk2 @ sk3 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[2082,180]) ).
thf(2569,plain,
( ( ( sk2 @ ( sk2 @ sk3 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2568]) ).
thf(2603,plain,
( ( sk2 != sk2 )
| ( ( sk2 @ sk3 )
!= sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2569]) ).
thf(2614,plain,
( ( ( sk2 @ sk3 )
!= sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2603]) ).
thf(6303,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1324,147]) ).
thf(6304,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ ( sk2 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6303]) ).
thf(6305,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ multiplication ) @ ( sk2 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6304:[bind(A,$thf( sk2 )),bind(B,$thf( sk2 @ c )),bind(C,$thf( C ))]]) ).
thf(6517,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ multiplication ) @ ( sk2 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6305]) ).
thf(17766,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7533,72]) ).
thf(17767,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17766]) ).
thf(17768,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17767:[bind(A,$thf( sk1 @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c @ sk3 ))]]) ).
thf(127,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ multiplication ) @ multiplication ) )
!= ( E @ ( D @ multiplication ) ) )
| ( ( F @ ( C @ ( B @ multiplication ) @ ( A @ multiplication ) @ multiplication ) )
= ( F @ ( E @ multiplication ) @ ( D @ multiplication ) ) ) ),
inference(paramod_ordered,[status(thm)],[30,30]) ).
thf(128,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ ( C @ multiplication ) @ multiplication ) ) ),
inference(pattern_uni,[status(thm)],[127:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ multiplication ) )),bind(E,$thf( C ))]]) ).
thf(143,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ ( C @ multiplication ) @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ ( C @ multiplication ) @ multiplication ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(5446,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ multiplication ) @ multiplication ) @ ( C @ multiplication ) )
= ( B @ ( A @ multiplication ) @ ( D @ multiplication ) @ ( C @ multiplication ) ) ),
inference(rewrite,[status(thm)],[143,30]) ).
thf(1959,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ) )
| ( one != one )
| ~ ( A @ ( B @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[73,219]) ).
thf(1960,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ) )
| ~ ( A @ ( B @ complement ) ) ),
inference(simp,[status(thm)],[1959]) ).
thf(1961,plain,
~ ( sk1 @ ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ complement ) ),
inference(pattern_uni,[status(thm)],[1960:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) ))]]) ).
thf(8700,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7221,54]) ).
thf(8701,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[8700:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c ))]]) ).
thf(1366,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[604,72]) ).
thf(1367,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1366]) ).
thf(1368,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1367:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c ))]]) ).
thf(7616,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[985,72]) ).
thf(7617,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7616]) ).
thf(7618,plain,
( ( sk1 @ c @ c @ ( sk1 @ c @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7617:[bind(A,$thf( sk1 @ c @ c )),bind(B,$thf( sk1 @ c @ c @ sk3 ))]]) ).
thf(7262,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[881,72]) ).
thf(7263,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7262]) ).
thf(7264,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7263:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c ))]]) ).
thf(166,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) ) )
| ( ( A @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(paramod_ordered,[status(thm)],[78,24]) ).
thf(173,plain,
! [A: $i] :
( ( ( sk2 @ c )
!= one )
| ( A
!= ( sk1 @ c ) )
| ( ( A @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[166]) ).
thf(178,plain,
( ( ( sk2 @ c )
!= one )
| ( ( sk1 @ c @ ( sk2 @ ( sk1 @ addition ) @ addition ) )
!= one ) ),
inference(simp,[status(thm)],[173]) ).
thf(12124,plain,
( ( ( sk2 @ c )
!= one )
| ( ( sk1 @ c @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= one ) ),
inference(rewrite,[status(thm)],[178,33]) ).
thf(1036,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[604,71]) ).
thf(1037,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1036]) ).
thf(1038,plain,
( ( sk2 @ c @ ( sk2 @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1037:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c ))]]) ).
thf(3713,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( C @ ( B @ addition ) ) )
| ( C @ ( B @ leq ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[51,95]) ).
thf(3714,plain,
! [A: $i] :
( ( A @ ( A @ leq ) )
| ( A != A ) ),
inference(pattern_uni,[status(thm)],[3713:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(3715,plain,
! [A: $i] : ( A @ ( A @ leq ) ),
inference(simp,[status(thm)],[3714]) ).
thf(19753,plain,
( ( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( one @ ( sk1 @ complement ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[590,19736]) ).
thf(19754,plain,
( ( sk2 @ c @ ( sk2 @ complement ) )
!= ( one @ ( sk1 @ complement ) ) ),
inference(simp,[status(thm)],[19753]) ).
thf(19788,plain,
( ( ( sk2 @ c )
!= one )
| ( sk2 != sk1 ) ),
inference(simp,[status(thm)],[19754]) ).
thf(1351,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[593,72]) ).
thf(1352,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( A @ ( B @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[1351]) ).
thf(1353,plain,
( ( sk1 @ c @ ( sk1 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[1352:[bind(A,$thf( sk1 @ c )),bind(B,$thf( sk1 ))]]) ).
thf(6469,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1353,147]) ).
thf(6470,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6469]) ).
thf(6471,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6470:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 @ c )),bind(C,$thf( C ))]]) ).
thf(6526,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6471]) ).
thf(113,plain,
! [B: $i,A: $i] :
( ( ( A @ ( one @ multiplication ) )
!= ( B @ ( zero @ multiplication ) ) )
| ( A = zero ) ),
inference(paramod_ordered,[status(thm)],[42,27]) ).
thf(115,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( zero != one )
| ( A = zero ) ),
inference(simp,[status(thm)],[113]) ).
thf(118,plain,
! [A: $i] :
( ( zero != one )
| ( A = zero ) ),
inference(simp,[status(thm)],[115]) ).
thf(4200,plain,
! [A: $i] :
( ( A
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ) )
| ( zero != one )
| ( zero != one ) ),
inference(paramod_ordered,[status(thm)],[118,219]) ).
thf(4201,plain,
! [A: $i] :
( ( A
!= ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ) )
| ( zero != one ) ),
inference(simp,[status(thm)],[4200]) ).
thf(4202,plain,
zero != one,
inference(pattern_uni,[status(thm)],[4201:[bind(A,$thf( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) ))]]) ).
thf(7390,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[884,73]) ).
thf(7391,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ addition ) )
= one ) ),
inference(simp,[status(thm)],[7390]) ).
thf(7392,plain,
( ( sk2 @ c @ c @ sk3 @ ( sk2 @ c @ c @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[7391:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c @ c @ sk3 ))]]) ).
thf(9441,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ sk3 @ ( sk2 @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[7392,54]) ).
thf(9442,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[9441:[bind(A,$thf( sk2 @ c @ c )),bind(B,$thf( sk2 @ c @ c @ sk3 ))]]) ).
thf(2235,plain,
( ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= ( sk1 @ sk3 @ ( sk1 @ addition ) ) )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[1980,219]) ).
thf(2236,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) @ ( sk1 @ addition ) )
!= ( sk1 @ sk3 @ ( sk1 @ addition ) ) ),
inference(simp,[status(thm)],[2235]) ).
thf(2255,plain,
( ( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) )
!= ( sk1 @ sk3 ) )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[2236]) ).
thf(2266,plain,
( ( sk2 @ c @ ( sk1 @ c @ multiplication ) @ ( sk2 @ addition ) )
!= ( sk1 @ sk3 ) ),
inference(simp,[status(thm)],[2255]) ).
thf(1938,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( one != one )
| ~ ( A @ ( B @ complement ) ) ),
inference(paramod_ordered,[status(thm)],[73,180]) ).
thf(1939,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ~ ( A @ ( B @ complement ) ) ),
inference(simp,[status(thm)],[1938]) ).
thf(1940,plain,
( ( ( sk2 @ c )
!= zero )
| ~ ( sk1 @ ( sk2 @ complement ) ) ),
inference(pattern_uni,[status(thm)],[1939:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(86,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(cnf,[status(esa)],[85]) ).
thf(87,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ addition ) @ ( A @ multiplication ) )
= ( C @ ( A @ multiplication ) @ ( B @ ( A @ multiplication ) @ addition ) ) ),
inference(lifteq,[status(thm)],[86]) ).
thf(17541,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7296,71]) ).
thf(17542,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ c @ ( sk2 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17541]) ).
thf(17543,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17542:[bind(A,$thf( sk2 @ c @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c ))]]) ).
thf(17840,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[7536,71]) ).
thf(17841,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[17840]) ).
thf(17842,plain,
( ( sk1 @ c @ c @ c @ ( sk1 @ c @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[17841:[bind(A,$thf( sk1 @ c @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c ))]]) ).
thf(2929,plain,
! [A: $i] :
( ( ( A @ ( A @ addition ) )
!= ( sk1 @ c @ ( sk1 @ addition ) ) )
| ( A = one ) ),
inference(paramod_ordered,[status(thm)],[51,2151]) ).
thf(2930,plain,
! [A: $i] :
( ( A
!= ( sk1 @ c ) )
| ( A != sk1 )
| ( A = one ) ),
inference(simp,[status(thm)],[2929]) ).
thf(2945,plain,
( ( ( sk1 @ c )
!= sk1 )
| ( sk1 = one ) ),
inference(simp,[status(thm)],[2930]) ).
thf(31219,plain,
( ( sk1 @ c )
!= sk1 ),
inference(simplifyReflect,[status(thm)],[2945,31207]) ).
thf(6321,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1799,147]) ).
thf(6322,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ c @ ( sk1 @ c @ sk3 @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6321]) ).
thf(6323,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ c @ sk3 @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6322:[bind(A,$thf( sk1 @ c @ sk3 )),bind(B,$thf( sk1 @ c )),bind(C,$thf( C ))]]) ).
thf(6521,plain,
! [A: $i] :
( ( A @ ( sk1 @ c @ multiplication ) @ ( sk1 @ c @ sk3 @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6323]) ).
thf(18849,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ sk3 @ ( sk2 @ c @ c @ c @ addition ) )
!= ( B @ ( A @ addition ) ) )
| ( ( A @ ( B @ addition ) )
= one ) ),
inference(paramod_ordered,[status(thm)],[17404,54]) ).
thf(18850,plain,
( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ c @ sk3 @ addition ) )
= one ),
inference(pattern_uni,[status(thm)],[18849:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c @ c @ sk3 ))]]) ).
thf(70,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ complement ) )
| ( ( B @ ( A @ addition ) )
!= one )
| ( ( A @ ( B @ multiplication ) )
!= zero )
| ( ( B @ ( A @ multiplication ) )
!= zero ) ),
inference(cnfConj,[status(thm)],[66]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ complement ) )
| ( ( B @ ( A @ addition ) )
!= one )
| ( ( A @ ( B @ multiplication ) )
!= zero )
| ( ( B @ ( A @ multiplication ) )
!= zero ) ),
inference(lifteq,[status(thm)],[70]) ).
thf(75,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ complement ) )
| ( ( B @ ( A @ addition ) )
!= one )
| ( ( A @ ( B @ multiplication ) )
!= zero )
| ( ( B @ ( A @ multiplication ) )
!= zero ) ),
inference(simp,[status(thm)],[74]) ).
thf(2901,plain,
( ( ( sk1 @ c @ ( sk1 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero )
| ( one != one ) ),
inference(paramod_ordered,[status(thm)],[2151,180]) ).
thf(2902,plain,
( ( ( sk1 @ c @ ( sk1 @ addition ) )
!= ( sk2 @ ( sk1 @ addition ) ) )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2901]) ).
thf(2942,plain,
( ( ( sk1 @ c )
!= sk2 )
| ( sk1 != sk1 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2902]) ).
thf(2956,plain,
( ( ( sk1 @ c )
!= sk2 )
| ( ( sk2 @ c )
!= zero ) ),
inference(simp,[status(thm)],[2942]) ).
thf(1258,plain,
! [A: $i] :
( ( ( one @ ( A @ multiplication ) )
!= ( sk1 @ sk3 @ ( sk1 @ multiplication ) ) )
| ( A = zero ) ),
inference(paramod_ordered,[status(thm)],[78,1064]) ).
thf(1293,plain,
! [A: $i] :
( ( ( sk1 @ sk3 )
!= one )
| ( A != sk1 )
| ( A = zero ) ),
inference(simp,[status(thm)],[1258]) ).
thf(1302,plain,
( ( ( sk1 @ sk3 )
!= one )
| ( sk1 = zero ) ),
inference(simp,[status(thm)],[1293]) ).
thf(19805,plain,
( ( sk1 @ sk3 )
!= one ),
inference(simplifyReflect,[status(thm)],[1302,19804]) ).
thf(35,plain,
! [A: $i] :
( ( ( A @ c )
= zero )
| ( A @ test ) ),
inference(cnf,[status(esa)],[34]) ).
thf(36,plain,
! [A: $i] :
( ( A @ test )
| ( ( A @ c )
= zero ) ),
inference(lifteq,[status(thm)],[35]) ).
thf(7229,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ~ $true
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[881,71]) ).
thf(7230,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ c @ c @ c @ ( sk2 @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( ( B @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[7229]) ).
thf(7231,plain,
( ( sk2 @ c @ c @ ( sk2 @ c @ c @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[7230:[bind(A,$thf( sk2 @ c @ c @ c )),bind(B,$thf( sk2 @ c @ c ))]]) ).
thf(6442,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( zero != zero )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(paramod_ordered,[status(thm)],[1368,147]) ).
thf(6443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ c @ c @ ( sk2 @ c @ multiplication ) )
!= ( B @ ( A @ multiplication ) ) )
| ( ( C @ ( B @ multiplication ) @ ( A @ multiplication ) )
= zero ) ),
inference(simp,[status(thm)],[6442]) ).
thf(6444,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ c @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(pattern_uni,[status(thm)],[6443:[bind(A,$thf( sk2 @ c )),bind(B,$thf( sk2 @ c @ c )),bind(C,$thf( C ))]]) ).
thf(6520,plain,
! [A: $i] :
( ( A @ ( sk2 @ c @ c @ multiplication ) @ ( sk2 @ c @ multiplication ) )
= zero ),
inference(simp,[status(thm)],[6444]) ).
thf(17847,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[7536,48]) ).
thf(17848,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ c @ c @ c @ c @ ( sk1 @ c @ c @ c @ complement ) )
!= ( A @ ( B @ complement ) ) )
| ( A @ test ) ),
inference(simp,[status(thm)],[17847]) ).
thf(17849,plain,
sk1 @ c @ c @ c @ c @ test,
inference(pattern_uni,[status(thm)],[17848:[bind(A,$thf( sk1 @ c @ c @ c @ c )),bind(B,$thf( sk1 @ c @ c @ c ))]]) ).
thf(39568,plain,
$false,
inference(e,[status(thm)],[17404,2263,234,21326,88,18272,19804,31207,17715,6522,6505,930,31220,5227,42,2010,2082,37,25,52,6552,7401,22777,6519,1922,853,20276,93,881,17588,289,261,7236,19736,46,78,17459,6523,84,147,1928,61,5370,24450,10113,30902,2954,7533,439,85,1067,28,192,21,6509,33,7432,6556,31221,7503,2228,1968,17887,19800,1012,1983,1064,17550,593,884,6518,1182,17531,2053,1937,590,7293,1324,1776,985,7221,7587,7702,17416,1799,6514,73,266,5090,5833,34,148,64,180,444,1403,27,22,1389,71,10883,54,1239,49,7536,3719,604,219,2151,81,18235,76,2116,39,7470,32145,599,17725,31218,187,16686,1029,1344,30609,1015,6504,18254,1973,2054,2614,7296,1958,617,6517,17768,5446,48,1961,1400,95,8701,1368,7462,7618,63,7475,1053,7264,12124,1038,17832,1980,3715,31,19788,7580,6526,1353,72,612,4202,9442,43,2266,1940,31866,87,17543,17842,40,30748,31219,55,6521,18850,82,75,2956,19805,620,36,7231,30,51,19,79,6520,982,277,442,17849,7392,607]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE013+1 : TPTP v9.3.1. Released v4.0.0.
% 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.23/0.47 % Computer : n011.cluster.edu
% 0.23/0.47 % Model : x86_64 x86_64
% 0.23/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.47 % Memory : 8046.5625MB
% 0.23/0.47 % OS : Linux 6.8.0-71-generic
% 0.23/0.47 % CPULimit : 300
% 0.23/0.48 % WCLimit : 300
% 0.23/0.48 % DateTime : Fri Sep 25 19:13:00 UTC 2026
% 0.23/0.48 % CPUTime :
% 0.23/0.48 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.59/1.40 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.16/1.73 % [INFO] Parsing done (325ms).
% 2.16/1.75 % [INFO] Running in sequential loop mode.
% 3.50/2.40 % [INFO] eprover registered as external prover.
% 3.50/2.41 % [INFO] Scanning for conjecture ...
% 3.68/2.57 % [INFO] Found a conjecture (or negated_conjecture) and 16 axioms. Running axiom selection ...
% 3.87/2.68 % [INFO] Axiom selection finished. Selected 16 axioms (removed 0 axioms).
% 4.07/2.73 % [INFO] Problem is first-order (TPTP FOF).
% 4.07/2.74 % [INFO] Type checking passed.
% 4.07/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 ...
% 105.72/21.97 % External prover 'e' found a proof!
% 105.72/21.97 % [INFO] Killing All external provers ...
% 105.72/21.97 % Time passed: 21254ms (effective reasoning time: 20204ms)
% 105.72/21.97 % Solved by 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)>
% 105.72/21.97 % Axioms used in derivation (16): additive_identity, test_3, test_4, left_annihilation, right_distributivity, multiplicative_right_identity, test_1, right_annihilation, additive_idempotence, additive_associativity, order, additive_commutativity, test_2, multiplicative_left_identity, multiplicative_associativity, left_distributivity
% 105.72/21.97 % No. of inferences in proof: 590
% 105.72/21.97 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 21254 ms resp. 20204 ms w/o parsing
% 108.95/22.34 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 108.95/22.35 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------