%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LCL672+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 : n014.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:16:04 PM UTC 2026
% Result : Theorem 122.27s 18.39s
% Output : CNFRefutation 122.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 3
% Syntax : Number of formulae : 45 ( 23 unt; 0 def)
% Number of atoms : 2811 ( 0 equ)
% Maximal formula atoms : 1080 ( 62 avg)
% Number of connectives : 5349 (2583 ~;2165 |; 600 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 416 ( 16 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-2 aty)
% Number of functors : 111 ( 111 usr; 86 con; 0-7 aty)
% Number of variables : 1259 ( 0 sgn1218 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X1] :
~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(transitivity,axiom,
! [X1,X2,X3] :
( ( r1(X2,X3)
& r1(X1,X2) )
=> r1(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(reflexivity,axiom,
! [X1] : r1(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(c_0_3,negated_conjecture,
~ ~ ? [X1] :
~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(c_0_4,negated_conjecture,
~ ~ ? [X1] :
~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ $true
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( p2(X2)
| ~ r1(X1,X2) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( ~ $true
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ~ ( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ~ ( p1(X2)
& ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( p2(X2)
| ~ r1(X1,X2) ) ) ),
inference(fof_simplification,[status(thm)],[c_0_3]) ).
fof(c_0_5,plain,
! [X5,X6,X7] :
( r1(X5,X7)
| ~ r1(X6,X7)
| ~ r1(X5,X6) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])]) ).
fof(c_0_6,negated_conjecture,
! [X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X39,X40,X41,X42,X43,X44,X45,X46,X47,X48,X49,X50,X51,X52,X53,X54,X55,X57,X58,X60,X61,X62,X63,X64,X65,X66,X67,X68,X69,X70,X71,X72,X73,X74,X76,X77,X78,X79,X80,X92,X99,X100,X101,X102,X103,X104,X105,X106,X107,X109,X110,X111,X112,X113,X114,X115,X116,X117,X118,X119,X120,X121,X122,X124,X125,X126,X127,X128,X129,X130,X131,X132,X133,X134,X135,X136,X137,X139,X140,X142,X143,X144,X145,X146,X147,X148,X149,X150,X151,X152,X153,X155,X156,X157,X158,X170,X177,X178,X179,X180,X181,X182,X183,X185,X186,X187,X188,X189,X190,X191,X192,X193,X194,X195,X197,X198,X199,X200,X201,X202,X203,X204,X205,X206,X207,X209,X210,X212,X213,X214,X215,X216,X217,X218,X219,X220,X222,X223,X224,X236,X243,X244,X245,X246,X247,X249,X250,X251,X252,X253,X254,X255,X256,X258,X259,X260,X261,X262,X263,X264,X265,X267,X268,X270,X271,X272,X273,X274,X275,X277,X278,X290,X297,X298,X299,X301,X302,X303,X304,X305,X307,X308,X309,X310,X311,X313,X314,X316,X317,X318,X320,X332] :
( ~ p1(esk111_0)
& r1(esk1_0,esk111_0)
& ~ p1(esk110_0)
& r1(esk96_0,esk110_0)
& ~ p1(esk109_0)
& r1(esk98_0,esk109_0)
& ~ p1(esk108_0)
& r1(esk100_0,esk108_0)
& ~ p1(esk107_0)
& r1(esk102_0,esk107_0)
& ~ p1(esk106_0)
& r1(esk104_0,esk106_0)
& ( p1(X332)
| ~ r1(esk105_0,X332) )
& r1(esk104_0,esk105_0)
& r1(esk102_0,esk104_0)
& ~ p2(esk103_0)
& r1(esk102_0,esk103_0)
& r1(esk100_0,esk102_0)
& ~ p2(esk101_0)
& r1(esk100_0,esk101_0)
& r1(esk98_0,esk100_0)
& ~ p2(esk99_0)
& r1(esk98_0,esk99_0)
& r1(esk96_0,esk98_0)
& ~ p2(esk97_0)
& r1(esk96_0,esk97_0)
& r1(esk1_0,esk96_0)
& ~ p2(esk95_0)
& r1(esk1_0,esk95_0)
& ( p1(X320)
| ~ r1(esk1_0,X320)
| p2(X317)
| ~ r1(esk1_0,X317)
| ~ r1(esk1_0,X318)
| $true )
& ( p1(X320)
| ~ r1(esk1_0,X320)
| p2(X317)
| ~ r1(esk1_0,X317)
| ~ r1(esk1_0,X318)
| r1(X318,esk94_1(X318)) )
& ( p1(X316)
| ~ r1(esk1_0,X316)
| p2(X309)
| ~ r1(esk1_0,X309)
| ~ r1(esk1_0,X310)
| ~ r1(X310,X311)
| p1(X313)
| ~ r1(esk92_2(X310,X311),X313)
| ~ r1(X310,X314)
| ~ p1(esk93_2(X310,X314)) )
& ( p1(X316)
| ~ r1(esk1_0,X316)
| p2(X309)
| ~ r1(esk1_0,X309)
| ~ r1(esk1_0,X310)
| ~ r1(X310,X311)
| p1(X313)
| ~ r1(esk92_2(X310,X311),X313)
| ~ r1(X310,X314)
| r1(X314,esk93_2(X310,X314)) )
& ( p1(X316)
| ~ r1(esk1_0,X316)
| p2(X309)
| ~ r1(esk1_0,X309)
| ~ r1(esk1_0,X310)
| ~ r1(X310,X311)
| r1(X311,esk92_2(X310,X311))
| ~ r1(X310,X314)
| ~ p1(esk93_2(X310,X314)) )
& ( p1(X316)
| ~ r1(esk1_0,X316)
| p2(X309)
| ~ r1(esk1_0,X309)
| ~ r1(esk1_0,X310)
| ~ r1(X310,X311)
| r1(X311,esk92_2(X310,X311))
| ~ r1(X310,X314)
| r1(X314,esk93_2(X310,X314)) )
& ( p1(X308)
| ~ r1(esk1_0,X308)
| p2(X302)
| ~ r1(esk1_0,X302)
| ~ r1(esk1_0,X303)
| ~ r1(X303,X304)
| p1(X307)
| ~ r1(X304,X307)
| ~ r1(X304,X305)
| ~ p1(esk91_3(X303,X304,X305)) )
& ( p1(X308)
| ~ r1(esk1_0,X308)
| p2(X302)
| ~ r1(esk1_0,X302)
| ~ r1(esk1_0,X303)
| ~ r1(X303,X304)
| p1(X307)
| ~ r1(X304,X307)
| ~ r1(X304,X305)
| r1(X305,esk91_3(X303,X304,X305)) )
& ( p1(X301)
| ~ r1(esk1_0,X301)
| p2(X297)
| ~ r1(esk1_0,X297)
| ~ r1(esk1_0,X298)
| ~ p1(X298)
| ~ r1(X298,X299)
| p1(esk90_2(X298,X299)) )
& ( p1(X301)
| ~ r1(esk1_0,X301)
| p2(X297)
| ~ r1(esk1_0,X297)
| ~ r1(esk1_0,X298)
| ~ p1(X298)
| ~ r1(X298,X299)
| r1(X299,esk90_2(X298,X299)) )
& ~ p1(esk89_0)
& r1(esk1_0,esk89_0)
& ~ p1(esk88_0)
& r1(esk74_0,esk88_0)
& ~ p1(esk87_0)
& r1(esk76_0,esk87_0)
& ~ p1(esk86_0)
& r1(esk78_0,esk86_0)
& ~ p1(esk85_0)
& r1(esk80_0,esk85_0)
& ~ p1(esk84_0)
& r1(esk82_0,esk84_0)
& ( p1(X290)
| ~ r1(esk83_0,X290) )
& r1(esk82_0,esk83_0)
& r1(esk80_0,esk82_0)
& ~ p2(esk81_0)
& r1(esk80_0,esk81_0)
& r1(esk78_0,esk80_0)
& ~ p2(esk79_0)
& r1(esk78_0,esk79_0)
& r1(esk76_0,esk78_0)
& ~ p2(esk77_0)
& r1(esk76_0,esk77_0)
& r1(esk74_0,esk76_0)
& ~ p2(esk75_0)
& r1(esk74_0,esk75_0)
& r1(esk1_0,esk74_0)
& ~ p2(esk73_0)
& r1(esk1_0,esk73_0)
& ( p1(X278)
| ~ r1(esk1_0,X278)
| p2(X272)
| ~ r1(esk1_0,X272)
| ~ r1(esk1_0,X273)
| p1(X277)
| ~ r1(X273,X277)
| p2(X274)
| ~ r1(X273,X274)
| ~ r1(X273,X275)
| $true )
& ( p1(X278)
| ~ r1(esk1_0,X278)
| p2(X272)
| ~ r1(esk1_0,X272)
| ~ r1(esk1_0,X273)
| p1(X277)
| ~ r1(X273,X277)
| p2(X274)
| ~ r1(X273,X274)
| ~ r1(X273,X275)
| r1(X275,esk72_2(X273,X275)) )
& ( p1(X271)
| ~ r1(esk1_0,X271)
| p2(X261)
| ~ r1(esk1_0,X261)
| ~ r1(esk1_0,X262)
| p1(X270)
| ~ r1(X262,X270)
| p2(X263)
| ~ r1(X262,X263)
| ~ r1(X262,X264)
| ~ r1(X264,X265)
| p1(X267)
| ~ r1(esk70_3(X262,X264,X265),X267)
| ~ r1(X264,X268)
| ~ p1(esk71_3(X262,X264,X268)) )
& ( p1(X271)
| ~ r1(esk1_0,X271)
| p2(X261)
| ~ r1(esk1_0,X261)
| ~ r1(esk1_0,X262)
| p1(X270)
| ~ r1(X262,X270)
| p2(X263)
| ~ r1(X262,X263)
| ~ r1(X262,X264)
| ~ r1(X264,X265)
| p1(X267)
| ~ r1(esk70_3(X262,X264,X265),X267)
| ~ r1(X264,X268)
| r1(X268,esk71_3(X262,X264,X268)) )
& ( p1(X271)
| ~ r1(esk1_0,X271)
| p2(X261)
| ~ r1(esk1_0,X261)
| ~ r1(esk1_0,X262)
| p1(X270)
| ~ r1(X262,X270)
| p2(X263)
| ~ r1(X262,X263)
| ~ r1(X262,X264)
| ~ r1(X264,X265)
| r1(X265,esk70_3(X262,X264,X265))
| ~ r1(X264,X268)
| ~ p1(esk71_3(X262,X264,X268)) )
& ( p1(X271)
| ~ r1(esk1_0,X271)
| p2(X261)
| ~ r1(esk1_0,X261)
| ~ r1(esk1_0,X262)
| p1(X270)
| ~ r1(X262,X270)
| p2(X263)
| ~ r1(X262,X263)
| ~ r1(X262,X264)
| ~ r1(X264,X265)
| r1(X265,esk70_3(X262,X264,X265))
| ~ r1(X264,X268)
| r1(X268,esk71_3(X262,X264,X268)) )
& ( p1(X260)
| ~ r1(esk1_0,X260)
| p2(X251)
| ~ r1(esk1_0,X251)
| ~ r1(esk1_0,X252)
| p1(X259)
| ~ r1(X252,X259)
| p2(X253)
| ~ r1(X252,X253)
| ~ r1(X252,X254)
| ~ r1(X254,X255)
| p1(X258)
| ~ r1(X255,X258)
| ~ r1(X255,X256)
| ~ p1(esk69_4(X252,X254,X255,X256)) )
& ( p1(X260)
| ~ r1(esk1_0,X260)
| p2(X251)
| ~ r1(esk1_0,X251)
| ~ r1(esk1_0,X252)
| p1(X259)
| ~ r1(X252,X259)
| p2(X253)
| ~ r1(X252,X253)
| ~ r1(X252,X254)
| ~ r1(X254,X255)
| p1(X258)
| ~ r1(X255,X258)
| ~ r1(X255,X256)
| r1(X256,esk69_4(X252,X254,X255,X256)) )
& ( p1(X250)
| ~ r1(esk1_0,X250)
| p2(X243)
| ~ r1(esk1_0,X243)
| ~ r1(esk1_0,X244)
| p1(X249)
| ~ r1(X244,X249)
| p2(X245)
| ~ r1(X244,X245)
| ~ r1(X244,X246)
| ~ p1(X246)
| ~ r1(X246,X247)
| p1(esk68_3(X244,X246,X247)) )
& ( p1(X250)
| ~ r1(esk1_0,X250)
| p2(X243)
| ~ r1(esk1_0,X243)
| ~ r1(esk1_0,X244)
| p1(X249)
| ~ r1(X244,X249)
| p2(X245)
| ~ r1(X244,X245)
| ~ r1(X244,X246)
| ~ p1(X246)
| ~ r1(X246,X247)
| r1(X247,esk68_3(X244,X246,X247)) )
& ~ p1(esk67_0)
& r1(esk1_0,esk67_0)
& ~ p1(esk66_0)
& r1(esk52_0,esk66_0)
& ~ p1(esk65_0)
& r1(esk54_0,esk65_0)
& ~ p1(esk64_0)
& r1(esk56_0,esk64_0)
& ~ p1(esk63_0)
& r1(esk58_0,esk63_0)
& ~ p1(esk62_0)
& r1(esk60_0,esk62_0)
& ( p1(X236)
| ~ r1(esk61_0,X236) )
& r1(esk60_0,esk61_0)
& r1(esk58_0,esk60_0)
& ~ p2(esk59_0)
& r1(esk58_0,esk59_0)
& r1(esk56_0,esk58_0)
& ~ p2(esk57_0)
& r1(esk56_0,esk57_0)
& r1(esk54_0,esk56_0)
& ~ p2(esk55_0)
& r1(esk54_0,esk55_0)
& r1(esk52_0,esk54_0)
& ~ p2(esk53_0)
& r1(esk52_0,esk53_0)
& r1(esk1_0,esk52_0)
& ~ p2(esk51_0)
& r1(esk1_0,esk51_0)
& ( p1(X224)
| ~ r1(esk1_0,X224)
| p2(X215)
| ~ r1(esk1_0,X215)
| ~ r1(esk1_0,X216)
| p1(X223)
| ~ r1(X216,X223)
| p2(X217)
| ~ r1(X216,X217)
| ~ r1(X216,X218)
| p1(X222)
| ~ r1(X218,X222)
| p2(X219)
| ~ r1(X218,X219)
| ~ r1(X218,X220)
| $true )
& ( p1(X224)
| ~ r1(esk1_0,X224)
| p2(X215)
| ~ r1(esk1_0,X215)
| ~ r1(esk1_0,X216)
| p1(X223)
| ~ r1(X216,X223)
| p2(X217)
| ~ r1(X216,X217)
| ~ r1(X216,X218)
| p1(X222)
| ~ r1(X218,X222)
| p2(X219)
| ~ r1(X218,X219)
| ~ r1(X218,X220)
| r1(X220,esk50_3(X216,X218,X220)) )
& ( p1(X214)
| ~ r1(esk1_0,X214)
| p2(X201)
| ~ r1(esk1_0,X201)
| ~ r1(esk1_0,X202)
| p1(X213)
| ~ r1(X202,X213)
| p2(X203)
| ~ r1(X202,X203)
| ~ r1(X202,X204)
| p1(X212)
| ~ r1(X204,X212)
| p2(X205)
| ~ r1(X204,X205)
| ~ r1(X204,X206)
| ~ r1(X206,X207)
| p1(X209)
| ~ r1(esk48_4(X202,X204,X206,X207),X209)
| ~ r1(X206,X210)
| ~ p1(esk49_4(X202,X204,X206,X210)) )
& ( p1(X214)
| ~ r1(esk1_0,X214)
| p2(X201)
| ~ r1(esk1_0,X201)
| ~ r1(esk1_0,X202)
| p1(X213)
| ~ r1(X202,X213)
| p2(X203)
| ~ r1(X202,X203)
| ~ r1(X202,X204)
| p1(X212)
| ~ r1(X204,X212)
| p2(X205)
| ~ r1(X204,X205)
| ~ r1(X204,X206)
| ~ r1(X206,X207)
| p1(X209)
| ~ r1(esk48_4(X202,X204,X206,X207),X209)
| ~ r1(X206,X210)
| r1(X210,esk49_4(X202,X204,X206,X210)) )
& ( p1(X214)
| ~ r1(esk1_0,X214)
| p2(X201)
| ~ r1(esk1_0,X201)
| ~ r1(esk1_0,X202)
| p1(X213)
| ~ r1(X202,X213)
| p2(X203)
| ~ r1(X202,X203)
| ~ r1(X202,X204)
| p1(X212)
| ~ r1(X204,X212)
| p2(X205)
| ~ r1(X204,X205)
| ~ r1(X204,X206)
| ~ r1(X206,X207)
| r1(X207,esk48_4(X202,X204,X206,X207))
| ~ r1(X206,X210)
| ~ p1(esk49_4(X202,X204,X206,X210)) )
& ( p1(X214)
| ~ r1(esk1_0,X214)
| p2(X201)
| ~ r1(esk1_0,X201)
| ~ r1(esk1_0,X202)
| p1(X213)
| ~ r1(X202,X213)
| p2(X203)
| ~ r1(X202,X203)
| ~ r1(X202,X204)
| p1(X212)
| ~ r1(X204,X212)
| p2(X205)
| ~ r1(X204,X205)
| ~ r1(X204,X206)
| ~ r1(X206,X207)
| r1(X207,esk48_4(X202,X204,X206,X207))
| ~ r1(X206,X210)
| r1(X210,esk49_4(X202,X204,X206,X210)) )
& ( p1(X200)
| ~ r1(esk1_0,X200)
| p2(X188)
| ~ r1(esk1_0,X188)
| ~ r1(esk1_0,X189)
| p1(X199)
| ~ r1(X189,X199)
| p2(X190)
| ~ r1(X189,X190)
| ~ r1(X189,X191)
| p1(X198)
| ~ r1(X191,X198)
| p2(X192)
| ~ r1(X191,X192)
| ~ r1(X191,X193)
| ~ r1(X193,X194)
| p1(X197)
| ~ r1(X194,X197)
| ~ r1(X194,X195)
| ~ p1(esk47_5(X189,X191,X193,X194,X195)) )
& ( p1(X200)
| ~ r1(esk1_0,X200)
| p2(X188)
| ~ r1(esk1_0,X188)
| ~ r1(esk1_0,X189)
| p1(X199)
| ~ r1(X189,X199)
| p2(X190)
| ~ r1(X189,X190)
| ~ r1(X189,X191)
| p1(X198)
| ~ r1(X191,X198)
| p2(X192)
| ~ r1(X191,X192)
| ~ r1(X191,X193)
| ~ r1(X193,X194)
| p1(X197)
| ~ r1(X194,X197)
| ~ r1(X194,X195)
| r1(X195,esk47_5(X189,X191,X193,X194,X195)) )
& ( p1(X187)
| ~ r1(esk1_0,X187)
| p2(X177)
| ~ r1(esk1_0,X177)
| ~ r1(esk1_0,X178)
| p1(X186)
| ~ r1(X178,X186)
| p2(X179)
| ~ r1(X178,X179)
| ~ r1(X178,X180)
| p1(X185)
| ~ r1(X180,X185)
| p2(X181)
| ~ r1(X180,X181)
| ~ r1(X180,X182)
| ~ p1(X182)
| ~ r1(X182,X183)
| p1(esk46_4(X178,X180,X182,X183)) )
& ( p1(X187)
| ~ r1(esk1_0,X187)
| p2(X177)
| ~ r1(esk1_0,X177)
| ~ r1(esk1_0,X178)
| p1(X186)
| ~ r1(X178,X186)
| p2(X179)
| ~ r1(X178,X179)
| ~ r1(X178,X180)
| p1(X185)
| ~ r1(X180,X185)
| p2(X181)
| ~ r1(X180,X181)
| ~ r1(X180,X182)
| ~ p1(X182)
| ~ r1(X182,X183)
| r1(X183,esk46_4(X178,X180,X182,X183)) )
& ~ p1(esk45_0)
& r1(esk1_0,esk45_0)
& ~ p1(esk44_0)
& r1(esk30_0,esk44_0)
& ~ p1(esk43_0)
& r1(esk32_0,esk43_0)
& ~ p1(esk42_0)
& r1(esk34_0,esk42_0)
& ~ p1(esk41_0)
& r1(esk36_0,esk41_0)
& ~ p1(esk40_0)
& r1(esk38_0,esk40_0)
& ( p1(X170)
| ~ r1(esk39_0,X170) )
& r1(esk38_0,esk39_0)
& r1(esk36_0,esk38_0)
& ~ p2(esk37_0)
& r1(esk36_0,esk37_0)
& r1(esk34_0,esk36_0)
& ~ p2(esk35_0)
& r1(esk34_0,esk35_0)
& r1(esk32_0,esk34_0)
& ~ p2(esk33_0)
& r1(esk32_0,esk33_0)
& r1(esk30_0,esk32_0)
& ~ p2(esk31_0)
& r1(esk30_0,esk31_0)
& r1(esk1_0,esk30_0)
& ~ p2(esk29_0)
& r1(esk1_0,esk29_0)
& ( p1(X158)
| ~ r1(esk1_0,X158)
| p2(X146)
| ~ r1(esk1_0,X146)
| ~ r1(esk1_0,X147)
| p1(X157)
| ~ r1(X147,X157)
| p2(X148)
| ~ r1(X147,X148)
| ~ r1(X147,X149)
| p1(X156)
| ~ r1(X149,X156)
| p2(X150)
| ~ r1(X149,X150)
| ~ r1(X149,X151)
| p1(X155)
| ~ r1(X151,X155)
| p2(X152)
| ~ r1(X151,X152)
| ~ r1(X151,X153)
| $true )
& ( p1(X158)
| ~ r1(esk1_0,X158)
| p2(X146)
| ~ r1(esk1_0,X146)
| ~ r1(esk1_0,X147)
| p1(X157)
| ~ r1(X147,X157)
| p2(X148)
| ~ r1(X147,X148)
| ~ r1(X147,X149)
| p1(X156)
| ~ r1(X149,X156)
| p2(X150)
| ~ r1(X149,X150)
| ~ r1(X149,X151)
| p1(X155)
| ~ r1(X151,X155)
| p2(X152)
| ~ r1(X151,X152)
| ~ r1(X151,X153)
| r1(X153,esk28_4(X147,X149,X151,X153)) )
& ( p1(X145)
| ~ r1(esk1_0,X145)
| p2(X129)
| ~ r1(esk1_0,X129)
| ~ r1(esk1_0,X130)
| p1(X144)
| ~ r1(X130,X144)
| p2(X131)
| ~ r1(X130,X131)
| ~ r1(X130,X132)
| p1(X143)
| ~ r1(X132,X143)
| p2(X133)
| ~ r1(X132,X133)
| ~ r1(X132,X134)
| p1(X142)
| ~ r1(X134,X142)
| p2(X135)
| ~ r1(X134,X135)
| ~ r1(X134,X136)
| ~ r1(X136,X137)
| p1(X139)
| ~ r1(esk26_5(X130,X132,X134,X136,X137),X139)
| ~ r1(X136,X140)
| ~ p1(esk27_5(X130,X132,X134,X136,X140)) )
& ( p1(X145)
| ~ r1(esk1_0,X145)
| p2(X129)
| ~ r1(esk1_0,X129)
| ~ r1(esk1_0,X130)
| p1(X144)
| ~ r1(X130,X144)
| p2(X131)
| ~ r1(X130,X131)
| ~ r1(X130,X132)
| p1(X143)
| ~ r1(X132,X143)
| p2(X133)
| ~ r1(X132,X133)
| ~ r1(X132,X134)
| p1(X142)
| ~ r1(X134,X142)
| p2(X135)
| ~ r1(X134,X135)
| ~ r1(X134,X136)
| ~ r1(X136,X137)
| p1(X139)
| ~ r1(esk26_5(X130,X132,X134,X136,X137),X139)
| ~ r1(X136,X140)
| r1(X140,esk27_5(X130,X132,X134,X136,X140)) )
& ( p1(X145)
| ~ r1(esk1_0,X145)
| p2(X129)
| ~ r1(esk1_0,X129)
| ~ r1(esk1_0,X130)
| p1(X144)
| ~ r1(X130,X144)
| p2(X131)
| ~ r1(X130,X131)
| ~ r1(X130,X132)
| p1(X143)
| ~ r1(X132,X143)
| p2(X133)
| ~ r1(X132,X133)
| ~ r1(X132,X134)
| p1(X142)
| ~ r1(X134,X142)
| p2(X135)
| ~ r1(X134,X135)
| ~ r1(X134,X136)
| ~ r1(X136,X137)
| r1(X137,esk26_5(X130,X132,X134,X136,X137))
| ~ r1(X136,X140)
| ~ p1(esk27_5(X130,X132,X134,X136,X140)) )
& ( p1(X145)
| ~ r1(esk1_0,X145)
| p2(X129)
| ~ r1(esk1_0,X129)
| ~ r1(esk1_0,X130)
| p1(X144)
| ~ r1(X130,X144)
| p2(X131)
| ~ r1(X130,X131)
| ~ r1(X130,X132)
| p1(X143)
| ~ r1(X132,X143)
| p2(X133)
| ~ r1(X132,X133)
| ~ r1(X132,X134)
| p1(X142)
| ~ r1(X134,X142)
| p2(X135)
| ~ r1(X134,X135)
| ~ r1(X134,X136)
| ~ r1(X136,X137)
| r1(X137,esk26_5(X130,X132,X134,X136,X137))
| ~ r1(X136,X140)
| r1(X140,esk27_5(X130,X132,X134,X136,X140)) )
& ( p1(X128)
| ~ r1(esk1_0,X128)
| p2(X113)
| ~ r1(esk1_0,X113)
| ~ r1(esk1_0,X114)
| p1(X127)
| ~ r1(X114,X127)
| p2(X115)
| ~ r1(X114,X115)
| ~ r1(X114,X116)
| p1(X126)
| ~ r1(X116,X126)
| p2(X117)
| ~ r1(X116,X117)
| ~ r1(X116,X118)
| p1(X125)
| ~ r1(X118,X125)
| p2(X119)
| ~ r1(X118,X119)
| ~ r1(X118,X120)
| ~ r1(X120,X121)
| p1(X124)
| ~ r1(X121,X124)
| ~ r1(X121,X122)
| ~ p1(esk25_6(X114,X116,X118,X120,X121,X122)) )
& ( p1(X128)
| ~ r1(esk1_0,X128)
| p2(X113)
| ~ r1(esk1_0,X113)
| ~ r1(esk1_0,X114)
| p1(X127)
| ~ r1(X114,X127)
| p2(X115)
| ~ r1(X114,X115)
| ~ r1(X114,X116)
| p1(X126)
| ~ r1(X116,X126)
| p2(X117)
| ~ r1(X116,X117)
| ~ r1(X116,X118)
| p1(X125)
| ~ r1(X118,X125)
| p2(X119)
| ~ r1(X118,X119)
| ~ r1(X118,X120)
| ~ r1(X120,X121)
| p1(X124)
| ~ r1(X121,X124)
| ~ r1(X121,X122)
| r1(X122,esk25_6(X114,X116,X118,X120,X121,X122)) )
& ( p1(X112)
| ~ r1(esk1_0,X112)
| p2(X99)
| ~ r1(esk1_0,X99)
| ~ r1(esk1_0,X100)
| p1(X111)
| ~ r1(X100,X111)
| p2(X101)
| ~ r1(X100,X101)
| ~ r1(X100,X102)
| p1(X110)
| ~ r1(X102,X110)
| p2(X103)
| ~ r1(X102,X103)
| ~ r1(X102,X104)
| p1(X109)
| ~ r1(X104,X109)
| p2(X105)
| ~ r1(X104,X105)
| ~ r1(X104,X106)
| ~ p1(X106)
| ~ r1(X106,X107)
| p1(esk24_5(X100,X102,X104,X106,X107)) )
& ( p1(X112)
| ~ r1(esk1_0,X112)
| p2(X99)
| ~ r1(esk1_0,X99)
| ~ r1(esk1_0,X100)
| p1(X111)
| ~ r1(X100,X111)
| p2(X101)
| ~ r1(X100,X101)
| ~ r1(X100,X102)
| p1(X110)
| ~ r1(X102,X110)
| p2(X103)
| ~ r1(X102,X103)
| ~ r1(X102,X104)
| p1(X109)
| ~ r1(X104,X109)
| p2(X105)
| ~ r1(X104,X105)
| ~ r1(X104,X106)
| ~ p1(X106)
| ~ r1(X106,X107)
| r1(X107,esk24_5(X100,X102,X104,X106,X107)) )
& ~ p1(esk23_0)
& r1(esk1_0,esk23_0)
& ~ p1(esk22_0)
& r1(esk8_0,esk22_0)
& ~ p1(esk21_0)
& r1(esk10_0,esk21_0)
& ~ p1(esk20_0)
& r1(esk12_0,esk20_0)
& ~ p1(esk19_0)
& r1(esk14_0,esk19_0)
& ~ p1(esk18_0)
& r1(esk16_0,esk18_0)
& ( p1(X92)
| ~ r1(esk17_0,X92) )
& r1(esk16_0,esk17_0)
& r1(esk14_0,esk16_0)
& ~ p2(esk15_0)
& r1(esk14_0,esk15_0)
& r1(esk12_0,esk14_0)
& ~ p2(esk13_0)
& r1(esk12_0,esk13_0)
& r1(esk10_0,esk12_0)
& ~ p2(esk11_0)
& r1(esk10_0,esk11_0)
& r1(esk8_0,esk10_0)
& ~ p2(esk9_0)
& r1(esk8_0,esk9_0)
& r1(esk1_0,esk8_0)
& ~ p2(esk7_0)
& r1(esk1_0,esk7_0)
& ( p1(X80)
| ~ r1(esk1_0,X80)
| p2(X65)
| ~ r1(esk1_0,X65)
| ~ r1(esk1_0,X66)
| p1(X79)
| ~ r1(X66,X79)
| p2(X67)
| ~ r1(X66,X67)
| ~ r1(X66,X68)
| p1(X78)
| ~ r1(X68,X78)
| p2(X69)
| ~ r1(X68,X69)
| ~ r1(X68,X70)
| p1(X77)
| ~ r1(X70,X77)
| p2(X71)
| ~ r1(X70,X71)
| ~ r1(X70,X72)
| p1(X76)
| ~ r1(X72,X76)
| p2(X73)
| ~ r1(X72,X73)
| ~ r1(X72,X74)
| $true )
& ( p1(X80)
| ~ r1(esk1_0,X80)
| p2(X65)
| ~ r1(esk1_0,X65)
| ~ r1(esk1_0,X66)
| p1(X79)
| ~ r1(X66,X79)
| p2(X67)
| ~ r1(X66,X67)
| ~ r1(X66,X68)
| p1(X78)
| ~ r1(X68,X78)
| p2(X69)
| ~ r1(X68,X69)
| ~ r1(X68,X70)
| p1(X77)
| ~ r1(X70,X77)
| p2(X71)
| ~ r1(X70,X71)
| ~ r1(X70,X72)
| p1(X76)
| ~ r1(X72,X76)
| p2(X73)
| ~ r1(X72,X73)
| ~ r1(X72,X74)
| r1(X74,esk6_5(X66,X68,X70,X72,X74)) )
& ( p1(X64)
| ~ r1(esk1_0,X64)
| p2(X45)
| ~ r1(esk1_0,X45)
| ~ r1(esk1_0,X46)
| p1(X63)
| ~ r1(X46,X63)
| p2(X47)
| ~ r1(X46,X47)
| ~ r1(X46,X48)
| p1(X62)
| ~ r1(X48,X62)
| p2(X49)
| ~ r1(X48,X49)
| ~ r1(X48,X50)
| p1(X61)
| ~ r1(X50,X61)
| p2(X51)
| ~ r1(X50,X51)
| ~ r1(X50,X52)
| p1(X60)
| ~ r1(X52,X60)
| p2(X53)
| ~ r1(X52,X53)
| ~ r1(X52,X54)
| ~ r1(X54,X55)
| p1(X57)
| ~ r1(esk4_6(X46,X48,X50,X52,X54,X55),X57)
| ~ r1(X54,X58)
| ~ p1(esk5_6(X46,X48,X50,X52,X54,X58)) )
& ( p1(X64)
| ~ r1(esk1_0,X64)
| p2(X45)
| ~ r1(esk1_0,X45)
| ~ r1(esk1_0,X46)
| p1(X63)
| ~ r1(X46,X63)
| p2(X47)
| ~ r1(X46,X47)
| ~ r1(X46,X48)
| p1(X62)
| ~ r1(X48,X62)
| p2(X49)
| ~ r1(X48,X49)
| ~ r1(X48,X50)
| p1(X61)
| ~ r1(X50,X61)
| p2(X51)
| ~ r1(X50,X51)
| ~ r1(X50,X52)
| p1(X60)
| ~ r1(X52,X60)
| p2(X53)
| ~ r1(X52,X53)
| ~ r1(X52,X54)
| ~ r1(X54,X55)
| p1(X57)
| ~ r1(esk4_6(X46,X48,X50,X52,X54,X55),X57)
| ~ r1(X54,X58)
| r1(X58,esk5_6(X46,X48,X50,X52,X54,X58)) )
& ( p1(X64)
| ~ r1(esk1_0,X64)
| p2(X45)
| ~ r1(esk1_0,X45)
| ~ r1(esk1_0,X46)
| p1(X63)
| ~ r1(X46,X63)
| p2(X47)
| ~ r1(X46,X47)
| ~ r1(X46,X48)
| p1(X62)
| ~ r1(X48,X62)
| p2(X49)
| ~ r1(X48,X49)
| ~ r1(X48,X50)
| p1(X61)
| ~ r1(X50,X61)
| p2(X51)
| ~ r1(X50,X51)
| ~ r1(X50,X52)
| p1(X60)
| ~ r1(X52,X60)
| p2(X53)
| ~ r1(X52,X53)
| ~ r1(X52,X54)
| ~ r1(X54,X55)
| r1(X55,esk4_6(X46,X48,X50,X52,X54,X55))
| ~ r1(X54,X58)
| ~ p1(esk5_6(X46,X48,X50,X52,X54,X58)) )
& ( p1(X64)
| ~ r1(esk1_0,X64)
| p2(X45)
| ~ r1(esk1_0,X45)
| ~ r1(esk1_0,X46)
| p1(X63)
| ~ r1(X46,X63)
| p2(X47)
| ~ r1(X46,X47)
| ~ r1(X46,X48)
| p1(X62)
| ~ r1(X48,X62)
| p2(X49)
| ~ r1(X48,X49)
| ~ r1(X48,X50)
| p1(X61)
| ~ r1(X50,X61)
| p2(X51)
| ~ r1(X50,X51)
| ~ r1(X50,X52)
| p1(X60)
| ~ r1(X52,X60)
| p2(X53)
| ~ r1(X52,X53)
| ~ r1(X52,X54)
| ~ r1(X54,X55)
| r1(X55,esk4_6(X46,X48,X50,X52,X54,X55))
| ~ r1(X54,X58)
| r1(X58,esk5_6(X46,X48,X50,X52,X54,X58)) )
& ( p1(X44)
| ~ r1(esk1_0,X44)
| p2(X26)
| ~ r1(esk1_0,X26)
| ~ r1(esk1_0,X27)
| p1(X43)
| ~ r1(X27,X43)
| p2(X28)
| ~ r1(X27,X28)
| ~ r1(X27,X29)
| p1(X42)
| ~ r1(X29,X42)
| p2(X30)
| ~ r1(X29,X30)
| ~ r1(X29,X31)
| p1(X41)
| ~ r1(X31,X41)
| p2(X32)
| ~ r1(X31,X32)
| ~ r1(X31,X33)
| p1(X40)
| ~ r1(X33,X40)
| p2(X34)
| ~ r1(X33,X34)
| ~ r1(X33,X35)
| ~ r1(X35,X36)
| p1(X39)
| ~ r1(X36,X39)
| ~ r1(X36,X37)
| ~ p1(esk3_7(X27,X29,X31,X33,X35,X36,X37)) )
& ( p1(X44)
| ~ r1(esk1_0,X44)
| p2(X26)
| ~ r1(esk1_0,X26)
| ~ r1(esk1_0,X27)
| p1(X43)
| ~ r1(X27,X43)
| p2(X28)
| ~ r1(X27,X28)
| ~ r1(X27,X29)
| p1(X42)
| ~ r1(X29,X42)
| p2(X30)
| ~ r1(X29,X30)
| ~ r1(X29,X31)
| p1(X41)
| ~ r1(X31,X41)
| p2(X32)
| ~ r1(X31,X32)
| ~ r1(X31,X33)
| p1(X40)
| ~ r1(X33,X40)
| p2(X34)
| ~ r1(X33,X34)
| ~ r1(X33,X35)
| ~ r1(X35,X36)
| p1(X39)
| ~ r1(X36,X39)
| ~ r1(X36,X37)
| r1(X37,esk3_7(X27,X29,X31,X33,X35,X36,X37)) )
& ( p1(X25)
| ~ r1(esk1_0,X25)
| p2(X9)
| ~ r1(esk1_0,X9)
| ~ r1(esk1_0,X10)
| p1(X24)
| ~ r1(X10,X24)
| p2(X11)
| ~ r1(X10,X11)
| ~ r1(X10,X12)
| p1(X23)
| ~ r1(X12,X23)
| p2(X13)
| ~ r1(X12,X13)
| ~ r1(X12,X14)
| p1(X22)
| ~ r1(X14,X22)
| p2(X15)
| ~ r1(X14,X15)
| ~ r1(X14,X16)
| p1(X21)
| ~ r1(X16,X21)
| p2(X17)
| ~ r1(X16,X17)
| ~ r1(X16,X18)
| ~ p1(X18)
| ~ r1(X18,X19)
| p1(esk2_6(X10,X12,X14,X16,X18,X19)) )
& ( p1(X25)
| ~ r1(esk1_0,X25)
| p2(X9)
| ~ r1(esk1_0,X9)
| ~ r1(esk1_0,X10)
| p1(X24)
| ~ r1(X10,X24)
| p2(X11)
| ~ r1(X10,X11)
| ~ r1(X10,X12)
| p1(X23)
| ~ r1(X12,X23)
| p2(X13)
| ~ r1(X12,X13)
| ~ r1(X12,X14)
| p1(X22)
| ~ r1(X14,X22)
| p2(X15)
| ~ r1(X14,X15)
| ~ r1(X14,X16)
| p1(X21)
| ~ r1(X16,X21)
| p2(X17)
| ~ r1(X16,X17)
| ~ r1(X16,X18)
| ~ p1(X18)
| ~ r1(X18,X19)
| r1(X19,esk2_6(X10,X12,X14,X16,X18,X19)) ) ),
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_4])])])])])]) ).
cnf(c_0_7,plain,
( ~ r1(X2,X3)
| ~ r1(X1,X2)
| r1(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_8,negated_conjecture,
r1(esk96_0,esk98_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_9,negated_conjecture,
r1(esk98_0,esk100_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_10,negated_conjecture,
( ~ r1(X1,esk96_0)
| r1(X1,esk98_0) ),
inference(spm,[status(thm)],[c_0_7,c_0_8]) ).
cnf(c_0_11,negated_conjecture,
r1(esk1_0,esk96_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_12,negated_conjecture,
r1(esk100_0,esk102_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_13,negated_conjecture,
( ~ r1(X1,esk98_0)
| r1(X1,esk100_0) ),
inference(spm,[status(thm)],[c_0_7,c_0_9]) ).
cnf(c_0_14,negated_conjecture,
r1(esk1_0,esk98_0),
inference(spm,[status(thm)],[c_0_10,c_0_11]) ).
cnf(c_0_15,negated_conjecture,
( ~ r1(esk1_0,X6)
| ~ r1(esk1_0,X5)
| ~ r1(esk1_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X3,X1)
| p1(X6)
| p2(X5)
| p1(X4)
| r1(X1,esk91_3(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_16,negated_conjecture,
r1(esk104_0,esk106_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_17,negated_conjecture,
~ p1(esk106_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_18,negated_conjecture,
r1(esk102_0,esk103_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_19,negated_conjecture,
( ~ r1(X1,esk100_0)
| r1(X1,esk102_0) ),
inference(spm,[status(thm)],[c_0_7,c_0_12]) ).
cnf(c_0_20,negated_conjecture,
r1(esk1_0,esk100_0),
inference(spm,[status(thm)],[c_0_13,c_0_14]) ).
cnf(c_0_21,negated_conjecture,
( ~ r1(X4,esk104_0)
| ~ r1(esk104_0,X3)
| ~ r1(esk1_0,X4)
| ~ r1(esk1_0,X2)
| ~ r1(esk1_0,X1)
| r1(X3,esk91_3(X4,esk104_0,X3))
| p2(X2)
| p1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_16]),c_0_17]) ).
cnf(c_0_22,negated_conjecture,
r1(esk1_0,esk111_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_23,negated_conjecture,
~ p1(esk111_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_24,negated_conjecture,
( ~ r1(X1,esk102_0)
| r1(X1,esk103_0) ),
inference(spm,[status(thm)],[c_0_7,c_0_18]) ).
cnf(c_0_25,negated_conjecture,
r1(esk1_0,esk102_0),
inference(spm,[status(thm)],[c_0_19,c_0_20]) ).
cnf(c_0_26,negated_conjecture,
r1(esk102_0,esk104_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_27,negated_conjecture,
( ~ r1(X3,esk104_0)
| ~ r1(esk104_0,X2)
| ~ r1(esk1_0,X3)
| ~ r1(esk1_0,X1)
| r1(X2,esk91_3(X3,esk104_0,X2))
| p2(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_22]),c_0_23]) ).
cnf(c_0_28,negated_conjecture,
r1(esk1_0,esk103_0),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_29,negated_conjecture,
~ p2(esk103_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
fof(c_0_30,plain,
! [X4] : r1(X4,X4),
inference(variable_rename,[status(thm)],[reflexivity]) ).
cnf(c_0_31,negated_conjecture,
( ~ r1(X1,esk102_0)
| r1(X1,esk104_0) ),
inference(spm,[status(thm)],[c_0_7,c_0_26]) ).
cnf(c_0_32,negated_conjecture,
( ~ r1(X2,esk104_0)
| ~ r1(esk104_0,X1)
| ~ r1(esk1_0,X2)
| r1(X1,esk91_3(X2,esk104_0,X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_27,c_0_28]),c_0_29]) ).
cnf(c_0_33,plain,
r1(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_34,negated_conjecture,
r1(esk1_0,esk104_0),
inference(spm,[status(thm)],[c_0_31,c_0_25]) ).
cnf(c_0_35,negated_conjecture,
( ~ r1(esk104_0,X1)
| r1(X1,esk91_3(esk1_0,esk104_0,X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_34])]) ).
cnf(c_0_36,negated_conjecture,
r1(esk104_0,esk105_0),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_37,negated_conjecture,
( ~ r1(esk105_0,X1)
| p1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_38,negated_conjecture,
r1(esk105_0,esk91_3(esk1_0,esk104_0,esk105_0)),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_39,negated_conjecture,
( ~ r1(esk1_0,X6)
| ~ r1(esk1_0,X5)
| ~ r1(esk1_0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X4)
| ~ r1(X2,X3)
| ~ p1(esk91_3(X1,X2,X3))
| p1(X6)
| p2(X5)
| p1(X4) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_40,negated_conjecture,
p1(esk91_3(esk1_0,esk104_0,esk105_0)),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_41,negated_conjecture,
( ~ r1(esk104_0,X2)
| ~ r1(esk1_0,X3)
| ~ r1(esk1_0,X1)
| p2(X3)
| p1(X2)
| p1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_40]),c_0_33]),c_0_36]),c_0_34])]) ).
cnf(c_0_42,negated_conjecture,
( ~ r1(esk104_0,X1)
| ~ r1(esk1_0,X2)
| p2(X2)
| p1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41,c_0_22]),c_0_23]) ).
cnf(c_0_43,negated_conjecture,
( ~ r1(esk104_0,X1)
| p1(X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_28]),c_0_29]) ).
cnf(c_0_44,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_16]),c_0_17]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL672+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.43 % Computer : n014.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 00:53:05 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.51 Running first-order theorem proving
% 0.26/0.51 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
% 122.27/18.39 % Version: 3.5.1
% 122.27/18.39 % Preprocessing class: FSLSSMSSSSSNFFN.
% 122.27/18.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 122.27/18.39 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 122.27/18.39 % Starting new_bool_3 with 300s (1) cores
% 122.27/18.39 % Starting new_bool_1 with 300s (1) cores
% 122.27/18.39 % Starting sh5l with 300s (1) cores
% 122.27/18.39 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 2804313 completed with status 0
% 122.27/18.39 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 122.27/18.39 % Preprocessing class: FSLSSMSSSSSNFFN.
% 122.27/18.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 122.27/18.39 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 122.27/18.39 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 122.27/18.39 % No SInE strategy applied
% 122.27/18.39 % Search class: FGUNF-FSLM33-SFFFFFNN
% 122.27/18.39 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 122.27/18.39 % Starting SubtermCWHack with 136s (1) cores
% 122.27/18.39 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 122.27/18.39 % Starting new_bool_3 with 407s (1) cores
% 122.27/18.39 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 296s (1) cores
% 122.27/18.39 % Starting H----_047_B31_F1_PI_AE_R4_CS_SP_S4d with 136s (1) cores
% 122.27/18.39 % H----_047_B31_F1_PI_AE_R4_CS_SP_S4d with pid 2804321 completed with status 0
% 122.27/18.39 % Result found by H----_047_B31_F1_PI_AE_R4_CS_SP_S4d
% 122.27/18.39 % Preprocessing class: FSLSSMSSSSSNFFN.
% 122.27/18.39 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 122.27/18.39 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 122.27/18.39 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 122.27/18.39 % No SInE strategy applied
% 122.27/18.39 % Search class: FGUNF-FSLM33-SFFFFFNN
% 122.27/18.39 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 122.27/18.39 % Starting SubtermCWHack with 136s (1) cores
% 122.27/18.39 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 122.27/18.39 % Starting new_bool_3 with 407s (1) cores
% 122.27/18.39 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 296s (1) cores
% 122.27/18.39 % Starting H----_047_B31_F1_PI_AE_R4_CS_SP_S4d with 136s (1) cores
% 122.27/18.39 % Preprocessing time : 0.009 s
% 122.27/18.39
% 122.27/18.39 % Proof found!
% 122.27/18.39 % SZS status Theorem
% 122.27/18.39 % SZS output start CNFRefutation
% See solution above
% 122.27/18.39 % Parsed axioms : 3
% 122.27/18.39 % Removed by relevancy pruning/SinE : 0
% 122.27/18.39 % Initial clauses : 197
% 122.27/18.39 % Removed in clause preprocessing : 5
% 122.27/18.39 % Initial clauses in saturation : 192
% 122.27/18.39 % Processed clauses : 7692
% 122.27/18.39 % ...of these trivial : 29
% 122.27/18.39 % ...subsumed : 100
% 122.27/18.39 % ...remaining for further processing : 7563
% 122.27/18.39 % Other redundant clauses eliminated : 0
% 122.27/18.39 % Clauses deleted for lack of memory : 0
% 122.27/18.39 % Backward-subsumed : 21
% 122.27/18.39 % Backward-rewritten : 10
% 122.27/18.39 % Generated clauses : 170200
% 122.27/18.39 % ...of the previous two non-redundant : 150987
% 122.27/18.39 % ...aggressively subsumed : 0
% 122.27/18.39 % Contextual simplify-reflections : 0
% 122.27/18.39 % Paramodulations : 170200
% 122.27/18.39 % Factorizations : 0
% 122.27/18.39 % NegExts : 0
% 122.27/18.39 % Equation resolutions : 0
% 122.27/18.39 % Disequality decompositions : 0
% 122.27/18.39 % Total rewrite steps : 38936
% 122.27/18.39 % ...of those cached : 35948
% 122.27/18.39 % Propositional unsat checks : 0
% 122.27/18.39 % Propositional check models : 0
% 122.27/18.39 % Propositional check unsatisfiable : 0
% 122.27/18.39 % Propositional clauses : 0
% 122.27/18.39 % Propositional clauses after purity: 0
% 122.27/18.39 % Propositional unsat core size : 0
% 122.27/18.39 % Propositional preprocessing time : 0.000
% 122.27/18.39 % Propositional encoding time : 0.000
% 122.27/18.39 % Propositional solver time : 0.000
% 122.27/18.39 % Success case prop preproc time : 0.000
% 122.27/18.39 % Success case prop encoding time : 0.000
% 122.27/18.39 % Success case prop solver time : 0.000
% 122.27/18.39 % Current number of processed clauses : 7532
% 122.27/18.39 % Positive orientable unit clauses : 3131
% 122.27/18.39 % Positive unorientable unit clauses: 0
% 122.27/18.39 % Negative unit clauses : 55
% 122.27/18.39 % Non-unit-clauses : 4346
% 122.27/18.39 % Current number of unprocessed clauses: 134996
% 122.27/18.39 % ...number of literals in the above : 1770098
% 122.27/18.39 % Current number of archived formulas : 0
% 122.27/18.39 % Current number of archived clauses : 31
% 122.27/18.39 % Clause-clause subsumption calls (NU) : 8100252
% 122.27/18.39 % Rec. Clause-clause subsumption calls : 1682138
% 122.27/18.39 % Non-unit clause-clause subsumptions : 31
% 122.27/18.39 % Unit Clause-clause subsumption calls : 1110875
% 122.27/18.39 % Rewrite failures with RHS unbound : 0
% 122.27/18.39 % BW rewrite match attempts : 151499
% 122.27/18.39 % BW rewrite match successes : 10
% 122.27/18.39 % Condensation attempts : 0
% 122.27/18.39 % Condensation successes : 0
% 122.27/18.39 % Termbank termtop insertions : 6464701
% 122.27/18.39 % Search garbage collected termcells : 4887
% 122.27/18.39
% 122.27/18.39 % -------------------------------------------------
% 122.27/18.39 % User time : 16.696 s
% 122.27/18.39 % System time : 0.284 s
% 122.27/18.39 % Total time : 16.979 s
% 122.27/18.39 % Maximum resident set size: 4692 pages
% 122.27/18.39
% 122.27/18.39 % -------------------------------------------------
% 122.27/18.39 % User time : 85.365 s
% 122.27/18.39 % System time : 1.328 s
% 122.27/18.39 % Total time : 86.694 s
% 122.27/18.39 % Maximum resident set size: 4864 pages
% 122.27/18.39 % E exiting
%------------------------------------------------------------------------------