%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL652+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:07:08 PM UTC 2026
% Result : Theorem 32.00s 5.51s
% Output : CNFRefutation 32.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 177 ( 14 unt; 8 def)
% Number of atoms : 2812 ( 0 equ)
% Maximal formula atoms : 186 ( 15 avg)
% Number of connectives : 4931 (2424 ~;1959 |; 548 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 57 ( 10 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 16 usr; 1 prp; 0-2 aty)
% Number of functors : 53 ( 53 usr; 21 con; 0-1 aty)
% Number of variables : 1654 ( 0 sgn1401 !; 253 ?; 123 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& p2(X0)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ( ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p2(X0)
| ! [X1] :
( p3(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ ! [X0] :
( ~ ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& p2(X0)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X0] :
( p3(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X126] :
( ~ ! [X129] :
( ~ p1(X129)
| ~ r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ! [X87] :
( ~ ! [X122] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
| ! [X92] :
( ~ ! [X118] :
( ~ ! [X121] :
( ~ p1(X121)
| ~ r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
| ! [X97] :
( ~ ! [X114] :
( ~ ! [X117] :
( ~ p1(X117)
| ~ r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
| ! [X102] :
( ~ ! [X110] :
( ~ ! [X113] :
( ~ p1(X113)
| ~ r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
| ! [X107] :
( ~ ! [X108] :
( ~ ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X102,X107) )
| ! [X103] :
( ! [X106] :
( p1(X106)
| ~ r1(X103,X106) )
| ! [X104] :
( ~ ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X97,X102) )
| ! [X98] :
( ! [X101] :
( p1(X101)
| ~ r1(X98,X101) )
| ! [X99] :
( ~ ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X92,X97) )
| ! [X93] :
( ! [X96] :
( p1(X96)
| ~ r1(X93,X96) )
| ! [X94] :
( ~ ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X87,X92) )
| ! [X88] :
( ! [X91] :
( p1(X91)
| ~ r1(X88,X91) )
| ! [X89] :
( ~ ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X0,X87) )
| ! [X83] :
( ! [X86] :
( p1(X86)
| ~ r1(X83,X86) )
| ! [X84] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X0,X83) )
| ~ ! [X79] :
( ~ ( ! [X82] :
( p1(X82)
| ~ r1(X79,X82) )
& ~ ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X0,X79) )
| ~ ! [X8] :
( ~ ( ~ ! [X75] :
( ~ ( ! [X78] :
( p1(X78)
| ~ r1(X75,X78) )
& ~ ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) ) )
| ~ r1(X8,X75) )
| ~ ! [X15] :
( ~ ( ~ ! [X71] :
( ~ ( ! [X74] :
( p1(X74)
| ~ r1(X71,X74) )
& ~ ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) ) )
| ~ r1(X15,X71) )
| ~ ! [X22] :
( ~ ( ~ ! [X67] :
( ~ ( ! [X70] :
( p1(X70)
| ~ r1(X67,X70) )
& ~ ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) ) )
| ~ r1(X22,X67) )
| ~ ! [X29] :
( ~ ( ~ ! [X63] :
( ~ ( ! [X66] :
( p1(X66)
| ~ r1(X63,X66) )
& ~ ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) ) )
| ~ r1(X29,X63) )
| ~ ! [X36] :
( ~ ( ( ! [X61] :
( ~ ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
| ~ r1(X36,X61) )
& ! [X59] :
( ~ p2(X59)
| ! [X60] :
( p3(X60)
| ~ r1(X59,X60) )
| ~ r1(X36,X59) ) )
| ~ ! [X52] :
( ~ ( ! [X55] :
( ~ ! [X56] :
( ~ ! [X57] :
( ~ p2(X57)
| ! [X58] :
( p3(X58)
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X52,X55) )
& ! [X53] :
( ~ ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) ) )
| ~ r1(X36,X52) )
| ( ! [X50] :
( ~ ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
| ~ r1(X36,X50) )
& ~ ! [X46] :
( ! [X47] :
( ~ ! [X48] :
( ~ p2(X48)
| ! [X49] :
( p3(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
| ~ ! [X40] :
( ~ ( ~ ! [X43] :
( ~ ! [X44] :
( ~ ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X40,X43) )
& p2(X40)
& ~ ! [X41] :
( ~ ( ~ p2(X41)
| ! [X42] :
( p3(X42)
| ~ r1(X41,X42) ) )
| ~ r1(X40,X41) ) )
| ~ r1(X36,X40) )
| ~ ! [X37] :
( ~ ! [X38] :
( ~ p2(X38)
| ! [X39] :
( p3(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
| ~ ! [X30] :
( ~ ( ! [X34] :
( ~ ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
| ~ r1(X30,X34) )
& ~ ! [X31] :
( ! [X32] :
( ~ ! [X33] :
( ~ p1(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
| ~ ! [X23] :
( ~ ( ! [X27] :
( ~ ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X23,X27) )
& ~ ! [X24] :
( ! [X25] :
( ~ ! [X26] :
( ~ p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) ) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
| ~ ! [X16] :
( ~ ( ! [X20] :
( ~ ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
| ~ r1(X16,X20) )
& ~ ! [X17] :
( ! [X18] :
( ~ ! [X19] :
( ~ p1(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) ) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
| ~ ! [X9] :
( ~ ( ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X9,X13) )
& ~ ! [X10] :
( ! [X11] :
( ~ ! [X12] :
( ~ p1(X12)
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) ) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
| ~ ! [X2] :
( ~ ( ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X2,X6) )
& ~ ! [X3] :
( ! [X4] :
( ~ ! [X5] :
( ~ p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X126] :
( ~ ! [X129] :
( ~ p1(X129)
| ~ r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ! [X87] :
( ~ ! [X122] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
| ! [X92] :
( ~ ! [X118] :
( ~ ! [X121] :
( ~ p1(X121)
| ~ r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
| ! [X97] :
( ~ ! [X114] :
( ~ ! [X117] :
( ~ p1(X117)
| ~ r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
| ! [X102] :
( ~ ! [X110] :
( ~ ! [X113] :
( ~ p1(X113)
| ~ r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
| ! [X107] :
( ~ ! [X108] :
( ~ ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X102,X107) )
| ! [X103] :
( ! [X106] :
( p1(X106)
| ~ r1(X103,X106) )
| ! [X104] :
( ~ ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X97,X102) )
| ! [X98] :
( ! [X101] :
( p1(X101)
| ~ r1(X98,X101) )
| ! [X99] :
( ~ ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X92,X97) )
| ! [X93] :
( ! [X96] :
( p1(X96)
| ~ r1(X93,X96) )
| ! [X94] :
( ~ ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X87,X92) )
| ! [X88] :
( ! [X91] :
( p1(X91)
| ~ r1(X88,X91) )
| ! [X89] :
( ~ ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X0,X87) )
| ! [X83] :
( ! [X86] :
( p1(X86)
| ~ r1(X83,X86) )
| ! [X84] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X0,X83) )
| ~ ! [X79] :
( ~ ( ! [X82] :
( p1(X82)
| ~ r1(X79,X82) )
& ~ ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X0,X79) )
| ~ ! [X8] :
( ~ ( ~ ! [X75] :
( ~ ( ! [X78] :
( p1(X78)
| ~ r1(X75,X78) )
& ~ ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) ) )
| ~ r1(X8,X75) )
| ~ ! [X15] :
( ~ ( ~ ! [X71] :
( ~ ( ! [X74] :
( p1(X74)
| ~ r1(X71,X74) )
& ~ ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) ) )
| ~ r1(X15,X71) )
| ~ ! [X22] :
( ~ ( ~ ! [X67] :
( ~ ( ! [X70] :
( p1(X70)
| ~ r1(X67,X70) )
& ~ ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) ) )
| ~ r1(X22,X67) )
| ~ ! [X29] :
( ~ ( ~ ! [X63] :
( ~ ( ! [X66] :
( p1(X66)
| ~ r1(X63,X66) )
& ~ ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) ) )
| ~ r1(X29,X63) )
| ~ ! [X36] :
( ~ ( ( ! [X61] :
( ~ ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
| ~ r1(X36,X61) )
& ! [X59] :
( ~ p2(X59)
| ! [X60] :
( p3(X60)
| ~ r1(X59,X60) )
| ~ r1(X36,X59) ) )
| ~ ! [X52] :
( ~ ( ! [X55] :
( ~ ! [X56] :
( ~ ! [X57] :
( ~ p2(X57)
| ! [X58] :
( p3(X58)
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X52,X55) )
& ! [X53] :
( ~ ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) ) )
| ~ r1(X36,X52) )
| ( ! [X50] :
( ~ ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
| ~ r1(X36,X50) )
& ~ ! [X46] :
( ! [X47] :
( ~ ! [X48] :
( ~ p2(X48)
| ! [X49] :
( p3(X49)
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
| ~ ! [X40] :
( ~ ( ~ ! [X43] :
( ~ ! [X44] :
( ~ ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X40,X43) )
& p2(X40)
& ~ ! [X41] :
( ~ ( ~ p2(X41)
| ! [X42] :
( p3(X42)
| ~ r1(X41,X42) ) )
| ~ r1(X40,X41) ) )
| ~ r1(X36,X40) )
| ~ ! [X37] :
( ~ ! [X38] :
( ~ p2(X38)
| ! [X39] :
( p3(X39)
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
| ~ ! [X30] :
( ~ ( ! [X34] :
( ~ ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
| ~ r1(X30,X34) )
& ~ ! [X31] :
( ! [X32] :
( ~ ! [X33] :
( ~ p1(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
| ~ ! [X23] :
( ~ ( ! [X27] :
( ~ ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X23,X27) )
& ~ ! [X24] :
( ! [X25] :
( ~ ! [X26] :
( ~ p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) ) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
| ~ ! [X16] :
( ~ ( ! [X20] :
( ~ ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
| ~ r1(X16,X20) )
& ~ ! [X17] :
( ! [X18] :
( ~ ! [X19] :
( ~ p1(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) ) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
| ~ ! [X9] :
( ~ ( ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X9,X13) )
& ~ ! [X10] :
( ! [X11] :
( ~ ! [X12] :
( ~ p1(X12)
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) ) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
| ~ ! [X2] :
( ~ ( ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X2,X6) )
& ~ ! [X3] :
( ! [X4] :
( ~ ! [X5] :
( ~ p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X126] :
( ~ ! [X129] :
( ~ p1(X129)
| ~ r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ! [X87] :
( ~ ! [X122] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
| ! [X92] :
( ~ ! [X118] :
( ~ ! [X121] :
( ~ p1(X121)
| ~ r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
| ! [X97] :
( ~ ! [X114] :
( ~ ! [X117] :
( ~ p1(X117)
| ~ r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
| ! [X102] :
( ~ ! [X110] :
( ~ ! [X113] :
( ~ p1(X113)
| ~ r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
| ! [X107] :
( ~ ! [X108] :
( ~ ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X102,X107) )
| ! [X103] :
( ! [X106] :
( p1(X106)
| ~ r1(X103,X106) )
| ! [X104] :
( ~ ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X97,X102) )
| ! [X98] :
( ! [X101] :
( p1(X101)
| ~ r1(X98,X101) )
| ! [X99] :
( ~ ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X92,X97) )
| ! [X93] :
( ! [X96] :
( p1(X96)
| ~ r1(X93,X96) )
| ! [X94] :
( ~ ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X87,X92) )
| ! [X88] :
( ! [X91] :
( p1(X91)
| ~ r1(X88,X91) )
| ! [X89] :
( ~ ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X0,X87) )
| ! [X83] :
( ! [X86] :
( p1(X86)
| ~ r1(X83,X86) )
| ! [X84] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X0,X83) )
| ~ ! [X79] :
( ~ ( ! [X82] :
( p1(X82)
| ~ r1(X79,X82) )
& ~ ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X0,X79) )
| ~ ! [X8] :
( ~ ( ~ ! [X75] :
( ~ ( ! [X78] :
( p1(X78)
| ~ r1(X75,X78) )
& ~ ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) ) )
| ~ r1(X8,X75) )
| ~ ! [X15] :
( ~ ( ~ ! [X71] :
( ~ ( ! [X74] :
( p1(X74)
| ~ r1(X71,X74) )
& ~ ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) ) )
| ~ r1(X15,X71) )
| ~ ! [X22] :
( ~ ( ~ ! [X67] :
( ~ ( ! [X70] :
( p1(X70)
| ~ r1(X67,X70) )
& ~ ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) ) )
| ~ r1(X22,X67) )
| ~ ! [X29] :
( ~ ( ~ ! [X63] :
( ~ ( ! [X66] :
( p1(X66)
| ~ r1(X63,X66) )
& ~ ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) ) )
| ~ r1(X29,X63) )
| ~ ! [X36] :
( ~ ( ( ! [X61] :
( ~ ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
| ~ r1(X36,X61) )
& ! [X59] :
( ~ p2(X59)
| ! [X60] : ~ r1(X59,X60)
| ~ r1(X36,X59) ) )
| ~ ! [X52] :
( ~ ( ! [X55] :
( ~ ! [X56] :
( ~ ! [X57] :
( ~ p2(X57)
| ! [X58] : ~ r1(X57,X58)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X52,X55) )
& ! [X53] :
( ~ ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) ) )
| ~ r1(X36,X52) )
| ( ! [X50] :
( ~ ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
| ~ r1(X36,X50) )
& ~ ! [X46] :
( ! [X47] :
( ~ ! [X48] :
( ~ p2(X48)
| ! [X49] : ~ r1(X48,X49)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
| ~ ! [X40] :
( ~ ( ~ ! [X43] :
( ~ ! [X44] :
( ~ ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X40,X43) )
& p2(X40)
& ~ ! [X41] :
( ~ ( ~ p2(X41)
| ! [X42] : ~ r1(X41,X42) )
| ~ r1(X40,X41) ) )
| ~ r1(X36,X40) )
| ~ ! [X37] :
( ~ ! [X38] :
( ~ p2(X38)
| ! [X39] : ~ r1(X38,X39)
| ~ r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
| ~ ! [X30] :
( ~ ( ! [X34] :
( ~ ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
| ~ r1(X30,X34) )
& ~ ! [X31] :
( ! [X32] :
( ~ ! [X33] :
( ~ p1(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
| ~ ! [X23] :
( ~ ( ! [X27] :
( ~ ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X23,X27) )
& ~ ! [X24] :
( ! [X25] :
( ~ ! [X26] :
( ~ p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) ) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
| ~ ! [X16] :
( ~ ( ! [X20] :
( ~ ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
| ~ r1(X16,X20) )
& ~ ! [X17] :
( ! [X18] :
( ~ ! [X19] :
( ~ p1(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) ) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
| ~ ! [X9] :
( ~ ( ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X9,X13) )
& ~ ! [X10] :
( ! [X11] :
( ~ ! [X12] :
( ~ p1(X12)
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) ) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
| ~ ! [X2] :
( ~ ( ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X2,X6) )
& ~ ! [X3] :
( ! [X4] :
( ~ ! [X5] :
( ~ p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) )
| ~ ! [X1] :
( ~ p4(X1)
| ~ r1(X0,X1) ) ),
inference(pure_predicate_removal,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ~ ! [X126] :
( ~ ! [X129] :
( ~ p1(X129)
| ~ r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ! [X87] :
( ~ ! [X122] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
| ! [X92] :
( ~ ! [X118] :
( ~ ! [X121] :
( ~ p1(X121)
| ~ r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
| ! [X97] :
( ~ ! [X114] :
( ~ ! [X117] :
( ~ p1(X117)
| ~ r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
| ! [X102] :
( ~ ! [X110] :
( ~ ! [X113] :
( ~ p1(X113)
| ~ r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
| ! [X107] :
( ~ ! [X108] :
( ~ ! [X109] :
( p2(X109)
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X102,X107) )
| ! [X103] :
( ! [X106] :
( p1(X106)
| ~ r1(X103,X106) )
| ! [X104] :
( ~ ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X97,X102) )
| ! [X98] :
( ! [X101] :
( p1(X101)
| ~ r1(X98,X101) )
| ! [X99] :
( ~ ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X92,X97) )
| ! [X93] :
( ! [X96] :
( p1(X96)
| ~ r1(X93,X96) )
| ! [X94] :
( ~ ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X87,X92) )
| ! [X88] :
( ! [X91] :
( p1(X91)
| ~ r1(X88,X91) )
| ! [X89] :
( ~ ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X0,X87) )
| ! [X83] :
( ! [X86] :
( p1(X86)
| ~ r1(X83,X86) )
| ! [X84] :
( ~ ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X0,X83) )
| ~ ! [X79] :
( ~ ( ! [X82] :
( p1(X82)
| ~ r1(X79,X82) )
& ~ ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) ) )
| ~ r1(X0,X79) )
| ~ ! [X8] :
( ~ ( ~ ! [X75] :
( ~ ( ! [X78] :
( p1(X78)
| ~ r1(X75,X78) )
& ~ ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) ) )
| ~ r1(X8,X75) )
| ~ ! [X15] :
( ~ ( ~ ! [X71] :
( ~ ( ! [X74] :
( p1(X74)
| ~ r1(X71,X74) )
& ~ ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) ) )
| ~ r1(X15,X71) )
| ~ ! [X22] :
( ~ ( ~ ! [X67] :
( ~ ( ! [X70] :
( p1(X70)
| ~ r1(X67,X70) )
& ~ ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) ) )
| ~ r1(X22,X67) )
| ~ ! [X29] :
( ~ ( ~ ! [X63] :
( ~ ( ! [X66] :
( p1(X66)
| ~ r1(X63,X66) )
& ~ ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) ) )
| ~ r1(X29,X63) )
| ~ ! [X36] :
( ~ ( ( ! [X61] :
( ~ ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
| ~ r1(X36,X61) )
& ! [X59] :
( ~ p2(X59)
| ! [X60] : ~ r1(X59,X60)
| ~ r1(X36,X59) ) )
| ~ ! [X52] :
( ~ ( ! [X55] :
( ~ ! [X56] :
( ~ ! [X57] :
( ~ p2(X57)
| ! [X58] : ~ r1(X57,X58)
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X52,X55) )
& ! [X53] :
( ~ ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
| ~ r1(X52,X53) ) )
| ~ r1(X36,X52) )
| ( ! [X50] :
( ~ ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
| ~ r1(X36,X50) )
& ~ ! [X46] :
( ! [X47] :
( ~ ! [X48] :
( ~ p2(X48)
| ! [X49] : ~ r1(X48,X49)
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
| ~ ! [X40] :
( ~ ( ~ ! [X43] :
( ~ ! [X44] :
( ~ ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
| ~ r1(X43,X44) )
| ~ r1(X40,X43) )
& p2(X40)
& ~ ! [X41] :
( ~ ( ~ p2(X41)
| ! [X42] : ~ r1(X41,X42) )
| ~ r1(X40,X41) ) )
| ~ r1(X36,X40) )
| ~ ! [X37] :
( ~ ! [X38] :
( ~ p2(X38)
| ! [X39] : ~ r1(X38,X39)
| ~ r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
| ~ ! [X30] :
( ~ ( ! [X34] :
( ~ ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
| ~ r1(X30,X34) )
& ~ ! [X31] :
( ! [X32] :
( ~ ! [X33] :
( ~ p1(X33)
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) ) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
| ~ ! [X23] :
( ~ ( ! [X27] :
( ~ ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X23,X27) )
& ~ ! [X24] :
( ! [X25] :
( ~ ! [X26] :
( ~ p1(X26)
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) ) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
| ~ ! [X16] :
( ~ ( ! [X20] :
( ~ ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
| ~ r1(X16,X20) )
& ~ ! [X17] :
( ! [X18] :
( ~ ! [X19] :
( ~ p1(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) ) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
| ~ ! [X9] :
( ~ ( ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X9,X13) )
& ~ ! [X10] :
( ! [X11] :
( ~ ! [X12] :
( ~ p1(X12)
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) ) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
| ~ ! [X2] :
( ~ ( ! [X6] :
( ~ ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X2,X6) )
& ~ ! [X3] :
( ! [X4] :
( ~ ! [X5] :
( ~ p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) ) )
| ~ r1(X0,X2) ) ),
inference(pure_predicate_removal,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ! [X126] :
( ? [X129] :
( p1(X129)
& r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ? [X87] :
( ! [X122] :
( ? [X125] :
( p1(X125)
& r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
& ? [X92] :
( ! [X118] :
( ? [X121] :
( p1(X121)
& r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
& ? [X97] :
( ! [X114] :
( ? [X117] :
( p1(X117)
& r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
& ? [X102] :
( ! [X110] :
( ? [X113] :
( p1(X113)
& r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
& ? [X107] :
( ! [X108] :
( ? [X109] :
( ~ p2(X109)
& r1(X108,X109) )
| ~ r1(X107,X108) )
& r1(X102,X107) )
& ? [X103] :
( ? [X106] :
( ~ p1(X106)
& r1(X103,X106) )
& ? [X104] :
( ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
& r1(X103,X104) )
& r1(X102,X103) )
& r1(X97,X102) )
& ? [X98] :
( ? [X101] :
( ~ p1(X101)
& r1(X98,X101) )
& ? [X99] :
( ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
& r1(X98,X99) )
& r1(X97,X98) )
& r1(X92,X97) )
& ? [X93] :
( ? [X96] :
( ~ p1(X96)
& r1(X93,X96) )
& ? [X94] :
( ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
& r1(X93,X94) )
& r1(X92,X93) )
& r1(X87,X92) )
& ? [X88] :
( ? [X91] :
( ~ p1(X91)
& r1(X88,X91) )
& ? [X89] :
( ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X0,X87) )
& ? [X83] :
( ? [X86] :
( ~ p1(X86)
& r1(X83,X86) )
& ? [X84] :
( ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
& r1(X83,X84) )
& r1(X0,X83) )
& ! [X79] :
( ? [X82] :
( ~ p1(X82)
& r1(X79,X82) )
| ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X0,X79) )
& ! [X8] :
( ( ! [X75] :
( ? [X78] :
( ~ p1(X78)
& r1(X75,X78) )
| ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X8,X75) )
& ! [X15] :
( ( ! [X71] :
( ? [X74] :
( ~ p1(X74)
& r1(X71,X74) )
| ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X15,X71) )
& ! [X22] :
( ( ! [X67] :
( ? [X70] :
( ~ p1(X70)
& r1(X67,X70) )
| ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X22,X67) )
& ! [X29] :
( ( ! [X63] :
( ? [X66] :
( ~ p1(X66)
& r1(X63,X66) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X29,X63) )
& ! [X36] :
( ( ( ? [X61] :
( ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
& r1(X36,X61) )
| ? [X59] :
( p2(X59)
& ? [X60] : r1(X59,X60)
& r1(X36,X59) ) )
& ! [X52] :
( ? [X55] :
( ! [X56] :
( ? [X57] :
( p2(X57)
& ? [X58] : r1(X57,X58)
& r1(X56,X57) )
| ~ r1(X55,X56) )
& r1(X52,X55) )
| ? [X53] :
( ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
| ~ r1(X36,X52) )
& ( ? [X50] :
( ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
& r1(X36,X50) )
| ! [X46] :
( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] : r1(X48,X49)
& r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
& ! [X40] :
( ! [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
& r1(X43,X44) )
| ~ r1(X40,X43) )
| ~ p2(X40)
| ! [X41] :
( ( p2(X41)
& ? [X42] : r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X36,X40) )
& ! [X37] :
( ? [X38] :
( p2(X38)
& ? [X39] : r1(X38,X39)
& r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
& ! [X30] :
( ? [X34] :
( ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
& r1(X30,X34) )
| ! [X31] :
( ! [X32] :
( ? [X33] :
( p1(X33)
& r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
& ! [X23] :
( ? [X27] :
( ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
& r1(X23,X27) )
| ! [X24] :
( ! [X25] :
( ? [X26] :
( p1(X26)
& r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
& ! [X16] :
( ? [X20] :
( ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
& r1(X16,X20) )
| ! [X17] :
( ! [X18] :
( ? [X19] :
( p1(X19)
& r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
& ! [X9] :
( ? [X13] :
( ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
& r1(X9,X13) )
| ! [X10] :
( ! [X11] :
( ? [X12] :
( p1(X12)
& r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X0,X2) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f8,plain,
? [X0] :
( ! [X126] :
( ? [X129] :
( p1(X129)
& r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ? [X87] :
( ! [X122] :
( ? [X125] :
( p1(X125)
& r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
& ? [X92] :
( ! [X118] :
( ? [X121] :
( p1(X121)
& r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
& ? [X97] :
( ! [X114] :
( ? [X117] :
( p1(X117)
& r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
& ? [X102] :
( ! [X110] :
( ? [X113] :
( p1(X113)
& r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
& ? [X107] :
( ! [X108] :
( ? [X109] :
( ~ p2(X109)
& r1(X108,X109) )
| ~ r1(X107,X108) )
& r1(X102,X107) )
& ? [X103] :
( ? [X106] :
( ~ p1(X106)
& r1(X103,X106) )
& ? [X104] :
( ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
& r1(X103,X104) )
& r1(X102,X103) )
& r1(X97,X102) )
& ? [X98] :
( ? [X101] :
( ~ p1(X101)
& r1(X98,X101) )
& ? [X99] :
( ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
& r1(X98,X99) )
& r1(X97,X98) )
& r1(X92,X97) )
& ? [X93] :
( ? [X96] :
( ~ p1(X96)
& r1(X93,X96) )
& ? [X94] :
( ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
& r1(X93,X94) )
& r1(X92,X93) )
& r1(X87,X92) )
& ? [X88] :
( ? [X91] :
( ~ p1(X91)
& r1(X88,X91) )
& ? [X89] :
( ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X0,X87) )
& ? [X83] :
( ? [X86] :
( ~ p1(X86)
& r1(X83,X86) )
& ? [X84] :
( ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
& r1(X83,X84) )
& r1(X0,X83) )
& ! [X79] :
( ? [X82] :
( ~ p1(X82)
& r1(X79,X82) )
| ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X0,X79) )
& ! [X8] :
( ( ! [X75] :
( ? [X78] :
( ~ p1(X78)
& r1(X75,X78) )
| ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X8,X75) )
& ! [X15] :
( ( ! [X71] :
( ? [X74] :
( ~ p1(X74)
& r1(X71,X74) )
| ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X15,X71) )
& ! [X22] :
( ( ! [X67] :
( ? [X70] :
( ~ p1(X70)
& r1(X67,X70) )
| ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X22,X67) )
& ! [X29] :
( ( ! [X63] :
( ? [X66] :
( ~ p1(X66)
& r1(X63,X66) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X29,X63) )
& ! [X36] :
( ( ( ? [X61] :
( ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
& r1(X36,X61) )
| ? [X59] :
( p2(X59)
& ? [X60] : r1(X59,X60)
& r1(X36,X59) ) )
& ! [X52] :
( ? [X55] :
( ! [X56] :
( ? [X57] :
( p2(X57)
& ? [X58] : r1(X57,X58)
& r1(X56,X57) )
| ~ r1(X55,X56) )
& r1(X52,X55) )
| ? [X53] :
( ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
| ~ r1(X36,X52) )
& ( ? [X50] :
( ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
& r1(X36,X50) )
| ! [X46] :
( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] : r1(X48,X49)
& r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) )
& ! [X40] :
( ! [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
& r1(X43,X44) )
| ~ r1(X40,X43) )
| ~ p2(X40)
| ! [X41] :
( ( p2(X41)
& ? [X42] : r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X36,X40) )
& ! [X37] :
( ? [X38] :
( p2(X38)
& ? [X39] : r1(X38,X39)
& r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) )
& ! [X30] :
( ? [X34] :
( ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
& r1(X30,X34) )
| ! [X31] :
( ! [X32] :
( ? [X33] :
( p1(X33)
& r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) )
& ! [X23] :
( ? [X27] :
( ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
& r1(X23,X27) )
| ! [X24] :
( ! [X25] :
( ? [X26] :
( p1(X26)
& r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) )
& ! [X16] :
( ? [X20] :
( ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
& r1(X16,X20) )
| ! [X17] :
( ! [X18] :
( ? [X19] :
( p1(X19)
& r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) )
& ! [X9] :
( ? [X13] :
( ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
& r1(X9,X13) )
| ! [X10] :
( ! [X11] :
( ? [X12] :
( p1(X12)
& r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X0,X2) ) ),
inference(flattening,[],[f7]) ).
fof(f18,plain,
! [X8] :
( ~ sP7(X8)
| ! [X15] :
( ( ! [X71] :
( ? [X74] :
( ~ p1(X74)
& r1(X71,X74) )
| ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X15,X71) )
& sP6(X15)
& ! [X16] :
( ? [X20] :
( ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
& r1(X16,X20) )
| ! [X17] :
( ! [X18] :
( ? [X19] :
( p1(X19)
& r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f19,plain,
! [X0] :
( ~ sP7(X0)
| ! [X1] :
( ( ! [X8] :
( ? [X11] :
( ~ p1(X11)
& r1(X8,X11) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP6(X1)
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ~ sP7(X0)
| ! [X1] :
( ( ! [X8] :
( ( ~ p1(sK10(X8))
& r1(X8,sK10(X8)) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP6(X1)
& ! [X2] :
( ( ! [X7] :
( ~ p1(X7)
| ~ r1(sK9(X2),X7) )
& r1(X2,sK9(X2)) )
| ! [X3] :
( ! [X4] :
( ( p1(sK8(X4))
& r1(X4,sK8(X4)) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X5,sK8(X4)),skolemize(X6,sK9(X2)),skolemize(X11,sK10(X8))],[f19]) ).
fof(f21,plain,
! [X15] :
( ~ sP6(X15)
| ! [X22] :
( ( ! [X67] :
( ? [X70] :
( ~ p1(X70)
& r1(X67,X70) )
| ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X22,X67) )
& sP5(X22)
& ! [X23] :
( ? [X27] :
( ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
& r1(X23,X27) )
| ! [X24] :
( ! [X25] :
( ? [X26] :
( p1(X26)
& r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f22,plain,
! [X0] :
( ~ sP6(X0)
| ! [X1] :
( ( ! [X8] :
( ? [X11] :
( ~ p1(X11)
& r1(X8,X11) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP5(X1)
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0] :
( ~ sP6(X0)
| ! [X1] :
( ( ! [X8] :
( ( ~ p1(sK13(X8))
& r1(X8,sK13(X8)) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP5(X1)
& ! [X2] :
( ( ! [X7] :
( ~ p1(X7)
| ~ r1(sK12(X2),X7) )
& r1(X2,sK12(X2)) )
| ! [X3] :
( ! [X4] :
( ( p1(sK11(X4))
& r1(X4,sK11(X4)) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X5,sK11(X4)),skolemize(X6,sK12(X2)),skolemize(X11,sK13(X8))],[f22]) ).
fof(f24,plain,
! [X22] :
( ~ sP5(X22)
| ! [X29] :
( ( ! [X63] :
( ? [X66] :
( ~ p1(X66)
& r1(X63,X66) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X29,X63) )
& sP4(X29)
& ! [X30] :
( ? [X34] :
( ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
& r1(X30,X34) )
| ! [X31] :
( ! [X32] :
( ? [X33] :
( p1(X33)
& r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f25,plain,
! [X0] :
( ~ sP5(X0)
| ! [X1] :
( ( ! [X8] :
( ? [X11] :
( ~ p1(X11)
& r1(X8,X11) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP4(X1)
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f24]) ).
fof(f26,plain,
! [X0] :
( ~ sP5(X0)
| ! [X1] :
( ( ! [X8] :
( ( ~ p1(sK16(X8))
& r1(X8,sK16(X8)) )
| ! [X9] :
( ! [X10] :
( p1(X10)
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X1,X8) )
& sP4(X1)
& ! [X2] :
( ( ! [X7] :
( ~ p1(X7)
| ~ r1(sK15(X2),X7) )
& r1(X2,sK15(X2)) )
| ! [X3] :
( ! [X4] :
( ( p1(sK14(X4))
& r1(X4,sK14(X4)) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16]),skolemize(X5,sK14(X4)),skolemize(X6,sK15(X2)),skolemize(X11,sK16(X8))],[f25]) ).
fof(f27,plain,
! [X29] :
( ~ sP4(X29)
| ! [X36] :
( ( sP1(X36)
& sP0(X36)
& sP2(X36)
& sP3(X36)
& ! [X37] :
( ? [X38] :
( p2(X38)
& ? [X39] : r1(X38,X39)
& r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X0] :
( ~ sP4(X0)
| ! [X1] :
( ( sP1(X1)
& sP0(X1)
& sP2(X1)
& sP3(X1)
& ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] : r1(X3,X4)
& r1(X2,X3) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f27]) ).
fof(f29,plain,
! [X0] :
( ~ sP4(X0)
| ! [X1] :
( ( sP1(X1)
& sP0(X1)
& sP2(X1)
& sP3(X1)
& ! [X2] :
( ( p2(sK17(X2))
& r1(sK17(X2),sK18(X2))
& r1(X2,sK17(X2)) )
| ~ r1(X1,X2) ) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18]),skolemize(X3,sK17(X2)),skolemize(X4,sK18(X2))],[f28]) ).
fof(f30,plain,
! [X36] :
( ~ sP3(X36)
| ! [X40] :
( ! [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
& r1(X43,X44) )
| ~ r1(X40,X43) )
| ~ p2(X40)
| ! [X41] :
( ( p2(X41)
& ? [X42] : r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X36,X40) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f31,plain,
! [X0] :
( ~ sP3(X0)
| ! [X1] :
( ! [X4] :
( ? [X5] :
( ! [X6] :
( ~ p2(X6)
| ~ r1(X5,X6) )
& r1(X4,X5) )
| ~ r1(X1,X4) )
| ~ p2(X1)
| ! [X2] :
( ( p2(X2)
& ? [X3] : r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f30]) ).
fof(f32,plain,
! [X0] :
( ~ sP3(X0)
| ! [X1] :
( ! [X4] :
( ( ! [X6] :
( ~ p2(X6)
| ~ r1(sK20(X4),X6) )
& r1(X4,sK20(X4)) )
| ~ r1(X1,X4) )
| ~ p2(X1)
| ! [X2] :
( ( p2(X2)
& r1(X2,sK19(X2)) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19,sK20]),skolemize(X3,sK19(X2)),skolemize(X5,sK20(X4))],[f31]) ).
fof(f33,plain,
! [X36] :
( ~ sP2(X36)
| ? [X50] :
( ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
& r1(X36,X50) )
| ! [X46] :
( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] : r1(X48,X49)
& r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f34,plain,
! [X0] :
( ~ sP2(X0)
| ? [X5] :
( ! [X6] :
( ~ p2(X6)
| ~ r1(X5,X6) )
& r1(X0,X5) )
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p2(X3)
& ? [X4] : r1(X3,X4)
& r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f33]) ).
fof(f35,plain,
! [X0] :
( ~ sP2(X0)
| ( ! [X6] :
( ~ p2(X6)
| ~ r1(sK23(X0),X6) )
& r1(X0,sK23(X0)) )
| ! [X1] :
( ! [X2] :
( ( p2(sK21(X2))
& r1(sK21(X2),sK22(X2))
& r1(X2,sK21(X2)) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X3,sK21(X2)),skolemize(X4,sK22(X2)),skolemize(X5,sK23(X0))],[f34]) ).
fof(f36,plain,
! [X36] :
( ~ sP1(X36)
| ? [X61] :
( ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
& r1(X36,X61) )
| ? [X59] :
( p2(X59)
& ? [X60] : r1(X59,X60)
& r1(X36,X59) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f37,plain,
! [X0] :
( ~ sP1(X0)
| ? [X3] :
( ! [X4] :
( ~ p2(X4)
| ~ r1(X3,X4) )
& r1(X0,X3) )
| ? [X1] :
( p2(X1)
& ? [X2] : r1(X1,X2)
& r1(X0,X1) ) ),
inference(rectify,[],[f36]) ).
fof(f38,plain,
! [X0] :
( ~ sP1(X0)
| ( ! [X4] :
( ~ p2(X4)
| ~ r1(sK26(X0),X4) )
& r1(X0,sK26(X0)) )
| ( p2(sK24(X0))
& r1(sK24(X0),sK25(X0))
& r1(X0,sK24(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24,sK25,sK26]),skolemize(X1,sK24(X0)),skolemize(X2,sK25(X0)),skolemize(X3,sK26(X0))],[f37]) ).
fof(f42,plain,
? [X0] :
( ! [X65] :
( ? [X68] :
( p1(X68)
& r1(X65,X68) )
| ! [X66] :
( ! [X67] :
( ~ p1(X67)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X0,X65) )
& ? [X26] :
( ! [X61] :
( ? [X64] :
( p1(X64)
& r1(X61,X64) )
| ! [X62] :
( ! [X63] :
( ~ p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X26,X61) )
& ? [X31] :
( ! [X57] :
( ? [X60] :
( p1(X60)
& r1(X57,X60) )
| ! [X58] :
( ! [X59] :
( ~ p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X31,X57) )
& ? [X36] :
( ! [X53] :
( ? [X56] :
( p1(X56)
& r1(X53,X56) )
| ! [X54] :
( ! [X55] :
( ~ p1(X55)
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X36,X53) )
& ? [X41] :
( ! [X49] :
( ? [X52] :
( p1(X52)
& r1(X49,X52) )
| ! [X50] :
( ! [X51] :
( ~ p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(X41,X49) )
& ? [X46] :
( ! [X47] :
( ? [X48] :
( ~ p2(X48)
& r1(X47,X48) )
| ~ r1(X46,X47) )
& r1(X41,X46) )
& ? [X42] :
( ? [X45] :
( ~ p1(X45)
& r1(X42,X45) )
& ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& r1(X42,X43) )
& r1(X41,X42) )
& r1(X36,X41) )
& ? [X37] :
( ? [X40] :
( ~ p1(X40)
& r1(X37,X40) )
& ? [X38] :
( ! [X39] :
( p1(X39)
| ~ r1(X38,X39) )
& r1(X37,X38) )
& r1(X36,X37) )
& r1(X31,X36) )
& ? [X32] :
( ? [X35] :
( ~ p1(X35)
& r1(X32,X35) )
& ? [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
& r1(X32,X33) )
& r1(X31,X32) )
& r1(X26,X31) )
& ? [X27] :
( ? [X30] :
( ~ p1(X30)
& r1(X27,X30) )
& ? [X28] :
( ! [X29] :
( p1(X29)
| ~ r1(X28,X29) )
& r1(X27,X28) )
& r1(X26,X27) )
& r1(X0,X26) )
& ? [X22] :
( ? [X25] :
( ~ p1(X25)
& r1(X22,X25) )
& ? [X23] :
( ! [X24] :
( p1(X24)
| ~ r1(X23,X24) )
& r1(X22,X23) )
& r1(X0,X22) )
& ! [X18] :
( ? [X21] :
( ~ p1(X21)
& r1(X18,X21) )
| ! [X19] :
( ! [X20] :
( p1(X20)
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X0,X18) )
& ! [X7] :
( ( ! [X14] :
( ? [X17] :
( ~ p1(X17)
& r1(X14,X17) )
| ! [X15] :
( ! [X16] :
( p1(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X7,X14) )
& sP7(X7)
& ! [X8] :
( ? [X12] :
( ! [X13] :
( ~ p1(X13)
| ~ r1(X12,X13) )
& r1(X8,X12) )
| ! [X9] :
( ! [X10] :
( ? [X11] :
( p1(X11)
& r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) ) )
| ~ r1(X0,X7) )
& ! [X1] :
( ? [X5] :
( ! [X6] :
( ~ p1(X6)
| ~ r1(X5,X6) )
& r1(X1,X5) )
| ! [X2] :
( ! [X3] :
( ? [X4] :
( p1(X4)
& r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f17]) ).
fof(f43,plain,
( ! [X65] :
( ( p1(sK63(X65))
& r1(X65,sK63(X65)) )
| ! [X66] :
( ! [X67] :
( ~ p1(X67)
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(sK31,X65) )
& ! [X61] :
( ( p1(sK62(X61))
& r1(X61,sK62(X61)) )
| ! [X62] :
( ! [X63] :
( ~ p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(sK41,X61) )
& ! [X57] :
( ( p1(sK61(X57))
& r1(X57,sK61(X57)) )
| ! [X58] :
( ! [X59] :
( ~ p1(X59)
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(sK45,X57) )
& ! [X53] :
( ( p1(sK60(X53))
& r1(X53,sK60(X53)) )
| ! [X54] :
( ! [X55] :
( ~ p1(X55)
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(sK49,X53) )
& ! [X49] :
( ( p1(sK59(X49))
& r1(X49,sK59(X49)) )
| ! [X50] :
( ! [X51] :
( ~ p1(X51)
| ~ r1(X50,X51) )
| ~ r1(X49,X50) )
| ~ r1(sK53,X49) )
& ! [X47] :
( ( ~ p2(sK58(X47))
& r1(X47,sK58(X47)) )
| ~ r1(sK57,X47) )
& r1(sK53,sK57)
& ~ p1(sK56)
& r1(sK54,sK56)
& ! [X44] :
( p1(X44)
| ~ r1(sK55,X44) )
& r1(sK54,sK55)
& r1(sK53,sK54)
& r1(sK49,sK53)
& ~ p1(sK52)
& r1(sK50,sK52)
& ! [X39] :
( p1(X39)
| ~ r1(sK51,X39) )
& r1(sK50,sK51)
& r1(sK49,sK50)
& r1(sK45,sK49)
& ~ p1(sK48)
& r1(sK46,sK48)
& ! [X34] :
( p1(X34)
| ~ r1(sK47,X34) )
& r1(sK46,sK47)
& r1(sK45,sK46)
& r1(sK41,sK45)
& ~ p1(sK44)
& r1(sK42,sK44)
& ! [X29] :
( p1(X29)
| ~ r1(sK43,X29) )
& r1(sK42,sK43)
& r1(sK41,sK42)
& r1(sK31,sK41)
& ~ p1(sK40)
& r1(sK38,sK40)
& ! [X24] :
( p1(X24)
| ~ r1(sK39,X24) )
& r1(sK38,sK39)
& r1(sK31,sK38)
& ! [X18] :
( ( ~ p1(sK37(X18))
& r1(X18,sK37(X18)) )
| ! [X19] :
( ! [X20] :
( p1(X20)
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(sK31,X18) )
& ! [X7] :
( ( ! [X14] :
( ( ~ p1(sK36(X14))
& r1(X14,sK36(X14)) )
| ! [X15] :
( ! [X16] :
( p1(X16)
| ~ r1(X15,X16) )
| ~ r1(X14,X15) )
| ~ r1(X7,X14) )
& sP7(X7)
& ! [X8] :
( ( ! [X13] :
( ~ p1(X13)
| ~ r1(sK35(X8),X13) )
& r1(X8,sK35(X8)) )
| ! [X9] :
( ! [X10] :
( ( p1(sK34(X10))
& r1(X10,sK34(X10)) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) ) )
| ~ r1(sK31,X7) )
& ! [X1] :
( ( ! [X6] :
( ~ p1(X6)
| ~ r1(sK33(X1),X6) )
& r1(X1,sK33(X1)) )
| ! [X2] :
( ! [X3] :
( ( p1(sK32(X3))
& r1(X3,sK32(X3)) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK31,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK58,sK59,sK60,sK61,sK62,sK63]),skolemize(X0,sK31),skolemize(X4,sK32(X3)),skolemize(X5,sK33(X1)),skolemize(X11,sK34(X10)),skolemize(X12,sK35(X8)),skolemize(X17,sK36(X14)),skolemize(X21,sK37(X18)),skolemize(X22,sK38),skolemize(X23,sK39),skolemize(X25,sK40),skolemize(X26,sK41),skolemize(X27,sK42),skolemize(X28,sK43),skolemize(X30,sK44),skolemize(X31,sK45),skolemize(X32,sK46),skolemize(X33,sK47),skolemize(X35,sK48),skolemize(X36,sK49),skolemize(X37,sK50),skolemize(X38,sK51),skolemize(X40,sK52),skolemize(X41,sK53),skolemize(X42,sK54),skolemize(X43,sK55),skolemize(X45,sK56),skolemize(X46,sK57),skolemize(X48,sK58(X47)),skolemize(X52,sK59(X49)),skolemize(X56,sK60(X53)),skolemize(X60,sK61(X57)),skolemize(X64,sK62(X61)),skolemize(X68,sK63(X65))],[f42]) ).
fof(f46,plain,
! [X0,X1] :
( ~ sP7(X0)
| sP6(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f53,plain,
! [X0,X1] :
( ~ sP6(X0)
| sP5(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f60,plain,
! [X0,X1] :
( ~ sP5(X0)
| sP4(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f26]) ).
fof(f65,plain,
! [X0,X1] :
( ~ sP4(X0)
| sP1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f66,plain,
! [X0,X1] :
( ~ sP4(X0)
| sP0(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f67,plain,
! [X0,X1] :
( ~ sP4(X0)
| sP2(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f68,plain,
! [X0,X1] :
( ~ sP4(X0)
| sP3(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f69,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| p2(sK17(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f71,plain,
! [X2,X0,X1] :
( ~ sP4(X0)
| r1(X2,sK17(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f72,plain,
! [X2,X0,X1,X6,X4] :
( ~ sP3(X0)
| ~ p2(X6)
| ~ r1(sK20(X4),X6)
| ~ r1(X1,X4)
| ~ p2(X1)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f73,plain,
! [X2,X0,X1,X4] :
( ~ sP3(X0)
| r1(X4,sK20(X4))
| ~ r1(X1,X4)
| ~ p2(X1)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
fof(f76,plain,
! [X2,X0,X1,X6] :
( ~ sP2(X0)
| ~ p2(X6)
| ~ r1(sK23(X0),X6)
| p2(sK21(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f77,plain,
! [X2,X0,X1] :
( ~ sP2(X0)
| r1(X0,sK23(X0))
| p2(sK21(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f80,plain,
! [X2,X0,X1,X6] :
( ~ sP2(X0)
| ~ p2(X6)
| ~ r1(sK23(X0),X6)
| r1(X2,sK21(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f81,plain,
! [X2,X0,X1] :
( ~ sP2(X0)
| r1(X0,sK23(X0))
| r1(X2,sK21(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f82,plain,
! [X0,X4] :
( ~ sP1(X0)
| ~ p2(X4)
| ~ r1(sK26(X0),X4)
| p2(sK24(X0)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f83,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK26(X0))
| p2(sK24(X0)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f86,plain,
! [X0,X4] :
( ~ sP1(X0)
| ~ p2(X4)
| ~ r1(sK26(X0),X4)
| r1(X0,sK24(X0)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f87,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK26(X0))
| r1(X0,sK24(X0)) ),
inference(cnf_transformation,[],[f38]) ).
fof(f106,plain,
! [X47] :
( ~ p2(sK58(X47))
| ~ r1(sK57,X47) ),
inference(cnf_transformation,[],[f43]) ).
fof(f107,plain,
! [X47] :
( r1(X47,sK58(X47))
| ~ r1(sK57,X47) ),
inference(cnf_transformation,[],[f43]) ).
fof(f108,plain,
r1(sK53,sK57),
inference(cnf_transformation,[],[f43]) ).
fof(f114,plain,
r1(sK49,sK53),
inference(cnf_transformation,[],[f43]) ).
fof(f120,plain,
r1(sK45,sK49),
inference(cnf_transformation,[],[f43]) ).
fof(f126,plain,
r1(sK41,sK45),
inference(cnf_transformation,[],[f43]) ).
fof(f132,plain,
r1(sK31,sK41),
inference(cnf_transformation,[],[f43]) ).
fof(f142,plain,
! [X7] :
( sP7(X7)
| ~ r1(sK31,X7) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( sP6(X1)
| ~ sP7(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i] :
( sP5(X1)
| ~ sP6(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] :
( sP4(X1)
| ~ sP5(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK17(X2))
| ~ sP4(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK17(X2))
| ~ sP4(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( sP3(X1)
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( sP2(X1)
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( sP1(X1)
| ~ sP4(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X2)
| r1(X3,sK20(X3))
| ~ sP3(X0)
| ~ p2(X1)
| ~ r1(X1,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(X4)
| ~ sP3(X2)
| ~ p2(X3)
| ~ p2(X1)
| ~ r1(X3,X4)
| ~ r1(X3,X0)
| ~ r1(X2,X3)
| ~ r1(sK20(X0),X1) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK21(X2))
| r1(X0,sK23(X0))
| ~ sP2(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK21(X3))
| ~ sP2(X0)
| ~ p2(X1)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| ~ r1(sK23(X0),X1) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK21(X2))
| r1(X0,sK23(X0))
| ~ sP2(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_86,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(sK21(X3))
| ~ sP2(X0)
| ~ p2(X1)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| ~ r1(sK23(X0),X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_87,plain,
! [X0: $i] :
( r1(X0,sK26(X0))
| r1(X0,sK24(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( r1(X0,sK24(X0))
| ~ sP1(X0)
| ~ p2(X1)
| ~ r1(sK26(X0),X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_91,plain,
! [X0: $i] :
( p2(sK24(X0))
| r1(X0,sK26(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( p2(sK24(X0))
| ~ sP1(X0)
| ~ p2(X1)
| ~ r1(sK26(X0),X1) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_109,negated_conjecture,
! [X0: $i] :
( sP7(X0)
| ~ r1(sK31,X0) ),
inference(cnf_transformation,[],[f142]) ).
tcf(c_119,negated_conjecture,
r1(sK31,sK41),
inference(cnf_transformation,[],[f132]) ).
tcf(c_125,negated_conjecture,
r1(sK41,sK45),
inference(cnf_transformation,[],[f126]) ).
tcf(c_131,negated_conjecture,
r1(sK45,sK49),
inference(cnf_transformation,[],[f120]) ).
tcf(c_137,negated_conjecture,
r1(sK49,sK53),
inference(cnf_transformation,[],[f114]) ).
tcf(c_143,negated_conjecture,
r1(sK53,sK57),
inference(cnf_transformation,[],[f108]) ).
tcf(c_144,negated_conjecture,
! [X0: $i] :
( r1(X0,sK58(X0))
| ~ r1(sK57,X0) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_145,negated_conjecture,
! [X0: $i] :
( ~ p2(sK58(X0))
| ~ r1(sK57,X0) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_237,plain,
( sP7(sK41)
| ~ r1(sK31,sK41) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_273,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP7(sK41)
| ~ r1(sK41,X0) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_701,plain,
( sP6(sK45)
| ~ sP7(sK41)
| ~ r1(sK41,sK45) ),
inference(instantiation,[status(thm)],[c_273]) ).
tcf(c_1124,plain,
( sP5(sK49)
| ~ sP6(sK45) ),
inference(superposition,[status(thm)],[c_131,c_60]) ).
tcf(c_1334,plain,
( sP4(sK53)
| ~ sP5(sK49) ),
inference(superposition,[status(thm)],[c_137,c_67]) ).
tcf(c_1413,plain,
( sP3(sK57)
| ~ sP4(sK53) ),
inference(superposition,[status(thm)],[c_143,c_73]) ).
tcf(c_2822,plain,
( sP2(sK57)
| ~ sP4(sK53) ),
inference(superposition,[status(thm)],[c_143,c_74]) ).
tcf(c_2906,plain,
( sP0(sK57)
| ~ sP4(sK53) ),
inference(superposition,[status(thm)],[c_143,c_75]) ).
tcf(c_3467,plain,
( sP1(sK57)
| ~ sP4(sK53) ),
inference(superposition,[status(thm)],[c_143,c_76]) ).
tcf(c_3587,plain,
( p2(sK24(sK57))
| ~ sP1(sK57)
| ~ p2(sK58(sK26(sK57))) ),
inference(superposition,[status(thm)],[c_91,c_145]) ).
tcf(c_5279,plain,
! [X0: $i] :
( p2(sK17(X0))
| ~ sP4(sK53)
| ~ r1(sK57,X0) ),
inference(superposition,[status(thm)],[c_143,c_72]) ).
tcf(c_5985,plain,
! [X0: $i] :
( r1(X0,sK17(X0))
| ~ sP4(sK53)
| ~ r1(sK57,X0) ),
inference(superposition,[status(thm)],[c_143,c_70]) ).
tcf(c_8613,plain,
! [X0: $i] :
( r1(sK57,sK24(sK57))
| ~ sP1(sK57)
| ~ p2(X0)
| ~ r1(sK26(sK57),X0) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_8614,plain,
! [X0: $i] :
( p2(sK24(sK57))
| ~ sP1(sK57)
| ~ p2(X0)
| ~ r1(sK26(sK57),X0) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_8616,plain,
( r1(sK57,sK26(sK57))
| r1(sK57,sK24(sK57))
| ~ sP1(sK57) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_8617,plain,
( p2(sK24(sK57))
| r1(sK57,sK26(sK57))
| ~ sP1(sK57) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_12772,plain,
( r1(sK24(sK57),sK58(sK24(sK57)))
| ~ r1(sK57,sK24(sK57)) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_16914,plain,
! [X0: $i] :
( p2(sK17(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5279,c_125,c_119,c_237,c_701,c_1124,c_1334,c_5279]) ).
tcf(c_16917,plain,
( p2(sK17(sK26(sK57)))
| r1(sK57,sK24(sK57))
| ~ sP1(sK57) ),
inference(superposition,[status(thm)],[c_87,c_16914]) ).
tcf(c_16918,plain,
( p2(sK24(sK57))
| p2(sK17(sK26(sK57)))
| ~ sP1(sK57) ),
inference(superposition,[status(thm)],[c_91,c_16914]) ).
tcf(c_18098,plain,
( p2(sK24(sK57))
| ~ sP1(sK57)
| ~ p2(sK17(sK26(sK57)))
| ~ r1(sK26(sK57),sK17(sK26(sK57))) ),
inference(instantiation,[status(thm)],[c_8614]) ).
tcf(c_18099,plain,
( r1(sK57,sK24(sK57))
| ~ sP1(sK57)
| ~ p2(sK17(sK26(sK57)))
| ~ r1(sK26(sK57),sK17(sK26(sK57))) ),
inference(instantiation,[status(thm)],[c_8613]) ).
tcf(c_21818,plain,
( r1(sK23(sK57),sK17(sK23(sK57)))
| ~ sP4(sK53)
| ~ r1(sK57,sK23(sK57)) ),
inference(instantiation,[status(thm)],[c_5985]) ).
tcf(c_21938,plain,
( r1(sK26(sK57),sK17(sK26(sK57)))
| ~ sP4(sK53)
| ~ r1(sK57,sK26(sK57)) ),
inference(instantiation,[status(thm)],[c_5985]) ).
tcf(c_33768,plain,
! [X0: $i] :
( p2(sK17(X0))
| ~ r1(sK57,X0) ),
inference(global_subsumption_just,[status(thm)],[c_5279,c_125,c_119,c_237,c_701,c_1124,c_1334,c_5279]) ).
tcf(c_33770,plain,
( p2(sK17(sK26(sK57)))
| r1(sK57,sK24(sK57))
| ~ sP1(sK57) ),
inference(superposition,[status(thm)],[c_87,c_33768]) ).
tcf(c_33773,plain,
p2(sK24(sK57)),
inference(global_subsumption_just,[status(thm)],[c_3587,c_125,c_119,c_237,c_701,c_1124,c_1334,c_3467,c_8617,c_16918,c_18098,c_21938]) ).
tcf(c_35065,plain,
r1(sK57,sK24(sK57)),
inference(global_subsumption_just,[status(thm)],[c_33770,c_125,c_119,c_237,c_701,c_1124,c_1334,c_3467,c_8616,c_16917,c_18099,c_21938]) ).
tcf(c_35121,plain,
~ p2(sK58(sK24(sK57))),
inference(superposition,[status(thm)],[c_35065,c_145]) ).
tcf(c_45780,plain,
! [X0: $i,X1: $i] :
( p2(sK21(X1))
| r1(sK57,sK23(sK57))
| ~ sP2(sK57)
| ~ r1(sK57,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_85]) ).
tcf(c_45798,plain,
! [X0: $i,X1: $i] :
( r1(sK57,sK23(sK57))
| r1(X1,sK21(X1))
| ~ sP2(sK57)
| ~ r1(sK57,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_45862,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(X1)
| r1(X2,sK20(X2))
| ~ sP3(X3)
| ~ p2(sK24(X0))
| ~ r1(X3,sK24(X0))
| ~ r1(sK24(X0),X2)
| ~ r1(sK24(X0),X1) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_47283,plain,
! [X0: $i] :
( p2(sK21(X0))
| r1(sK57,sK23(sK57))
| ~ sP2(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0) ),
inference(instantiation,[status(thm)],[c_45780]) ).
tcf(c_47375,plain,
! [X0: $i] :
( r1(sK57,sK23(sK57))
| r1(X0,sK21(X0))
| ~ sP2(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0) ),
inference(instantiation,[status(thm)],[c_45798]) ).
tcf(c_49272,plain,
( r1(sK57,sK23(sK57))
| p2(sK21(sK27(sK24(sK57))))
| ~ sP2(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),sK27(sK24(sK57))) ),
inference(instantiation,[status(thm)],[c_47283]) ).
tcf(c_49314,plain,
( r1(sK57,sK23(sK57))
| r1(sK27(sK24(sK57)),sK21(sK27(sK24(sK57))))
| ~ sP2(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),sK27(sK24(sK57))) ),
inference(instantiation,[status(thm)],[c_47375]) ).
tcf(c_50147,plain,
( p2(sK17(sK23(sK57)))
| ~ sP4(sK53)
| ~ r1(sK57,sK23(sK57)) ),
inference(instantiation,[status(thm)],[c_5279]) ).
tcf(c_52218,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK21(X1))
| ~ sP2(sK57)
| ~ r1(sK57,X0)
| ~ r1(X0,X1)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_52219,plain,
! [X0: $i,X1: $i] :
( p2(sK21(X1))
| ~ sP2(sK57)
| ~ r1(sK57,X0)
| ~ r1(X0,X1)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_54078,plain,
! [X0: $i,X1: $i] :
( p2(X0)
| r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57))))
| ~ sP3(X1)
| ~ p2(sK24(sK57))
| ~ r1(X1,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ r1(sK24(sK57),sK28(sK24(sK57))) ),
inference(instantiation,[status(thm)],[c_45862]) ).
tcf(c_55746,plain,
! [X0: $i] :
( p2(sK21(X0))
| ~ sP2(sK57)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_52219]) ).
tcf(c_55784,plain,
! [X0: $i] :
( r1(X0,sK21(X0))
| ~ sP2(sK57)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_52218]) ).
tcf(c_57861,plain,
( p2(sK21(sK27(sK24(sK57))))
| ~ sP2(sK57)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),sK27(sK24(sK57)))
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_55746]) ).
tcf(c_57911,plain,
( r1(sK27(sK24(sK57)),sK21(sK27(sK24(sK57))))
| ~ sP2(sK57)
| ~ p2(sK17(sK23(sK57)))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),sK27(sK24(sK57)))
| ~ r1(sK23(sK57),sK17(sK23(sK57))) ),
inference(instantiation,[status(thm)],[c_55784]) ).
tcf(c_59653,plain,
! [X0: $i] :
( p2(X0)
| r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57))))
| ~ sP3(sK57)
| ~ p2(sK24(sK57))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ r1(sK24(sK57),sK28(sK24(sK57))) ),
inference(instantiation,[status(thm)],[c_54078]) ).
tcf(c_62121,plain,
( p2(sK58(sK24(sK57)))
| r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57))))
| ~ sP3(sK57)
| ~ p2(sK24(sK57))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),sK58(sK24(sK57)))
| ~ r1(sK24(sK57),sK28(sK24(sK57))) ),
inference(instantiation,[status(thm)],[c_59653]) ).
tcf(c_69755,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2)
| ~ sP3(X1)
| ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(X0,X2)
| ~ r1(X0,sK28(sK24(sK57)))
| ~ p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57))))) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_74421,plain,
! [X0: $i,X1: $i] :
( p2(X0)
| ~ sP3(X1)
| ~ p2(sK24(sK57))
| ~ r1(X1,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ r1(sK24(sK57),sK28(sK24(sK57)))
| ~ r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57))))) ),
inference(instantiation,[status(thm)],[c_69755]) ).
tcf(c_76833,plain,
! [X0: $i] :
( p2(X0)
| ~ sP3(sK57)
| ~ p2(sK24(sK57))
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK24(sK57),X0)
| ~ p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ r1(sK24(sK57),sK28(sK24(sK57)))
| ~ r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57))))) ),
inference(instantiation,[status(thm)],[c_74421]) ).
tcf(c_78219,plain,
( p2(sK58(sK24(sK57)))
| ~ sP3(sK57)
| ~ p2(sK24(sK57))
| ~ r1(sK57,sK24(sK57))
| ~ p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ r1(sK24(sK57),sK58(sK24(sK57)))
| ~ r1(sK24(sK57),sK28(sK24(sK57)))
| ~ r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57))))) ),
inference(instantiation,[status(thm)],[c_76833]) ).
fof(f9,definition,
! [X36] :
( ~ sP0(X36)
| ! [X52] :
( ? [X55] :
( ! [X56] :
( ? [X57] :
( p2(X57)
& ? [X58] : r1(X57,X58)
& r1(X56,X57) )
| ~ r1(X55,X56) )
& r1(X52,X55) )
| ? [X53] :
( ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
| ~ r1(X36,X52) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X36] :
( ~ sP1(X36)
| ? [X61] :
( ! [X62] :
( ~ p2(X62)
| ~ r1(X61,X62) )
& r1(X36,X61) )
| ? [X59] :
( p2(X59)
& ? [X60] : r1(X59,X60)
& r1(X36,X59) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X36] :
( ~ sP2(X36)
| ? [X50] :
( ! [X51] :
( ~ p2(X51)
| ~ r1(X50,X51) )
& r1(X36,X50) )
| ! [X46] :
( ! [X47] :
( ? [X48] :
( p2(X48)
& ? [X49] : r1(X48,X49)
& r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X36,X46) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X36] :
( ~ sP3(X36)
| ! [X40] :
( ! [X43] :
( ? [X44] :
( ! [X45] :
( ~ p2(X45)
| ~ r1(X44,X45) )
& r1(X43,X44) )
| ~ r1(X40,X43) )
| ~ p2(X40)
| ! [X41] :
( ( p2(X41)
& ? [X42] : r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X36,X40) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X29] :
( ~ sP4(X29)
| ! [X36] :
( ( sP1(X36)
& sP0(X36)
& sP2(X36)
& sP3(X36)
& ! [X37] :
( ? [X38] :
( p2(X38)
& ? [X39] : r1(X38,X39)
& r1(X37,X38) )
| ~ r1(X36,X37) ) )
| ~ r1(X29,X36) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X22] :
( ~ sP5(X22)
| ! [X29] :
( ( ! [X63] :
( ? [X66] :
( ~ p1(X66)
& r1(X63,X66) )
| ! [X64] :
( ! [X65] :
( p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X63,X64) )
| ~ r1(X29,X63) )
& sP4(X29)
& ! [X30] :
( ? [X34] :
( ! [X35] :
( ~ p1(X35)
| ~ r1(X34,X35) )
& r1(X30,X34) )
| ! [X31] :
( ! [X32] :
( ? [X33] :
( p1(X33)
& r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X22,X29) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X15] :
( ~ sP6(X15)
| ! [X22] :
( ( ! [X67] :
( ? [X70] :
( ~ p1(X70)
& r1(X67,X70) )
| ! [X68] :
( ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X22,X67) )
& sP5(X22)
& ! [X23] :
( ? [X27] :
( ! [X28] :
( ~ p1(X28)
| ~ r1(X27,X28) )
& r1(X23,X27) )
| ! [X24] :
( ! [X25] :
( ? [X26] :
( p1(X26)
& r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) ) )
| ~ r1(X15,X22) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X8] :
( ~ sP7(X8)
| ! [X15] :
( ( ! [X71] :
( ? [X74] :
( ~ p1(X74)
& r1(X71,X74) )
| ! [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
| ~ r1(X71,X72) )
| ~ r1(X15,X71) )
& sP6(X15)
& ! [X16] :
( ? [X20] :
( ! [X21] :
( ~ p1(X21)
| ~ r1(X20,X21) )
& r1(X16,X20) )
| ! [X17] :
( ! [X18] :
( ? [X19] :
( p1(X19)
& r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) ) )
| ~ r1(X8,X15) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f17,plain,
? [X0] :
( ! [X126] :
( ? [X129] :
( p1(X129)
& r1(X126,X129) )
| ! [X127] :
( ! [X128] :
( ~ p1(X128)
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ? [X87] :
( ! [X122] :
( ? [X125] :
( p1(X125)
& r1(X122,X125) )
| ! [X123] :
( ! [X124] :
( ~ p1(X124)
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X87,X122) )
& ? [X92] :
( ! [X118] :
( ? [X121] :
( p1(X121)
& r1(X118,X121) )
| ! [X119] :
( ! [X120] :
( ~ p1(X120)
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X92,X118) )
& ? [X97] :
( ! [X114] :
( ? [X117] :
( p1(X117)
& r1(X114,X117) )
| ! [X115] :
( ! [X116] :
( ~ p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X97,X114) )
& ? [X102] :
( ! [X110] :
( ? [X113] :
( p1(X113)
& r1(X110,X113) )
| ! [X111] :
( ! [X112] :
( ~ p1(X112)
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X102,X110) )
& ? [X107] :
( ! [X108] :
( ? [X109] :
( ~ p2(X109)
& r1(X108,X109) )
| ~ r1(X107,X108) )
& r1(X102,X107) )
& ? [X103] :
( ? [X106] :
( ~ p1(X106)
& r1(X103,X106) )
& ? [X104] :
( ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
& r1(X103,X104) )
& r1(X102,X103) )
& r1(X97,X102) )
& ? [X98] :
( ? [X101] :
( ~ p1(X101)
& r1(X98,X101) )
& ? [X99] :
( ! [X100] :
( p1(X100)
| ~ r1(X99,X100) )
& r1(X98,X99) )
& r1(X97,X98) )
& r1(X92,X97) )
& ? [X93] :
( ? [X96] :
( ~ p1(X96)
& r1(X93,X96) )
& ? [X94] :
( ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
& r1(X93,X94) )
& r1(X92,X93) )
& r1(X87,X92) )
& ? [X88] :
( ? [X91] :
( ~ p1(X91)
& r1(X88,X91) )
& ? [X89] :
( ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X0,X87) )
& ? [X83] :
( ? [X86] :
( ~ p1(X86)
& r1(X83,X86) )
& ? [X84] :
( ! [X85] :
( p1(X85)
| ~ r1(X84,X85) )
& r1(X83,X84) )
& r1(X0,X83) )
& ! [X79] :
( ? [X82] :
( ~ p1(X82)
& r1(X79,X82) )
| ! [X80] :
( ! [X81] :
( p1(X81)
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X0,X79) )
& ! [X8] :
( ( ! [X75] :
( ? [X78] :
( ~ p1(X78)
& r1(X75,X78) )
| ! [X76] :
( ! [X77] :
( p1(X77)
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X8,X75) )
& sP7(X8)
& ! [X9] :
( ? [X13] :
( ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
& r1(X9,X13) )
| ! [X10] :
( ! [X11] :
( ? [X12] :
( p1(X12)
& r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) ) )
| ~ r1(X0,X8) )
& ! [X2] :
( ? [X6] :
( ! [X7] :
( ~ p1(X7)
| ~ r1(X6,X7) )
& r1(X2,X6) )
| ! [X3] :
( ! [X4] :
( ? [X5] :
( p1(X5)
& r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X0,X2) ) ),
inference(definition_folding,[],[f8,f16,f15,f14,f13,f12,f11,f10,f9]) ).
fof(f39,plain,
! [X36] :
( ~ sP0(X36)
| ! [X52] :
( ? [X55] :
( ! [X56] :
( ? [X57] :
( p2(X57)
& ? [X58] : r1(X57,X58)
& r1(X56,X57) )
| ~ r1(X55,X56) )
& r1(X52,X55) )
| ? [X53] :
( ! [X54] :
( ~ p2(X54)
| ~ r1(X53,X54) )
& r1(X52,X53) )
| ~ r1(X36,X52) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f40,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ? [X4] :
( ! [X5] :
( ? [X6] :
( p2(X6)
& ? [X7] : r1(X6,X7)
& r1(X5,X6) )
| ~ r1(X4,X5) )
& r1(X1,X4) )
| ? [X2] :
( ! [X3] :
( ~ p2(X3)
| ~ r1(X2,X3) )
& r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f39]) ).
fof(f41,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ( ! [X5] :
( ( p2(sK29(X5))
& r1(sK29(X5),sK30(X5))
& r1(X5,sK29(X5)) )
| ~ r1(sK28(X1),X5) )
& r1(X1,sK28(X1)) )
| ( ! [X3] :
( ~ p2(X3)
| ~ r1(sK27(X1),X3) )
& r1(X1,sK27(X1)) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30]),skolemize(X2,sK27(X1)),skolemize(X4,sK28(X1)),skolemize(X6,sK29(X5)),skolemize(X7,sK30(X5))],[f40]) ).
fof(f88,plain,
! [X3,X0,X1,X5] :
( ~ sP0(X0)
| p2(sK29(X5))
| ~ r1(sK28(X1),X5)
| ~ p2(X3)
| ~ r1(sK27(X1),X3)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f90,plain,
! [X3,X0,X1,X5] :
( ~ sP0(X0)
| r1(X5,sK29(X5))
| ~ r1(sK28(X1),X5)
| ~ p2(X3)
| ~ r1(sK27(X1),X3)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f91,plain,
! [X3,X0,X1] :
( ~ sP0(X0)
| r1(X1,sK28(X1))
| ~ p2(X3)
| ~ r1(sK27(X1),X3)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f92,plain,
! [X0,X1,X5] :
( ~ sP0(X0)
| p2(sK29(X5))
| ~ r1(sK28(X1),X5)
| r1(X1,sK27(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f94,plain,
! [X0,X1,X5] :
( ~ sP0(X0)
| r1(X5,sK29(X5))
| ~ r1(sK28(X1),X5)
| r1(X1,sK27(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f95,plain,
! [X0,X1] :
( ~ sP0(X0)
| r1(X1,sK28(X1))
| r1(X1,sK27(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK28(X1))
| r1(X1,sK27(X1))
| ~ sP0(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X1,sK29(X1))
| r1(X0,sK27(X0))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(sK28(X0),X1) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK29(X1))
| r1(X0,sK27(X0))
| ~ sP0(X2)
| ~ r1(X2,X0)
| ~ r1(sK28(X0),X1) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X0,sK28(X0))
| ~ sP0(X2)
| ~ p2(X1)
| ~ r1(X2,X0)
| ~ r1(sK27(X0),X1) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X2,sK29(X2))
| ~ sP0(X3)
| ~ p2(X1)
| ~ r1(X3,X0)
| ~ r1(sK28(X0),X2)
| ~ r1(sK27(X0),X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(sK29(X2))
| ~ sP0(X3)
| ~ p2(X1)
| ~ r1(X3,X0)
| ~ r1(sK28(X0),X2)
| ~ r1(sK27(X0),X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_35085,plain,
( r1(sK24(sK57),sK28(sK24(sK57)))
| r1(sK24(sK57),sK27(sK24(sK57)))
| ~ sP0(sK57) ),
inference(superposition,[status(thm)],[c_35065,c_93]) ).
tcf(c_45802,plain,
! [X0: $i,X1: $i] :
( p2(sK29(X1))
| r1(X0,sK27(X0))
| ~ sP0(sK57)
| ~ r1(sK57,X0)
| ~ r1(sK28(X0),X1) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_45808,plain,
! [X0: $i,X1: $i] :
( r1(X0,sK28(X0))
| ~ sP0(sK57)
| ~ p2(X1)
| ~ r1(sK57,X0)
| ~ r1(sK27(X0),X1) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_45834,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK29(X1))
| r1(X0,sK27(X0))
| ~ sP0(sK57)
| ~ r1(sK57,X0)
| ~ r1(sK28(X0),X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_45860,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(sK29(X2))
| ~ sP0(sK57)
| ~ p2(X1)
| ~ r1(sK57,X0)
| ~ r1(sK28(X0),X2)
| ~ r1(sK27(X0),X1) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_45881,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK29(X2))
| ~ sP0(sK57)
| ~ p2(X1)
| ~ r1(sK57,X0)
| ~ r1(sK28(X0),X2)
| ~ r1(sK27(X0),X1) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_56657,plain,
( r1(sK24(sK57),sK28(sK24(sK57)))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ p2(sK21(sK27(sK24(sK57))))
| ~ r1(sK27(sK24(sK57)),sK21(sK27(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_45808]) ).
tcf(c_61901,plain,
! [X0: $i] :
( p2(sK29(X0))
| r1(sK24(sK57),sK27(sK24(sK57)))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),X0) ),
inference(instantiation,[status(thm)],[c_45802]) ).
tcf(c_61931,plain,
! [X0: $i] :
( r1(X0,sK29(X0))
| r1(sK24(sK57),sK27(sK24(sK57)))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),X0) ),
inference(instantiation,[status(thm)],[c_45834]) ).
tcf(c_61991,plain,
! [X0: $i,X1: $i] :
( p2(sK29(X1))
| ~ sP0(sK57)
| ~ p2(X0)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),X1)
| ~ r1(sK27(sK24(sK57)),X0) ),
inference(instantiation,[status(thm)],[c_45860]) ).
tcf(c_62021,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK29(X1))
| ~ sP0(sK57)
| ~ p2(X0)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),X1)
| ~ r1(sK27(sK24(sK57)),X0) ),
inference(instantiation,[status(thm)],[c_45881]) ).
tcf(c_63502,plain,
( p2(sK29(sK20(sK28(sK24(sK57)))))
| r1(sK24(sK57),sK27(sK24(sK57)))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_61901]) ).
tcf(c_63824,plain,
( r1(sK24(sK57),sK27(sK24(sK57)))
| r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57)))))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_61931]) ).
tcf(c_64321,plain,
! [X0: $i] :
( p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ sP0(sK57)
| ~ p2(X0)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK27(sK24(sK57)),X0)
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_61991]) ).
tcf(c_64482,plain,
! [X0: $i] :
( r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57)))))
| ~ sP0(sK57)
| ~ p2(X0)
| ~ r1(sK57,sK24(sK57))
| ~ r1(sK27(sK24(sK57)),X0)
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_62021]) ).
tcf(c_66695,plain,
( p2(sK29(sK20(sK28(sK24(sK57)))))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ p2(sK21(sK27(sK24(sK57))))
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57))))
| ~ r1(sK27(sK24(sK57)),sK21(sK27(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_64321]) ).
tcf(c_66698,plain,
( r1(sK20(sK28(sK24(sK57))),sK29(sK20(sK28(sK24(sK57)))))
| ~ sP0(sK57)
| ~ r1(sK57,sK24(sK57))
| ~ p2(sK21(sK27(sK24(sK57))))
| ~ r1(sK28(sK24(sK57)),sK20(sK28(sK24(sK57))))
| ~ r1(sK27(sK24(sK57)),sK21(sK27(sK24(sK57)))) ),
inference(instantiation,[status(thm)],[c_64482]) ).
tcf(c_79374,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_78219,c_66698,c_66695,c_63824,c_63502,c_62121,c_57911,c_57861,c_56657,c_50147,c_49314,c_49272,c_35085,c_35121,c_35065,c_33773,c_21818,c_12772,c_2906,c_2822,c_1413,c_1334,c_1124,c_701,c_237,c_119,c_125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL652+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Wed Sep 23 23:59:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.06/0.33 Running first-order theorem proving
% 0.06/0.33 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.33
% 0.06/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.33
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.34 % Proving...
% 32.00/5.51 % SZS status Started for theBenchmark.p
% 32.00/5.51 % SZS status Theorem for theBenchmark.p
% 32.00/5.51
% 32.00/5.51 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 32.00/5.51
% 32.00/5.51 % ------ iProver source info
% 32.00/5.51
% 32.00/5.51 % git: date: 2026-07-19 20:42:38 +0200
% 32.00/5.51 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 32.00/5.51 % git: non_committed_changes: false
% 32.00/5.51
% 32.00/5.51 % ------ Parsing...
% 32.00/5.51 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 32.00/5.51
% 32.00/5.51 % ------ Preprocessing... sf_s rm: 0 0s sf_e %
% 32.00/5.51
% 32.00/5.51 % ------ Preprocessing...
% 32.00/5.51 % ------ Proving...
% 32.00/5.51 % ------ Problem Properties
% 32.00/5.51
% 32.00/5.51 %
% 32.00/5.51 % clauses 107
% 32.00/5.51 % conjectures 55
% 32.00/5.51 % EPR 38
% 32.00/5.51 % Horn 80
% 32.00/5.51 % unary 25
% 32.00/5.51 % binary 8
% 32.00/5.51 % lits 452
% 32.00/5.51 % lits eq 0
% 32.00/5.51 % fd_pure 0
% 32.00/5.51 % fd_pseudo 0
% 32.00/5.51 % fd_cond 0
% 32.00/5.51 % fd_pseudo_cond 0
% 32.00/5.52 % AC symbols 0
% 32.00/5.52
% 32.00/5.52 % ------ Input Options Time Limit: Unbounded
% 32.00/5.52
% 32.00/5.52
% 32.00/5.52 % ------
% 32.00/5.52 % Current options:
% 32.00/5.52 % ------
% 32.00/5.52
% 32.00/5.52
% 32.00/5.52 %
% 32.00/5.52
% 32.00/5.52 % ------ Proving...
% 32.00/5.52 %
% 32.00/5.52
% 32.00/5.52 % SZS status Theorem for theBenchmark.p
% 32.00/5.52
% 32.00/5.52 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 32.00/5.52
% 32.00/5.52
%------------------------------------------------------------------------------