%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LCL662+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 : Thu Sep 24 01:15:50 PM UTC 2026
% Result : Theorem 0.20s 15.80s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 2
% Syntax : Number of formulae : 38 ( 5 unt; 0 def)
% Number of atoms : 1348 ( 0 equ)
% Maximal formula atoms : 416 ( 35 avg)
% Number of connectives : 2885 (1575 ~;1227 |; 83 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 203 ( 19 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 1 con; 0-13 aty)
% Number of variables : 972 ( 0 sgn 696 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X1] :
~ ( p1(X1)
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(reflexivity,axiom,
! [X1] : r1(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(c_0_2,negated_conjecture,
~ ~ ? [X1] :
~ ( p1(X1)
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(c_0_3,negated_conjecture,
~ ~ ? [X1] :
~ ( p1(X1)
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ( ~ p2(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ ( ~ p2(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[c_0_2]) ).
fof(c_0_4,negated_conjecture,
! [X5,X6,X7,X8,X10,X11,X12,X14,X15,X16,X18,X19,X20,X22,X23,X24,X25,X26,X27,X29,X30,X31,X33,X34,X35,X37,X38,X39,X40,X42,X43,X44,X45,X46,X47,X48,X50,X51,X52,X54,X55,X56,X58,X59,X60,X61,X63,X64,X65,X66,X67,X68,X69,X71,X72,X73,X75,X76,X77,X79,X80,X81,X82,X84,X85,X86,X87,X88,X89,X91,X92,X93,X95,X96,X97,X98,X100,X101,X102,X103,X104,X105,X107,X108,X109,X111,X112,X113,X114,X116,X117,X118,X119,X120,X121,X123,X124,X125,X127,X128,X129,X130,X132,X133,X134,X135,X136,X138,X139,X140,X141,X143,X144,X145,X146,X147,X149,X150,X151,X152,X154,X155,X156,X157,X158,X160,X161,X162,X163,X165,X166,X167,X168,X169,X171,X172,X173,X174,X175,X177,X178,X179,X180,X181,X183,X184,X185,X186] :
( ~ p1(esk1_0)
& ( p1(esk1_0)
| ~ r1(esk1_0,X181)
| ~ p2(X186)
| ~ r1(X185,X186)
| ~ r1(X184,X185)
| ~ r1(X183,X184)
| ~ r1(esk35_1(X181),X183) )
& ( p1(esk1_0)
| ~ r1(esk1_0,X181)
| r1(X181,esk35_1(X181)) )
& ( p1(esk1_0)
| ~ r1(esk1_0,X175)
| ~ p1(X180)
| ~ r1(X179,X180)
| ~ r1(X178,X179)
| ~ r1(X177,X178)
| ~ r1(esk34_1(X175),X177) )
& ( p1(esk1_0)
| ~ r1(esk1_0,X175)
| r1(X175,esk34_1(X175)) )
& ( p2(esk1_0)
| ~ r1(esk1_0,X169)
| ~ p1(X174)
| ~ r1(X173,X174)
| ~ r1(X172,X173)
| ~ r1(X171,X172)
| ~ r1(esk33_1(X169),X171) )
& ( p2(esk1_0)
| ~ r1(esk1_0,X169)
| r1(X169,esk33_1(X169)) )
& ( ~ r1(esk1_0,X158)
| ~ r1(esk31_1(X158),X160)
| ~ r1(X160,X161)
| ~ r1(X161,X162)
| p1(X162)
| ~ r1(X162,X163)
| ~ p2(X168)
| ~ r1(X167,X168)
| ~ r1(X166,X167)
| ~ r1(X165,X166)
| ~ r1(esk32_5(X158,X160,X161,X162,X163),X165) )
& ( ~ r1(esk1_0,X158)
| ~ r1(esk31_1(X158),X160)
| ~ r1(X160,X161)
| ~ r1(X161,X162)
| p1(X162)
| ~ r1(X162,X163)
| r1(X163,esk32_5(X158,X160,X161,X162,X163)) )
& ( ~ r1(esk1_0,X158)
| r1(X158,esk31_1(X158)) )
& ( ~ r1(esk1_0,X147)
| ~ r1(esk29_1(X147),X149)
| ~ r1(X149,X150)
| ~ r1(X150,X151)
| p1(X151)
| ~ r1(X151,X152)
| ~ p1(X157)
| ~ r1(X156,X157)
| ~ r1(X155,X156)
| ~ r1(X154,X155)
| ~ r1(esk30_5(X147,X149,X150,X151,X152),X154) )
& ( ~ r1(esk1_0,X147)
| ~ r1(esk29_1(X147),X149)
| ~ r1(X149,X150)
| ~ r1(X150,X151)
| p1(X151)
| ~ r1(X151,X152)
| r1(X152,esk30_5(X147,X149,X150,X151,X152)) )
& ( ~ r1(esk1_0,X147)
| r1(X147,esk29_1(X147)) )
& ( ~ r1(esk1_0,X136)
| ~ r1(esk27_1(X136),X138)
| ~ r1(X138,X139)
| ~ r1(X139,X140)
| p2(X140)
| ~ r1(X140,X141)
| ~ p1(X146)
| ~ r1(X145,X146)
| ~ r1(X144,X145)
| ~ r1(X143,X144)
| ~ r1(esk28_5(X136,X138,X139,X140,X141),X143) )
& ( ~ r1(esk1_0,X136)
| ~ r1(esk27_1(X136),X138)
| ~ r1(X138,X139)
| ~ r1(X139,X140)
| p2(X140)
| ~ r1(X140,X141)
| r1(X141,esk28_5(X136,X138,X139,X140,X141)) )
& ( ~ r1(esk1_0,X136)
| r1(X136,esk27_1(X136)) )
& ( ~ r1(esk1_0,X120)
| ~ r1(X120,X121)
| ~ r1(esk24_2(X120,X121),X123)
| ~ r1(X123,X124)
| ~ r1(X124,X125)
| ~ r1(esk25_5(X120,X121,X123,X124,X125),X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| p1(X129)
| ~ r1(X129,X130)
| ~ p2(X135)
| ~ r1(X134,X135)
| ~ r1(X133,X134)
| ~ r1(X132,X133)
| ~ r1(esk26_9(X120,X121,X123,X124,X125,X127,X128,X129,X130),X132) )
& ( ~ r1(esk1_0,X120)
| ~ r1(X120,X121)
| ~ r1(esk24_2(X120,X121),X123)
| ~ r1(X123,X124)
| ~ r1(X124,X125)
| ~ r1(esk25_5(X120,X121,X123,X124,X125),X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| p1(X129)
| ~ r1(X129,X130)
| r1(X130,esk26_9(X120,X121,X123,X124,X125,X127,X128,X129,X130)) )
& ( ~ r1(esk1_0,X120)
| ~ r1(X120,X121)
| ~ r1(esk24_2(X120,X121),X123)
| ~ r1(X123,X124)
| ~ r1(X124,X125)
| r1(X125,esk25_5(X120,X121,X123,X124,X125)) )
& ( ~ r1(esk1_0,X120)
| ~ r1(X120,X121)
| r1(X121,esk24_2(X120,X121)) )
& ( ~ r1(esk1_0,X104)
| ~ r1(X104,X105)
| ~ r1(esk21_2(X104,X105),X107)
| ~ r1(X107,X108)
| ~ r1(X108,X109)
| ~ r1(esk22_5(X104,X105,X107,X108,X109),X111)
| ~ r1(X111,X112)
| ~ r1(X112,X113)
| p1(X113)
| ~ r1(X113,X114)
| ~ p1(X119)
| ~ r1(X118,X119)
| ~ r1(X117,X118)
| ~ r1(X116,X117)
| ~ r1(esk23_9(X104,X105,X107,X108,X109,X111,X112,X113,X114),X116) )
& ( ~ r1(esk1_0,X104)
| ~ r1(X104,X105)
| ~ r1(esk21_2(X104,X105),X107)
| ~ r1(X107,X108)
| ~ r1(X108,X109)
| ~ r1(esk22_5(X104,X105,X107,X108,X109),X111)
| ~ r1(X111,X112)
| ~ r1(X112,X113)
| p1(X113)
| ~ r1(X113,X114)
| r1(X114,esk23_9(X104,X105,X107,X108,X109,X111,X112,X113,X114)) )
& ( ~ r1(esk1_0,X104)
| ~ r1(X104,X105)
| ~ r1(esk21_2(X104,X105),X107)
| ~ r1(X107,X108)
| ~ r1(X108,X109)
| r1(X109,esk22_5(X104,X105,X107,X108,X109)) )
& ( ~ r1(esk1_0,X104)
| ~ r1(X104,X105)
| r1(X105,esk21_2(X104,X105)) )
& ( ~ r1(esk1_0,X88)
| ~ r1(X88,X89)
| ~ r1(esk18_2(X88,X89),X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(esk19_5(X88,X89,X91,X92,X93),X95)
| ~ r1(X95,X96)
| ~ r1(X96,X97)
| p2(X97)
| ~ r1(X97,X98)
| ~ p1(X103)
| ~ r1(X102,X103)
| ~ r1(X101,X102)
| ~ r1(X100,X101)
| ~ r1(esk20_9(X88,X89,X91,X92,X93,X95,X96,X97,X98),X100) )
& ( ~ r1(esk1_0,X88)
| ~ r1(X88,X89)
| ~ r1(esk18_2(X88,X89),X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(esk19_5(X88,X89,X91,X92,X93),X95)
| ~ r1(X95,X96)
| ~ r1(X96,X97)
| p2(X97)
| ~ r1(X97,X98)
| r1(X98,esk20_9(X88,X89,X91,X92,X93,X95,X96,X97,X98)) )
& ( ~ r1(esk1_0,X88)
| ~ r1(X88,X89)
| ~ r1(esk18_2(X88,X89),X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| r1(X93,esk19_5(X88,X89,X91,X92,X93)) )
& ( ~ r1(esk1_0,X88)
| ~ r1(X88,X89)
| r1(X89,esk18_2(X88,X89)) )
& ( ~ r1(esk1_0,X67)
| ~ r1(X67,X68)
| ~ r1(X68,X69)
| ~ r1(esk14_3(X67,X68,X69),X71)
| ~ r1(X71,X72)
| ~ r1(X72,X73)
| ~ r1(esk15_6(X67,X68,X69,X71,X72,X73),X75)
| ~ r1(X75,X76)
| ~ r1(X76,X77)
| ~ r1(esk16_9(X67,X68,X69,X71,X72,X73,X75,X76,X77),X79)
| ~ r1(X79,X80)
| ~ r1(X80,X81)
| p1(X81)
| ~ r1(X81,X82)
| ~ p2(X87)
| ~ r1(X86,X87)
| ~ r1(X85,X86)
| ~ r1(X84,X85)
| ~ r1(esk17_13(X67,X68,X69,X71,X72,X73,X75,X76,X77,X79,X80,X81,X82),X84) )
& ( ~ r1(esk1_0,X67)
| ~ r1(X67,X68)
| ~ r1(X68,X69)
| ~ r1(esk14_3(X67,X68,X69),X71)
| ~ r1(X71,X72)
| ~ r1(X72,X73)
| ~ r1(esk15_6(X67,X68,X69,X71,X72,X73),X75)
| ~ r1(X75,X76)
| ~ r1(X76,X77)
| ~ r1(esk16_9(X67,X68,X69,X71,X72,X73,X75,X76,X77),X79)
| ~ r1(X79,X80)
| ~ r1(X80,X81)
| p1(X81)
| ~ r1(X81,X82)
| r1(X82,esk17_13(X67,X68,X69,X71,X72,X73,X75,X76,X77,X79,X80,X81,X82)) )
& ( ~ r1(esk1_0,X67)
| ~ r1(X67,X68)
| ~ r1(X68,X69)
| ~ r1(esk14_3(X67,X68,X69),X71)
| ~ r1(X71,X72)
| ~ r1(X72,X73)
| ~ r1(esk15_6(X67,X68,X69,X71,X72,X73),X75)
| ~ r1(X75,X76)
| ~ r1(X76,X77)
| r1(X77,esk16_9(X67,X68,X69,X71,X72,X73,X75,X76,X77)) )
& ( ~ r1(esk1_0,X67)
| ~ r1(X67,X68)
| ~ r1(X68,X69)
| ~ r1(esk14_3(X67,X68,X69),X71)
| ~ r1(X71,X72)
| ~ r1(X72,X73)
| r1(X73,esk15_6(X67,X68,X69,X71,X72,X73)) )
& ( ~ r1(esk1_0,X67)
| ~ r1(X67,X68)
| ~ r1(X68,X69)
| r1(X69,esk14_3(X67,X68,X69)) )
& ( ~ r1(esk1_0,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(esk10_3(X46,X47,X48),X50)
| ~ r1(X50,X51)
| ~ r1(X51,X52)
| ~ r1(esk11_6(X46,X47,X48,X50,X51,X52),X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(esk12_9(X46,X47,X48,X50,X51,X52,X54,X55,X56),X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| ~ r1(X60,X61)
| ~ p1(X66)
| ~ r1(X65,X66)
| ~ r1(X64,X65)
| ~ r1(X63,X64)
| ~ r1(esk13_13(X46,X47,X48,X50,X51,X52,X54,X55,X56,X58,X59,X60,X61),X63) )
& ( ~ r1(esk1_0,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(esk10_3(X46,X47,X48),X50)
| ~ r1(X50,X51)
| ~ r1(X51,X52)
| ~ r1(esk11_6(X46,X47,X48,X50,X51,X52),X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(esk12_9(X46,X47,X48,X50,X51,X52,X54,X55,X56),X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| ~ r1(X60,X61)
| r1(X61,esk13_13(X46,X47,X48,X50,X51,X52,X54,X55,X56,X58,X59,X60,X61)) )
& ( ~ r1(esk1_0,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(esk10_3(X46,X47,X48),X50)
| ~ r1(X50,X51)
| ~ r1(X51,X52)
| ~ r1(esk11_6(X46,X47,X48,X50,X51,X52),X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| r1(X56,esk12_9(X46,X47,X48,X50,X51,X52,X54,X55,X56)) )
& ( ~ r1(esk1_0,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(esk10_3(X46,X47,X48),X50)
| ~ r1(X50,X51)
| ~ r1(X51,X52)
| r1(X52,esk11_6(X46,X47,X48,X50,X51,X52)) )
& ( ~ r1(esk1_0,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| r1(X48,esk10_3(X46,X47,X48)) )
& ( ~ r1(esk1_0,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(esk6_3(X25,X26,X27),X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(esk7_6(X25,X26,X27,X29,X30,X31),X33)
| ~ r1(X33,X34)
| ~ r1(X34,X35)
| ~ r1(esk8_9(X25,X26,X27,X29,X30,X31,X33,X34,X35),X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| p2(X39)
| ~ r1(X39,X40)
| ~ p1(X45)
| ~ r1(X44,X45)
| ~ r1(X43,X44)
| ~ r1(X42,X43)
| ~ r1(esk9_13(X25,X26,X27,X29,X30,X31,X33,X34,X35,X37,X38,X39,X40),X42) )
& ( ~ r1(esk1_0,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(esk6_3(X25,X26,X27),X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(esk7_6(X25,X26,X27,X29,X30,X31),X33)
| ~ r1(X33,X34)
| ~ r1(X34,X35)
| ~ r1(esk8_9(X25,X26,X27,X29,X30,X31,X33,X34,X35),X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| p2(X39)
| ~ r1(X39,X40)
| r1(X40,esk9_13(X25,X26,X27,X29,X30,X31,X33,X34,X35,X37,X38,X39,X40)) )
& ( ~ r1(esk1_0,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(esk6_3(X25,X26,X27),X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(esk7_6(X25,X26,X27,X29,X30,X31),X33)
| ~ r1(X33,X34)
| ~ r1(X34,X35)
| r1(X35,esk8_9(X25,X26,X27,X29,X30,X31,X33,X34,X35)) )
& ( ~ r1(esk1_0,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(esk6_3(X25,X26,X27),X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| r1(X31,esk7_6(X25,X26,X27,X29,X30,X31)) )
& ( ~ r1(esk1_0,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| r1(X27,esk6_3(X25,X26,X27)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk2_4(X5,X6,X7,X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(esk3_7(X5,X6,X7,X8,X10,X11,X12),X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(esk4_10(X5,X6,X7,X8,X10,X11,X12,X14,X15,X16),X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| p1(X24)
| ~ r1(X23,X24)
| ~ r1(X22,X23)
| ~ r1(esk5_13(X5,X6,X7,X8,X10,X11,X12,X14,X15,X16,X18,X19,X20),X22) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk2_4(X5,X6,X7,X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(esk3_7(X5,X6,X7,X8,X10,X11,X12),X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(esk4_10(X5,X6,X7,X8,X10,X11,X12,X14,X15,X16),X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| r1(X20,esk5_13(X5,X6,X7,X8,X10,X11,X12,X14,X15,X16,X18,X19,X20)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk2_4(X5,X6,X7,X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(esk3_7(X5,X6,X7,X8,X10,X11,X12),X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| r1(X16,esk4_10(X5,X6,X7,X8,X10,X11,X12,X14,X15,X16)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk2_4(X5,X6,X7,X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| r1(X12,esk3_7(X5,X6,X7,X8,X10,X11,X12)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| r1(X8,esk2_4(X5,X6,X7,X8)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])]) ).
cnf(c_0_5,negated_conjecture,
( ~ r1(esk1_0,X1)
| ~ p1(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk34_1(X1),X2)
| p1(esk1_0) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_6,negated_conjecture,
~ p1(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_7,negated_conjecture,
( ~ r1(X3,X5)
| ~ r1(X5,X4)
| ~ r1(X4,X1)
| ~ r1(esk1_0,X2)
| ~ r1(esk34_1(X2),X3)
| ~ p1(X1) ),
inference(sr,[status(thm)],[c_0_5,c_0_6]) ).
cnf(c_0_8,negated_conjecture,
( ~ r1(esk1_0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X15,X16)
| ~ r1(X14,X15)
| ~ r1(esk5_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13),X14)
| p1(X16) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_9,plain,
! [X3] : r1(X3,X3),
inference(variable_rename,[status(thm)],[reflexivity]) ).
cnf(c_0_10,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X14,X20)
| ~ r1(X20,X18)
| ~ r1(X16,X19)
| ~ r1(X19,X17)
| ~ r1(X17,X18)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X15)
| ~ r1(esk34_1(X15),X16)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11)
| ~ r1(esk5_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13),X14) ),
inference(spm,[status(thm)],[c_0_7,c_0_8]) ).
cnf(c_0_11,plain,
r1(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
cnf(c_0_12,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X14,X18)
| ~ r1(X16,X19)
| ~ r1(X19,X17)
| ~ r1(X17,X18)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X15)
| ~ r1(esk34_1(X15),X16)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11)
| ~ r1(esk5_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13),X14) ),
inference(spm,[status(thm)],[c_0_10,c_0_11]) ).
cnf(c_0_13,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X16,X18)
| ~ r1(X18,X17)
| ~ r1(X17,X14)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X15)
| ~ r1(esk34_1(X15),X16)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11)
| ~ r1(esk5_13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13),X14) ),
inference(spm,[status(thm)],[c_0_12,c_0_11]) ).
cnf(c_0_14,negated_conjecture,
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X16,X17)
| ~ r1(X17,X1)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X15)
| ~ r1(esk34_1(X15),X16)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(esk3_7(X2,X3,X4,X5,X6,X7,X8),X9)
| ~ r1(esk4_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),X12)
| ~ r1(X1,esk5_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14)) ),
inference(spm,[status(thm)],[c_0_13,c_0_11]) ).
cnf(c_0_15,negated_conjecture,
( ~ r1(esk1_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk3_7(X2,X3,X4,X5,X6,X7,X8),X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(esk4_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11),X12)
| ~ r1(X12,X13)
| ~ r1(X13,X1)
| r1(X1,esk5_13(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_16,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X11,X16)
| ~ r1(X16,X15)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X12)
| ~ r1(esk34_1(X12),X13)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11) ),
inference(spm,[status(thm)],[c_0_14,c_0_15]) ).
cnf(c_0_17,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X11,X15)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X12)
| ~ r1(esk34_1(X12),X13)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11) ),
inference(spm,[status(thm)],[c_0_16,c_0_11]) ).
cnf(c_0_18,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(X13,X14)
| ~ r1(X14,X11)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X12)
| ~ r1(esk34_1(X12),X13)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8)
| ~ r1(esk4_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10),X11) ),
inference(spm,[status(thm)],[c_0_17,c_0_11]) ).
cnf(c_0_19,negated_conjecture,
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(X13,X1)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X12)
| ~ r1(esk34_1(X12),X13)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(esk3_7(X2,X3,X4,X5,X6,X7,X8),X9)
| ~ r1(X1,esk4_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11)) ),
inference(spm,[status(thm)],[c_0_18,c_0_11]) ).
cnf(c_0_20,negated_conjecture,
( ~ r1(esk1_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk3_7(X2,X3,X4,X5,X6,X7,X8),X9)
| ~ r1(X9,X10)
| ~ r1(X10,X1)
| r1(X1,esk4_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_21,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X12)
| ~ r1(X12,X11)
| ~ r1(X10,X11)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X9)
| ~ r1(esk34_1(X9),X10)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8) ),
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
cnf(c_0_22,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X8,X11)
| ~ r1(X10,X11)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X9)
| ~ r1(esk34_1(X9),X10)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8) ),
inference(spm,[status(thm)],[c_0_21,c_0_11]) ).
cnf(c_0_23,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X10,X8)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X9)
| ~ r1(esk34_1(X9),X10)
| ~ r1(esk2_4(X1,X2,X3,X4),X5)
| ~ r1(esk3_7(X1,X2,X3,X4,X5,X6,X7),X8) ),
inference(spm,[status(thm)],[c_0_22,c_0_11]) ).
cnf(c_0_24,negated_conjecture,
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X9)
| ~ r1(esk34_1(X9),X1)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(X1,esk3_7(X2,X3,X4,X5,X6,X7,X8)) ),
inference(spm,[status(thm)],[c_0_23,c_0_11]) ).
cnf(c_0_25,negated_conjecture,
( ~ r1(esk1_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(esk2_4(X2,X3,X4,X5),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X1)
| r1(X1,esk3_7(X2,X3,X4,X5,X6,X7,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_26,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X8)
| ~ r1(X8,X7)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X6)
| ~ r1(esk34_1(X6),X7)
| ~ r1(esk2_4(X1,X2,X3,X4),X5) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_27,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X7)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X6)
| ~ r1(esk34_1(X6),X7)
| ~ r1(esk2_4(X1,X2,X3,X4),X5) ),
inference(spm,[status(thm)],[c_0_26,c_0_11]) ).
cnf(c_0_28,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(esk1_0,X1)
| ~ r1(esk1_0,X6)
| ~ r1(esk34_1(X6),X5)
| ~ r1(esk2_4(X1,X2,X3,X4),X5) ),
inference(spm,[status(thm)],[c_0_27,c_0_11]) ).
cnf(c_0_29,negated_conjecture,
( ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X1)
| ~ r1(esk34_1(X1),esk2_4(X2,X3,X4,X5)) ),
inference(spm,[status(thm)],[c_0_28,c_0_11]) ).
cnf(c_0_30,negated_conjecture,
( ~ r1(esk1_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X1)
| r1(X1,esk2_4(X2,X3,X4,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_31,negated_conjecture,
( ~ r1(esk1_0,X1)
| p1(esk1_0)
| r1(X1,esk34_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_32,negated_conjecture,
( ~ r1(X3,X4)
| ~ r1(X4,X1)
| ~ r1(esk1_0,X3)
| ~ r1(esk1_0,X2)
| ~ r1(X1,esk34_1(X2)) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_33,negated_conjecture,
( ~ r1(esk1_0,X1)
| r1(X1,esk34_1(X1)) ),
inference(sr,[status(thm)],[c_0_31,c_0_6]) ).
cnf(c_0_34,negated_conjecture,
( ~ r1(X2,X3)
| ~ r1(X3,X1)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X1) ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_35,negated_conjecture,
( ~ r1(X1,X2)
| ~ r1(X2,esk1_0)
| ~ r1(esk1_0,X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_11]) ).
cnf(c_0_36,negated_conjecture,
( ~ r1(esk1_0,X1)
| ~ r1(X1,esk1_0) ),
inference(spm,[status(thm)],[c_0_35,c_0_11]) ).
cnf(c_0_37,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_11]),c_0_11])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL662+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/15.44 % Computer : n026.cluster.edu
% 0.17/15.44 % Model : x86_64 x86_64
% 0.17/15.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/15.44 % Memory : 8046.5625MB
% 0.17/15.44 % OS : Linux 6.8.0-71-generic
% 0.17/15.44 % CPULimit : 300
% 0.17/15.44 % WCLimit : 300
% 0.17/15.44 % DateTime : Mon Sep 21 00:52:22 UTC 2026
% 0.17/15.44 % CPUTime :
% 0.17/15.44 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/15.49 Running first-order theorem proving
% 0.17/15.49 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/15.80 % Version: 3.5.1
% 0.20/15.80 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.20/15.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/15.80 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.20/15.80 % Starting new_bool_3 with 300s (1) cores
% 0.20/15.80 % Starting new_bool_1 with 300s (1) cores
% 0.20/15.80 % Starting sh5l with 300s (1) cores
% 0.20/15.80 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 1010662 completed with status 0
% 0.20/15.80 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 0.20/15.80 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.20/15.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/15.80 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.20/15.80 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/15.80 % No SInE strategy applied
% 0.20/15.80 % Search class: FGUNF-FSLF33-SFFFFFNN
% 0.20/15.80 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/15.80 % Starting SubtermCWHack with 136s (1) cores
% 0.20/15.80 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 0.20/15.80 % Starting G----_406_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 473s (1) cores
% 0.20/15.80 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S05BN with 136s (1) cores
% 0.20/15.80 % Starting new_bool_3 with 136s (1) cores
% 0.20/15.80 % G----_406_C05_02_F1_SE_CS_SP_PS_RG_S04AI with pid 1010669 completed with status 0
% 0.20/15.80 % Result found by G----_406_C05_02_F1_SE_CS_SP_PS_RG_S04AI
% 0.20/15.80 % Preprocessing class: FSLSSMSSSSSNFFN.
% 0.20/15.80 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.20/15.80 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 0.20/15.80 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.20/15.80 % No SInE strategy applied
% 0.20/15.80 % Search class: FGUNF-FSLF33-SFFFFFNN
% 0.20/15.80 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.20/15.80 % Starting SubtermCWHack with 136s (1) cores
% 0.20/15.80 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 0.20/15.80 % Starting G----_406_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 473s (1) cores
% 0.20/15.80 % Preprocessing time : 0.002 s
% 0.20/15.80 % Presaturation interreduction done
% 0.20/15.80
% 0.20/15.80 % Proof found!
% 0.20/15.80 % SZS status Theorem
% 0.20/15.80 % SZS output start CNFRefutation
% See solution above
% 0.20/15.81 % Parsed axioms : 2
% 0.20/15.81 % Removed by relevancy pruning/SinE : 0
% 0.20/15.81 % Initial clauses : 49
% 0.20/15.81 % Removed in clause preprocessing : 0
% 0.20/15.81 % Initial clauses in saturation : 49
% 0.20/15.81 % Processed clauses : 1044
% 0.20/15.81 % ...of these trivial : 0
% 0.20/15.81 % ...subsumed : 225
% 0.20/15.81 % ...remaining for further processing : 819
% 0.20/15.81 % Other redundant clauses eliminated : 0
% 0.20/15.81 % Clauses deleted for lack of memory : 0
% 0.20/15.81 % Backward-subsumed : 52
% 0.20/15.81 % Backward-rewritten : 0
% 0.20/15.81 % Generated clauses : 6666
% 0.20/15.81 % ...of the previous two non-redundant : 6665
% 0.20/15.81 % ...aggressively subsumed : 0
% 0.20/15.81 % Contextual simplify-reflections : 0
% 0.20/15.81 % Paramodulations : 6666
% 0.20/15.81 % Factorizations : 0
% 0.20/15.81 % NegExts : 0
% 0.20/15.81 % Equation resolutions : 0
% 0.20/15.81 % Disequality decompositions : 0
% 0.20/15.81 % Total rewrite steps : 125
% 0.20/15.81 % ...of those cached : 124
% 0.20/15.81 % Propositional unsat checks : 0
% 0.20/15.81 % Propositional check models : 0
% 0.20/15.81 % Propositional check unsatisfiable : 0
% 0.20/15.81 % Propositional clauses : 0
% 0.20/15.81 % Propositional clauses after purity: 0
% 0.20/15.81 % Propositional unsat core size : 0
% 0.20/15.81 % Propositional preprocessing time : 0.000
% 0.20/15.81 % Propositional encoding time : 0.000
% 0.20/15.81 % Propositional solver time : 0.000
% 0.20/15.81 % Success case prop preproc time : 0.000
% 0.20/15.81 % Success case prop encoding time : 0.000
% 0.20/15.81 % Success case prop solver time : 0.000
% 0.20/15.81 % Current number of processed clauses : 718
% 0.20/15.81 % Positive orientable unit clauses : 1
% 0.20/15.81 % Positive unorientable unit clauses: 0
% 0.20/15.81 % Negative unit clauses : 1
% 0.20/15.81 % Non-unit-clauses : 716
% 0.20/15.81 % Current number of unprocessed clauses: 5719
% 0.20/15.81 % ...number of literals in the above : 61334
% 0.20/15.81 % Current number of archived formulas : 0
% 0.20/15.81 % Current number of archived clauses : 101
% 0.20/15.81 % Clause-clause subsumption calls (NU) : 143031
% 0.20/15.81 % Rec. Clause-clause subsumption calls : 12109
% 0.20/15.81 % Non-unit clause-clause subsumptions : 277
% 0.20/15.81 % Unit Clause-clause subsumption calls : 0
% 0.20/15.81 % Rewrite failures with RHS unbound : 0
% 0.20/15.81 % BW rewrite match attempts : 0
% 0.20/15.81 % BW rewrite match successes : 0
% 0.20/15.81 % Condensation attempts : 0
% 0.20/15.81 % Condensation successes : 0
% 0.20/15.81 % Termbank termtop insertions : 243971
% 0.20/15.81 % Search garbage collected termcells : 2648
% 0.20/15.81
% 0.20/15.81 % -------------------------------------------------
% 0.20/15.81 % User time : 0.277 s
% 0.20/15.81 % System time : 0.013 s
% 0.20/15.81 % Total time : 0.290 s
% 0.20/15.81 % Maximum resident set size: 4180 pages
% 0.20/15.81
% 0.20/15.81 % -------------------------------------------------
% 0.20/15.81 % User time : 1.080 s
% 0.20/15.81 % System time : 0.063 s
% 0.20/15.81 % Total time : 1.143 s
% 0.20/15.81 % Maximum resident set size: 4864 pages
% 0.20/15.81 % E exiting
%------------------------------------------------------------------------------