%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL654+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n002.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 : Fri Sep 25 02:07:09 PM UTC 2026
% Result : Theorem 40.51s 12.29s
% Output : CNFRefutation 82.64s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ! [X153] :
( ! [X154] :
( ! [X155] :
( ! [X156] :
( ! [X157] :
( ~ ! [X160] :
( p1(X160)
| ~ r1(X157,X160) )
| ! [X158] :
( ! [X159] :
( p1(X159)
| ~ r1(X158,X159) )
| ~ r1(X157,X158) )
| ~ r1(X156,X157) )
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X0,X153) )
| ~ ! [X151] :
( ~ ! [X152] :
( $false
| ~ r1(X151,X152) )
| ~ r1(X0,X151) )
| ~ ! [X145] :
( ~ ( ~ ! [X149] :
( ~ ! [X150] :
( p1(X150)
| ~ r1(X149,X150) )
| ~ r1(X145,X149) )
& ~ ! [X146] :
( ~ ! [X147] :
( ~ ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
| ~ r1(X146,X147) )
| ~ r1(X145,X146) ) )
| ~ r1(X0,X145) )
| ~ ! [X140] :
( ! [X141] :
( ~ ( ~ ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
& ~ ! [X142] :
( ~ ! [X143] :
( p1(X143)
| ~ r1(X142,X143) )
| ~ r1(X141,X142) ) )
| ~ r1(X140,X141) )
| ~ r1(X0,X140) )
| ~ ! [X137] :
( ~ ( p1(X137)
& ~ ! [X138] :
( ~ ! [X139] :
( ~ p1(X139)
| ~ r1(X138,X139) )
| ~ r1(X137,X138) ) )
| ~ r1(X0,X137) )
| ! [X129] :
( ! [X130] :
( ! [X131] :
( ! [X132] :
( ! [X133] :
( ~ ! [X136] :
( p1(X136)
| ~ r1(X133,X136) )
| ! [X134] :
( ! [X135] :
( p1(X135)
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
| ~ r1(X129,X130) )
| ~ r1(X0,X129) )
| ~ ! [X126] :
( ! [X127] :
( ~ ! [X128] :
( $false
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X119] :
( ! [X120] :
( ~ ( ~ ! [X124] :
( ~ ! [X125] :
( p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X120,X124) )
& ~ ! [X121] :
( ~ ! [X122] :
( ~ ! [X123] :
( p1(X123)
| ~ r1(X122,X123) )
| ~ r1(X121,X122) )
| ~ r1(X120,X121) ) )
| ~ r1(X119,X120) )
| ~ r1(X0,X119) )
| ~ ! [X113] :
( ! [X114] :
( ! [X115] :
( ~ ( ~ ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
& ~ ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| ~ r1(X115,X116) ) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X0,X113) )
| ~ ! [X109] :
( ! [X110] :
( ~ ( p1(X110)
& ~ ! [X111] :
( ~ ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) ) )
| ~ r1(X109,X110) )
| ~ r1(X0,X109) )
| ! [X101] :
( ! [X102] :
( ! [X103] :
( ! [X104] :
( ! [X105] :
( ~ ! [X108] :
( p1(X108)
| ~ r1(X105,X108) )
| ! [X106] :
( ! [X107] :
( p1(X107)
| ~ r1(X106,X107) )
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X101,X102) )
| ~ r1(X0,X101) )
| ~ ! [X97] :
( ! [X98] :
( ! [X99] :
( ~ ! [X100] :
( $false
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X0,X97) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( ~ ! [X95] :
( ~ ! [X96] :
( p1(X96)
| ~ r1(X95,X96) )
| ~ r1(X91,X95) )
& ~ ! [X92] :
( ~ ! [X93] :
( ~ ! [X94] :
( p1(X94)
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ~ ( ~ ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
& ~ ! [X86] :
( ~ ! [X87] :
( p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) ) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X0,X82) )
| ~ ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ ( p1(X79)
& ~ ! [X80] :
( ~ ! [X81] :
( ~ p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
| ! [X69] :
( ! [X70] :
( ! [X71] :
( ! [X72] :
( ! [X73] :
( ~ ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X0,X69) )
| ~ ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( ~ ! [X68] :
( $false
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X0,X64) )
| ~ ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ~ ( ~ ! [X62] :
( ~ ! [X63] :
( p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X58,X62) )
& ~ ! [X59] :
( ~ ! [X60] :
( ~ ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) ) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X0,X55) )
| ~ ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ~ ( ~ ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
& ~ ! [X52] :
( ~ ! [X53] :
( p1(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) ) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X0,X47) )
| ~ ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ ( p1(X44)
& ~ ! [X45] :
( ~ ! [X46] :
( ~ p1(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) ) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X0,X41) )
| ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X40] :
( p1(X40)
| ~ r1(X37,X40) )
| ! [X38] :
( ! [X39] :
( p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ~ ! [X32] :
( $false
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X0,X27) )
| ~ ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ~ ( ~ ! [X25] :
( ~ ! [X26] :
( p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X21,X25) )
& ~ ! [X22] :
( ~ ! [X23] :
( ~ ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) ) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X0,X17) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ~ ( ~ ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
& ~ ! [X14] :
( ~ ! [X15] :
( p1(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) ) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
~ ~ ? [X0] :
~ ( ! [X153] :
( ! [X154] :
( ! [X155] :
( ! [X156] :
( ! [X157] :
( ~ ! [X160] :
( p1(X160)
| ~ r1(X157,X160) )
| ! [X158] :
( ! [X159] :
( p1(X159)
| ~ r1(X158,X159) )
| ~ r1(X157,X158) )
| ~ r1(X156,X157) )
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X0,X153) )
| ~ ! [X151] :
( ~ ! [X152] : ~ r1(X151,X152)
| ~ r1(X0,X151) )
| ~ ! [X145] :
( ~ ( ~ ! [X149] :
( ~ ! [X150] :
( p1(X150)
| ~ r1(X149,X150) )
| ~ r1(X145,X149) )
& ~ ! [X146] :
( ~ ! [X147] :
( ~ ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
| ~ r1(X146,X147) )
| ~ r1(X145,X146) ) )
| ~ r1(X0,X145) )
| ~ ! [X140] :
( ! [X141] :
( ~ ( ~ ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
& ~ ! [X142] :
( ~ ! [X143] :
( p1(X143)
| ~ r1(X142,X143) )
| ~ r1(X141,X142) ) )
| ~ r1(X140,X141) )
| ~ r1(X0,X140) )
| ~ ! [X137] :
( ~ ( p1(X137)
& ~ ! [X138] :
( ~ ! [X139] :
( ~ p1(X139)
| ~ r1(X138,X139) )
| ~ r1(X137,X138) ) )
| ~ r1(X0,X137) )
| ! [X129] :
( ! [X130] :
( ! [X131] :
( ! [X132] :
( ! [X133] :
( ~ ! [X136] :
( p1(X136)
| ~ r1(X133,X136) )
| ! [X134] :
( ! [X135] :
( p1(X135)
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
| ~ r1(X129,X130) )
| ~ r1(X0,X129) )
| ~ ! [X126] :
( ! [X127] :
( ~ ! [X128] : ~ r1(X127,X128)
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X119] :
( ! [X120] :
( ~ ( ~ ! [X124] :
( ~ ! [X125] :
( p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X120,X124) )
& ~ ! [X121] :
( ~ ! [X122] :
( ~ ! [X123] :
( p1(X123)
| ~ r1(X122,X123) )
| ~ r1(X121,X122) )
| ~ r1(X120,X121) ) )
| ~ r1(X119,X120) )
| ~ r1(X0,X119) )
| ~ ! [X113] :
( ! [X114] :
( ! [X115] :
( ~ ( ~ ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
& ~ ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| ~ r1(X115,X116) ) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X0,X113) )
| ~ ! [X109] :
( ! [X110] :
( ~ ( p1(X110)
& ~ ! [X111] :
( ~ ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) ) )
| ~ r1(X109,X110) )
| ~ r1(X0,X109) )
| ! [X101] :
( ! [X102] :
( ! [X103] :
( ! [X104] :
( ! [X105] :
( ~ ! [X108] :
( p1(X108)
| ~ r1(X105,X108) )
| ! [X106] :
( ! [X107] :
( p1(X107)
| ~ r1(X106,X107) )
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X101,X102) )
| ~ r1(X0,X101) )
| ~ ! [X97] :
( ! [X98] :
( ! [X99] :
( ~ ! [X100] : ~ r1(X99,X100)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X0,X97) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( ~ ! [X95] :
( ~ ! [X96] :
( p1(X96)
| ~ r1(X95,X96) )
| ~ r1(X91,X95) )
& ~ ! [X92] :
( ~ ! [X93] :
( ~ ! [X94] :
( p1(X94)
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ~ ( ~ ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
& ~ ! [X86] :
( ~ ! [X87] :
( p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) ) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X0,X82) )
| ~ ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ ( p1(X79)
& ~ ! [X80] :
( ~ ! [X81] :
( ~ p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
| ! [X69] :
( ! [X70] :
( ! [X71] :
( ! [X72] :
( ! [X73] :
( ~ ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X0,X69) )
| ~ ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( ~ ! [X68] : ~ r1(X67,X68)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X0,X64) )
| ~ ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ~ ( ~ ! [X62] :
( ~ ! [X63] :
( p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X58,X62) )
& ~ ! [X59] :
( ~ ! [X60] :
( ~ ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) ) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X0,X55) )
| ~ ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ~ ( ~ ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
& ~ ! [X52] :
( ~ ! [X53] :
( p1(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) ) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X0,X47) )
| ~ ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ ( p1(X44)
& ~ ! [X45] :
( ~ ! [X46] :
( ~ p1(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) ) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X0,X41) )
| ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X40] :
( p1(X40)
| ~ r1(X37,X40) )
| ! [X38] :
( ! [X39] :
( p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ~ ! [X32] : ~ r1(X31,X32)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X0,X27) )
| ~ ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ~ ( ~ ! [X25] :
( ~ ! [X26] :
( p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X21,X25) )
& ~ ! [X22] :
( ~ ! [X23] :
( ~ ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) ) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X0,X17) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ~ ( ~ ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
& ~ ! [X14] :
( ~ ! [X15] :
( p1(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) ) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(true_and_false_elimination,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ! [X153] :
( ! [X154] :
( ! [X155] :
( ! [X156] :
( ! [X157] :
( ~ ! [X160] :
( p1(X160)
| ~ r1(X157,X160) )
| ! [X158] :
( ! [X159] :
( p1(X159)
| ~ r1(X158,X159) )
| ~ r1(X157,X158) )
| ~ r1(X156,X157) )
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X0,X153) )
| ~ ! [X151] :
( ~ ! [X152] : ~ r1(X151,X152)
| ~ r1(X0,X151) )
| ~ ! [X145] :
( ~ ( ~ ! [X149] :
( ~ ! [X150] :
( p1(X150)
| ~ r1(X149,X150) )
| ~ r1(X145,X149) )
& ~ ! [X146] :
( ~ ! [X147] :
( ~ ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
| ~ r1(X146,X147) )
| ~ r1(X145,X146) ) )
| ~ r1(X0,X145) )
| ~ ! [X140] :
( ! [X141] :
( ~ ( ~ ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
& ~ ! [X142] :
( ~ ! [X143] :
( p1(X143)
| ~ r1(X142,X143) )
| ~ r1(X141,X142) ) )
| ~ r1(X140,X141) )
| ~ r1(X0,X140) )
| ~ ! [X137] :
( ~ ( p1(X137)
& ~ ! [X138] :
( ~ ! [X139] :
( ~ p1(X139)
| ~ r1(X138,X139) )
| ~ r1(X137,X138) ) )
| ~ r1(X0,X137) )
| ! [X129] :
( ! [X130] :
( ! [X131] :
( ! [X132] :
( ! [X133] :
( ~ ! [X136] :
( p1(X136)
| ~ r1(X133,X136) )
| ! [X134] :
( ! [X135] :
( p1(X135)
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
| ~ r1(X129,X130) )
| ~ r1(X0,X129) )
| ~ ! [X126] :
( ! [X127] :
( ~ ! [X128] : ~ r1(X127,X128)
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X119] :
( ! [X120] :
( ~ ( ~ ! [X124] :
( ~ ! [X125] :
( p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X120,X124) )
& ~ ! [X121] :
( ~ ! [X122] :
( ~ ! [X123] :
( p1(X123)
| ~ r1(X122,X123) )
| ~ r1(X121,X122) )
| ~ r1(X120,X121) ) )
| ~ r1(X119,X120) )
| ~ r1(X0,X119) )
| ~ ! [X113] :
( ! [X114] :
( ! [X115] :
( ~ ( ~ ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
& ~ ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| ~ r1(X115,X116) ) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X0,X113) )
| ~ ! [X109] :
( ! [X110] :
( ~ ( p1(X110)
& ~ ! [X111] :
( ~ ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) ) )
| ~ r1(X109,X110) )
| ~ r1(X0,X109) )
| ! [X101] :
( ! [X102] :
( ! [X103] :
( ! [X104] :
( ! [X105] :
( ~ ! [X108] :
( p1(X108)
| ~ r1(X105,X108) )
| ! [X106] :
( ! [X107] :
( p1(X107)
| ~ r1(X106,X107) )
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X101,X102) )
| ~ r1(X0,X101) )
| ~ ! [X97] :
( ! [X98] :
( ! [X99] :
( ~ ! [X100] : ~ r1(X99,X100)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X0,X97) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( ~ ! [X95] :
( ~ ! [X96] :
( p1(X96)
| ~ r1(X95,X96) )
| ~ r1(X91,X95) )
& ~ ! [X92] :
( ~ ! [X93] :
( ~ ! [X94] :
( p1(X94)
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ~ ( ~ ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
& ~ ! [X86] :
( ~ ! [X87] :
( p1(X87)
| ~ r1(X86,X87) )
| ~ r1(X85,X86) ) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X0,X82) )
| ~ ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ ( p1(X79)
& ~ ! [X80] :
( ~ ! [X81] :
( ~ p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
| ! [X69] :
( ! [X70] :
( ! [X71] :
( ! [X72] :
( ! [X73] :
( ~ ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X0,X69) )
| ~ ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( ~ ! [X68] : ~ r1(X67,X68)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X0,X64) )
| ~ ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ~ ( ~ ! [X62] :
( ~ ! [X63] :
( p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X58,X62) )
& ~ ! [X59] :
( ~ ! [X60] :
( ~ ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) ) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X0,X55) )
| ~ ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ~ ( ~ ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
& ~ ! [X52] :
( ~ ! [X53] :
( p1(X53)
| ~ r1(X52,X53) )
| ~ r1(X51,X52) ) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X0,X47) )
| ~ ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ ( p1(X44)
& ~ ! [X45] :
( ~ ! [X46] :
( ~ p1(X46)
| ~ r1(X45,X46) )
| ~ r1(X44,X45) ) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X0,X41) )
| ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X40] :
( p1(X40)
| ~ r1(X37,X40) )
| ! [X38] :
( ! [X39] :
( p1(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ~ ! [X32] : ~ r1(X31,X32)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X0,X27) )
| ~ ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ~ ( ~ ! [X25] :
( ~ ! [X26] :
( p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X21,X25) )
& ~ ! [X22] :
( ~ ! [X23] :
( ~ ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) ) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X0,X17) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ~ ( ~ ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
& ~ ! [X14] :
( ~ ! [X15] :
( p1(X15)
| ~ r1(X14,X15) )
| ~ r1(X13,X14) ) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ? [X153] :
( ? [X154] :
( ? [X155] :
( ? [X156] :
( ? [X157] :
( ! [X160] :
( p1(X160)
| ~ r1(X157,X160) )
& ? [X158] :
( ? [X159] :
( ~ p1(X159)
& r1(X158,X159) )
& r1(X157,X158) )
& r1(X156,X157) )
& r1(X155,X156) )
& r1(X154,X155) )
& r1(X153,X154) )
& r1(X0,X153) )
& ! [X151] :
( ? [X152] : r1(X151,X152)
| ~ r1(X0,X151) )
& ! [X145] :
( ! [X149] :
( ? [X150] :
( ~ p1(X150)
& r1(X149,X150) )
| ~ r1(X145,X149) )
| ! [X146] :
( ? [X147] :
( ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
& r1(X146,X147) )
| ~ r1(X145,X146) )
| ~ r1(X0,X145) )
& ! [X140] :
( ! [X141] :
( ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
| ! [X142] :
( ? [X143] :
( ~ p1(X143)
& r1(X142,X143) )
| ~ r1(X141,X142) )
| ~ r1(X140,X141) )
| ~ r1(X0,X140) )
& ! [X137] :
( ~ p1(X137)
| ! [X138] :
( ? [X139] :
( p1(X139)
& r1(X138,X139) )
| ~ r1(X137,X138) )
| ~ r1(X0,X137) )
& ? [X129] :
( ? [X130] :
( ? [X131] :
( ? [X132] :
( ? [X133] :
( ! [X136] :
( p1(X136)
| ~ r1(X133,X136) )
& ? [X134] :
( ? [X135] :
( ~ p1(X135)
& r1(X134,X135) )
& r1(X133,X134) )
& r1(X132,X133) )
& r1(X131,X132) )
& r1(X130,X131) )
& r1(X129,X130) )
& r1(X0,X129) )
& ! [X126] :
( ! [X127] :
( ? [X128] : r1(X127,X128)
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ! [X119] :
( ! [X120] :
( ! [X124] :
( ? [X125] :
( ~ p1(X125)
& r1(X124,X125) )
| ~ r1(X120,X124) )
| ! [X121] :
( ? [X122] :
( ! [X123] :
( p1(X123)
| ~ r1(X122,X123) )
& r1(X121,X122) )
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X0,X119) )
& ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
| ! [X116] :
( ? [X117] :
( ~ p1(X117)
& r1(X116,X117) )
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X0,X113) )
& ! [X109] :
( ! [X110] :
( ~ p1(X110)
| ! [X111] :
( ? [X112] :
( p1(X112)
& r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
| ~ r1(X0,X109) )
& ? [X101] :
( ? [X102] :
( ? [X103] :
( ? [X104] :
( ? [X105] :
( ! [X108] :
( p1(X108)
| ~ r1(X105,X108) )
& ? [X106] :
( ? [X107] :
( ~ p1(X107)
& r1(X106,X107) )
& r1(X105,X106) )
& r1(X104,X105) )
& r1(X103,X104) )
& r1(X102,X103) )
& r1(X101,X102) )
& r1(X0,X101) )
& ! [X97] :
( ! [X98] :
( ! [X99] :
( ? [X100] : r1(X99,X100)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X0,X97) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ! [X95] :
( ? [X96] :
( ~ p1(X96)
& r1(X95,X96) )
| ~ r1(X91,X95) )
| ! [X92] :
( ? [X93] :
( ! [X94] :
( p1(X94)
| ~ r1(X93,X94) )
& r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
& ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ? [X87] :
( ~ p1(X87)
& r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X0,X82) )
& ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ! [X80] :
( ? [X81] :
( p1(X81)
& r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
& ? [X69] :
( ? [X70] :
( ? [X71] :
( ? [X72] :
( ? [X73] :
( ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
& ? [X74] :
( ? [X75] :
( ~ p1(X75)
& r1(X74,X75) )
& r1(X73,X74) )
& r1(X72,X73) )
& r1(X71,X72) )
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X0,X69) )
& ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( ? [X68] : r1(X67,X68)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X0,X64) )
& ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ! [X62] :
( ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
| ~ r1(X58,X62) )
| ! [X59] :
( ? [X60] :
( ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X0,X55) )
& ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
| ! [X52] :
( ? [X53] :
( ~ p1(X53)
& r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X0,X47) )
& ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ p1(X44)
| ! [X45] :
( ? [X46] :
( p1(X46)
& r1(X45,X46) )
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X0,X41) )
& ? [X33] :
( ? [X34] :
( ? [X35] :
( ? [X36] :
( ? [X37] :
( ! [X40] :
( p1(X40)
| ~ r1(X37,X40) )
& ? [X38] :
( ? [X39] :
( ~ p1(X39)
& r1(X38,X39) )
& r1(X37,X38) )
& r1(X36,X37) )
& r1(X35,X36) )
& r1(X34,X35) )
& r1(X33,X34) )
& r1(X0,X33) )
& ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ? [X32] : r1(X31,X32)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X0,X27) )
& ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X25] :
( ? [X26] :
( ~ p1(X26)
& r1(X25,X26) )
| ~ r1(X21,X25) )
| ! [X22] :
( ? [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
& r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X0,X17) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
| ! [X14] :
( ? [X15] :
( ~ p1(X15)
& r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ p1(X5)
| ! [X6] :
( ? [X7] :
( p1(X7)
& r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ? [X153] :
( ? [X154] :
( ? [X155] :
( ? [X156] :
( ? [X157] :
( ! [X160] :
( p1(X160)
| ~ r1(X157,X160) )
& ? [X158] :
( ? [X159] :
( ~ p1(X159)
& r1(X158,X159) )
& r1(X157,X158) )
& r1(X156,X157) )
& r1(X155,X156) )
& r1(X154,X155) )
& r1(X153,X154) )
& r1(X0,X153) )
& ! [X151] :
( ? [X152] : r1(X151,X152)
| ~ r1(X0,X151) )
& ! [X145] :
( ! [X149] :
( ? [X150] :
( ~ p1(X150)
& r1(X149,X150) )
| ~ r1(X145,X149) )
| ! [X146] :
( ? [X147] :
( ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
& r1(X146,X147) )
| ~ r1(X145,X146) )
| ~ r1(X0,X145) )
& ! [X140] :
( ! [X141] :
( ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
| ! [X142] :
( ? [X143] :
( ~ p1(X143)
& r1(X142,X143) )
| ~ r1(X141,X142) )
| ~ r1(X140,X141) )
| ~ r1(X0,X140) )
& ! [X137] :
( ~ p1(X137)
| ! [X138] :
( ? [X139] :
( p1(X139)
& r1(X138,X139) )
| ~ r1(X137,X138) )
| ~ r1(X0,X137) )
& ? [X129] :
( ? [X130] :
( ? [X131] :
( ? [X132] :
( ? [X133] :
( ! [X136] :
( p1(X136)
| ~ r1(X133,X136) )
& ? [X134] :
( ? [X135] :
( ~ p1(X135)
& r1(X134,X135) )
& r1(X133,X134) )
& r1(X132,X133) )
& r1(X131,X132) )
& r1(X130,X131) )
& r1(X129,X130) )
& r1(X0,X129) )
& ! [X126] :
( ! [X127] :
( ? [X128] : r1(X127,X128)
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ! [X119] :
( ! [X120] :
( ! [X124] :
( ? [X125] :
( ~ p1(X125)
& r1(X124,X125) )
| ~ r1(X120,X124) )
| ! [X121] :
( ? [X122] :
( ! [X123] :
( p1(X123)
| ~ r1(X122,X123) )
& r1(X121,X122) )
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X0,X119) )
& ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
| ! [X116] :
( ? [X117] :
( ~ p1(X117)
& r1(X116,X117) )
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X0,X113) )
& ! [X109] :
( ! [X110] :
( ~ p1(X110)
| ! [X111] :
( ? [X112] :
( p1(X112)
& r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
| ~ r1(X0,X109) )
& ? [X101] :
( ? [X102] :
( ? [X103] :
( ? [X104] :
( ? [X105] :
( ! [X108] :
( p1(X108)
| ~ r1(X105,X108) )
& ? [X106] :
( ? [X107] :
( ~ p1(X107)
& r1(X106,X107) )
& r1(X105,X106) )
& r1(X104,X105) )
& r1(X103,X104) )
& r1(X102,X103) )
& r1(X101,X102) )
& r1(X0,X101) )
& ! [X97] :
( ! [X98] :
( ! [X99] :
( ? [X100] : r1(X99,X100)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X0,X97) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ! [X95] :
( ? [X96] :
( ~ p1(X96)
& r1(X95,X96) )
| ~ r1(X91,X95) )
| ! [X92] :
( ? [X93] :
( ! [X94] :
( p1(X94)
| ~ r1(X93,X94) )
& r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
& ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ? [X87] :
( ~ p1(X87)
& r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(X0,X82) )
& ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ! [X80] :
( ? [X81] :
( p1(X81)
& r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
& ? [X69] :
( ? [X70] :
( ? [X71] :
( ? [X72] :
( ? [X73] :
( ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
& ? [X74] :
( ? [X75] :
( ~ p1(X75)
& r1(X74,X75) )
& r1(X73,X74) )
& r1(X72,X73) )
& r1(X71,X72) )
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X0,X69) )
& ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( ? [X68] : r1(X67,X68)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X0,X64) )
& ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ! [X62] :
( ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
| ~ r1(X58,X62) )
| ! [X59] :
( ? [X60] :
( ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X0,X55) )
& ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
| ! [X52] :
( ? [X53] :
( ~ p1(X53)
& r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X0,X47) )
& ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ p1(X44)
| ! [X45] :
( ? [X46] :
( p1(X46)
& r1(X45,X46) )
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X0,X41) )
& ? [X33] :
( ? [X34] :
( ? [X35] :
( ? [X36] :
( ? [X37] :
( ! [X40] :
( p1(X40)
| ~ r1(X37,X40) )
& ? [X38] :
( ? [X39] :
( ~ p1(X39)
& r1(X38,X39) )
& r1(X37,X38) )
& r1(X36,X37) )
& r1(X35,X36) )
& r1(X34,X35) )
& r1(X33,X34) )
& r1(X0,X33) )
& ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( ? [X32] : r1(X31,X32)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X0,X27) )
& ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X25] :
( ? [X26] :
( ~ p1(X26)
& r1(X25,X26) )
| ~ r1(X21,X25) )
| ! [X22] :
( ? [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
& r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X0,X17) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
| ! [X14] :
( ? [X15] :
( ~ p1(X15)
& r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ p1(X5)
| ! [X6] :
( ? [X7] :
( p1(X7)
& r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f7]) ).
fof(f9,plain,
( ! [X160] :
( p1(X160)
| ~ r1(sK58,X160) )
& ~ p1(sK60)
& r1(sK59,sK60)
& r1(sK58,sK59)
& r1(sK57,sK58)
& r1(sK56,sK57)
& r1(sK55,sK56)
& r1(sK54,sK55)
& r1(sK0,sK54)
& ! [X151] :
( r1(X151,sK53(X151))
| ~ r1(sK0,X151) )
& ! [X145] :
( ! [X149] :
( ( ~ p1(sK52(X149))
& r1(X149,sK52(X149)) )
| ~ r1(X145,X149) )
| ! [X146] :
( ( ! [X148] :
( p1(X148)
| ~ r1(sK51(X146),X148) )
& r1(X146,sK51(X146)) )
| ~ r1(X145,X146) )
| ~ r1(sK0,X145) )
& ! [X140] :
( ! [X141] :
( ! [X144] :
( p1(X144)
| ~ r1(X141,X144) )
| ! [X142] :
( ( ~ p1(sK50(X142))
& r1(X142,sK50(X142)) )
| ~ r1(X141,X142) )
| ~ r1(X140,X141) )
| ~ r1(sK0,X140) )
& ! [X137] :
( ~ p1(X137)
| ! [X138] :
( ( p1(sK49(X138))
& r1(X138,sK49(X138)) )
| ~ r1(X137,X138) )
| ~ r1(sK0,X137) )
& ! [X136] :
( p1(X136)
| ~ r1(sK46,X136) )
& ~ p1(sK48)
& r1(sK47,sK48)
& r1(sK46,sK47)
& r1(sK45,sK46)
& r1(sK44,sK45)
& r1(sK43,sK44)
& r1(sK42,sK43)
& r1(sK0,sK42)
& ! [X126] :
( ! [X127] :
( r1(X127,sK41(X127))
| ~ r1(X126,X127) )
| ~ r1(sK0,X126) )
& ! [X119] :
( ! [X120] :
( ! [X124] :
( ( ~ p1(sK40(X124))
& r1(X124,sK40(X124)) )
| ~ r1(X120,X124) )
| ! [X121] :
( ( ! [X123] :
( p1(X123)
| ~ r1(sK39(X121),X123) )
& r1(X121,sK39(X121)) )
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(sK0,X119) )
& ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X118] :
( p1(X118)
| ~ r1(X115,X118) )
| ! [X116] :
( ( ~ p1(sK38(X116))
& r1(X116,sK38(X116)) )
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(sK0,X113) )
& ! [X109] :
( ! [X110] :
( ~ p1(X110)
| ! [X111] :
( ( p1(sK37(X111))
& r1(X111,sK37(X111)) )
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
| ~ r1(sK0,X109) )
& ! [X108] :
( p1(X108)
| ~ r1(sK34,X108) )
& ~ p1(sK36)
& r1(sK35,sK36)
& r1(sK34,sK35)
& r1(sK33,sK34)
& r1(sK32,sK33)
& r1(sK31,sK32)
& r1(sK30,sK31)
& r1(sK0,sK30)
& ! [X97] :
( ! [X98] :
( ! [X99] :
( r1(X99,sK29(X99))
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(sK0,X97) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ! [X95] :
( ( ~ p1(sK28(X95))
& r1(X95,sK28(X95)) )
| ~ r1(X91,X95) )
| ! [X92] :
( ( ! [X94] :
( p1(X94)
| ~ r1(sK27(X92),X94) )
& r1(X92,sK27(X92)) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(sK0,X89) )
& ! [X82] :
( ! [X83] :
( ! [X84] :
( ! [X85] :
( ! [X88] :
( p1(X88)
| ~ r1(X85,X88) )
| ! [X86] :
( ( ~ p1(sK26(X86))
& r1(X86,sK26(X86)) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X82,X83) )
| ~ r1(sK0,X82) )
& ! [X77] :
( ! [X78] :
( ! [X79] :
( ~ p1(X79)
| ! [X80] :
( ( p1(sK25(X80))
& r1(X80,sK25(X80)) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(sK0,X77) )
& ! [X76] :
( p1(X76)
| ~ r1(sK22,X76) )
& ~ p1(sK24)
& r1(sK23,sK24)
& r1(sK22,sK23)
& r1(sK21,sK22)
& r1(sK20,sK21)
& r1(sK19,sK20)
& r1(sK18,sK19)
& r1(sK0,sK18)
& ! [X64] :
( ! [X65] :
( ! [X66] :
( ! [X67] :
( r1(X67,sK17(X67))
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(sK0,X64) )
& ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( ! [X62] :
( ( ~ p1(sK16(X62))
& r1(X62,sK16(X62)) )
| ~ r1(X58,X62) )
| ! [X59] :
( ( ! [X61] :
( p1(X61)
| ~ r1(sK15(X59),X61) )
& r1(X59,sK15(X59)) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(sK0,X55) )
& ! [X47] :
( ! [X48] :
( ! [X49] :
( ! [X50] :
( ! [X51] :
( ! [X54] :
( p1(X54)
| ~ r1(X51,X54) )
| ! [X52] :
( ( ~ p1(sK14(X52))
& r1(X52,sK14(X52)) )
| ~ r1(X51,X52) )
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(sK0,X47) )
& ! [X41] :
( ! [X42] :
( ! [X43] :
( ! [X44] :
( ~ p1(X44)
| ! [X45] :
( ( p1(sK13(X45))
& r1(X45,sK13(X45)) )
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(sK0,X41) )
& ! [X40] :
( p1(X40)
| ~ r1(sK10,X40) )
& ~ p1(sK12)
& r1(sK11,sK12)
& r1(sK10,sK11)
& r1(sK9,sK10)
& r1(sK8,sK9)
& r1(sK7,sK8)
& r1(sK6,sK7)
& r1(sK0,sK6)
& ! [X27] :
( ! [X28] :
( ! [X29] :
( ! [X30] :
( ! [X31] :
( r1(X31,sK5(X31))
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(sK0,X27) )
& ! [X17] :
( ! [X18] :
( ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X25] :
( ( ~ p1(sK4(X25))
& r1(X25,sK4(X25)) )
| ~ r1(X21,X25) )
| ! [X22] :
( ( ! [X24] :
( p1(X24)
| ~ r1(sK3(X22),X24) )
& r1(X22,sK3(X22)) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(sK0,X17) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X16] :
( p1(X16)
| ~ r1(X13,X16) )
| ! [X14] :
( ( ~ p1(sK2(X14))
& r1(X14,sK2(X14)) )
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(sK0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ p1(X5)
| ! [X6] :
( ( p1(sK1(X6))
& r1(X6,sK1(X6)) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK58,sK59,sK60]),skolemize(X0,sK0),skolemize(X7,sK1(X6)),skolemize(X15,sK2(X14)),skolemize(X23,sK3(X22)),skolemize(X26,sK4(X25)),skolemize(X32,sK5(X31)),skolemize(X33,sK6),skolemize(X34,sK7),skolemize(X35,sK8),skolemize(X36,sK9),skolemize(X37,sK10),skolemize(X38,sK11),skolemize(X39,sK12),skolemize(X46,sK13(X45)),skolemize(X53,sK14(X52)),skolemize(X60,sK15(X59)),skolemize(X63,sK16(X62)),skolemize(X68,sK17(X67)),skolemize(X69,sK18),skolemize(X70,sK19),skolemize(X71,sK20),skolemize(X72,sK21),skolemize(X73,sK22),skolemize(X74,sK23),skolemize(X75,sK24),skolemize(X81,sK25(X80)),skolemize(X87,sK26(X86)),skolemize(X93,sK27(X92)),skolemize(X96,sK28(X95)),skolemize(X100,sK29(X99)),skolemize(X101,sK30),skolemize(X102,sK31),skolemize(X103,sK32),skolemize(X104,sK33),skolemize(X105,sK34),skolemize(X106,sK35),skolemize(X107,sK36),skolemize(X112,sK37(X111)),skolemize(X117,sK38(X116)),skolemize(X122,sK39(X121)),skolemize(X125,sK40(X124)),skolemize(X128,sK41(X127)),skolemize(X129,sK42),skolemize(X130,sK43),skolemize(X131,sK44),skolemize(X132,sK45),skolemize(X133,sK46),skolemize(X134,sK47),skolemize(X135,sK48),skolemize(X139,sK49(X138)),skolemize(X143,sK50(X142)),skolemize(X147,sK51(X146)),skolemize(X150,sK52(X149)),skolemize(X152,sK53(X151)),skolemize(X153,sK54),skolemize(X154,sK55),skolemize(X155,sK56),skolemize(X156,sK57),skolemize(X157,sK58),skolemize(X158,sK59),skolemize(X159,sK60)],[f8]) ).
fof(f10,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f11,plain,
! [X160] :
( p1(X160)
| ~ r1(sK58,X160) ),
inference(cnf_transformation,[],[f9]) ).
fof(f12,plain,
~ p1(sK60),
inference(cnf_transformation,[],[f9]) ).
fof(f13,plain,
r1(sK59,sK60),
inference(cnf_transformation,[],[f9]) ).
fof(f14,plain,
r1(sK58,sK59),
inference(cnf_transformation,[],[f9]) ).
fof(f15,plain,
r1(sK57,sK58),
inference(cnf_transformation,[],[f9]) ).
fof(f16,plain,
r1(sK56,sK57),
inference(cnf_transformation,[],[f9]) ).
fof(f17,plain,
r1(sK55,sK56),
inference(cnf_transformation,[],[f9]) ).
fof(f18,plain,
r1(sK54,sK55),
inference(cnf_transformation,[],[f9]) ).
fof(f19,plain,
r1(sK0,sK54),
inference(cnf_transformation,[],[f9]) ).
fof(f75,plain,
! [X58,X59,X56,X57,X55,X62,X61] :
( ~ p1(sK16(X62))
| ~ r1(X58,X62)
| p1(X61)
| ~ r1(sK15(X59),X61)
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(sK0,X55) ),
inference(cnf_transformation,[],[f9]) ).
fof(f76,plain,
! [X58,X59,X56,X57,X55,X62,X61] :
( r1(X62,sK16(X62))
| ~ r1(X58,X62)
| p1(X61)
| ~ r1(sK15(X59),X61)
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(sK0,X55) ),
inference(cnf_transformation,[],[f9]) ).
fof(f77,plain,
! [X58,X59,X56,X57,X55,X62] :
( ~ p1(sK16(X62))
| ~ r1(X58,X62)
| r1(X59,sK15(X59))
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(sK0,X55) ),
inference(cnf_transformation,[],[f9]) ).
fof(f78,plain,
! [X58,X59,X56,X57,X55,X62] :
( r1(X62,sK16(X62))
| ~ r1(X58,X62)
| r1(X59,sK15(X59))
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(sK0,X55) ),
inference(cnf_transformation,[],[f9]) ).
fof(f93,plain,
! [X21,X18,X19,X17,X24,X22,X25,X20] :
( ~ p1(sK4(X25))
| ~ r1(X21,X25)
| p1(X24)
| ~ r1(sK3(X22),X24)
| ~ r1(X21,X22)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(sK0,X17) ),
inference(cnf_transformation,[],[f9]) ).
fof(f94,plain,
! [X21,X18,X19,X17,X24,X22,X25,X20] :
( r1(X25,sK4(X25))
| ~ r1(X21,X25)
| p1(X24)
| ~ r1(sK3(X22),X24)
| ~ r1(X21,X22)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(sK0,X17) ),
inference(cnf_transformation,[],[f9]) ).
fof(f95,plain,
! [X21,X18,X19,X17,X22,X25,X20] :
( ~ p1(sK4(X25))
| ~ r1(X21,X25)
| r1(X22,sK3(X22))
| ~ r1(X21,X22)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(sK0,X17) ),
inference(cnf_transformation,[],[f9]) ).
fof(f96,plain,
! [X21,X18,X19,X17,X22,X25,X20] :
( r1(X25,sK4(X25))
| ~ r1(X21,X25)
| r1(X22,sK3(X22))
| ~ r1(X21,X22)
| ~ r1(X20,X21)
| ~ r1(X19,X20)
| ~ r1(X18,X19)
| ~ r1(X17,X18)
| ~ r1(sK0,X17) ),
inference(cnf_transformation,[],[f9]) ).
fof(f97,plain,
! [X10,X11,X8,X9,X16,X14,X12,X13] :
( p1(X16)
| ~ r1(X13,X16)
| ~ p1(sK2(X14))
| ~ r1(X13,X14)
| ~ r1(X12,X13)
| ~ r1(X11,X12)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(sK0,X8) ),
inference(cnf_transformation,[],[f9]) ).
fof(f98,plain,
! [X10,X11,X8,X9,X16,X14,X12,X13] :
( p1(X16)
| ~ r1(X13,X16)
| r1(X14,sK2(X14))
| ~ r1(X13,X14)
| ~ r1(X12,X13)
| ~ r1(X11,X12)
| ~ r1(X10,X11)
| ~ r1(X9,X10)
| ~ r1(X8,X9)
| ~ r1(sK0,X8) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f10]) ).
tcf(c_52,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| r1(X6,sK2(X6))
| ~ r1(sK0,X0)
| ~ r1(X5,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_53,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| ~ p1(sK2(X6))
| ~ r1(sK0,X0)
| ~ r1(X5,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_54,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( r1(X6,sK4(X6))
| r1(X5,sK3(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_55,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( r1(X5,sK3(X5))
| ~ p1(sK4(X6))
| ~ r1(sK0,X0)
| ~ r1(X4,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_56,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X1)
| r1(X7,sK4(X7))
| ~ r1(sK0,X2)
| ~ r1(X6,X7)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(sK3(X0),X1) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_57,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X1)
| ~ p1(sK4(X7))
| ~ r1(sK0,X2)
| ~ r1(X6,X7)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(sK3(X0),X1) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_72,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r1(X5,sK16(X5))
| r1(X4,sK15(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_73,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r1(X4,sK15(X4))
| ~ p1(sK16(X5))
| ~ r1(sK0,X0)
| ~ r1(X3,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_74,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X1)
| r1(X6,sK16(X6))
| ~ r1(sK0,X2)
| ~ r1(X5,X6)
| ~ r1(X5,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(sK15(X0),X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_75,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X1)
| ~ p1(sK16(X6))
| ~ r1(sK0,X2)
| ~ r1(X5,X6)
| ~ r1(X5,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(sK15(X0),X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_131,negated_conjecture,
r1(sK0,sK54),
inference(cnf_transformation,[],[f19]) ).
tcf(c_132,negated_conjecture,
r1(sK54,sK55),
inference(cnf_transformation,[],[f18]) ).
tcf(c_133,negated_conjecture,
r1(sK55,sK56),
inference(cnf_transformation,[],[f17]) ).
tcf(c_134,negated_conjecture,
r1(sK56,sK57),
inference(cnf_transformation,[],[f16]) ).
tcf(c_135,negated_conjecture,
r1(sK57,sK58),
inference(cnf_transformation,[],[f15]) ).
tcf(c_136,negated_conjecture,
r1(sK58,sK59),
inference(cnf_transformation,[],[f14]) ).
tcf(c_137,negated_conjecture,
r1(sK59,sK60),
inference(cnf_transformation,[],[f13]) ).
tcf(c_138,negated_conjecture,
~ p1(sK60),
inference(cnf_transformation,[],[f12]) ).
tcf(c_139,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ r1(sK58,X0) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_950,plain,
r1(sK58,sK58),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1385,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X5,sK2(X5))
| ~ r1(sK54,X0)
| ~ r1(X4,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_52,c_131]) ).
tcf(c_1386,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X4,sK2(X4))
| ~ r1(sK55,X0)
| ~ r1(X3,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1385,c_132]) ).
tcf(c_1388,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X3,sK2(X3))
| ~ r1(sK56,X0)
| ~ r1(X2,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1386,c_133]) ).
tcf(c_1389,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X2,sK2(X2))
| ~ r1(sK57,X0)
| ~ r1(X1,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1388,c_134]) ).
tcf(c_1413,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X1,sK2(X1))
| ~ r1(sK58,X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1389,c_135]) ).
tcf(c_1414,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(X0,sK2(X0))
| ~ r1(sK59,X1)
| ~ r1(sK59,X0) ),
inference(resolution,[status(thm)],[c_1413,c_136]) ).
tcf(c_1416,plain,
! [X0: $i] :
( p1(sK60)
| r1(X0,sK2(X0))
| ~ r1(sK59,X0) ),
inference(resolution,[status(thm)],[c_1414,c_137]) ).
tcf(c_1418,plain,
! [X0: $i] :
( ~ r1(sK59,X0)
| r1(X0,sK2(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1416,c_138,c_1416]) ).
tcf(c_1419,plain,
! [X0: $i] :
( r1(X0,sK2(X0))
| ~ r1(sK59,X0) ),
inference(renaming,[status(thm)],[c_1418]) ).
tcf(c_1445,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r1(X5,sK4(X5))
| r1(X4,sK3(X4))
| ~ r1(sK54,X0)
| ~ r1(X3,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_54,c_131]) ).
tcf(c_1446,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK4(X4))
| r1(X3,sK3(X3))
| ~ r1(sK55,X0)
| ~ r1(X2,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1445,c_132]) ).
tcf(c_1560,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK4(X3))
| r1(X2,sK3(X2))
| ~ r1(sK56,X0)
| ~ r1(X1,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1446,c_133]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK4(X2))
| r1(X1,sK3(X1))
| ~ r1(sK57,X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1560,c_134]) ).
tcf(c_1740,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK3(X1))
| r1(X0,sK4(X0))
| ~ r1(sK58,X1)
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_1598,c_135]) ).
tcf(c_1742,plain,
! [X0: $i] :
( r1(sK59,sK3(sK59))
| r1(X0,sK4(X0))
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_1740,c_136]) ).
tcf(c_1854,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK16(X4))
| r1(X3,sK15(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_72,c_131]) ).
tcf(c_1955,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK16(X3))
| r1(X2,sK15(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1854,c_132]) ).
tcf(c_1957,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK16(X2))
| r1(X1,sK15(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_1955,c_133]) ).
tcf(c_1958,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK15(X1))
| r1(X0,sK16(X0))
| ~ r1(sK57,X1)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_1957,c_134]) ).
tcf(c_1960,plain,
! [X0: $i] :
( r1(sK58,sK15(sK58))
| r1(X0,sK16(X0))
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_1958,c_135]) ).
tcf(c_2068,plain,
( r1(sK58,sK16(sK58))
| r1(sK58,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_1960,c_135]) ).
tcf(c_2069,plain,
( p1(sK16(sK58))
| r1(sK58,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_2068,c_139]) ).
tcf(c_2080,plain,
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_2069,c_1742]) ).
tcf(c_3727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X4,sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_2080,c_74]) ).
tcf(c_4208,plain,
( p1(sK16(sK58))
| ~ r1(sK58,sK16(sK58)) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_4275,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r1(sK58,sK4(sK58))
| r1(X5,sK3(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,sK58)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_4276,plain,
( p1(sK4(sK58))
| ~ r1(sK58,sK4(sK58)) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_4373,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X3,sK16(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_3727,c_131]) ).
tcf(c_4387,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X2,sK16(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4373,c_132]) ).
tcf(c_4408,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X1,sK16(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4387,c_133]) ).
tcf(c_4422,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X0,sK16(X0))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_4408,c_134]) ).
tcf(c_4433,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X0,sK16(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_4422,c_135,c_4422]) ).
tcf(c_4436,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(sK58,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_4433,c_135]) ).
tcf(c_4437,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK59,sK3(sK59)) ),
inference(global_subsumption_just,[status(thm)],[c_4436,c_4208,c_4436]) ).
tcf(c_4444,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| r1(sK3(sK59),sK2(sK3(sK59))) ),
inference(resolution,[status(thm)],[c_4437,c_1419]) ).
tcf(c_4447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X5,sK4(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4444,c_56]) ).
tcf(c_4481,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X4,sK4(X4))
| ~ r1(sK54,X0)
| ~ r1(X3,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4447,c_131]) ).
tcf(c_4499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X3,sK4(X3))
| ~ r1(sK55,X0)
| ~ r1(X2,sK59)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4481,c_132]) ).
tcf(c_4669,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X2,sK4(X2))
| ~ r1(sK56,X0)
| ~ r1(X1,sK59)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4499,c_133]) ).
tcf(c_4817,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X1,sK4(X1))
| ~ r1(sK57,X0)
| ~ r1(X0,sK59)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4669,c_134]) ).
tcf(c_4874,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK4(X0))
| ~ r1(sK58,sK59)
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_4817,c_135]) ).
tcf(c_4928,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK4(X0))
| ~ r1(sK58,X0) ),
inference(global_subsumption_just,[status(thm)],[c_4874,c_136,c_4874]) ).
tcf(c_4940,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_4928,c_2069]) ).
tcf(c_5002,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X4,sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_4940,c_74]) ).
tcf(c_5420,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X3,sK16(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5002,c_131]) ).
tcf(c_5427,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X2,sK16(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5420,c_132]) ).
tcf(c_5500,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X1,sK16(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5427,c_133]) ).
tcf(c_5502,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK16(X0))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_5500,c_134]) ).
tcf(c_5504,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK16(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5502,c_135,c_5502]) ).
tcf(c_5569,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(sK58,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_5504,c_135]) ).
tcf(c_5582,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( r1(X5,sK3(X5))
| ~ p1(sK4(sK58))
| ~ r1(sK0,X0)
| ~ r1(X4,sK58)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_5598,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59))) ),
inference(global_subsumption_just,[status(thm)],[c_5569,c_4208,c_5569]) ).
tcf(c_5603,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(X5,sK3(X5))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_5598,c_55]) ).
tcf(c_5702,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(X4,sK3(X4))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5603,c_2069]) ).
tcf(c_5724,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5702,c_136]) ).
tcf(c_5863,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5724,c_131]) ).
tcf(c_5875,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5863,c_132]) ).
tcf(c_5899,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_5875,c_133]) ).
tcf(c_5959,plain,
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_5899,c_134]) ).
tcf(c_5960,plain,
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK59,sK3(sK59)) ),
inference(global_subsumption_just,[status(thm)],[c_5959,c_135,c_5959]) ).
tcf(c_5966,plain,
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| r1(sK3(sK59),sK2(sK3(sK59))) ),
inference(resolution,[status(thm)],[c_5960,c_1419]) ).
tcf(c_5972,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ p1(sK4(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5966,c_57]) ).
tcf(c_5985,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK0,X1)
| ~ r1(X0,sK59)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_5972,c_5598]) ).
tcf(c_5994,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK58,sK59)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_5985,c_2069]) ).
tcf(c_6069,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,sK58)
| ~ r1(sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5994,c_136,c_5994]) ).
tcf(c_6070,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_6069]) ).
tcf(c_6081,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6070,c_131]) ).
tcf(c_6091,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6081,c_132]) ).
tcf(c_6107,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_6091,c_133]) ).
tcf(c_6109,plain,
( p1(sK16(sK58))
| p1(sK2(sK3(sK59)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_6107,c_134]) ).
tcf(c_6110,plain,
( p1(sK16(sK58))
| p1(sK2(sK3(sK59))) ),
inference(global_subsumption_just,[status(thm)],[c_6109,c_135,c_6109]) ).
tcf(c_6181,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| p1(sK16(sK58))
| ~ r1(sK0,X1)
| ~ r1(X5,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X6)
| ~ r1(X0,sK3(sK59)) ),
inference(resolution,[status(thm)],[c_53,c_6110]) ).
tcf(c_6183,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK59,X5)
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6181,c_4437]) ).
tcf(c_6203,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK60)
| p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6183,c_137]) ).
tcf(c_6205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK3(sK59))
| p1(sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6183,c_4437]) ).
tcf(c_6256,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK59)
| ~ r1(sK0,X0)
| p1(sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_6205,c_138,c_6203]) ).
tcf(c_6257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_6256]) ).
tcf(c_6317,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X3,sK59)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6257,c_131]) ).
tcf(c_6327,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X2,sK59)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6317,c_132]) ).
tcf(c_6342,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X1,sK59)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6327,c_133]) ).
tcf(c_6406,plain,
! [X0: $i] :
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK57,X0)
| ~ r1(X0,sK59) ),
inference(resolution,[status(thm)],[c_6342,c_134]) ).
tcf(c_6416,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58)))
| ~ r1(sK58,sK59) ),
inference(resolution,[status(thm)],[c_6406,c_135]) ).
tcf(c_6421,plain,
( p1(sK16(sK58))
| p1(sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_6416,c_136,c_6416]) ).
tcf(c_6423,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK16(sK58))
| r1(X5,sK3(X5))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_6421,c_55]) ).
tcf(c_6430,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| r1(X4,sK3(X4))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6423,c_2069]) ).
tcf(c_6440,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6430,c_136]) ).
tcf(c_6623,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6440,c_131]) ).
tcf(c_6628,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6623,c_132]) ).
tcf(c_6648,plain,
! [X0: $i] :
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_6628,c_133]) ).
tcf(c_6662,plain,
( p1(sK16(sK58))
| r1(sK59,sK3(sK59))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_6648,c_134]) ).
tcf(c_6667,plain,
( p1(sK16(sK58))
| r1(sK59,sK3(sK59)) ),
inference(global_subsumption_just,[status(thm)],[c_6662,c_135,c_6662]) ).
tcf(c_6675,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| p1(sK16(sK58))
| ~ r1(sK59,X5)
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6667,c_6181]) ).
tcf(c_6769,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK60)
| p1(sK16(sK58))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6675,c_137]) ).
tcf(c_6773,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| p1(sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6675,c_6667]) ).
tcf(c_6819,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK59)
| ~ r1(sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_6773,c_138,c_6769]) ).
tcf(c_6820,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK16(sK58))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_6819]) ).
tcf(c_6822,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK16(sK58))
| ~ r1(sK54,X0)
| ~ r1(X3,sK59)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6820,c_131]) ).
tcf(c_6995,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK16(sK58))
| ~ r1(sK55,X0)
| ~ r1(X2,sK59)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6822,c_132]) ).
tcf(c_7015,plain,
! [X0: $i,X1: $i] :
( p1(sK16(sK58))
| ~ r1(sK56,X0)
| ~ r1(X1,sK59)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_6995,c_133]) ).
tcf(c_7017,plain,
! [X0: $i] :
( p1(sK16(sK58))
| ~ r1(sK57,X0)
| ~ r1(X0,sK59) ),
inference(resolution,[status(thm)],[c_7015,c_134]) ).
tcf(c_7019,plain,
( p1(sK16(sK58))
| ~ r1(sK58,sK59) ),
inference(resolution,[status(thm)],[c_7017,c_135]) ).
tcf(c_7024,plain,
p1(sK16(sK58)),
inference(global_subsumption_just,[status(thm)],[c_7019,c_136,c_7019]) ).
tcf(c_7026,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK15(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7024,c_73]) ).
tcf(c_7042,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK15(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7026,c_131]) ).
tcf(c_7053,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK15(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7042,c_132]) ).
tcf(c_7073,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK15(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7053,c_133]) ).
tcf(c_7084,plain,
! [X0: $i] :
( r1(X0,sK15(X0))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_7073,c_134]) ).
tcf(c_7091,plain,
! [X0: $i] :
( r1(X0,sK15(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7084,c_135,c_7084]) ).
tcf(c_7099,plain,
r1(sK58,sK15(sK58)),
inference(resolution,[status(thm)],[c_7091,c_135]) ).
tcf(c_7265,plain,
! [X0: $i] :
( r1(X0,sK4(X0))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_7099,c_1740]) ).
tcf(c_7302,plain,
( r1(sK15(sK58),sK4(sK15(sK58)))
| r1(sK15(sK58),sK3(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_7265,c_7099]) ).
tcf(c_7309,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| r1(X4,sK16(X4))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7302,c_74]) ).
tcf(c_7329,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| r1(X3,sK16(X3))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7309,c_131]) ).
tcf(c_7343,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| r1(X2,sK16(X2))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7329,c_132]) ).
tcf(c_7351,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| r1(X1,sK16(X1))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7343,c_133]) ).
tcf(c_7361,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| r1(X0,sK16(X0))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_7351,c_134]) ).
tcf(c_7371,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| r1(X0,sK16(X0))
| r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7361,c_135,c_7361]) ).
tcf(c_7377,plain,
( p1(sK4(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(sK15(sK58),sK3(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_7371,c_135]) ).
tcf(c_7378,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X4,sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7377,c_74]) ).
tcf(c_7400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X3,sK16(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7378,c_131]) ).
tcf(c_7581,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X2,sK16(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7400,c_132]) ).
tcf(c_7595,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X1,sK16(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7581,c_133]) ).
tcf(c_7605,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X0,sK16(X0))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_7595,c_134]) ).
tcf(c_7615,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58))
| r1(X0,sK16(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7605,c_135,c_7605]) ).
tcf(c_7622,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_7615,c_135]) ).
tcf(c_7628,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X1)
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_7622,c_1413]) ).
tcf(c_7634,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X0,sK4(X0))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_7622,c_1740]) ).
tcf(c_7658,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_7634,c_7099]) ).
tcf(c_7680,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X0,sK2(X0))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_7628,c_7658]) ).
tcf(c_7693,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| r1(sK3(sK16(sK58)),sK2(sK3(sK16(sK58)))) ),
inference(resolution,[status(thm)],[c_7680,c_7658]) ).
tcf(c_7706,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X5,sK4(X5))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_7693,c_56]) ).
tcf(c_7896,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X4,sK4(X4))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7706,c_7622]) ).
tcf(c_7909,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7896,c_7099]) ).
tcf(c_7912,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK16(sK58),sK4(sK16(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7896,c_7622]) ).
tcf(c_7947,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,sK58)
| ~ r1(sK0,X0)
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_7912,c_7909]) ).
tcf(c_7948,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_7947]) ).
tcf(c_7955,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7948,c_131]) ).
tcf(c_8039,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_7955,c_132]) ).
tcf(c_8067,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_8039,c_133]) ).
tcf(c_8081,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_8067,c_134]) ).
tcf(c_8086,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_8081,c_135,c_8081]) ).
tcf(c_8097,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ p1(sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8086,c_75]) ).
tcf(c_8344,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8097,c_7024]) ).
tcf(c_8362,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8344,c_131]) ).
tcf(c_8460,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8362,c_132]) ).
tcf(c_8480,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_8460,c_133]) ).
tcf(c_8489,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_8480,c_134]) ).
tcf(c_8496,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK16(sK58)))) ),
inference(global_subsumption_just,[status(thm)],[c_8489,c_135,c_8489]) ).
tcf(c_8498,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK0,X1)
| ~ r1(X5,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X6)
| ~ r1(X0,sK3(sK16(sK58))) ),
inference(resolution,[status(thm)],[c_8496,c_53]) ).
tcf(c_8510,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X0)
| p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X2)
| ~ r1(X5,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,sK16(sK58))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_8498,c_7658]) ).
tcf(c_8528,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X0)
| p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X1)
| ~ r1(X4,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_8510,c_7622]) ).
tcf(c_8602,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8528,c_7658]) ).
tcf(c_8624,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8602,c_131]) ).
tcf(c_8644,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8624,c_132]) ).
tcf(c_8665,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_8644,c_133]) ).
tcf(c_8672,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_8665,c_134]) ).
tcf(c_8678,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_8672,c_135,c_8672]) ).
tcf(c_8686,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ p1(sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8678,c_75]) ).
tcf(c_8732,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK3(X4))
| ~ p1(sK4(sK58))
| ~ r1(sK58,sK58)
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5582]) ).
tcf(c_8891,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8686,c_7024]) ).
tcf(c_8979,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8891,c_131]) ).
tcf(c_9070,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_8979,c_132]) ).
tcf(c_9081,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(sK58,sK4(sK58))
| r1(X4,sK3(X4))
| ~ r1(sK58,sK58)
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4275]) ).
tcf(c_9126,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_9070,c_133]) ).
tcf(c_9250,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_9126,c_134]) ).
tcf(c_9251,plain,
( p1(sK4(sK15(sK58)))
| p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_9250,c_135,c_9250]) ).
tcf(c_9253,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X5,sK3(X5))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_9251,c_55]) ).
tcf(c_9328,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK3(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(X4,sK3(X4))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9253,c_7099]) ).
tcf(c_9367,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK3(X4))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_9328,c_950,c_4276,c_8732,c_9081]) ).
tcf(c_9370,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9367,c_136]) ).
tcf(c_9372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9367,c_7099]) ).
tcf(c_9598,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9372,c_131]) ).
tcf(c_9600,plain,
! [X0: $i,X1: $i] :
( r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9598,c_132]) ).
tcf(c_9610,plain,
! [X0: $i] :
( r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_9600,c_133]) ).
tcf(c_9622,plain,
( r1(sK15(sK58),sK3(sK15(sK58)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_9610,c_134]) ).
tcf(c_9672,plain,
r1(sK15(sK58),sK3(sK15(sK58))),
inference(global_subsumption_just,[status(thm)],[c_9622,c_135,c_9622]) ).
tcf(c_9682,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK3(sK15(sK58)))
| r1(X4,sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9672,c_74]) ).
tcf(c_9751,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK3(sK15(sK58)))
| r1(X3,sK16(X3))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9682,c_131]) ).
tcf(c_9768,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK3(sK15(sK58)))
| r1(X2,sK16(X2))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9751,c_132]) ).
tcf(c_9837,plain,
! [X0: $i,X1: $i] :
( p1(sK3(sK15(sK58)))
| r1(X1,sK16(X1))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9768,c_133]) ).
tcf(c_9851,plain,
! [X0: $i] :
( p1(sK3(sK15(sK58)))
| r1(X0,sK16(X0))
| ~ r1(sK57,sK58)
| ~ r1(sK57,X0) ),
inference(resolution,[status(thm)],[c_9837,c_134]) ).
tcf(c_9937,plain,
! [X0: $i] :
( p1(sK3(sK15(sK58)))
| r1(X0,sK16(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_9851,c_135,c_9851]) ).
tcf(c_9940,plain,
( p1(sK3(sK15(sK58)))
| r1(sK58,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_9937,c_135]) ).
tcf(c_9942,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK3(sK15(sK58)))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X1)
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_9940,c_1413]) ).
tcf(c_9943,plain,
( p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(sK16(sK58),sK4(sK16(sK58))) ),
inference(resolution,[status(thm)],[c_9940,c_1742]) ).
tcf(c_9956,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9940,c_9367]) ).
tcf(c_10037,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_9956,c_131]) ).
tcf(c_10080,plain,
! [X0: $i,X1: $i] :
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_10037,c_132]) ).
tcf(c_10221,plain,
! [X0: $i] :
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_10080,c_133]) ).
tcf(c_10223,plain,
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_10221,c_134]) ).
tcf(c_10224,plain,
( p1(sK3(sK15(sK58)))
| r1(sK16(sK58),sK3(sK16(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_10223,c_135,c_10223]) ).
tcf(c_11343,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_9943,c_7628]) ).
tcf(c_11344,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_9943,c_9942]) ).
tcf(c_11465,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| ~ r1(sK16(sK58),X0)
| r1(X0,sK2(X0))
| r1(sK59,sK3(sK59))
| p1(sK3(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_11343,c_11344]) ).
tcf(c_11466,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(renaming,[status(thm)],[c_11465]) ).
tcf(c_11473,plain,
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| r1(sK3(sK16(sK58)),sK2(sK3(sK16(sK58)))) ),
inference(resolution,[status(thm)],[c_11466,c_10224]) ).
tcf(c_11474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| p1(sK2(sK3(sK16(sK58))))
| ~ p1(sK4(X5))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_11473,c_57]) ).
tcf(c_11620,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| r1(sK59,sK3(sK59))
| p1(sK2(sK3(sK16(sK58))))
| ~ p1(sK4(X4))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11474,c_9940]) ).
tcf(c_11622,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,sK58)
| ~ r1(sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_11620,c_9370]) ).
tcf(c_11623,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_11622]) ).
tcf(c_11624,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11623,c_131]) ).
tcf(c_11669,plain,
! [X0: $i,X1: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11624,c_132]) ).
tcf(c_11673,plain,
! [X0: $i] :
( r1(sK59,sK3(sK59))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_11669,c_133]) ).
tcf(c_11675,plain,
( r1(sK59,sK3(sK59))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_11673,c_134]) ).
tcf(c_11676,plain,
r1(sK59,sK3(sK59)),
inference(global_subsumption_just,[status(thm)],[c_11675,c_135,c_11675]) ).
tcf(c_11678,plain,
r1(sK3(sK59),sK2(sK3(sK59))),
inference(resolution,[status(thm)],[c_11676,c_1419]) ).
tcf(c_11683,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK2(sK3(sK59)))
| ~ p1(sK4(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11678,c_57]) ).
tcf(c_11684,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK2(sK3(sK59)))
| r1(X5,sK4(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11678,c_56]) ).
tcf(c_11788,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK2(sK3(sK59)))
| r1(X4,sK4(X4))
| ~ r1(sK54,X0)
| ~ r1(X3,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11684,c_131]) ).
tcf(c_11879,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK2(sK3(sK59)))
| r1(X3,sK4(X3))
| ~ r1(sK55,X0)
| ~ r1(X2,sK59)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11788,c_132]) ).
tcf(c_11948,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK2(sK3(sK59)))
| r1(X2,sK4(X2))
| ~ r1(sK56,X0)
| ~ r1(X1,sK59)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11879,c_133]) ).
tcf(c_11950,plain,
! [X0: $i,X1: $i] :
( p1(sK2(sK3(sK59)))
| r1(X1,sK4(X1))
| ~ r1(sK57,X0)
| ~ r1(X0,sK59)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_11948,c_134]) ).
tcf(c_11952,plain,
! [X0: $i] :
( p1(sK2(sK3(sK59)))
| r1(X0,sK4(X0))
| ~ r1(sK58,sK59)
| ~ r1(sK58,X0) ),
inference(resolution,[status(thm)],[c_11950,c_135]) ).
tcf(c_11954,plain,
! [X0: $i] :
( p1(sK2(sK3(sK59)))
| r1(X0,sK4(X0))
| ~ r1(sK58,X0) ),
inference(global_subsumption_just,[status(thm)],[c_11952,c_136,c_11952]) ).
tcf(c_11958,plain,
( p1(sK2(sK3(sK59)))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(resolution,[status(thm)],[c_11954,c_7099]) ).
tcf(c_11959,plain,
( p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(sK16(sK58),sK4(sK16(sK58))) ),
inference(resolution,[status(thm)],[c_11954,c_9940]) ).
tcf(c_12029,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK4(sK15(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_11959,c_7628]) ).
tcf(c_12030,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(resolution,[status(thm)],[c_11959,c_9942]) ).
tcf(c_12144,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| ~ r1(sK16(sK58),X0)
| r1(X0,sK2(X0))
| p1(sK2(sK3(sK59)))
| p1(sK3(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_12029,c_12030]) ).
tcf(c_12145,plain,
! [X0: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X0,sK2(X0))
| ~ r1(sK16(sK58),X0) ),
inference(renaming,[status(thm)],[c_12144]) ).
tcf(c_12153,plain,
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(sK3(sK16(sK58)),sK2(sK3(sK16(sK58)))) ),
inference(resolution,[status(thm)],[c_12145,c_10224]) ).
tcf(c_12222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X5,sK4(X5))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X5)
| ~ r1(X0,sK16(sK58)) ),
inference(resolution,[status(thm)],[c_12153,c_56]) ).
tcf(c_12333,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| r1(X4,sK4(X4))
| p1(sK2(sK3(sK16(sK58))))
| ~ r1(sK58,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_12222,c_9940]) ).
tcf(c_12402,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK16(sK58)))
| p1(sK3(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| p1(sK2(sK3(sK16(sK58))))
| r1(sK15(sK58),sK4(sK15(sK58)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_12333,c_7099]) ).
tcf(c_12407,plain,
( p1(sK2(sK3(sK59)))
| r1(sK15(sK58),sK4(sK15(sK58))) ),
inference(global_subsumption_just,[status(thm)],[c_12402,c_11958]) ).
tcf(c_12410,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ p1(sK16(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_12407,c_75]) ).
tcf(c_14094,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_12410,c_7024]) ).
tcf(c_14096,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_14094,c_131]) ).
tcf(c_14225,plain,
! [X0: $i,X1: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_14096,c_132]) ).
tcf(c_14229,plain,
! [X0: $i] :
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_14225,c_133]) ).
tcf(c_14231,plain,
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_14229,c_134]) ).
tcf(c_14410,plain,
( p1(sK4(sK15(sK58)))
| p1(sK2(sK3(sK59))) ),
inference(global_subsumption_just,[status(thm)],[c_14231,c_135,c_14231]) ).
tcf(c_14414,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK0,X1)
| ~ r1(X0,sK59)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,sK15(sK58)) ),
inference(resolution,[status(thm)],[c_14410,c_11683]) ).
tcf(c_15588,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK58,sK59)
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_14414,c_7099]) ).
tcf(c_15590,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,sK58)
| ~ r1(sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_15588,c_136,c_15588]) ).
tcf(c_15591,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK0,X0)
| ~ r1(X3,sK58)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_15590]) ).
tcf(c_15593,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK54,X0)
| ~ r1(X2,sK58)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15591,c_131]) ).
tcf(c_15717,plain,
! [X0: $i,X1: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK55,X0)
| ~ r1(X1,sK58)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15593,c_132]) ).
tcf(c_15721,plain,
! [X0: $i] :
( p1(sK2(sK3(sK59)))
| ~ r1(sK56,X0)
| ~ r1(X0,sK58) ),
inference(resolution,[status(thm)],[c_15717,c_133]) ).
tcf(c_15778,plain,
( p1(sK2(sK3(sK59)))
| ~ r1(sK57,sK58) ),
inference(resolution,[status(thm)],[c_15721,c_134]) ).
tcf(c_15779,plain,
p1(sK2(sK3(sK59))),
inference(global_subsumption_just,[status(thm)],[c_15778,c_135,c_15778]) ).
tcf(c_15781,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| ~ r1(sK0,X1)
| ~ r1(X5,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X6)
| ~ r1(X0,sK3(sK59)) ),
inference(resolution,[status(thm)],[c_15779,c_53]) ).
tcf(c_15783,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| ~ r1(sK59,X5)
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15781,c_11676]) ).
tcf(c_15850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK60)
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15783,c_137]) ).
tcf(c_15852,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(sK3(sK59))
| ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15783,c_11676]) ).
tcf(c_15863,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK59)
| ~ r1(sK0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_15852,c_138,c_15850]) ).
tcf(c_15864,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ r1(sK0,X0)
| ~ r1(X4,sK59)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(renaming,[status(thm)],[c_15863]) ).
tcf(c_15881,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ r1(sK54,X0)
| ~ r1(X3,sK59)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15864,c_131]) ).
tcf(c_15900,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ r1(sK55,X0)
| ~ r1(X2,sK59)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15881,c_132]) ).
tcf(c_15996,plain,
! [X0: $i,X1: $i] :
( ~ r1(sK56,X0)
| ~ r1(X1,sK59)
| ~ r1(X0,X1) ),
inference(resolution,[status(thm)],[c_15900,c_133]) ).
tcf(c_16003,plain,
! [X0: $i] :
( ~ r1(sK57,X0)
| ~ r1(X0,sK59) ),
inference(resolution,[status(thm)],[c_15996,c_134]) ).
tcf(c_16011,plain,
~ r1(sK58,sK59),
inference(resolution,[status(thm)],[c_16003,c_135]) ).
tcf(c_16012,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_16011,c_136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL654+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.19/0.45 % Computer : n002.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Thu Sep 24 00:03:19 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.23/0.51 Running first-order theorem proving
% 0.23/0.51 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.23/0.53
% 0.23/0.53 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.53
% 0.23/0.53 % Detected problem language: tptp
% 0.23/0.55 % Proving...
% 40.51/12.29 % SZS status Started for theBenchmark.p
% 40.51/12.29 % SZS status Theorem for theBenchmark.p
% 40.51/12.29
% 40.51/12.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 40.51/12.29
% 40.51/12.29 % ------ iProver source info
% 40.51/12.29
% 40.51/12.29 % git: date: 2026-07-19 20:42:38 +0200
% 40.51/12.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 40.51/12.29 % git: non_committed_changes: false
% 40.51/12.29
% 40.51/12.29 % ------ Parsing...
% 40.51/12.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 40.51/12.29
% 40.51/12.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 40.51/12.29
% 40.51/12.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 40.51/12.29 % ------ Proving...
% 40.51/12.29 % ------ Problem Properties
% 40.51/12.29
% 40.51/12.29 %
% 40.51/12.29 % clauses 91
% 40.51/12.29 % conjectures 90
% 40.51/12.29 % EPR 46
% 40.51/12.29 % Horn 76
% 40.51/12.29 % unary 41
% 40.51/12.29 % binary 6
% 40.51/12.29 % lits 361
% 40.51/12.29 % lits eq 0
% 40.51/12.29 % fd_pure 0
% 40.51/12.29 % fd_pseudo 0
% 40.51/12.29 % fd_cond 0
% 40.51/12.29 % fd_pseudo_cond 0
% 40.51/12.29 % AC symbols 0
% 40.51/12.29
% 40.51/12.29 % ------ Input Options Time Limit: Unbounded
% 40.51/12.29
% 40.51/12.29
% 40.51/12.29 % ------
% 40.51/12.29 % Current options:
% 40.51/12.29 % ------
% 40.51/12.29
% 40.51/12.29
% 40.51/12.29 %
% 40.51/12.29
% 40.51/12.29 % ------ Proving...
% 40.51/12.29 %
% 40.51/12.29
% 40.51/12.29 % SZS status Theorem for theBenchmark.p
% 40.51/12.29
% 40.51/12.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 82.64/12.30
% 82.64/12.30
%------------------------------------------------------------------------------