%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO500_8.002 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n013.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 09:44:48 AM UTC 2026
% Result : Theorem 52.63s 14.89s
% Output : Refutation 53.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 1
% Syntax : Number of formulae : 595 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 8683 ( 643 equ; 0 cnn)
% Maximal formula atoms : 23 ( 14 avg)
% Number of connectives : 8191 (1389 ~;1748 |; 0 &;5054 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 6 ( 3 usr; 3 con; 0-2 aty)
% Number of variables : 0 ( 0 ^; 0 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
thf(x_decl,type,
x: $o ).
thf(f0_decl,type,
f0: $o > $o ).
thf(f1_decl,type,
f1: $o > $o ).
thf(1,conjecture,
( ( x @ f1 @ f0 @ f0 @ f0 )
= ( x @ f1 @ f1 @ f1 @ f0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kaminski2) ).
thf(2,negated_conjecture,
( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(3,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(4,plain,
( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(lifteq,[status(thm)],[3]) ).
thf(5,plain,
( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[4]) ).
thf(9,plain,
( ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f1 @ f1 ) ),
inference(bool_ext,[status(thm)],[5]) ).
thf(7,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f1 @ f1 @ f0 ) ),
inference(bool_ext,[status(thm)],[4]) ).
thf(59,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(60,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[59:[]]) ).
thf(492,plain,
( ~ $true
| ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[60]) ).
thf(506,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[492]) ).
thf(1692,plain,
( ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[506]) ).
thf(1743,plain,
( ( x @ f1 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[1692]) ).
thf(1817,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1743,1743]) ).
thf(1818,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1817]) ).
thf(1846,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1818]) ).
thf(1898,plain,
( ( x @ f1 )
| ( x @ f1 @ f0 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(bool_ext,[status(thm)],[1846]) ).
thf(1920,plain,
( ( x @ f1 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1898]) ).
thf(2163,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1920,60]) ).
thf(2164,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2163]) ).
thf(2165,plain,
( ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[2164:[]]) ).
thf(7627,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1920,2165]) ).
thf(7628,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[7627]) ).
thf(7629,plain,
( ( $true @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[7628:[]]) ).
thf(7987,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7629,1743]) ).
thf(7988,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[7987]) ).
thf(7989,plain,
( ( x @ f1 @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[7988:[]]) ).
thf(8264,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( $true @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 )
| ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7629,7989]) ).
thf(8265,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8264]) ).
thf(8266,plain,
( ( $true @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8265:[]]) ).
thf(8571,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,60]) ).
thf(8572,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8571]) ).
thf(8711,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8572]) ).
thf(6,plain,
( ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 ) ),
inference(bool_ext,[status(thm)],[4]) ).
thf(53,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,6]) ).
thf(69,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[53]) ).
thf(24,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,9]) ).
thf(25,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[24]) ).
thf(31,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[25]) ).
thf(93,plain,
( ( ( x @ f1 )
!= x )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[31]) ).
thf(137,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[93,6]) ).
thf(138,plain,
( ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(pattern_uni,[status(thm)],[137:[]]) ).
thf(95,plain,
( ( x @ f1 )
| ( x @ f1 @ f1 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[31]) ).
thf(887,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ( x @ f1 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[95,9]) ).
thf(888,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[887]) ).
thf(889,plain,
( ( x @ f1 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[888:[]]) ).
thf(2172,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 )
| ( $true @ f1 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1920,889]) ).
thf(2173,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f1 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2172]) ).
thf(2174,plain,
( ( $true @ f1 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[2173:[]]) ).
thf(2436,plain,
( ~ $true
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[2174]) ).
thf(2492,plain,
( ~ x
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2436]) ).
thf(2588,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 )
| ( $true @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2492,1920]) ).
thf(2589,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( x @ f1 )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2588]) ).
thf(2688,plain,
( ~ x
| ~ x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2589]) ).
thf(2795,plain,
( ~ x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2688]) ).
thf(2557,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2492,5]) ).
thf(2661,plain,
( ~ x
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2557]) ).
thf(2776,plain,
( ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2661]) ).
thf(3827,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2492,2776]) ).
thf(3828,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[3827]) ).
thf(3829,plain,
( ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[3828:[]]) ).
thf(3872,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ x
| ( $true @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2492,3829]) ).
thf(3873,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[3872]) ).
thf(3874,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[3873:[]]) ).
thf(3944,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ x
| ( $true @ f0 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1743,3874]) ).
thf(3945,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ x
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[3944]) ).
thf(3946,plain,
( ~ x
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[3945:[]]) ).
thf(4773,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( $true @ f0 )
| ( $true @ f0 )
| ~ x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2795,3946]) ).
thf(4774,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[4773]) ).
thf(4775,plain,
( ~ x
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[4774:[]]) ).
thf(4899,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,6]) ).
thf(4900,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4899]) ).
thf(5024,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4900]) ).
thf(7443,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ $true
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,5024]) ).
thf(7444,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[7443]) ).
thf(7445,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[7444:[]]) ).
thf(12,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,4]) ).
thf(13,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[12:[]]) ).
thf(79,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,13]) ).
thf(80,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[79]) ).
thf(88,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[80]) ).
thf(8565,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ $true
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,6]) ).
thf(8566,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8565]) ).
thf(8717,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8566]) ).
thf(48515,plain,
( ( $true @ f0 )
| ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(bool_ext,[status(thm)],[8717]) ).
thf(48857,plain,
( ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[48515]) ).
thf(48889,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ~ $true
| ( $true @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,48857]) ).
thf(48890,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[48889]) ).
thf(49841,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[48890]) ).
thf(56062,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1920,49841]) ).
thf(56063,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[56062]) ).
thf(56064,plain,
( ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[56063:[]]) ).
thf(58658,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[56064,1920]) ).
thf(58659,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[58658]) ).
thf(59212,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[58659]) ).
thf(60488,plain,
( x
| ( x @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(bool_ext,[status(thm)],[59212]) ).
thf(2208,plain,
( ~ $true
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[1920]) ).
thf(2212,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2208]) ).
thf(61124,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 )
| ( $true @ f0 )
| x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[60488,2212]) ).
thf(61125,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[61124]) ).
thf(61464,plain,
( ( ( x @ f1 )
!= x )
| x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[61125]) ).
thf(69585,plain,
( x
| ( x @ f1 )
| x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(bool_ext,[status(thm)],[61464]) ).
thf(69629,plain,
( x
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[69585]) ).
thf(86,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[80]) ).
thf(618,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,86]) ).
thf(619,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[618]) ).
thf(620,plain,
( ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[619:[]]) ).
thf(8,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 ) ),
inference(bool_ext,[status(thm)],[5]) ).
thf(705,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[620,8]) ).
thf(706,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[705]) ).
thf(707,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[706:[]]) ).
thf(814,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[707]) ).
thf(816,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[814]) ).
thf(8510,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 )
| ~ $true
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,816]) ).
thf(8511,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8510]) ).
thf(8512,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8511:[]]) ).
thf(9152,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,8512]) ).
thf(9153,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9152]) ).
thf(9154,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[9153:[]]) ).
thf(11301,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 )
!= x )
| ( $true @ f1 )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,9154]) ).
thf(11302,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 )
!= x )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11301]) ).
thf(11303,plain,
( ( ( $true @ f1 )
!= x )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[11302:[]]) ).
thf(11326,plain,
( x
| ( $true @ f1 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(bool_ext,[status(thm)],[11303]) ).
thf(11343,plain,
( x
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11326]) ).
thf(8622,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ $true
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,707]) ).
thf(8623,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8622]) ).
thf(8624,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8623:[]]) ).
thf(11500,plain,
( ( ( x @ f1 @ f1 )
!= ( $true @ f1 ) )
| ~ ( $true @ f1 )
| ~ ( x @ f1 )
| ( $true @ f0 )
| x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[11343,8624]) ).
thf(11501,plain,
( ( ( x @ f1 @ f1 )
!= ( $true @ f1 ) )
| ~ ( $true @ f1 )
| ~ ( x @ f1 )
| x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11500]) ).
thf(11751,plain,
( ~ ( x @ f1 )
| ~ ( $true @ f1 )
| ~ ( x @ f1 )
| x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11501]) ).
thf(11803,plain,
( ~ ( $true @ f1 )
| ~ ( x @ f1 )
| x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11751]) ).
thf(11971,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ~ $true
| ~ ( x @ f1 )
| x
| ( $true @ f0 )
| x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[11343,11803]) ).
thf(11972,plain,
( ( ( $true @ f1 )
!= ( $true @ f1 ) )
| ~ ( x @ f1 )
| x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11971]) ).
thf(11973,plain,
( ~ ( x @ f1 )
| x
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[11972:[]]) ).
thf(70179,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ $true
| x
| ( $true @ f0 )
| x
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[69629,11973]) ).
thf(70180,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| x
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[70179]) ).
thf(70181,plain,
( x
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[70180:[]]) ).
thf(81,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,13]) ).
thf(82,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[81]) ).
thf(89,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[82]) ).
thf(12398,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,89]) ).
thf(12399,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[12398]) ).
thf(12400,plain,
( ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[12399:[]]) ).
thf(41,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,6]) ).
thf(42,plain,
( ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[41:[]]) ).
thf(33549,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ $true
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[12400,42]) ).
thf(33550,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[33549]) ).
thf(33551,plain,
( ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[33550:[]]) ).
thf(34468,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,33551]) ).
thf(34469,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[34468]) ).
thf(34805,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[34469]) ).
thf(70896,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[70181,34805]) ).
thf(70897,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[70896]) ).
thf(70898,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[70897:[]]) ).
thf(75032,plain,
( x
| ( x @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(bool_ext,[status(thm)],[70898]) ).
thf(75120,plain,
( ( x @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[75032]) ).
thf(831,plain,
( x
| ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[816]) ).
thf(46597,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ ( $true @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[831,707]) ).
thf(46598,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ ( $true @ f1 )
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[46597]) ).
thf(46599,plain,
( ~ ( $true @ f1 )
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[46598:[]]) ).
thf(48170,plain,
( ( ( x @ f1 @ f1 )
!= ( $true @ f1 ) )
| ~ $true
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[831,46599]) ).
thf(48171,plain,
( ( ( x @ f1 @ f1 )
!= ( $true @ f1 ) )
| x
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[48170]) ).
thf(48242,plain,
( ~ ( x @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[48171]) ).
thf(48279,plain,
( ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[48242]) ).
thf(48360,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| x
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[33551,48279]) ).
thf(48361,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| x
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[48360]) ).
thf(48400,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[48361]) ).
thf(48437,plain,
( ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[48400]) ).
thf(53566,plain,
( ~ $true
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| x ),
inference(eqfactor_ordered,[status(thm)],[48437]) ).
thf(53600,plain,
( ~ ( x @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| x ),
inference(simp,[status(thm)],[53566]) ).
thf(53611,plain,
( ~ ( x @ f1 )
| ~ ( $true @ f0 )
| x ),
inference(simp,[status(thm)],[53600]) ).
thf(70899,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ $true
| x
| x ),
inference(paramod_ordered,[status(thm)],[70181,53611]) ).
thf(70900,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| x ),
inference(simp,[status(thm)],[70899]) ).
thf(70901,plain,
( ~ ( x @ f1 )
| x ),
inference(pattern_uni,[status(thm)],[70900:[]]) ).
thf(75298,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| x
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[75120,70901]) ).
thf(75299,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[75298]) ).
thf(76061,plain,
( ( ( x @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[75299]) ).
thf(79428,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| x ),
inference(paramod_ordered,[status(thm)],[76061,8]) ).
thf(79429,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| x ),
inference(simp,[status(thm)],[79428]) ).
thf(79430,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| x ),
inference(pattern_uni,[status(thm)],[79429:[]]) ).
thf(8628,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,620]) ).
thf(8629,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8628]) ).
thf(8630,plain,
( ~ ( x @ f1 )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8629:[]]) ).
thf(9277,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,8630]) ).
thf(9278,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9277]) ).
thf(9279,plain,
( ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[9278:[]]) ).
thf(10047,plain,
( ~ $true
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[9279]) ).
thf(10163,plain,
( ~ ( x @ f1 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[10047]) ).
thf(9446,plain,
( ~ $true
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[8630]) ).
thf(9545,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9446]) ).
thf(17160,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[10163,9545]) ).
thf(17161,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[17160]) ).
thf(17283,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[17161]) ).
thf(17326,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[17283]) ).
thf(10,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,4]) ).
thf(28,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[10]) ).
thf(113,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,28]) ).
thf(114,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
( ~ ( x @ f1 )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[114:[]]) ).
thf(78941,plain,
( x
| ( x @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(bool_ext,[status(thm)],[76061]) ).
thf(79834,plain,
( ( x @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[78941]) ).
thf(80317,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| x ),
inference(paramod_ordered,[status(thm)],[79834,8]) ).
thf(80318,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| x ),
inference(simp,[status(thm)],[80317]) ).
thf(80319,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| x ),
inference(pattern_uni,[status(thm)],[80318:[]]) ).
thf(830,plain,
( ~ x
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[816]) ).
thf(4910,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ x
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,830]) ).
thf(4911,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4910]) ).
thf(4912,plain,
( ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ x ),
inference(pattern_uni,[status(thm)],[4911:[]]) ).
thf(5361,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ $true
| ~ x
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,4912]) ).
thf(5362,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ x ),
inference(simp,[status(thm)],[5361]) ).
thf(5363,plain,
( ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 )
| ~ x ),
inference(pattern_uni,[status(thm)],[5362:[]]) ).
thf(5432,plain,
( ~ $true
| ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ~ x ),
inference(eqfactor_ordered,[status(thm)],[5363]) ).
thf(5435,plain,
( ( ( x @ f1 )
!= x )
| ~ ( x @ f1 )
| ~ x ),
inference(simp,[status(thm)],[5432]) ).
thf(5448,plain,
( ~ x
| ~ ( x @ f1 )
| ~ ( x @ f1 )
| ~ x ),
inference(bool_ext,[status(thm)],[5435]) ).
thf(5475,plain,
( ~ ( x @ f1 )
| ~ x ),
inference(simp,[status(thm)],[5448]) ).
thf(5482,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,5475]) ).
thf(5483,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[5482]) ).
thf(5487,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[5483]) ).
thf(7153,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ x
| ~ x
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,5487]) ).
thf(7154,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[7153]) ).
thf(7163,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[7154]) ).
thf(14273,plain,
( ( ( x @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[7163]) ).
thf(11,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( $true @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,4]) ).
thf(35,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[11]) ).
thf(2899,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f1 )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,35]) ).
thf(2900,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f1 )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[2899]) ).
thf(2901,plain,
( ~ ( x @ f1 @ f1 )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[2900:[]]) ).
thf(151,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[93,8]) ).
thf(152,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[151]) ).
thf(153,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(pattern_uni,[status(thm)],[152:[]]) ).
thf(9290,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 )
| ( $true @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,8630]) ).
thf(9291,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9290]) ).
thf(9481,plain,
( ( ( x @ f1 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9291]) ).
thf(7134,plain,
( ~ x
| ~ ( x @ f1 @ f1 )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[5487]) ).
thf(7168,plain,
( ~ ( x @ f1 @ f1 )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[7134]) ).
thf(34393,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[33551,6]) ).
thf(34394,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[34393]) ).
thf(34395,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(pattern_uni,[status(thm)],[34394:[]]) ).
thf(35418,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[33551,34395]) ).
thf(35419,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[35418]) ).
thf(35488,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[35419]) ).
thf(2491,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[2436]) ).
thf(71107,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[70181,33551]) ).
thf(71108,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[71107]) ).
thf(71109,plain,
( ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[71108:[]]) ).
thf(14296,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,7163]) ).
thf(14297,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[14296]) ).
thf(14314,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[14297]) ).
thf(14328,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[14314]) ).
thf(14610,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(paramod_ordered,[status(thm)],[14273,8]) ).
thf(14611,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14610]) ).
thf(14612,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(pattern_uni,[status(thm)],[14611:[]]) ).
thf(4849,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,13]) ).
thf(4850,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4849]) ).
thf(5004,plain,
( ~ ( x @ f1 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[4850]) ).
thf(7511,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[5004,5024]) ).
thf(7512,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[7511]) ).
thf(7513,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(pattern_uni,[status(thm)],[7512:[]]) ).
thf(8876,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(eqfactor_ordered,[status(thm)],[7513]) ).
thf(8902,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[8876]) ).
thf(12227,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,8902]) ).
thf(12228,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[12227]) ).
thf(12289,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[12228]) ).
thf(12351,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[12289]) ).
thf(61,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,8]) ).
thf(62,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[61]) ).
thf(75,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[62]) ).
thf(11194,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[75]) ).
thf(11285,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[11194]) ).
thf(16,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,5]) ).
thf(34,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[16]) ).
thf(1609,plain,
( ( ( x @ f1 )
!= x )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[34]) ).
thf(8541,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,88]) ).
thf(8542,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8541]) ).
thf(8543,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8542:[]]) ).
thf(8618,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 )
| ( $true @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,1743]) ).
thf(8619,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8618]) ).
thf(8703,plain,
( ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8619]) ).
thf(58404,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[56064,5]) ).
thf(58405,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[58404:[]]) ).
thf(132,plain,
( x
| ( x @ f1 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[93]) ).
thf(237,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[132,6]) ).
thf(238,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[237]) ).
thf(261,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[238]) ).
thf(35457,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[34395]) ).
thf(35476,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[35457]) ).
thf(38704,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,35476]) ).
thf(38705,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[38704]) ).
thf(38706,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(pattern_uni,[status(thm)],[38705:[]]) ).
thf(39116,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ x
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,38706]) ).
thf(39117,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(simp,[status(thm)],[39116]) ).
thf(39396,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ x ),
inference(simp,[status(thm)],[39117]) ).
thf(1835,plain,
( ~ $true
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[1743]) ).
thf(1847,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1835]) ).
thf(29,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( $true @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[10]) ).
thf(8901,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[8876]) ).
thf(22895,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ $true
| ~ x
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,8901]) ).
thf(22896,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ x ),
inference(simp,[status(thm)],[22895]) ).
thf(23045,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x ),
inference(simp,[status(thm)],[22896]) ).
thf(9197,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ $true
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,8624]) ).
thf(9198,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9197]) ).
thf(9199,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[9198:[]]) ).
thf(9651,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,9279]) ).
thf(9652,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9651]) ).
thf(10189,plain,
( ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9652]) ).
thf(1836,plain,
( ~ $true
| ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[1743]) ).
thf(1858,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1836]) ).
thf(116,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,28]) ).
thf(117,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[116]) ).
thf(121,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[117]) ).
thf(75466,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[75120,9]) ).
thf(75467,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(simp,[status(thm)],[75466]) ).
thf(75468,plain,
( ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[75467:[]]) ).
thf(77661,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f1 )
| x ),
inference(paramod_ordered,[status(thm)],[75468,8]) ).
thf(77662,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f1 )
| x ),
inference(simp,[status(thm)],[77661]) ).
thf(77663,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f1 )
| x ),
inference(pattern_uni,[status(thm)],[77662:[]]) ).
thf(14448,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(paramod_ordered,[status(thm)],[14273,5024]) ).
thf(14449,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14448]) ).
thf(14450,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(pattern_uni,[status(thm)],[14449:[]]) ).
thf(14985,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ $true
| ( ( x @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,14450]) ).
thf(14986,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ( ( x @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[14985]) ).
thf(14987,plain,
( ( ( x @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[14986:[]]) ).
thf(8821,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,7513]) ).
thf(8822,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[8821]) ).
thf(8823,plain,
( ~ ( x @ f1 @ f0 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[8822:[]]) ).
thf(485,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[60,6]) ).
thf(486,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[485]) ).
thf(487,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[486:[]]) ).
thf(8514,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,487]) ).
thf(8515,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8514]) ).
thf(8691,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8515]) ).
thf(21900,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,8711]) ).
thf(21901,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[21900]) ).
thf(22548,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[21901]) ).
thf(23522,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,22548]) ).
thf(23523,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[23522]) ).
thf(23524,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[23523:[]]) ).
thf(232,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ $true
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[132,6]) ).
thf(233,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[232]) ).
thf(265,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[233]) ).
thf(58,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(74,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[58]) ).
thf(59175,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[56064]) ).
thf(59409,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[59175]) ).
thf(7516,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(eqfactor_ordered,[status(thm)],[5024]) ).
thf(7518,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[7516]) ).
thf(17372,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ $true
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1920,17326]) ).
thf(17373,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[17372]) ).
thf(17374,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[17373:[]]) ).
thf(98,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,31]) ).
thf(99,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[98]) ).
thf(102,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( $true @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[99]) ).
thf(48901,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,5]) ).
thf(48902,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[48901:[]]) ).
thf(12213,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[8902]) ).
thf(12435,plain,
( ~ x
| ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(bool_ext,[status(thm)],[12213]) ).
thf(12520,plain,
( ~ ( x @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[12435]) ).
thf(15292,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f1 )
| ~ $true
| ~ x
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(paramod_ordered,[status(thm)],[14987,12520]) ).
thf(15293,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[15292]) ).
thf(15330,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f1 )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[15293]) ).
thf(54,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,6]) ).
thf(70,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[54]) ).
thf(35456,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[34395]) ).
thf(35471,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[35456]) ).
thf(36457,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[35471]) ).
thf(71160,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ~ ( x @ f1 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[70181,36457]) ).
thf(71161,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[71160]) ).
thf(71162,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[71161:[]]) ).
thf(72924,plain,
( x
| ( x @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(bool_ext,[status(thm)],[71162]) ).
thf(73123,plain,
( ( x @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[72924]) ).
thf(73307,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| x
| ~ ( x @ f1 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[73123,70901]) ).
thf(73308,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[73307]) ).
thf(74121,plain,
( ( ( x @ f1 )
!= x )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[73308]) ).
thf(74766,plain,
( x
| ( x @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(bool_ext,[status(thm)],[74121]) ).
thf(74912,plain,
( ( x @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[74766]) ).
thf(80088,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 )
| ~ $true
| x
| ( x @ f1 )
| x ),
inference(paramod_ordered,[status(thm)],[79834,74912]) ).
thf(80089,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 )
| x ),
inference(simp,[status(thm)],[80088]) ).
thf(80637,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( x @ f1 )
| x ),
inference(simp,[status(thm)],[80089]) ).
thf(32047,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[12351]) ).
thf(33343,plain,
( ~ x
| ~ ( x @ f1 @ f1 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[32047]) ).
thf(33424,plain,
( ~ ( x @ f1 @ f1 )
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[33343]) ).
thf(815,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[814]) ).
thf(8874,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f0 )
| ~ x
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[5004,7513]) ).
thf(8875,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[8874]) ).
thf(8878,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[8875]) ).
thf(26,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,9]) ).
thf(27,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[26]) ).
thf(33,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[27]) ).
thf(4882,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,8]) ).
thf(4883,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ x ),
inference(simp,[status(thm)],[4882]) ).
thf(4989,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ x ),
inference(simp,[status(thm)],[4883]) ).
thf(83,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( $true @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,13]) ).
thf(92,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[83]) ).
thf(1250,plain,
( ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 @ f1 )
| ~ ( x @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[115]) ).
thf(1259,plain,
( ( $true @ f1 @ f1 )
| ~ ( x @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[1250]) ).
thf(140,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[93,6]) ).
thf(141,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[140]) ).
thf(156,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[141]) ).
thf(17355,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ $true
| ( $true @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8703,17326]) ).
thf(17356,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[17355]) ).
thf(17357,plain,
( ( ( x @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[17356:[]]) ).
thf(22060,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8711,8711]) ).
thf(22061,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[22060]) ).
thf(22567,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[22061]) ).
thf(28293,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,22567]) ).
thf(28294,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[28293]) ).
thf(28295,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[28294:[]]) ).
thf(58851,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[56064,7]) ).
thf(58852,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[58851]) ).
thf(58853,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[58852:[]]) ).
thf(63562,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[58853,6]) ).
thf(63563,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[63562]) ).
thf(63564,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[63563:[]]) ).
thf(11826,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f1 @ f1 )
| ( $true @ f1 )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,9199]) ).
thf(11827,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f1 @ f1 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[11826]) ).
thf(11828,plain,
( ~ ( $true @ f1 @ f1 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[11827:[]]) ).
thf(81055,plain,
( ( x @ f1 )
| ( x @ f1 @ f0 )
| ( x @ f1 )
| x ),
inference(bool_ext,[status(thm)],[80637]) ).
thf(81152,plain,
( ( x @ f1 @ f0 )
| ( x @ f1 )
| x ),
inference(simp,[status(thm)],[81055]) ).
thf(8532,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,8]) ).
thf(8533,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8532]) ).
thf(8739,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8533]) ).
thf(49277,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,8739]) ).
thf(49278,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49277]) ).
thf(49279,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[49278:[]]) ).
thf(1690,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[506]) ).
thf(20990,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1690,1690]) ).
thf(20991,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[20990]) ).
thf(21272,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[20991]) ).
thf(21368,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[21272]) ).
thf(63,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,8]) ).
thf(73,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[63]) ).
thf(55730,plain,
( ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49841]) ).
thf(61823,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[55730,5]) ).
thf(61824,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[61823:[]]) ).
thf(376,plain,
( x
| ( x @ f1 @ f1 )
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[33]) ).
thf(5523,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| x
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[376,7]) ).
thf(5524,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| x
| ( $true @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[5523:[]]) ).
thf(33620,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[12400,6]) ).
thf(33621,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[33620]) ).
thf(33622,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[33621:[]]) ).
thf(49033,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ $true
| ( $true @ f1 )
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,9199]) ).
thf(49034,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( $true @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49033]) ).
thf(49035,plain,
( ( $true @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[49034:[]]) ).
thf(2259,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f1 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,7]) ).
thf(2260,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f1 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[2259:[]]) ).
thf(8599,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,86]) ).
thf(8600,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8599]) ).
thf(8601,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8600:[]]) ).
thf(40,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,6]) ).
thf(49,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[40]) ).
thf(4885,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ $true
| ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,42]) ).
thf(4886,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4885]) ).
thf(4887,plain,
( ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ~ x ),
inference(pattern_uni,[status(thm)],[4886:[]]) ).
thf(61898,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 @ f0 )
| ~ $true
| ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[55730,11285]) ).
thf(61899,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[61898]) ).
thf(61900,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[61899:[]]) ).
thf(155,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[93,4]) ).
thf(159,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[155]) ).
thf(12237,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ~ x
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,8902]) ).
thf(12238,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ x ),
inference(simp,[status(thm)],[12237]) ).
thf(12297,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[12238]) ).
thf(34680,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[33551,8]) ).
thf(34681,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[34680]) ).
thf(34682,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(pattern_uni,[status(thm)],[34681:[]]) ).
thf(56165,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[49841,9545]) ).
thf(56166,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[56165]) ).
thf(57227,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[56166]) ).
thf(1773,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[1743,8]) ).
thf(1774,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[1773]) ).
thf(1775,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[1774:[]]) ).
thf(49449,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ $true
| ( x @ f1 @ f0 )
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,1775]) ).
thf(49450,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49449]) ).
thf(49451,plain,
( ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[49450:[]]) ).
thf(91,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[83]) ).
thf(65027,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ~ $true
| ( $true @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8703,61824]) ).
thf(65028,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[65027]) ).
thf(65029,plain,
( ~ ( x @ f1 @ f0 @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[65028:[]]) ).
thf(14627,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ~ x
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(paramod_ordered,[status(thm)],[14273,12213]) ).
thf(14628,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14627]) ).
thf(14752,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14628]) ).
thf(30881,plain,
( ( x != x )
| ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(eqfactor_ordered,[status(thm)],[14752]) ).
thf(30903,plain,
( ( ( x @ f1 )
!= x )
| ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[30881]) ).
thf(30967,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[30903]) ).
thf(139,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[93,6]) ).
thf(162,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 )
!= x )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[139]) ).
thf(14945,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ( ( x @ f1 )
!= x )
| ~ x
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(paramod_ordered,[status(thm)],[14273,14450]) ).
thf(14946,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14945]) ).
thf(15004,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 )
!= x )
| ~ x ),
inference(simp,[status(thm)],[14946]) ).
thf(111,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,28]) ).
thf(112,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[111]) ).
thf(123,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f1 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( ( $true @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[112]) ).
thf(21898,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8711,8266]) ).
thf(21899,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[21898]) ).
thf(22292,plain,
( ~ ( x @ f1 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[21899]) ).
thf(43,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,6]) ).
thf(48,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( $true @ f0 @ f0 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[43]) ).
thf(4895,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ $true
| ~ x ),
inference(paramod_ordered,[status(thm)],[4775,6]) ).
thf(4896,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4895]) ).
thf(4971,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ x ),
inference(simp,[status(thm)],[4896]) ).
thf(13006,plain,
( ~ $true
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[8703]) ).
thf(13037,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[13006]) ).
thf(47787,plain,
( ( x @ f1 @ f0 @ f0 )
| ( $true @ f1 )
| ~ ( x @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[2901]) ).
thf(48071,plain,
( ( $true @ f1 )
| ~ ( x @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[47787]) ).
thf(8577,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ~ $true
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8266,815]) ).
thf(8578,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8577]) ).
thf(8579,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[8578:[]]) ).
thf(16293,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,8579]) ).
thf(16294,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[16293]) ).
thf(16295,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[16294:[]]) ).
thf(10162,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[10047]) ).
thf(726,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[620,6]) ).
thf(727,plain,
( ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[726:[]]) ).
thf(2080,plain,
( ~ $true
| ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[727]) ).
thf(2088,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[2080]) ).
thf(34671,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[33551,2088]) ).
thf(34672,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[34671]) ).
thf(34850,plain,
( ~ ( x @ f1 @ f0 )
| ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[34672]) ).
thf(34967,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 ) ),
inference(simp,[status(thm)],[34850]) ).
thf(71083,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ $true
| ~ ( x @ f1 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[70181,34682]) ).
thf(71084,plain,
( ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[71083]) ).
thf(71085,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[71084:[]]) ).
thf(74000,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ ( $true @ f1 )
| ~ ( x @ f1 @ f0 )
| x
| ~ ( x @ f1 @ f0 )
| x ),
inference(paramod_ordered,[status(thm)],[73123,71085]) ).
thf(74001,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ ( $true @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(simp,[status(thm)],[74000]) ).
thf(74002,plain,
( ~ ( $true @ f1 )
| ~ ( x @ f1 @ f0 )
| x ),
inference(pattern_uni,[status(thm)],[74001:[]]) ).
thf(51059,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ~ ( $true @ f0 @ f0 @ f0 )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,49035]) ).
thf(51060,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ~ ( $true @ f0 @ f0 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[51059]) ).
thf(51061,plain,
( ~ ( $true @ f0 @ f0 @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[51060:[]]) ).
thf(63493,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ~ $true
| ( $true @ f0 )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[58853,8717]) ).
thf(63494,plain,
( ( ( x @ f1 @ f0 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[63493]) ).
thf(63495,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( $true @ f0 ) )
| ( x @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[63494:[]]) ).
thf(64327,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ~ $true
| ( $true @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8703,57227]) ).
thf(64328,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[64327]) ).
thf(64329,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[64328:[]]) ).
thf(87,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( $true @ f0 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[80]) ).
thf(40155,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,39396]) ).
thf(40156,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[40155]) ).
thf(40157,plain,
( ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[40156:[]]) ).
thf(40397,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ x
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(paramod_ordered,[status(thm)],[40157,7445]) ).
thf(40398,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(simp,[status(thm)],[40397]) ).
thf(40399,plain,
( ( x @ f1 @ f0 @ f0 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(pattern_uni,[status(thm)],[40398:[]]) ).
thf(20133,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,16295]) ).
thf(20134,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[20133]) ).
thf(20135,plain,
( ( ( $true @ f1 @ f1 )
!= ( x @ f1 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[20134:[]]) ).
thf(49603,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ $true
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,8579]) ).
thf(49604,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49603]) ).
thf(50192,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49604]) ).
thf(50350,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[50192]) ).
thf(234,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[132,6]) ).
thf(235,plain,
( ~ ( $true @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| x
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(pattern_uni,[status(thm)],[234:[]]) ).
thf(2314,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,5]) ).
thf(2315,plain,
( ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[2314:[]]) ).
thf(55879,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8703,49841]) ).
thf(55880,plain,
( ( ( x @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[55879]) ).
thf(55881,plain,
( ( x @ f1 @ f1 @ f1 )
| ( ( x @ f1 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[55880:[]]) ).
thf(1114,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(paramod_ordered,[status(thm)],[889,8]) ).
thf(1115,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(simp,[status(thm)],[1114]) ).
thf(1116,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( x @ f1 )
| ( $true @ f1 ) ),
inference(pattern_uni,[status(thm)],[1115:[]]) ).
thf(27814,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,14328]) ).
thf(27815,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( ( x @ f1 )
!= ( $true @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[27814]) ).
thf(27901,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ x
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[27815]) ).
thf(27934,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ~ x
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[27901]) ).
thf(49378,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ $true
| ~ ( x @ f1 )
| ( $true @ f0 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[48857,8624]) ).
thf(49379,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 @ f1 @ f1 ) )
| ~ ( x @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[49378]) ).
thf(49380,plain,
( ~ ( x @ f1 )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[49379:[]]) ).
thf(8663,plain,
( ~ $true
| ( ( $true @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(eqfactor_ordered,[status(thm)],[8266]) ).
thf(8675,plain,
( ( ( $true @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[8663]) ).
thf(9437,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ( ( $true @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[8630,8675]) ).
thf(9438,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9437]) ).
thf(9523,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 )
| ( $true @ f0 ) ),
inference(simp,[status(thm)],[9438]) ).
thf(36,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[11]) ).
thf(30,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( ( $true @ f1 @ f1 )
!= ( x @ f1 @ f0 @ f0 ) )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[10]) ).
thf(8508,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,8266]) ).
thf(8509,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( $true @ f0 ) )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[8508]) ).
thf(8737,plain,
( ~ ( x @ f1 @ f1 @ f1 )
| ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[8509]) ).
thf(35411,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ $true
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[7,34395]) ).
thf(35412,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f1 @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[35411]) ).
thf(35413,plain,
( ~ ( $true @ f0 )
| ~ ( x @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[35412:[]]) ).
thf(2416,plain,
( ( ( x @ f1 )
!= ( x @ f1 ) )
| ( ( $true @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(paramod_ordered,[status(thm)],[2174,4]) ).
thf(2417,plain,
( ( ( $true @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 @ f0 @ f0 ) )
| ( $true @ f1 )
| ( $true @ f0 ) ),
inference(pattern_uni,[status(thm)],[2416:[]]) ).
thf(2070,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[620,727]) ).
thf(2071,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( $true @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[2070]) ).
thf(2091,plain,
( ~ ( x @ f1 @ f0 )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ ( x @ f1 )
| ~ ( $true @ f0 @ f0 ) ),
inference(simp,[status(thm)],[2071]) ).
thf(40439,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ $true
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ~ x
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(paramod_ordered,[status(thm)],[40157,5024]) ).
thf(40440,plain,
( ( ( x @ f1 @ f0 @ f0 )
!= ( x @ f1 @ f0 @ f0 ) )
| ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(simp,[status(thm)],[40439]) ).
thf(40441,plain,
( ~ ( x @ f1 @ f1 @ f1 @ f0 )
| ( ( x @ f1 @ f0 )
!= ( $true @ f0 ) )
| ~ x ),
inference(pattern_uni,[status(thm)],[40440:[]]) ).
thf(39,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,6]) ).
thf(47,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ~ ( x @ f1 @ f0 @ f0 @ f0 )
| ~ ( $true @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[39]) ).
thf(57,plain,
( ( ( x @ f1 @ f1 @ f1 )
!= ( x @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[9,7]) ).
thf(68,plain,
( ( ( x @ f1 @ f1 )
!= x )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[57]) ).
thf(90,plain,
( ( ( x @ f1 @ f1 @ f1 @ f0 )
!= ( x @ f1 @ f0 ) )
| ~ ( $true @ f0 )
| ( x @ f1 @ f0 @ f0 )
| ( x @ f1 @ f0 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[83]) ).
thf(3520,plain,
( ( x @ f1 )
| ( x @ f1 @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(bool_ext,[status(thm)],[36]) ).
thf(43699,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(paramod_ordered,[status(thm)],[3520,7]) ).
thf(43700,plain,
( ( ( x @ f1 @ f1 )
!= ( x @ f1 @ f1 ) )
| ( x @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(simp,[status(thm)],[43699]) ).
thf(43701,plain,
( ( x @ f1 )
| ( x @ f1 @ f0 @ f0 @ f0 )
| ( $true @ f1 @ f0 )
| ( x @ f1 @ f0 @ f0 ) ),
inference(pattern_uni,[status(thm)],[43700:[]]) ).
thf(83750,plain,
$false,
inference(e,[status(thm)],[8711,69,138,7445,88,79430,8266,17326,115,5,80319,14273,11303,2901,153,9481,7168,35488,2491,42,71109,14328,14612,4775,5024,12351,34805,8902,11285,8717,1609,93,8543,8703,58405,261,39396,1847,29,23045,9199,70901,10189,1858,121,49841,77663,14987,8823,89,8691,23524,265,74,6,60,59409,5487,7518,17374,8630,102,48902,15330,59212,70,80637,33424,815,8878,33,4989,28,1920,889,70181,92,1259,156,75468,9,22548,7513,17357,5475,28295,10163,56064,63564,48857,11828,81152,13,74912,75120,71162,49279,70898,21368,73,8739,8512,73123,61824,9545,5524,33622,49035,34,9154,2260,8601,55730,49,12400,4887,61900,35471,8624,86,159,12297,34682,7,57227,816,49451,91,32047,65029,2212,33551,1775,30967,3,74121,35,162,35476,15004,487,123,58853,22292,48,4971,13037,1743,707,48071,16295,10162,34967,36457,31,74002,7163,727,51061,63495,64329,9279,2088,87,40399,8579,20135,2174,50350,40157,76061,8,75,235,2315,55881,1116,34395,620,27934,5004,49380,9523,8901,12213,36,12520,30,79834,22567,8737,506,35413,2417,71085,2091,38706,40441,4,8675,47,68,90,43701,14450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO500_8.002 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41 % Computer : n013.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sat Sep 26 19:24:08 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.83/0.98 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.07/1.06 % [INFO] Parsing done (86ms).
% 1.07/1.07 % [INFO] Running in sequential loop mode.
% 1.38/1.26 % [INFO] eprover registered as external prover.
% 1.38/1.27 % [INFO] Scanning for conjecture ...
% 1.61/1.31 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.61/1.32 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.61/1.32 % [INFO] Problem is typed first-order (TPTP TFF).
% 1.61/1.33 % [INFO] Type checking passed.
% 1.61/1.33 % [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 ...
% 52.63/14.89 % External prover 'e' found a proof!
% 52.63/14.89 % [INFO] Killing All external provers ...
% 52.63/14.89 % Time passed: 14344ms (effective reasoning time: 13817ms)
% 52.63/14.89 % 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)>
% 52.63/14.89 % Axioms used in derivation (0):
% 52.63/14.89 % No. of inferences in proof: 595
% 52.63/14.89 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 14344 ms resp. 13817 ms w/o parsing
% 53.03/14.99 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 53.03/14.99 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------