%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 : Mon Sep 7 01:09:52 PM UTC 2026
% Result : Theorem 0.11s 0.38s
% Output : Proof 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 51
% Syntax : Number of formulae : 59 ( 3 unt; 50 def)
% Number of atoms : 2123 ( 0 equ)
% Maximal formula atoms : 440 ( 35 avg)
% Number of connectives : 3302 (1238 ~;1412 |; 602 &)
% ( 0 <=>; 0 =>; 50 <=; 0 <~>)
% Maximal formula depth : 34 ( 12 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 63 ( 62 usr; 1 prp; 0-2 aty)
% Number of functors : 53 ( 53 usr; 33 con; 0-1 aty)
% Number of variables : 817 ( 0 sgn 760 !; 57 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p11(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p11(X2) ) )
| p10(X1) )
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p11(X1)
| ~ ( p10(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p10(X2) )
& p10(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2)
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p10(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p10(X2) ) )
| p9(X1) )
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p10(X1)
| ~ ( p9(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p9(X2) )
& p9(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2)
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p9(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p9(X2) ) )
| p8(X1) )
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p9(X1)
| ~ ( p8(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p8(X2) )
& p8(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2)
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p8(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p8(X2) ) )
| p7(X1) )
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p8(X1)
| ~ ( p7(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p7(X2) )
& p7(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2)
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p7(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p7(X2) ) )
| p6(X1) )
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p7(X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& p6(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2)
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) )
| p5(X1) )
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& p5(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) ) )
| p4(X1) )
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& p4(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) )
| p3(X1) )
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& p3(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) )
| p2(X1) )
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& p2(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) )
| p1(X1) )
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ ( p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& p1(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) ) ) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p11(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p11(X2) ) )
| p10(X1) )
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p11(X1)
| ~ ( p10(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p10(X2) )
& p10(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) ) )
| p10(X2)
| p11(X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p10(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p10(X2) ) )
| p9(X1) )
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p10(X1)
| ~ ( p9(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p9(X2) )
& p9(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p10(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p10(X1) ) )
| p9(X2)
| p10(X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) )
& p9(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p9(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p9(X2) ) )
| p8(X1) )
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p9(X1)
| ~ ( p8(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p8(X2) )
& p8(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p9(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p9(X1) ) )
| p8(X2)
| p9(X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) )
& p8(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p8(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p8(X2) ) )
| p7(X1) )
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p8(X1)
| ~ ( p7(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p7(X2) )
& p7(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p8(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p8(X1) ) )
| p7(X2)
| p8(X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) )
& p7(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p7(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p7(X2) ) )
| p6(X1) )
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p7(X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& p6(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p7(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p7(X1) ) )
| p6(X2)
| p7(X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& p6(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) )
| p5(X1) )
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& p5(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p6(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p6(X1) ) )
| p5(X2)
| p6(X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& p5(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p5(X2) ) )
| p4(X1) )
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& p4(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p5(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p5(X1) ) )
| p4(X2)
| p5(X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& p4(X2) ) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p10(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1) )
& p10(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) )
| p3(X1) )
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& p3(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p4(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p4(X1) ) )
| p3(X2)
| p4(X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& p3(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) )
| p2(X1) )
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& p2(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p3(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p3(X1) ) )
| p2(X2)
| p3(X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& p2(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) )
| p1(X1) )
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ ( p1(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& p1(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p2(X1) ) )
| p1(X2)
| p2(X2)
| ~ ( p1(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& p1(X2) ) ) ) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X3] :
( ~ r1(X2,X3)
| p11(X3) ) )
| p10(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p11(X4)
| ~ ( p10(X4)
& ! [X5] :
( ~ r1(X4,X5)
| p10(X5) )
& p10(X4) ) )
| ~ ( ! [X6] :
( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ( p11(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p11(X8) ) )
| p10(X7) )
| p11(X6)
| ~ ( p10(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p10(X9) )
& p10(X6) ) )
& ! [X10] :
( ~ r1(X1,X10)
| ~ ( p11(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p11(X11) ) )
| p10(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p11(X12)
| ~ ( p10(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p10(X13) )
& p10(X12) ) ) )
& ! [X14] :
( ~ r1(X1,X14)
| ~ ( p11(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p11(X15) ) )
| p10(X14)
| p11(X14)
| ~ ( p10(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p10(X16) )
& p10(X14) ) ) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p10(X17)
& ! [X18] :
( ~ r1(X17,X18)
| p10(X18) ) )
| p9(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p10(X19)
| ~ ( p9(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p9(X20) )
& p9(X19) ) )
| ~ ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ~ ( p10(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p10(X23) ) )
| p9(X22) )
| p10(X21)
| ~ ( p9(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p9(X24) )
& p9(X21) ) )
& ! [X25] :
( ~ r1(X1,X25)
| ~ ( p10(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p10(X26) ) )
| p9(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p10(X27)
| ~ ( p9(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p9(X28) )
& p9(X27) ) ) )
& ! [X29] :
( ~ r1(X1,X29)
| ~ ( p10(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p10(X30) ) )
| p9(X29)
| p10(X29)
| ~ ( p9(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p9(X31) )
& p9(X29) ) ) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p9(X32)
& ! [X33] :
( ~ r1(X32,X33)
| p9(X33) ) )
| p8(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p9(X34)
| ~ ( p8(X34)
& ! [X35] :
( ~ r1(X34,X35)
| p8(X35) )
& p8(X34) ) )
| ~ ( ! [X36] :
( ~ r1(X1,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( p9(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p9(X38) ) )
| p8(X37) )
| p9(X36)
| ~ ( p8(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p8(X39) )
& p8(X36) ) )
& ! [X40] :
( ~ r1(X1,X40)
| ~ ( p9(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p9(X41) ) )
| p8(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p9(X42)
| ~ ( p8(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p8(X43) )
& p8(X42) ) ) )
& ! [X44] :
( ~ r1(X1,X44)
| ~ ( p9(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p9(X45) ) )
| p8(X44)
| p9(X44)
| ~ ( p8(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p8(X46) )
& p8(X44) ) ) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p8(X47)
& ! [X48] :
( ~ r1(X47,X48)
| p8(X48) ) )
| p7(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p8(X49)
| ~ ( p7(X49)
& ! [X50] :
( ~ r1(X49,X50)
| p7(X50) )
& p7(X49) ) )
| ~ ( ! [X51] :
( ~ r1(X1,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ( p8(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p8(X53) ) )
| p7(X52) )
| p8(X51)
| ~ ( p7(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p7(X54) )
& p7(X51) ) )
& ! [X55] :
( ~ r1(X1,X55)
| ~ ( p8(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p8(X56) ) )
| p7(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p8(X57)
| ~ ( p7(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p7(X58) )
& p7(X57) ) ) )
& ! [X59] :
( ~ r1(X1,X59)
| ~ ( p8(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p8(X60) ) )
| p7(X59)
| p8(X59)
| ~ ( p7(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p7(X61) )
& p7(X59) ) ) ) )
| ~ ( ! [X62] :
( ~ r1(X1,X62)
| ~ ( p7(X62)
& ! [X63] :
( ~ r1(X62,X63)
| p7(X63) ) )
| p6(X62) )
| ! [X64] :
( ~ r1(X1,X64)
| p7(X64)
| ~ ( p6(X64)
& ! [X65] :
( ~ r1(X64,X65)
| p6(X65) )
& p6(X64) ) )
| ~ ( ! [X66] :
( ~ r1(X1,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ~ ( p7(X67)
& ! [X68] :
( ~ r1(X67,X68)
| p7(X68) ) )
| p6(X67) )
| p7(X66)
| ~ ( p6(X66)
& ! [X69] :
( ~ r1(X66,X69)
| p6(X69) )
& p6(X66) ) )
& ! [X70] :
( ~ r1(X1,X70)
| ~ ( p7(X70)
& ! [X71] :
( ~ r1(X70,X71)
| p7(X71) ) )
| p6(X70)
| ! [X72] :
( ~ r1(X70,X72)
| p7(X72)
| ~ ( p6(X72)
& ! [X73] :
( ~ r1(X72,X73)
| p6(X73) )
& p6(X72) ) ) )
& ! [X74] :
( ~ r1(X1,X74)
| ~ ( p7(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p7(X75) ) )
| p6(X74)
| p7(X74)
| ~ ( p6(X74)
& ! [X76] :
( ~ r1(X74,X76)
| p6(X76) )
& p6(X74) ) ) ) )
| ~ ( ! [X77] :
( ~ r1(X1,X77)
| ~ ( p6(X77)
& ! [X78] :
( ~ r1(X77,X78)
| p6(X78) ) )
| p5(X77) )
| ! [X79] :
( ~ r1(X1,X79)
| p6(X79)
| ~ ( p5(X79)
& ! [X80] :
( ~ r1(X79,X80)
| p5(X80) )
& p5(X79) ) )
| ~ ( ! [X81] :
( ~ r1(X1,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ~ ( p6(X82)
& ! [X83] :
( ~ r1(X82,X83)
| p6(X83) ) )
| p5(X82) )
| p6(X81)
| ~ ( p5(X81)
& ! [X84] :
( ~ r1(X81,X84)
| p5(X84) )
& p5(X81) ) )
& ! [X85] :
( ~ r1(X1,X85)
| ~ ( p6(X85)
& ! [X86] :
( ~ r1(X85,X86)
| p6(X86) ) )
| p5(X85)
| ! [X87] :
( ~ r1(X85,X87)
| p6(X87)
| ~ ( p5(X87)
& ! [X88] :
( ~ r1(X87,X88)
| p5(X88) )
& p5(X87) ) ) )
& ! [X89] :
( ~ r1(X1,X89)
| ~ ( p6(X89)
& ! [X90] :
( ~ r1(X89,X90)
| p6(X90) ) )
| p5(X89)
| p6(X89)
| ~ ( p5(X89)
& ! [X91] :
( ~ r1(X89,X91)
| p5(X91) )
& p5(X89) ) ) ) )
| ~ ( ! [X92] :
( ~ r1(X1,X92)
| ~ ( p5(X92)
& ! [X93] :
( ~ r1(X92,X93)
| p5(X93) ) )
| p4(X92) )
| ! [X94] :
( ~ r1(X1,X94)
| p5(X94)
| ~ ( p4(X94)
& ! [X95] :
( ~ r1(X94,X95)
| p4(X95) )
& p4(X94) ) )
| ~ ( ! [X96] :
( ~ r1(X1,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ~ ( p5(X97)
& ! [X98] :
( ~ r1(X97,X98)
| p5(X98) ) )
| p4(X97) )
| p5(X96)
| ~ ( p4(X96)
& ! [X99] :
( ~ r1(X96,X99)
| p4(X99) )
& p4(X96) ) )
& ! [X100] :
( ~ r1(X1,X100)
| ~ ( p5(X100)
& ! [X101] :
( ~ r1(X100,X101)
| p5(X101) ) )
| p4(X100)
| ! [X102] :
( ~ r1(X100,X102)
| p5(X102)
| ~ ( p4(X102)
& ! [X103] :
( ~ r1(X102,X103)
| p4(X103) )
& p4(X102) ) ) )
& ! [X104] :
( ~ r1(X1,X104)
| ~ ( p5(X104)
& ! [X105] :
( ~ r1(X104,X105)
| p5(X105) ) )
| p4(X104)
| p5(X104)
| ~ ( p4(X104)
& ! [X106] :
( ~ r1(X104,X106)
| p4(X106) )
& p4(X104) ) ) ) )
| ! [X107] :
( ~ r1(X1,X107)
| p10(X107)
| ~ ( ! [X108] :
( ~ r1(X107,X108)
| p10(X108) )
& p10(X107) ) )
| ! [X109] :
( ~ r1(X1,X109)
| p10(X109)
| ~ ( ! [X110] :
( ~ r1(X109,X110)
| p10(X110) )
& p10(X109) ) )
| ~ ( ! [X111] :
( ~ r1(X1,X111)
| ~ ( p4(X111)
& ! [X112] :
( ~ r1(X111,X112)
| p4(X112) ) )
| p3(X111) )
| ! [X113] :
( ~ r1(X1,X113)
| p4(X113)
| ~ ( p3(X113)
& ! [X114] :
( ~ r1(X113,X114)
| p3(X114) )
& p3(X113) ) )
| ~ ( ! [X115] :
( ~ r1(X1,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ ( p4(X116)
& ! [X117] :
( ~ r1(X116,X117)
| p4(X117) ) )
| p3(X116) )
| p4(X115)
| ~ ( p3(X115)
& ! [X118] :
( ~ r1(X115,X118)
| p3(X118) )
& p3(X115) ) )
& ! [X119] :
( ~ r1(X1,X119)
| ~ ( p4(X119)
& ! [X120] :
( ~ r1(X119,X120)
| p4(X120) ) )
| p3(X119)
| ! [X121] :
( ~ r1(X119,X121)
| p4(X121)
| ~ ( p3(X121)
& ! [X122] :
( ~ r1(X121,X122)
| p3(X122) )
& p3(X121) ) ) )
& ! [X123] :
( ~ r1(X1,X123)
| ~ ( p4(X123)
& ! [X124] :
( ~ r1(X123,X124)
| p4(X124) ) )
| p3(X123)
| p4(X123)
| ~ ( p3(X123)
& ! [X125] :
( ~ r1(X123,X125)
| p3(X125) )
& p3(X123) ) ) ) )
| ~ ( ! [X126] :
( ~ r1(X1,X126)
| ~ ( p3(X126)
& ! [X127] :
( ~ r1(X126,X127)
| p3(X127) ) )
| p2(X126) )
| ! [X128] :
( ~ r1(X1,X128)
| p3(X128)
| ~ ( p2(X128)
& ! [X129] :
( ~ r1(X128,X129)
| p2(X129) )
& p2(X128) ) )
| ~ ( ! [X130] :
( ~ r1(X1,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ ( p3(X131)
& ! [X132] :
( ~ r1(X131,X132)
| p3(X132) ) )
| p2(X131) )
| p3(X130)
| ~ ( p2(X130)
& ! [X133] :
( ~ r1(X130,X133)
| p2(X133) )
& p2(X130) ) )
& ! [X134] :
( ~ r1(X1,X134)
| ~ ( p3(X134)
& ! [X135] :
( ~ r1(X134,X135)
| p3(X135) ) )
| p2(X134)
| ! [X136] :
( ~ r1(X134,X136)
| p3(X136)
| ~ ( p2(X136)
& ! [X137] :
( ~ r1(X136,X137)
| p2(X137) )
& p2(X136) ) ) )
& ! [X138] :
( ~ r1(X1,X138)
| ~ ( p3(X138)
& ! [X139] :
( ~ r1(X138,X139)
| p3(X139) ) )
| p2(X138)
| p3(X138)
| ~ ( p2(X138)
& ! [X140] :
( ~ r1(X138,X140)
| p2(X140) )
& p2(X138) ) ) ) )
| ~ ( ! [X141] :
( ~ r1(X1,X141)
| ~ ( p2(X141)
& ! [X142] :
( ~ r1(X141,X142)
| p2(X142) ) )
| p1(X141) )
| ! [X143] :
( ~ r1(X1,X143)
| p2(X143)
| ~ ( p1(X143)
& ! [X144] :
( ~ r1(X143,X144)
| p1(X144) )
& p1(X143) ) )
| ~ ( ! [X145] :
( ~ r1(X1,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ~ ( p2(X146)
& ! [X147] :
( ~ r1(X146,X147)
| p2(X147) ) )
| p1(X146) )
| p2(X145)
| ~ ( p1(X145)
& ! [X148] :
( ~ r1(X145,X148)
| p1(X148) )
& p1(X145) ) )
& ! [X149] :
( ~ r1(X1,X149)
| ~ ( p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| p2(X150) ) )
| p1(X149)
| ! [X151] :
( ~ r1(X149,X151)
| p2(X151)
| ~ ( p1(X151)
& ! [X152] :
( ~ r1(X151,X152)
| p1(X152) )
& p1(X151) ) ) )
& ! [X153] :
( ~ r1(X1,X153)
| ~ ( p2(X153)
& ! [X154] :
( ~ r1(X153,X154)
| p2(X154) ) )
| p1(X153)
| p2(X153)
| ~ ( p1(X153)
& ! [X155] :
( ~ r1(X153,X155)
| p1(X155) )
& p1(X153) ) ) ) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X2,X3] :
( ren1(X2,X3)
<= ( ~ r1(X2,X3)
| p11(X3) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X4,X5] :
( ren2(X4,X5)
<= ( ~ r1(X4,X5)
| p10(X5) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X1,X6] :
( ren3(X1,X6)
<= ( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ( p11(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p11(X8) ) )
| p10(X7) )
| p11(X6)
| ~ ( p10(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p10(X9) )
& p10(X6) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X1,X10] :
( ren4(X1,X10)
<= ( ~ r1(X1,X10)
| ~ ( p11(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p11(X11) ) )
| p10(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p11(X12)
| ~ ( p10(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p10(X13) )
& p10(X12) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X1,X14] :
( ren5(X1,X14)
<= ( ~ r1(X1,X14)
| ~ ( p11(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p11(X15) ) )
| p10(X14)
| p11(X14)
| ~ ( p10(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p10(X16) )
& p10(X14) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X17,X18] :
( ren6(X17,X18)
<= ( ~ r1(X17,X18)
| p10(X18) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X19,X20] :
( ren7(X19,X20)
<= ( ~ r1(X19,X20)
| p9(X20) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X1,X21] :
( ren8(X1,X21)
<= ( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ~ ( p10(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p10(X23) ) )
| p9(X22) )
| p10(X21)
| ~ ( p9(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p9(X24) )
& p9(X21) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X1,X25] :
( ren9(X1,X25)
<= ( ~ r1(X1,X25)
| ~ ( p10(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p10(X26) ) )
| p9(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p10(X27)
| ~ ( p9(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p9(X28) )
& p9(X27) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X1,X29] :
( ren10(X1,X29)
<= ( ~ r1(X1,X29)
| ~ ( p10(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p10(X30) ) )
| p9(X29)
| p10(X29)
| ~ ( p9(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p9(X31) )
& p9(X29) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X32,X33] :
( ren11(X32,X33)
<= ( ~ r1(X32,X33)
| p9(X33) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X34,X35] :
( ren12(X34,X35)
<= ( ~ r1(X34,X35)
| p8(X35) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren13_defn,definition,
! [X1,X36] :
( ren13(X1,X36)
<= ( ~ r1(X1,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( p9(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p9(X38) ) )
| p8(X37) )
| p9(X36)
| ~ ( p8(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p8(X39) )
& p8(X36) ) ) ),
introduced(definition,[new_symbols(definition,[ren13])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren14_defn,definition,
! [X1,X40] :
( ren14(X1,X40)
<= ( ~ r1(X1,X40)
| ~ ( p9(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p9(X41) ) )
| p8(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p9(X42)
| ~ ( p8(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p8(X43) )
& p8(X42) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren14])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren15_defn,definition,
! [X1,X44] :
( ren15(X1,X44)
<= ( ~ r1(X1,X44)
| ~ ( p9(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p9(X45) ) )
| p8(X44)
| p9(X44)
| ~ ( p8(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p8(X46) )
& p8(X44) ) ) ),
introduced(definition,[new_symbols(definition,[ren15])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren16_defn,definition,
! [X47,X48] :
( ren16(X47,X48)
<= ( ~ r1(X47,X48)
| p8(X48) ) ),
introduced(definition,[new_symbols(definition,[ren16])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren17_defn,definition,
! [X49,X50] :
( ren17(X49,X50)
<= ( ~ r1(X49,X50)
| p7(X50) ) ),
introduced(definition,[new_symbols(definition,[ren17])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren18_defn,definition,
! [X1,X51] :
( ren18(X1,X51)
<= ( ~ r1(X1,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ( p8(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p8(X53) ) )
| p7(X52) )
| p8(X51)
| ~ ( p7(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p7(X54) )
& p7(X51) ) ) ),
introduced(definition,[new_symbols(definition,[ren18])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren19_defn,definition,
! [X1,X55] :
( ren19(X1,X55)
<= ( ~ r1(X1,X55)
| ~ ( p8(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p8(X56) ) )
| p7(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p8(X57)
| ~ ( p7(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p7(X58) )
& p7(X57) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren19])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren20_defn,definition,
! [X1,X59] :
( ren20(X1,X59)
<= ( ~ r1(X1,X59)
| ~ ( p8(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p8(X60) ) )
| p7(X59)
| p8(X59)
| ~ ( p7(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p7(X61) )
& p7(X59) ) ) ),
introduced(definition,[new_symbols(definition,[ren20])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren21_defn,definition,
! [X62,X63] :
( ren21(X62,X63)
<= ( ~ r1(X62,X63)
| p7(X63) ) ),
introduced(definition,[new_symbols(definition,[ren21])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren22_defn,definition,
! [X64,X65] :
( ren22(X64,X65)
<= ( ~ r1(X64,X65)
| p6(X65) ) ),
introduced(definition,[new_symbols(definition,[ren22])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren23_defn,definition,
! [X1,X66] :
( ren23(X1,X66)
<= ( ~ r1(X1,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ~ ( p7(X67)
& ! [X68] :
( ~ r1(X67,X68)
| p7(X68) ) )
| p6(X67) )
| p7(X66)
| ~ ( p6(X66)
& ! [X69] :
( ~ r1(X66,X69)
| p6(X69) )
& p6(X66) ) ) ),
introduced(definition,[new_symbols(definition,[ren23])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren24_defn,definition,
! [X1,X70] :
( ren24(X1,X70)
<= ( ~ r1(X1,X70)
| ~ ( p7(X70)
& ! [X71] :
( ~ r1(X70,X71)
| p7(X71) ) )
| p6(X70)
| ! [X72] :
( ~ r1(X70,X72)
| p7(X72)
| ~ ( p6(X72)
& ! [X73] :
( ~ r1(X72,X73)
| p6(X73) )
& p6(X72) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren24])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren25_defn,definition,
! [X1,X74] :
( ren25(X1,X74)
<= ( ~ r1(X1,X74)
| ~ ( p7(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p7(X75) ) )
| p6(X74)
| p7(X74)
| ~ ( p6(X74)
& ! [X76] :
( ~ r1(X74,X76)
| p6(X76) )
& p6(X74) ) ) ),
introduced(definition,[new_symbols(definition,[ren25])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren26_defn,definition,
! [X77,X78] :
( ren26(X77,X78)
<= ( ~ r1(X77,X78)
| p6(X78) ) ),
introduced(definition,[new_symbols(definition,[ren26])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren27_defn,definition,
! [X79,X80] :
( ren27(X79,X80)
<= ( ~ r1(X79,X80)
| p5(X80) ) ),
introduced(definition,[new_symbols(definition,[ren27])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren28_defn,definition,
! [X1,X81] :
( ren28(X1,X81)
<= ( ~ r1(X1,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ~ ( p6(X82)
& ! [X83] :
( ~ r1(X82,X83)
| p6(X83) ) )
| p5(X82) )
| p6(X81)
| ~ ( p5(X81)
& ! [X84] :
( ~ r1(X81,X84)
| p5(X84) )
& p5(X81) ) ) ),
introduced(definition,[new_symbols(definition,[ren28])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren29_defn,definition,
! [X1,X85] :
( ren29(X1,X85)
<= ( ~ r1(X1,X85)
| ~ ( p6(X85)
& ! [X86] :
( ~ r1(X85,X86)
| p6(X86) ) )
| p5(X85)
| ! [X87] :
( ~ r1(X85,X87)
| p6(X87)
| ~ ( p5(X87)
& ! [X88] :
( ~ r1(X87,X88)
| p5(X88) )
& p5(X87) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren29])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren30_defn,definition,
! [X1,X89] :
( ren30(X1,X89)
<= ( ~ r1(X1,X89)
| ~ ( p6(X89)
& ! [X90] :
( ~ r1(X89,X90)
| p6(X90) ) )
| p5(X89)
| p6(X89)
| ~ ( p5(X89)
& ! [X91] :
( ~ r1(X89,X91)
| p5(X91) )
& p5(X89) ) ) ),
introduced(definition,[new_symbols(definition,[ren30])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren31_defn,definition,
! [X92,X93] :
( ren31(X92,X93)
<= ( ~ r1(X92,X93)
| p5(X93) ) ),
introduced(definition,[new_symbols(definition,[ren31])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren32_defn,definition,
! [X94,X95] :
( ren32(X94,X95)
<= ( ~ r1(X94,X95)
| p4(X95) ) ),
introduced(definition,[new_symbols(definition,[ren32])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren33_defn,definition,
! [X1,X96] :
( ren33(X1,X96)
<= ( ~ r1(X1,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ~ ( p5(X97)
& ! [X98] :
( ~ r1(X97,X98)
| p5(X98) ) )
| p4(X97) )
| p5(X96)
| ~ ( p4(X96)
& ! [X99] :
( ~ r1(X96,X99)
| p4(X99) )
& p4(X96) ) ) ),
introduced(definition,[new_symbols(definition,[ren33])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren34_defn,definition,
! [X1,X100] :
( ren34(X1,X100)
<= ( ~ r1(X1,X100)
| ~ ( p5(X100)
& ! [X101] :
( ~ r1(X100,X101)
| p5(X101) ) )
| p4(X100)
| ! [X102] :
( ~ r1(X100,X102)
| p5(X102)
| ~ ( p4(X102)
& ! [X103] :
( ~ r1(X102,X103)
| p4(X103) )
& p4(X102) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren34])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren35_defn,definition,
! [X1,X104] :
( ren35(X1,X104)
<= ( ~ r1(X1,X104)
| ~ ( p5(X104)
& ! [X105] :
( ~ r1(X104,X105)
| p5(X105) ) )
| p4(X104)
| p5(X104)
| ~ ( p4(X104)
& ! [X106] :
( ~ r1(X104,X106)
| p4(X106) )
& p4(X104) ) ) ),
introduced(definition,[new_symbols(definition,[ren35])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren36_defn,definition,
! [X111,X112] :
( ren36(X111,X112)
<= ( ~ r1(X111,X112)
| p4(X112) ) ),
introduced(definition,[new_symbols(definition,[ren36])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren37_defn,definition,
! [X113,X114] :
( ren37(X113,X114)
<= ( ~ r1(X113,X114)
| p3(X114) ) ),
introduced(definition,[new_symbols(definition,[ren37])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren38_defn,definition,
! [X1,X115] :
( ren38(X1,X115)
<= ( ~ r1(X1,X115)
| ! [X116] :
( ~ r1(X115,X116)
| ~ ( p4(X116)
& ! [X117] :
( ~ r1(X116,X117)
| p4(X117) ) )
| p3(X116) )
| p4(X115)
| ~ ( p3(X115)
& ! [X118] :
( ~ r1(X115,X118)
| p3(X118) )
& p3(X115) ) ) ),
introduced(definition,[new_symbols(definition,[ren38])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren39_defn,definition,
! [X1,X119] :
( ren39(X1,X119)
<= ( ~ r1(X1,X119)
| ~ ( p4(X119)
& ! [X120] :
( ~ r1(X119,X120)
| p4(X120) ) )
| p3(X119)
| ! [X121] :
( ~ r1(X119,X121)
| p4(X121)
| ~ ( p3(X121)
& ! [X122] :
( ~ r1(X121,X122)
| p3(X122) )
& p3(X121) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren39])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren40_defn,definition,
! [X1,X123] :
( ren40(X1,X123)
<= ( ~ r1(X1,X123)
| ~ ( p4(X123)
& ! [X124] :
( ~ r1(X123,X124)
| p4(X124) ) )
| p3(X123)
| p4(X123)
| ~ ( p3(X123)
& ! [X125] :
( ~ r1(X123,X125)
| p3(X125) )
& p3(X123) ) ) ),
introduced(definition,[new_symbols(definition,[ren40])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren41_defn,definition,
! [X126,X127] :
( ren41(X126,X127)
<= ( ~ r1(X126,X127)
| p3(X127) ) ),
introduced(definition,[new_symbols(definition,[ren41])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren42_defn,definition,
! [X128,X129] :
( ren42(X128,X129)
<= ( ~ r1(X128,X129)
| p2(X129) ) ),
introduced(definition,[new_symbols(definition,[ren42])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren43_defn,definition,
! [X1,X130] :
( ren43(X1,X130)
<= ( ~ r1(X1,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ ( p3(X131)
& ! [X132] :
( ~ r1(X131,X132)
| p3(X132) ) )
| p2(X131) )
| p3(X130)
| ~ ( p2(X130)
& ! [X133] :
( ~ r1(X130,X133)
| p2(X133) )
& p2(X130) ) ) ),
introduced(definition,[new_symbols(definition,[ren43])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren44_defn,definition,
! [X1,X134] :
( ren44(X1,X134)
<= ( ~ r1(X1,X134)
| ~ ( p3(X134)
& ! [X135] :
( ~ r1(X134,X135)
| p3(X135) ) )
| p2(X134)
| ! [X136] :
( ~ r1(X134,X136)
| p3(X136)
| ~ ( p2(X136)
& ! [X137] :
( ~ r1(X136,X137)
| p2(X137) )
& p2(X136) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren44])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren45_defn,definition,
! [X1,X138] :
( ren45(X1,X138)
<= ( ~ r1(X1,X138)
| ~ ( p3(X138)
& ! [X139] :
( ~ r1(X138,X139)
| p3(X139) ) )
| p2(X138)
| p3(X138)
| ~ ( p2(X138)
& ! [X140] :
( ~ r1(X138,X140)
| p2(X140) )
& p2(X138) ) ) ),
introduced(definition,[new_symbols(definition,[ren45])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren46_defn,definition,
! [X141,X142] :
( ren46(X141,X142)
<= ( ~ r1(X141,X142)
| p2(X142) ) ),
introduced(definition,[new_symbols(definition,[ren46])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren47_defn,definition,
! [X143,X144] :
( ren47(X143,X144)
<= ( ~ r1(X143,X144)
| p1(X144) ) ),
introduced(definition,[new_symbols(definition,[ren47])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren48_defn,definition,
! [X1,X145] :
( ren48(X1,X145)
<= ( ~ r1(X1,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ~ ( p2(X146)
& ! [X147] :
( ~ r1(X146,X147)
| p2(X147) ) )
| p1(X146) )
| p2(X145)
| ~ ( p1(X145)
& ! [X148] :
( ~ r1(X145,X148)
| p1(X148) )
& p1(X145) ) ) ),
introduced(definition,[new_symbols(definition,[ren48])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren49_defn,definition,
! [X1,X149] :
( ren49(X1,X149)
<= ( ~ r1(X1,X149)
| ~ ( p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| p2(X150) ) )
| p1(X149)
| ! [X151] :
( ~ r1(X149,X151)
| p2(X151)
| ~ ( p1(X151)
& ! [X152] :
( ~ r1(X151,X152)
| p1(X152) )
& p1(X151) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren49])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren50_defn,definition,
! [X1,X153] :
( ren50(X1,X153)
<= ( ~ r1(X1,X153)
| ~ ( p2(X153)
& ! [X154] :
( ~ r1(X153,X154)
| p2(X154) ) )
| p1(X153)
| p2(X153)
| ~ ( p1(X153)
& ! [X155] :
( ~ r1(X153,X155)
| p1(X155) )
& p1(X153) ) ) ),
introduced(definition,[new_symbols(definition,[ren50])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p11(X2)
& ! [X3] : ren1(X2,X3) )
| p10(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p11(X4)
| ~ ( p10(X4)
& ! [X5] : ren2(X4,X5)
& p10(X4) ) )
| ~ ( ! [X6] : ren3(X1,X6)
& ! [X10] : ren4(X1,X10)
& ! [X14] : ren5(X1,X14) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p10(X17)
& ! [X18] : ren6(X17,X18) )
| p9(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p10(X19)
| ~ ( p9(X19)
& ! [X20] : ren7(X19,X20)
& p9(X19) ) )
| ~ ( ! [X21] : ren8(X1,X21)
& ! [X25] : ren9(X1,X25)
& ! [X29] : ren10(X1,X29) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p9(X32)
& ! [X33] : ren11(X32,X33) )
| p8(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p9(X34)
| ~ ( p8(X34)
& ! [X35] : ren12(X34,X35)
& p8(X34) ) )
| ~ ( ! [X36] : ren13(X1,X36)
& ! [X40] : ren14(X1,X40)
& ! [X44] : ren15(X1,X44) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p8(X47)
& ! [X48] : ren16(X47,X48) )
| p7(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p8(X49)
| ~ ( p7(X49)
& ! [X50] : ren17(X49,X50)
& p7(X49) ) )
| ~ ( ! [X51] : ren18(X1,X51)
& ! [X55] : ren19(X1,X55)
& ! [X59] : ren20(X1,X59) ) )
| ~ ( ! [X62] :
( ~ r1(X1,X62)
| ~ ( p7(X62)
& ! [X63] : ren21(X62,X63) )
| p6(X62) )
| ! [X64] :
( ~ r1(X1,X64)
| p7(X64)
| ~ ( p6(X64)
& ! [X65] : ren22(X64,X65)
& p6(X64) ) )
| ~ ( ! [X66] : ren23(X1,X66)
& ! [X70] : ren24(X1,X70)
& ! [X74] : ren25(X1,X74) ) )
| ~ ( ! [X77] :
( ~ r1(X1,X77)
| ~ ( p6(X77)
& ! [X78] : ren26(X77,X78) )
| p5(X77) )
| ! [X79] :
( ~ r1(X1,X79)
| p6(X79)
| ~ ( p5(X79)
& ! [X80] : ren27(X79,X80)
& p5(X79) ) )
| ~ ( ! [X81] : ren28(X1,X81)
& ! [X85] : ren29(X1,X85)
& ! [X89] : ren30(X1,X89) ) )
| ~ ( ! [X92] :
( ~ r1(X1,X92)
| ~ ( p5(X92)
& ! [X93] : ren31(X92,X93) )
| p4(X92) )
| ! [X94] :
( ~ r1(X1,X94)
| p5(X94)
| ~ ( p4(X94)
& ! [X95] : ren32(X94,X95)
& p4(X94) ) )
| ~ ( ! [X96] : ren33(X1,X96)
& ! [X100] : ren34(X1,X100)
& ! [X104] : ren35(X1,X104) ) )
| ! [X107] :
( ~ r1(X1,X107)
| p10(X107)
| ~ ( ! [X108] :
( ~ r1(X107,X108)
| p10(X108) )
& p10(X107) ) )
| ! [X109] :
( ~ r1(X1,X109)
| p10(X109)
| ~ ( ! [X110] :
( ~ r1(X109,X110)
| p10(X110) )
& p10(X109) ) )
| ~ ( ! [X111] :
( ~ r1(X1,X111)
| ~ ( p4(X111)
& ! [X112] : ren36(X111,X112) )
| p3(X111) )
| ! [X113] :
( ~ r1(X1,X113)
| p4(X113)
| ~ ( p3(X113)
& ! [X114] : ren37(X113,X114)
& p3(X113) ) )
| ~ ( ! [X115] : ren38(X1,X115)
& ! [X119] : ren39(X1,X119)
& ! [X123] : ren40(X1,X123) ) )
| ~ ( ! [X126] :
( ~ r1(X1,X126)
| ~ ( p3(X126)
& ! [X127] : ren41(X126,X127) )
| p2(X126) )
| ! [X128] :
( ~ r1(X1,X128)
| p3(X128)
| ~ ( p2(X128)
& ! [X129] : ren42(X128,X129)
& p2(X128) ) )
| ~ ( ! [X130] : ren43(X1,X130)
& ! [X134] : ren44(X1,X134)
& ! [X138] : ren45(X1,X138) ) )
| ~ ( ! [X141] :
( ~ r1(X1,X141)
| ~ ( p2(X141)
& ! [X142] : ren46(X141,X142) )
| p1(X141) )
| ! [X143] :
( ~ r1(X1,X143)
| p2(X143)
| ~ ( p1(X143)
& ! [X144] : ren47(X143,X144)
& p1(X143) ) )
| ~ ( ! [X145] : ren48(X1,X145)
& ! [X149] : ren49(X1,X149)
& ! [X153] : ren50(X1,X153) ) ) ),
inference(renaming,[status(esa)],[main_nc_elimTB,ren1_defn,ren2_defn,ren3_defn,ren4_defn,ren5_defn,ren6_defn,ren7_defn,ren8_defn,ren9_defn,ren10_defn,ren11_defn,ren12_defn,ren13_defn,ren14_defn,ren15_defn,ren16_defn,ren17_defn,ren18_defn,ren19_defn,ren20_defn,ren21_defn,ren22_defn,ren23_defn,ren24_defn,ren25_defn,ren26_defn,ren27_defn,ren28_defn,ren29_defn,ren30_defn,ren31_defn,ren32_defn,ren33_defn,ren34_defn,ren35_defn,ren36_defn,ren37_defn,ren38_defn,ren39_defn,ren40_defn,ren41_defn,ren42_defn,ren43_defn,ren44_defn,ren45_defn,ren46_defn,ren47_defn,ren48_defn,ren49_defn,ren50_defn]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ~ p11(X2)
| ? [X3] : ~ ren1(X2,X3)
| p10(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p11(X4)
| ~ p10(X4)
| ? [X5] : ~ ren2(X4,X5)
| ~ p10(X4) )
| ? [X6] : ~ ren3(X1,X6)
| ? [X7] : ~ ren4(X1,X7)
| ? [X8] : ~ ren5(X1,X8) )
& ( ! [X9] :
( ~ r1(X1,X9)
| ~ p10(X9)
| ? [X10] : ~ ren6(X9,X10)
| p9(X9) )
| ! [X11] :
( ~ r1(X1,X11)
| p10(X11)
| ~ p9(X11)
| ? [X12] : ~ ren7(X11,X12)
| ~ p9(X11) )
| ? [X13] : ~ ren8(X1,X13)
| ? [X14] : ~ ren9(X1,X14)
| ? [X15] : ~ ren10(X1,X15) )
& ( ! [X16] :
( ~ r1(X1,X16)
| ~ p9(X16)
| ? [X17] : ~ ren11(X16,X17)
| p8(X16) )
| ! [X18] :
( ~ r1(X1,X18)
| p9(X18)
| ~ p8(X18)
| ? [X19] : ~ ren12(X18,X19)
| ~ p8(X18) )
| ? [X20] : ~ ren13(X1,X20)
| ? [X21] : ~ ren14(X1,X21)
| ? [X22] : ~ ren15(X1,X22) )
& ( ! [X23] :
( ~ r1(X1,X23)
| ~ p8(X23)
| ? [X24] : ~ ren16(X23,X24)
| p7(X23) )
| ! [X25] :
( ~ r1(X1,X25)
| p8(X25)
| ~ p7(X25)
| ? [X26] : ~ ren17(X25,X26)
| ~ p7(X25) )
| ? [X27] : ~ ren18(X1,X27)
| ? [X28] : ~ ren19(X1,X28)
| ? [X29] : ~ ren20(X1,X29) )
& ( ! [X30] :
( ~ r1(X1,X30)
| ~ p7(X30)
| ? [X31] : ~ ren21(X30,X31)
| p6(X30) )
| ! [X32] :
( ~ r1(X1,X32)
| p7(X32)
| ~ p6(X32)
| ? [X33] : ~ ren22(X32,X33)
| ~ p6(X32) )
| ? [X34] : ~ ren23(X1,X34)
| ? [X35] : ~ ren24(X1,X35)
| ? [X36] : ~ ren25(X1,X36) )
& ( ! [X37] :
( ~ r1(X1,X37)
| ~ p6(X37)
| ? [X38] : ~ ren26(X37,X38)
| p5(X37) )
| ! [X39] :
( ~ r1(X1,X39)
| p6(X39)
| ~ p5(X39)
| ? [X40] : ~ ren27(X39,X40)
| ~ p5(X39) )
| ? [X41] : ~ ren28(X1,X41)
| ? [X42] : ~ ren29(X1,X42)
| ? [X43] : ~ ren30(X1,X43) )
& ( ! [X44] :
( ~ r1(X1,X44)
| ~ p5(X44)
| ? [X45] : ~ ren31(X44,X45)
| p4(X44) )
| ! [X46] :
( ~ r1(X1,X46)
| p5(X46)
| ~ p4(X46)
| ? [X47] : ~ ren32(X46,X47)
| ~ p4(X46) )
| ? [X48] : ~ ren33(X1,X48)
| ? [X49] : ~ ren34(X1,X49)
| ? [X50] : ~ ren35(X1,X50) )
& ? [X51] :
( r1(X1,X51)
& ~ p10(X51)
& ! [X52] :
( ~ r1(X51,X52)
| p10(X52) )
& p10(X51) )
& ? [X53] :
( r1(X1,X53)
& ~ p10(X53)
& ! [X54] :
( ~ r1(X53,X54)
| p10(X54) )
& p10(X53) )
& ( ! [X55] :
( ~ r1(X1,X55)
| ~ p4(X55)
| ? [X56] : ~ ren36(X55,X56)
| p3(X55) )
| ! [X57] :
( ~ r1(X1,X57)
| p4(X57)
| ~ p3(X57)
| ? [X58] : ~ ren37(X57,X58)
| ~ p3(X57) )
| ? [X59] : ~ ren38(X1,X59)
| ? [X60] : ~ ren39(X1,X60)
| ? [X61] : ~ ren40(X1,X61) )
& ( ! [X62] :
( ~ r1(X1,X62)
| ~ p3(X62)
| ? [X63] : ~ ren41(X62,X63)
| p2(X62) )
| ! [X64] :
( ~ r1(X1,X64)
| p3(X64)
| ~ p2(X64)
| ? [X65] : ~ ren42(X64,X65)
| ~ p2(X64) )
| ? [X66] : ~ ren43(X1,X66)
| ? [X67] : ~ ren44(X1,X67)
| ? [X68] : ~ ren45(X1,X68) )
& ( ! [X69] :
( ~ r1(X1,X69)
| ~ p2(X69)
| ? [X70] : ~ ren46(X69,X70)
| p1(X69) )
| ! [X71] :
( ~ r1(X1,X71)
| p2(X71)
| ~ p1(X71)
| ? [X72] : ~ ren47(X71,X72)
| ~ p1(X71) )
| ? [X73] : ~ ren48(X1,X73)
| ? [X74] : ~ ren49(X1,X74)
| ? [X75] : ~ ren50(X1,X75) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ( ! [X2] :
( ~ r1(skc21,X2)
| ~ p11(X2)
| ~ ren1(X2,skf22(X2))
| p10(X2) )
| ! [X4] :
( ~ r1(skc21,X4)
| p11(X4)
| ~ p10(X4)
| ~ ren2(X4,skf23(X4))
| ~ p10(X4) )
| ~ ren3(skc21,skc24)
| ~ ren4(skc21,skc25)
| ~ ren5(skc21,skc26) )
& ( ! [X9] :
( ~ r1(skc21,X9)
| ~ p10(X9)
| ~ ren6(X9,skf27(X9))
| p9(X9) )
| ! [X11] :
( ~ r1(skc21,X11)
| p10(X11)
| ~ p9(X11)
| ~ ren7(X11,skf28(X11))
| ~ p9(X11) )
| ~ ren8(skc21,skc29)
| ~ ren9(skc21,skc30)
| ~ ren10(skc21,skc31) )
& ( ! [X16] :
( ~ r1(skc21,X16)
| ~ p9(X16)
| ~ ren11(X16,skf32(X16))
| p8(X16) )
| ! [X18] :
( ~ r1(skc21,X18)
| p9(X18)
| ~ p8(X18)
| ~ ren12(X18,skf33(X18))
| ~ p8(X18) )
| ~ ren13(skc21,skc34)
| ~ ren14(skc21,skc35)
| ~ ren15(skc21,skc36) )
& ( ! [X23] :
( ~ r1(skc21,X23)
| ~ p8(X23)
| ~ ren16(X23,skf37(X23))
| p7(X23) )
| ! [X25] :
( ~ r1(skc21,X25)
| p8(X25)
| ~ p7(X25)
| ~ ren17(X25,skf38(X25))
| ~ p7(X25) )
| ~ ren18(skc21,skc39)
| ~ ren19(skc21,skc40)
| ~ ren20(skc21,skc41) )
& ( ! [X30] :
( ~ r1(skc21,X30)
| ~ p7(X30)
| ~ ren21(X30,skf42(X30))
| p6(X30) )
| ! [X32] :
( ~ r1(skc21,X32)
| p7(X32)
| ~ p6(X32)
| ~ ren22(X32,skf43(X32))
| ~ p6(X32) )
| ~ ren23(skc21,skc44)
| ~ ren24(skc21,skc45)
| ~ ren25(skc21,skc46) )
& ( ! [X37] :
( ~ r1(skc21,X37)
| ~ p6(X37)
| ~ ren26(X37,skf47(X37))
| p5(X37) )
| ! [X39] :
( ~ r1(skc21,X39)
| p6(X39)
| ~ p5(X39)
| ~ ren27(X39,skf48(X39))
| ~ p5(X39) )
| ~ ren28(skc21,skc49)
| ~ ren29(skc21,skc50)
| ~ ren30(skc21,skc51) )
& ( ! [X44] :
( ~ r1(skc21,X44)
| ~ p5(X44)
| ~ ren31(X44,skf52(X44))
| p4(X44) )
| ! [X46] :
( ~ r1(skc21,X46)
| p5(X46)
| ~ p4(X46)
| ~ ren32(X46,skf53(X46))
| ~ p4(X46) )
| ~ ren33(skc21,skc54)
| ~ ren34(skc21,skc55)
| ~ ren35(skc21,skc56) )
& r1(skc21,skc57)
& ~ p10(skc57)
& ! [X52] :
( ~ r1(skc57,X52)
| p10(X52) )
& p10(skc57)
& r1(skc21,skc58)
& ~ p10(skc58)
& ! [X54] :
( ~ r1(skc58,X54)
| p10(X54) )
& p10(skc58)
& ( ! [X55] :
( ~ r1(skc21,X55)
| ~ p4(X55)
| ~ ren36(X55,skf59(X55))
| p3(X55) )
| ! [X57] :
( ~ r1(skc21,X57)
| p4(X57)
| ~ p3(X57)
| ~ ren37(X57,skf60(X57))
| ~ p3(X57) )
| ~ ren38(skc21,skc61)
| ~ ren39(skc21,skc62)
| ~ ren40(skc21,skc63) )
& ( ! [X62] :
( ~ r1(skc21,X62)
| ~ p3(X62)
| ~ ren41(X62,skf64(X62))
| p2(X62) )
| ! [X64] :
( ~ r1(skc21,X64)
| p3(X64)
| ~ p2(X64)
| ~ ren42(X64,skf65(X64))
| ~ p2(X64) )
| ~ ren43(skc21,skc66)
| ~ ren44(skc21,skc67)
| ~ ren45(skc21,skc68) )
& ( ! [X69] :
( ~ r1(skc21,X69)
| ~ p2(X69)
| ~ ren46(X69,skf69(X69))
| p1(X69) )
| ! [X71] :
( ~ r1(skc21,X71)
| p2(X71)
| ~ p1(X71)
| ~ ren47(X71,skf70(X71))
| ~ p1(X71) )
| ~ ren48(skc21,skc71)
| ~ ren49(skc21,skc72)
| ~ ren50(skc21,skc73) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc21,skf22,skf23,skc24,skc25,skc26,skf27,skf28,skc29,skc30,skc31,skf32,skf33,skc34,skc35,skc36,skf37,skf38,skc39,skc40,skc41,skf42,skf43,skc44,skc45,skc46,skf47,skf48,skc49,skc50,skc51,skf52,skf53,skc54,skc55,skc56,skc57,skc58,skf59,skf60,skc61,skc62,skc63,skf64,skf65,skc66,skc67,skc68,skf69,skf70,skc71,skc72,skc73]),skolemize(X1,skc21),skolemize(X3,skf22(X2)),skolemize(X5,skf23(X4)),skolemize(X6,skc24),skolemize(X7,skc25),skolemize(X8,skc26),skolemize(X10,skf27(X9)),skolemize(X12,skf28(X11)),skolemize(X13,skc29),skolemize(X14,skc30),skolemize(X15,skc31),skolemize(X17,skf32(X16)),skolemize(X19,skf33(X18)),skolemize(X20,skc34),skolemize(X21,skc35),skolemize(X22,skc36),skolemize(X24,skf37(X23)),skolemize(X26,skf38(X25)),skolemize(X27,skc39),skolemize(X28,skc40),skolemize(X29,skc41),skolemize(X31,skf42(X30)),skolemize(X33,skf43(X32)),skolemize(X34,skc44),skolemize(X35,skc45),skolemize(X36,skc46),skolemize(X38,skf47(X37)),skolemize(X40,skf48(X39)),skolemize(X41,skc49),skolemize(X42,skc50),skolemize(X43,skc51),skolemize(X45,skf52(X44)),skolemize(X47,skf53(X46)),skolemize(X48,skc54),skolemize(X49,skc55),skolemize(X50,skc56),skolemize(X51,skc57),skolemize(X53,skc58),skolemize(X56,skf59(X55)),skolemize(X58,skf60(X57)),skolemize(X59,skc61),skolemize(X60,skc62),skolemize(X61,skc63),skolemize(X63,skf64(X62)),skolemize(X65,skf65(X64)),skolemize(X66,skc66),skolemize(X67,skc67),skolemize(X68,skc68),skolemize(X70,skf69(X69)),skolemize(X72,skf70(X71)),skolemize(X73,skc71),skolemize(X74,skc72),skolemize(X75,skc73)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_315,plain,
p10(skc58),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_313,plain,
~ p10(skc58),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_347,plain,
$false,
inference(resolution,[status(thm)],[c_315,c_313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 4 13:05:24 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running /export/starexec/sandbox2/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37
% 0.11/0.37 % Input Clauses:
% 0.11/0.37 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.11/0.37 % 2:2:2:INP:TopTop: p11(x0) -> ren1(x1,x0)
% 0.11/0.37 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.11/0.37 % 4:2:2:INP:TopTop: p10(x0) -> ren2(x1,x0)
% 0.11/0.37 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.11/0.37 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.11/0.37 % 7:2:2:INP:TopTop: -> p11(skf1(x0)),ren3(x1,x0)
% 0.11/0.37 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p11(x1),ren3(x2,x0)
% 0.11/0.37 % 9:2:2:INP:TopTop: p10(skf1(x0)) -> ren3(x1,x0)
% 0.11/0.37 % 10:2:2:INP:TopTop: p11(x0) -> ren3(x1,x0)
% 0.11/0.37 % 11:2:2:INP:TopTop: -> p10(x0),ren3(x1,x0)
% 0.11/0.37 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren3(x2,x0)
% 0.11/0.37 % 13:2:2:INP:TopTop: -> p10(x0),ren3(x1,x0)
% 0.11/0.37 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.11/0.37 % 15:2:2:INP:TopTop: -> p11(x0),ren4(x1,x0)
% 0.11/0.37 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren4(x2,x0)
% 0.11/0.37 % 17:2:2:INP:TopTop: p10(x0) -> ren4(x1,x0)
% 0.11/0.37 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.11/0.37 % 19:2:2:INP:TopTop: p11(skf2(x0)) -> ren4(x1,x0)
% 0.11/0.37 % 20:2:2:INP:TopTop: -> p10(skf2(x0)),ren4(x1,x0)
% 0.11/0.37 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p10(x1),ren4(x2,x0)
% 0.11/0.37 % 22:2:2:INP:TopTop: -> p10(skf2(x0)),ren4(x1,x0)
% 0.11/0.37 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.11/0.37 % 24:2:2:INP:TopTop: -> p11(x0),ren5(x1,x0)
% 0.11/0.37 % 25:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren5(x2,x0)
% 0.11/0.37 % 26:2:2:INP:TopTop: p10(x0) -> ren5(x1,x0)
% 0.11/0.37 % 27:2:2:INP:TopTop: p11(x0) -> ren5(x1,x0)
% 0.11/0.37 % 28:2:2:INP:TopTop: -> p10(x0),ren5(x1,x0)
% 0.11/0.37 % 29:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren5(x2,x0)
% 0.11/0.37 % 30:2:2:INP:TopTop: -> p10(x0),ren5(x1,x0)
% 0.11/0.37 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.11/0.37 % 32:2:2:INP:TopTop: p10(x0) -> ren6(x1,x0)
% 0.11/0.37 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.11/0.37 % 34:2:2:INP:TopTop: p9(x0) -> ren7(x1,x0)
% 0.11/0.37 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.11/0.37 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.11/0.37 % 37:2:2:INP:TopTop: -> p10(skf3(x0)),ren8(x1,x0)
% 0.11/0.37 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p10(x1),ren8(x2,x0)
% 0.11/0.37 % 39:2:2:INP:TopTop: p9(skf3(x0)) -> ren8(x1,x0)
% 0.11/0.37 % 40:2:2:INP:TopTop: p10(x0) -> ren8(x1,x0)
% 0.11/0.37 % 41:2:2:INP:TopTop: -> p9(x0),ren8(x1,x0)
% 0.11/0.37 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren8(x2,x0)
% 0.11/0.37 % 43:2:2:INP:TopTop: -> p9(x0),ren8(x1,x0)
% 0.11/0.37 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.11/0.37 % 45:2:2:INP:TopTop: -> p10(x0),ren9(x1,x0)
% 0.11/0.37 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren9(x2,x0)
% 0.11/0.37 % 47:2:2:INP:TopTop: p9(x0) -> ren9(x1,x0)
% 0.11/0.37 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.11/0.37 % 49:2:2:INP:TopTop: p10(skf4(x0)) -> ren9(x1,x0)
% 0.11/0.37 % 50:2:2:INP:TopTop: -> p9(skf4(x0)),ren9(x1,x0)
% 0.11/0.37 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p9(x1),ren9(x2,x0)
% 0.11/0.37 % 52:2:2:INP:TopTop: -> p9(skf4(x0)),ren9(x1,x0)
% 0.11/0.37 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.11/0.37 % 54:2:2:INP:TopTop: -> p10(x0),ren10(x1,x0)
% 0.11/0.37 % 55:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren10(x2,x0)
% 0.11/0.37 % 56:2:2:INP:TopTop: p9(x0) -> ren10(x1,x0)
% 0.11/0.37 % 57:2:2:INP:TopTop: p10(x0) -> ren10(x1,x0)
% 0.11/0.37 % 58:2:2:INP:TopTop: -> p9(x0),ren10(x1,x0)
% 0.11/0.37 % 59:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren10(x2,x0)
% 0.11/0.37 % 60:2:2:INP:TopTop: -> p9(x0),ren10(x1,x0)
% 0.11/0.37 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.11/0.37 % 62:2:2:INP:TopTop: p9(x0) -> ren11(x1,x0)
% 0.11/0.37 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.11/0.37 % 64:2:2:INP:TopTop: p8(x0) -> ren12(x1,x0)
% 0.11/0.37 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.11/0.37 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.11/0.37 % 67:2:2:INP:TopTop: -> p9(skf5(x0)),ren13(x1,x0)
% 0.11/0.37 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p9(x1),ren13(x2,x0)
% 0.11/0.37 % 69:2:2:INP:TopTop: p8(skf5(x0)) -> ren13(x1,x0)
% 0.11/0.37 % 70:2:2:INP:TopTop: p9(x0) -> ren13(x1,x0)
% 0.11/0.37 % 71:2:2:INP:TopTop: -> p8(x0),ren13(x1,x0)
% 0.11/0.37 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren13(x2,x0)
% 0.11/0.37 % 73:2:2:INP:TopTop: -> p8(x0),ren13(x1,x0)
% 0.11/0.37 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.11/0.37 % 75:2:2:INP:TopTop: -> p9(x0),ren14(x1,x0)
% 0.11/0.37 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren14(x2,x0)
% 0.11/0.37 % 77:2:2:INP:TopTop: p8(x0) -> ren14(x1,x0)
% 0.11/0.37 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.11/0.37 % 79:2:2:INP:TopTop: p9(skf6(x0)) -> ren14(x1,x0)
% 0.11/0.37 % 80:2:2:INP:TopTop: -> p8(skf6(x0)),ren14(x1,x0)
% 0.11/0.37 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p8(x1),ren14(x2,x0)
% 0.11/0.37 % 82:2:2:INP:TopTop: -> p8(skf6(x0)),ren14(x1,x0)
% 0.11/0.37 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.11/0.37 % 84:2:2:INP:TopTop: -> p9(x0),ren15(x1,x0)
% 0.11/0.37 % 85:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren15(x2,x0)
% 0.11/0.37 % 86:2:2:INP:TopTop: p8(x0) -> ren15(x1,x0)
% 0.11/0.37 % 87:2:2:INP:TopTop: p9(x0) -> ren15(x1,x0)
% 0.11/0.37 % 88:2:2:INP:TopTop: -> p8(x0),ren15(x1,x0)
% 0.11/0.37 % 89:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren15(x2,x0)
% 0.11/0.37 % 90:2:2:INP:TopTop: -> p8(x0),ren15(x1,x0)
% 0.11/0.37 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.11/0.37 % 92:2:2:INP:TopTop: p8(x0) -> ren16(x1,x0)
% 0.11/0.37 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.11/0.37 % 94:2:2:INP:TopTop: p7(x0) -> ren17(x1,x0)
% 0.11/0.37 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.11/0.37 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.11/0.37 % 97:2:2:INP:TopTop: -> p8(skf7(x0)),ren18(x1,x0)
% 0.11/0.37 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p8(x1),ren18(x2,x0)
% 0.11/0.37 % 99:2:2:INP:TopTop: p7(skf7(x0)) -> ren18(x1,x0)
% 0.11/0.37 % 100:2:2:INP:TopTop: p8(x0) -> ren18(x1,x0)
% 0.11/0.37 % 101:2:2:INP:TopTop: -> p7(x0),ren18(x1,x0)
% 0.11/0.37 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren18(x2,x0)
% 0.11/0.37 % 103:2:2:INP:TopTop: -> p7(x0),ren18(x1,x0)
% 0.11/0.37 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.11/0.37 % 105:2:2:INP:TopTop: -> p8(x0),ren19(x1,x0)
% 0.11/0.37 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren19(x2,x0)
% 0.11/0.37 % 107:2:2:INP:TopTop: p7(x0) -> ren19(x1,x0)
% 0.11/0.37 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.11/0.37 % 109:2:2:INP:TopTop: p8(skf8(x0)) -> ren19(x1,x0)
% 0.11/0.37 % 110:2:2:INP:TopTop: -> p7(skf8(x0)),ren19(x1,x0)
% 0.11/0.37 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p7(x1),ren19(x2,x0)
% 0.11/0.37 % 112:2:2:INP:TopTop: -> p7(skf8(x0)),ren19(x1,x0)
% 0.11/0.37 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.11/0.37 % 114:2:2:INP:TopTop: -> p8(x0),ren20(x1,x0)
% 0.11/0.37 % 115:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren20(x2,x0)
% 0.11/0.37 % 116:2:2:INP:TopTop: p7(x0) -> ren20(x1,x0)
% 0.11/0.37 % 117:2:2:INP:TopTop: p8(x0) -> ren20(x1,x0)
% 0.11/0.37 % 118:2:2:INP:TopTop: -> p7(x0),ren20(x1,x0)
% 0.11/0.37 % 119:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren20(x2,x0)
% 0.11/0.37 % 120:2:2:INP:TopTop: -> p7(x0),ren20(x1,x0)
% 0.11/0.37 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.11/0.37 % 122:2:2:INP:TopTop: p7(x0) -> ren21(x1,x0)
% 0.11/0.37 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.11/0.37 % 124:2:2:INP:TopTop: p6(x0) -> ren22(x1,x0)
% 0.11/0.37 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.11/0.37 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.11/0.37 % 127:2:2:INP:TopTop: -> p7(skf9(x0)),ren23(x1,x0)
% 0.11/0.37 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p7(x1),ren23(x2,x0)
% 0.11/0.37 % 129:2:2:INP:TopTop: p6(skf9(x0)) -> ren23(x1,x0)
% 0.11/0.37 % 130:2:2:INP:TopTop: p7(x0) -> ren23(x1,x0)
% 0.11/0.37 % 131:2:2:INP:TopTop: -> p6(x0),ren23(x1,x0)
% 0.11/0.37 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren23(x2,x0)
% 0.11/0.37 % 133:2:2:INP:TopTop: -> p6(x0),ren23(x1,x0)
% 0.11/0.37 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.11/0.37 % 135:2:2:INP:TopTop: -> p7(x0),ren24(x1,x0)
% 0.11/0.37 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren24(x2,x0)
% 0.11/0.37 % 137:2:2:INP:TopTop: p6(x0) -> ren24(x1,x0)
% 0.11/0.37 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.11/0.37 % 139:2:2:INP:TopTop: p7(skf10(x0)) -> ren24(x1,x0)
% 0.11/0.37 % 140:2:2:INP:TopTop: -> p6(skf10(x0)),ren24(x1,x0)
% 0.11/0.37 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p6(x1),ren24(x2,x0)
% 0.11/0.37 % 142:2:2:INP:TopTop: -> p6(skf10(x0)),ren24(x1,x0)
% 0.11/0.37 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.11/0.37 % 144:2:2:INP:TopTop: -> p7(x0),ren25(x1,x0)
% 0.11/0.37 % 145:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren25(x2,x0)
% 0.11/0.37 % 146:2:2:INP:TopTop: p6(x0) -> ren25(x1,x0)
% 0.11/0.37 % 147:2:2:INP:TopTop: p7(x0) -> ren25(x1,x0)
% 0.11/0.37 % 148:2:2:INP:TopTop: -> p6(x0),ren25(x1,x0)
% 0.11/0.37 % 149:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren25(x2,x0)
% 0.11/0.37 % 150:2:2:INP:TopTop: -> p6(x0),ren25(x1,x0)
% 0.11/0.37 % 151:2:2:INP:TopTop: -> r1(x0,x1),ren26(x0,x1)
% 0.11/0.37 % 152:2:2:INP:TopTop: p6(x0) -> ren26(x1,x0)
% 0.11/0.37 % 153:2:2:INP:TopTop: -> r1(x0,x1),ren27(x0,x1)
% 0.11/0.37 % 154:2:2:INP:TopTop: p5(x0) -> ren27(x1,x0)
% 0.11/0.37 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren28(x0,x1)
% 0.11/0.37 % 156:2:2:INP:TopTop: -> r1(x0,skf11(x0)),ren28(x1,x0)
% 0.11/0.37 % 157:2:2:INP:TopTop: -> p6(skf11(x0)),ren28(x1,x0)
% 0.11/0.37 % 158:3:3:INP:TopTopTop: r1(skf11(x0),x1) -> p6(x1),ren28(x2,x0)
% 0.11/0.37 % 159:2:2:INP:TopTop: p5(skf11(x0)) -> ren28(x1,x0)
% 0.11/0.37 % 160:2:2:INP:TopTop: p6(x0) -> ren28(x1,x0)
% 0.11/0.37 % 161:2:2:INP:TopTop: -> p5(x0),ren28(x1,x0)
% 0.11/0.37 % 162:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren28(x2,x0)
% 0.11/0.37 % 163:2:2:INP:TopTop: -> p5(x0),ren28(x1,x0)
% 0.11/0.37 % 164:2:2:INP:TopTop: -> r1(x0,x1),ren29(x0,x1)
% 0.11/0.37 % 165:2:2:INP:TopTop: -> p6(x0),ren29(x1,x0)
% 0.11/0.37 % 166:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren29(x2,x0)
% 0.11/0.37 % 167:2:2:INP:TopTop: p5(x0) -> ren29(x1,x0)
% 0.11/0.37 % 168:2:2:INP:TopTop: -> r1(x0,skf12(x0)),ren29(x1,x0)
% 0.11/0.37 % 169:2:2:INP:TopTop: p6(skf12(x0)) -> ren29(x1,x0)
% 0.11/0.37 % 170:2:2:INP:TopTop: -> p5(skf12(x0)),ren29(x1,x0)
% 0.11/0.37 % 171:3:3:INP:TopTopTop: r1(skf12(x0),x1) -> p5(x1),ren29(x2,x0)
% 0.11/0.37 % 172:2:2:INP:TopTop: -> p5(skf12(x0)),ren29(x1,x0)
% 0.11/0.37 % 173:2:2:INP:TopTop: -> r1(x0,x1),ren30(x0,x1)
% 0.11/0.37 % 174:2:2:INP:TopTop: -> p6(x0),ren30(x1,x0)
% 0.11/0.37 % 175:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren30(x2,x0)
% 0.11/0.37 % 176:2:2:INP:TopTop: p5(x0) -> ren30(x1,x0)
% 0.11/0.37 % 177:2:2:INP:TopTop: p6(x0) -> ren30(x1,x0)
% 0.11/0.37 % 178:2:2:INP:TopTop: -> p5(x0),ren30(x1,x0)
% 0.11/0.37 % 179:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren30(x2,x0)
% 0.11/0.37 % 180:2:2:INP:TopTop: -> p5(x0),ren30(x1,x0)
% 0.11/0.37 % 181:2:2:INP:TopTop: -> r1(x0,x1),ren31(x0,x1)
% 0.11/0.37 % 182:2:2:INP:TopTop: p5(x0) -> ren31(x1,x0)
% 0.11/0.37 % 183:2:2:INP:TopTop: -> r1(x0,x1),ren32(x0,x1)
% 0.11/0.37 % 184:2:2:INP:TopTop: p4(x0) -> ren32(x1,x0)
% 0.11/0.37 % 185:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1)
% 0.11/0.37 % 186:2:2:INP:TopTop: -> r1(x0,skf13(x0)),ren33(x1,x0)
% 0.11/0.37 % 187:2:2:INP:TopTop: -> p5(skf13(x0)),ren33(x1,x0)
% 0.11/0.37 % 188:3:3:INP:TopTopTop: r1(skf13(x0),x1) -> p5(x1),ren33(x2,x0)
% 0.11/0.37 % 189:2:2:INP:TopTop: p4(skf13(x0)) -> ren33(x1,x0)
% 0.11/0.37 % 190:2:2:INP:TopTop: p5(x0) -> ren33(x1,x0)
% 0.11/0.37 % 191:2:2:INP:TopTop: -> p4(x0),ren33(x1,x0)
% 0.11/0.37 % 192:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren33(x2,x0)
% 0.11/0.37 % 193:2:2:INP:TopTop: -> p4(x0),ren33(x1,x0)
% 0.11/0.37 % 194:2:2:INP:TopTop: -> r1(x0,x1),ren34(x0,x1)
% 0.11/0.37 % 195:2:2:INP:TopTop: -> p5(x0),ren34(x1,x0)
% 0.11/0.37 % 196:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren34(x2,x0)
% 0.11/0.37 % 197:2:2:INP:TopTop: p4(x0) -> ren34(x1,x0)
% 0.11/0.37 % 198:2:2:INP:TopTop: -> r1(x0,skf14(x0)),ren34(x1,x0)
% 0.11/0.37 % 199:2:2:INP:TopTop: p5(skf14(x0)) -> ren34(x1,x0)
% 0.11/0.37 % 200:2:2:INP:TopTop: -> p4(skf14(x0)),ren34(x1,x0)
% 0.11/0.37 % 201:3:3:INP:TopTopTop: r1(skf14(x0),x1) -> p4(x1),ren34(x2,x0)
% 0.11/0.37 % 202:2:2:INP:TopTop: -> p4(skf14(x0)),ren34(x1,x0)
% 0.11/0.37 % 203:2:2:INP:TopTop: -> r1(x0,x1),ren35(x0,x1)
% 0.11/0.37 % 204:2:2:INP:TopTop: -> p5(x0),ren35(x1,x0)
% 0.11/0.37 % 205:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren35(x2,x0)
% 0.11/0.37 % 206:2:2:INP:TopTop: p4(x0) -> ren35(x1,x0)
% 0.11/0.37 % 207:2:2:INP:TopTop: p5(x0) -> ren35(x1,x0)
% 0.11/0.37 % 208:2:2:INP:TopTop: -> p4(x0),ren35(x1,x0)
% 0.11/0.37 % 209:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren35(x2,x0)
% 0.11/0.37 % 210:2:2:INP:TopTop: -> p4(x0),ren35(x1,x0)
% 0.11/0.37 % 211:2:2:INP:TopTop: -> r1(x0,x1),ren36(x0,x1)
% 0.11/0.37 % 212:2:2:INP:TopTop: p4(x0) -> ren36(x1,x0)
% 0.11/0.37 % 213:2:2:INP:TopTop: -> r1(x0,x1),ren37(x0,x1)
% 0.11/0.37 % 214:2:2:INP:TopTop: p3(x0) -> ren37(x1,x0)
% 0.11/0.37 % 215:2:2:INP:TopTop: -> r1(x0,x1),ren38(x0,x1)
% 0.11/0.37 % 216:2:2:INP:TopTop: -> r1(x0,skf15(x0)),ren38(x1,x0)
% 0.11/0.37 % 217:2:2:INP:TopTop: -> p4(skf15(x0)),ren38(x1,x0)
% 0.11/0.37 % 218:3:3:INP:TopTopTop: r1(skf15(x0),x1) -> p4(x1),ren38(x2,x0)
% 0.11/0.37 % 219:2:2:INP:TopTop: p3(skf15(x0)) -> ren38(x1,x0)
% 0.11/0.37 % 220:2:2:INP:TopTop: p4(x0) -> ren38(x1,x0)
% 0.11/0.37 % 221:2:2:INP:TopTop: -> p3(x0),ren38(x1,x0)
% 0.11/0.37 % 222:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren38(x2,x0)
% 0.11/0.37 % 223:2:2:INP:TopTop: -> p3(x0),ren38(x1,x0)
% 0.11/0.37 % 224:2:2:INP:TopTop: -> r1(x0,x1),ren39(x0,x1)
% 0.11/0.37 % 225:2:2:INP:TopTop: -> p4(x0),ren39(x1,x0)
% 0.11/0.37 % 226:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren39(x2,x0)
% 0.11/0.37 % 227:2:2:INP:TopTop: p3(x0) -> ren39(x1,x0)
% 0.11/0.37 % 228:2:2:INP:TopTop: -> r1(x0,skf16(x0)),ren39(x1,x0)
% 0.11/0.37 % 229:2:2:INP:TopTop: p4(skf16(x0)) -> ren39(x1,x0)
% 0.11/0.37 % 230:2:2:INP:TopTop: -> p3(skf16(x0)),ren39(x1,x0)
% 0.11/0.37 % 231:3:3:INP:TopTopTop: r1(skf16(x0),x1) -> p3(x1),ren39(x2,x0)
% 0.11/0.37 % 232:2:2:INP:TopTop: -> p3(skf16(x0)),ren39(x1,x0)
% 0.11/0.37 % 233:2:2:INP:TopTop: -> r1(x0,x1),ren40(x0,x1)
% 0.11/0.37 % 234:2:2:INP:TopTop: -> p4(x0),ren40(x1,x0)
% 0.11/0.37 % 235:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren40(x2,x0)
% 0.11/0.37 % 236:2:2:INP:TopTop: p3(x0) -> ren40(x1,x0)
% 0.11/0.37 % 237:2:2:INP:TopTop: p4(x0) -> ren40(x1,x0)
% 0.11/0.37 % 238:2:2:INP:TopTop: -> p3(x0),ren40(x1,x0)
% 0.11/0.37 % 239:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren40(x2,x0)
% 0.11/0.37 % 240:2:2:INP:TopTop: -> p3(x0),ren40(x1,x0)
% 0.11/0.37 % 241:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1)
% 0.11/0.37 % 242:2:2:INP:TopTop: p3(x0) -> ren41(x1,x0)
% 0.11/0.37 % 243:2:2:INP:TopTop: -> r1(x0,x1),ren42(x0,x1)
% 0.11/0.37 % 244:2:2:INP:TopTop: p2(x0) -> ren42(x1,x0)
% 0.11/0.37 % 245:2:2:INP:TopTop: -> r1(x0,x1),ren43(x0,x1)
% 0.11/0.37 % 246:2:2:INP:TopTop: -> r1(x0,skf17(x0)),ren43(x1,x0)
% 0.11/0.37 % 247:2:2:INP:TopTop: -> p3(skf17(x0)),ren43(x1,x0)
% 0.11/0.37 % 248:3:3:INP:TopTopTop: r1(skf17(x0),x1) -> p3(x1),ren43(x2,x0)
% 0.11/0.37 % 249:2:2:INP:TopTop: p2(skf17(x0)) -> ren43(x1,x0)
% 0.11/0.37 % 250:2:2:INP:TopTop: p3(x0) -> ren43(x1,x0)
% 0.11/0.37 % 251:2:2:INP:TopTop: -> p2(x0),ren43(x1,x0)
% 0.11/0.37 % 252:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren43(x2,x0)
% 0.11/0.37 % 253:2:2:INP:TopTop: -> p2(x0),ren43(x1,x0)
% 0.11/0.37 % 254:2:2:INP:TopTop: -> r1(x0,x1),ren44(x0,x1)
% 0.11/0.37 % 255:2:2:INP:TopTop: -> p3(x0),ren44(x1,x0)
% 0.11/0.37 % 256:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren44(x2,x0)
% 0.11/0.37 % 257:2:2:INP:TopTop: p2(x0) -> ren44(x1,x0)
% 0.11/0.37 % 258:2:2:INP:TopTop: -> r1(x0,skf18(x0)),ren44(x1,x0)
% 0.11/0.37 % 259:2:2:INP:TopTop: p3(skf18(x0)) -> ren44(x1,x0)
% 0.11/0.37 % 260:2:2:INP:TopTop: -> p2(skf18(x0)),ren44(x1,x0)
% 0.11/0.37 % 261:3:3:INP:TopTopTop: r1(skf18(x0),x1) -> p2(x1),ren44(x2,x0)
% 0.11/0.37 % 262:2:2:INP:TopTop: -> p2(skf18(x0)),ren44(x1,x0)
% 0.11/0.37 % 263:2:2:INP:TopTop: -> r1(x0,x1),ren45(x0,x1)
% 0.11/0.37 % 264:2:2:INP:TopTop: -> p3(x0),ren45(x1,x0)
% 0.11/0.37 % 265:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren45(x2,x0)
% 0.11/0.37 % 266:2:2:INP:TopTop: p2(x0) -> ren45(x1,x0)
% 0.11/0.37 % 267:2:2:INP:TopTop: p3(x0) -> ren45(x1,x0)
% 0.11/0.37 % 268:2:2:INP:TopTop: -> p2(x0),ren45(x1,x0)
% 0.11/0.37 % 269:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren45(x2,x0)
% 0.11/0.37 % 270:2:2:INP:TopTop: -> p2(x0),ren45(x1,x0)
% 0.11/0.37 % 271:2:2:INP:TopTop: -> r1(x0,x1),ren46(x0,x1)
% 0.11/0.37 % 272:2:2:INP:TopTop: p2(x0) -> ren46(x1,x0)
% 0.11/0.37 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren47(x0,x1)
% 0.11/0.37 % 274:2:2:INP:TopTop: p1(x0) -> ren47(x1,x0)
% 0.11/0.37 % 275:2:2:INP:TopTop: -> r1(x0,x1),ren48(x0,x1)
% 0.11/0.37 % 276:2:2:INP:TopTop: -> r1(x0,skf19(x0)),ren48(x1,x0)
% 0.11/0.37 % 277:2:2:INP:TopTop: -> p2(skf19(x0)),ren48(x1,x0)
% 0.11/0.37 % 278:3:3:INP:TopTopTop: r1(skf19(x0),x1) -> p2(x1),ren48(x2,x0)
% 0.11/0.37 % 279:2:2:INP:TopTop: p1(skf19(x0)) -> ren48(x1,x0)
% 0.11/0.37 % 280:2:2:INP:TopTop: p2(x0) -> ren48(x1,x0)
% 0.11/0.37 % 281:2:2:INP:TopTop: -> p1(x0),ren48(x1,x0)
% 0.11/0.37 % 282:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren48(x2,x0)
% 0.11/0.37 % 283:2:2:INP:TopTop: -> p1(x0),ren48(x1,x0)
% 0.11/0.37 % 284:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1)
% 0.11/0.37 % 285:2:2:INP:TopTop: -> p2(x0),ren49(x1,x0)
% 0.11/0.37 % 286:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren49(x2,x0)
% 0.11/0.37 % 287:2:2:INP:TopTop: p1(x0) -> ren49(x1,x0)
% 0.11/0.37 % 288:2:2:INP:TopTop: -> r1(x0,skf20(x0)),ren49(x1,x0)
% 0.11/0.37 % 289:2:2:INP:TopTop: p2(skf20(x0)) -> ren49(x1,x0)
% 0.11/0.37 % 290:2:2:INP:TopTop: -> p1(skf20(x0)),ren49(x1,x0)
% 0.11/0.37 % 291:3:3:INP:TopTopTop: r1(skf20(x0),x1) -> p1(x1),ren49(x2,x0)
% 0.11/0.37 % 292:2:2:INP:TopTop: -> p1(skf20(x0)),ren49(x1,x0)
% 0.11/0.37 % 293:2:2:INP:TopTop: -> r1(x0,x1),ren50(x0,x1)
% 0.11/0.37 % 294:2:2:INP:TopTop: -> p2(x0),ren50(x1,x0)
% 0.11/0.37 % 295:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren50(x2,x0)
% 0.11/0.37 % 296:2:2:INP:TopTop: p1(x0) -> ren50(x1,x0)
% 0.11/0.37 % 297:2:2:INP:TopTop: p2(x0) -> ren50(x1,x0)
% 0.11/0.37 % 298:2:2:INP:TopTop: -> p1(x0),ren50(x1,x0)
% 0.11/0.37 % 299:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren50(x2,x0)
% 0.11/0.37 % 300:2:2:INP:TopTop: -> p1(x0),ren50(x1,x0)
% 0.11/0.37 % 301:12:2:INP:TopTop: r1(skc21,x0),p11(x0),ren1(x0,skf22(x0)),r1(skc21,x1),p10(x1),ren2(x1,skf23(x1)),p10(x1),ren3(skc21,skc24),ren4(skc21,skc25),ren5(skc21,skc26) -> p10(x0),p11(x1)
% 0.11/0.37 % 302:12:2:INP:TopTop: r1(skc21,x0),p10(x0),ren6(x0,skf27(x0)),r1(skc21,x1),p9(x1),ren7(x1,skf28(x1)),p9(x1),ren8(skc21,skc29),ren9(skc21,skc30),ren10(skc21,skc31) -> p9(x0),p10(x1)
% 0.11/0.37 % 303:12:2:INP:TopTop: r1(skc21,x0),p9(x0),ren11(x0,skf32(x0)),r1(skc21,x1),p8(x1),ren12(x1,skf33(x1)),p8(x1),ren13(skc21,skc34),ren14(skc21,skc35),ren15(skc21,skc36) -> p8(x0),p9(x1)
% 0.11/0.37 % 304:12:2:INP:TopTop: r1(skc21,x0),p8(x0),ren16(x0,skf37(x0)),r1(skc21,x1),p7(x1),ren17(x1,skf38(x1)),p7(x1),ren18(skc21,skc39),ren19(skc21,skc40),ren20(skc21,skc41) -> p7(x0),p8(x1)
% 0.11/0.37 % 305:12:2:INP:TopTop: r1(skc21,x0),p7(x0),ren21(x0,skf42(x0)),r1(skc21,x1),p6(x1),ren22(x1,skf43(x1)),p6(x1),ren23(skc21,skc44),ren24(skc21,skc45),ren25(skc21,skc46) -> p6(x0),p7(x1)
% 0.11/0.37 % 306:12:2:INP:TopTop: r1(skc21,x0),p6(x0),ren26(x0,skf47(x0)),r1(skc21,x1),p5(x1),ren27(x1,skf48(x1)),p5(x1),ren28(skc21,skc49),ren29(skc21,skc50),ren30(skc21,skc51) -> p5(x0),p6(x1)
% 0.11/0.37 % 307:12:2:INP:TopTop: r1(skc21,x0),p5(x0),ren31(x0,skf52(x0)),r1(skc21,x1),p4(x1),ren32(x1,skf53(x1)),p4(x1),ren33(skc21,skc54),ren34(skc21,skc55),ren35(skc21,skc56) -> p4(x0),p5(x1)
% 0.11/0.38 % 308:1:0:INP:: -> r1(skc21,skc57)
% 0.11/0.38 % 309:1:0:INP:: p10(skc57) ->
% 0.11/0.38 % 310:2:1:INP:Top: r1(skc57,x0) -> p10(x0)
% 0.11/0.38 % 311:1:0:INP:: -> p10(skc57)
% 0.11/0.38 % 312:1:0:INP:: -> r1(skc21,skc58)
% 0.11/0.38 % 313:1:0:INP:: p10(skc58) ->
% 0.11/0.38 % 314:2:1:INP:Top: r1(skc58,x0) -> p10(x0)
% 0.11/0.38 % 315:1:0:INP:: -> p10(skc58)
% 0.11/0.38 % 316:12:2:INP:TopTop: r1(skc21,x0),p4(x0),ren36(x0,skf59(x0)),r1(skc21,x1),p3(x1),ren37(x1,skf60(x1)),p3(x1),ren38(skc21,skc61),ren39(skc21,skc62),ren40(skc21,skc63) -> p3(x0),p4(x1)
% 0.11/0.38 % 317:12:2:INP:TopTop: r1(skc21,x0),p3(x0),ren41(x0,skf64(x0)),r1(skc21,x1),p2(x1),ren42(x1,skf65(x1)),p2(x1),ren43(skc21,skc66),ren44(skc21,skc67),ren45(skc21,skc68) -> p2(x0),p3(x1)
% 0.11/0.38 % 318:12:2:INP:TopTop: r1(skc21,x0),p2(x0),ren46(x0,skf69(x0)),r1(skc21,x1),p1(x1),ren47(x1,skf70(x1)),p1(x1),ren48(skc21,skc71),ren49(skc21,skc72),ren50(skc21,skc73) -> p1(x0),p2(x1)
% 0.11/0.38
% 0.11/0.38 % Predicates: r1 p11 p10 p9 p8 p7 p6 p5 p4 p3 p2 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50
% 0.11/0.38 % Fol Constants: skc21 skc24 skc25 skc26 skc29 skc30 skc31 skc34 skc35 skc36 skc39 skc40 skc41 skc44 skc45 skc46 skc49 skc50 skc51 skc54 skc55 skc56 skc57 skc58 skc61 skc62 skc63 skc66 skc67 skc68 skc71 skc72 skc73
% 0.11/0.38 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf22 skf23 skf27 skf28 skf32 skf33 skf37 skf38 skf42 skf43 skf47 skf48 skf52 skf53 skf59 skf60 skf64 skf65 skf69 skf70
% 0.11/0.38 % Problem Properties:
% 0.11/0.38 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.11/0.38
% 0.11/0.38
% 0.11/0.38 % Reduced Input Axiom Clauses:
% 0.11/0.38 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.11/0.38 % 2:2:2:INP:TopTop: p11(x0) -> ren1(x1,x0)
% 0.11/0.38 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.11/0.38 % 4:2:2:INP:TopTop: p10(x0) -> ren2(x1,x0)
% 0.11/0.38 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.11/0.38 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.11/0.38 % 7:2:2:INP:TopTop: -> p11(skf1(x0)),ren3(x1,x0)
% 0.11/0.38 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p11(x1),ren3(x2,x0)
% 0.11/0.38 % 9:2:2:INP:TopTop: p10(skf1(x0)) -> ren3(x1,x0)
% 0.11/0.38 % 10:2:2:INP:TopTop: p11(x0) -> ren3(x1,x0)
% 0.11/0.38 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren3(x2,x0)
% 0.11/0.38 % 13:2:2:INP:TopTop: -> p10(x0),ren3(x1,x0)
% 0.11/0.38 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.11/0.38 % 15:2:2:INP:TopTop: -> p11(x0),ren4(x1,x0)
% 0.11/0.38 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren4(x2,x0)
% 0.11/0.38 % 17:2:2:INP:TopTop: p10(x0) -> ren4(x1,x0)
% 0.11/0.38 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.11/0.38 % 19:2:2:INP:TopTop: p11(skf2(x0)) -> ren4(x1,x0)
% 0.11/0.38 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p10(x1),ren4(x2,x0)
% 0.11/0.38 % 22:2:2:INP:TopTop: -> p10(skf2(x0)),ren4(x1,x0)
% 0.11/0.38 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.11/0.38 % 319:1:2:[27.0,24.0]:TopTop: -> ren5(x0,x1)
% 0.11/0.38 % 320:1:2:[28.0,26.0]:TopTop: -> ren5(x0,x1)
% 0.11/0.38 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.11/0.38 % 32:2:2:INP:TopTop: p10(x0) -> ren6(x1,x0)
% 0.11/0.38 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.11/0.38 % 34:2:2:INP:TopTop: p9(x0) -> ren7(x1,x0)
% 0.11/0.38 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.11/0.38 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.11/0.38 % 37:2:2:INP:TopTop: -> p10(skf3(x0)),ren8(x1,x0)
% 0.11/0.38 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p10(x1),ren8(x2,x0)
% 0.11/0.38 % 39:2:2:INP:TopTop: p9(skf3(x0)) -> ren8(x1,x0)
% 0.11/0.38 % 40:2:2:INP:TopTop: p10(x0) -> ren8(x1,x0)
% 0.11/0.38 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren8(x2,x0)
% 0.11/0.38 % 43:2:2:INP:TopTop: -> p9(x0),ren8(x1,x0)
% 0.11/0.38 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.11/0.38 % 45:2:2:INP:TopTop: -> p10(x0),ren9(x1,x0)
% 0.11/0.38 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren9(x2,x0)
% 0.11/0.38 % 47:2:2:INP:TopTop: p9(x0) -> ren9(x1,x0)
% 0.11/0.38 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.11/0.38 % 49:2:2:INP:TopTop: p10(skf4(x0)) -> ren9(x1,x0)
% 0.11/0.38 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p9(x1),ren9(x2,x0)
% 0.11/0.38 % 52:2:2:INP:TopTop: -> p9(skf4(x0)),ren9(x1,x0)
% 0.11/0.38 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.11/0.38 % 321:1:2:[57.0,54.0]:TopTop: -> ren10(x0,x1)
% 0.11/0.38 % 322:1:2:[58.0,56.0]:TopTop: -> ren10(x0,x1)
% 0.11/0.38 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.11/0.38 % 62:2:2:INP:TopTop: p9(x0) -> ren11(x1,x0)
% 0.11/0.38 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.11/0.38 % 64:2:2:INP:TopTop: p8(x0) -> ren12(x1,x0)
% 0.11/0.38 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.11/0.38 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.11/0.38 % 67:2:2:INP:TopTop: -> p9(skf5(x0)),ren13(x1,x0)
% 0.11/0.38 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p9(x1),ren13(x2,x0)
% 0.11/0.38 % 69:2:2:INP:TopTop: p8(skf5(x0)) -> ren13(x1,x0)
% 0.11/0.38 % 70:2:2:INP:TopTop: p9(x0) -> ren13(x1,x0)
% 0.11/0.38 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren13(x2,x0)
% 0.11/0.38 % 73:2:2:INP:TopTop: -> p8(x0),ren13(x1,x0)
% 0.11/0.38 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.11/0.38 % 75:2:2:INP:TopTop: -> p9(x0),ren14(x1,x0)
% 0.11/0.38 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren14(x2,x0)
% 0.11/0.38 % 77:2:2:INP:TopTop: p8(x0) -> ren14(x1,x0)
% 0.11/0.38 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.11/0.38 % 79:2:2:INP:TopTop: p9(skf6(x0)) -> ren14(x1,x0)
% 0.11/0.38 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p8(x1),ren14(x2,x0)
% 0.11/0.38 % 82:2:2:INP:TopTop: -> p8(skf6(x0)),ren14(x1,x0)
% 0.11/0.38 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.11/0.38 % 323:1:2:[87.0,84.0]:TopTop: -> ren15(x0,x1)
% 0.11/0.38 % 324:1:2:[88.0,86.0]:TopTop: -> ren15(x0,x1)
% 0.11/0.38 % 338:1:2:[298.0,296.0]:TopTop: -> ren50(x0,x1)
% 0.11/0.38 % 337:1:2:[297.0,294.0]:TopTop: -> ren50(x0,x1)
% 0.11/0.38 % 293:2:2:INP:TopTop: -> r1(x0,x1),ren50(x0,x1)
% 0.11/0.38 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.11/0.38 % 92:2:2:INP:TopTop: p8(x0) -> ren16(x1,x0)
% 0.11/0.38 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.11/0.38 % 94:2:2:INP:TopTop: p7(x0) -> ren17(x1,x0)
% 0.11/0.38 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.11/0.38 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.11/0.38 % 97:2:2:INP:TopTop: -> p8(skf7(x0)),ren18(x1,x0)
% 0.11/0.38 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p8(x1),ren18(x2,x0)
% 0.11/0.38 % 99:2:2:INP:TopTop: p7(skf7(x0)) -> ren18(x1,x0)
% 0.11/0.38 % 100:2:2:INP:TopTop: p8(x0) -> ren18(x1,x0)
% 0.11/0.38 % 292:2:2:INP:TopTop: -> p1(skf20(x0)),ren49(x1,x0)
% 0.11/0.38 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren18(x2,x0)
% 0.11/0.38 % 103:2:2:INP:TopTop: -> p7(x0),ren18(x1,x0)
% 0.11/0.38 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.11/0.38 % 105:2:2:INP:TopTop: -> p8(x0),ren19(x1,x0)
% 0.11/0.38 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren19(x2,x0)
% 0.11/0.38 % 107:2:2:INP:TopTop: p7(x0) -> ren19(x1,x0)
% 0.11/0.38 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.11/0.38 % 109:2:2:INP:TopTop: p8(skf8(x0)) -> ren19(x1,x0)
% 0.11/0.38 % 291:3:3:INP:TopTopTop: r1(skf20(x0),x1) -> p1(x1),ren49(x2,x0)
% 0.11/0.38 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p7(x1),ren19(x2,x0)
% 0.11/0.38 % 112:2:2:INP:TopTop: -> p7(skf8(x0)),ren19(x1,x0)
% 0.11/0.38 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.11/0.38 % 325:1:2:[117.0,114.0]:TopTop: -> ren20(x0,x1)
% 0.11/0.38 % 289:2:2:INP:TopTop: p2(skf20(x0)) -> ren49(x1,x0)
% 0.11/0.38 % 326:1:2:[120.0,116.0]:TopTop: -> ren20(x0,x1)
% 0.11/0.38 % 288:2:2:INP:TopTop: -> r1(x0,skf20(x0)),ren49(x1,x0)
% 0.11/0.38 % 287:2:2:INP:TopTop: p1(x0) -> ren49(x1,x0)
% 0.11/0.38 % 286:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren49(x2,x0)
% 0.11/0.38 % 285:2:2:INP:TopTop: -> p2(x0),ren49(x1,x0)
% 0.11/0.38 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.11/0.38 % 122:2:2:INP:TopTop: p7(x0) -> ren21(x1,x0)
% 0.11/0.38 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.11/0.38 % 124:2:2:INP:TopTop: p6(x0) -> ren22(x1,x0)
% 0.11/0.38 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.11/0.38 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.11/0.38 % 127:2:2:INP:TopTop: -> p7(skf9(x0)),ren23(x1,x0)
% 0.11/0.38 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p7(x1),ren23(x2,x0)
% 0.11/0.38 % 129:2:2:INP:TopTop: p6(skf9(x0)) -> ren23(x1,x0)
% 0.11/0.38 % 130:2:2:INP:TopTop: p7(x0) -> ren23(x1,x0)
% 0.11/0.38 % 284:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1)
% 0.11/0.38 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren23(x2,x0)
% 0.11/0.38 % 133:2:2:INP:TopTop: -> p6(x0),ren23(x1,x0)
% 0.11/0.38 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.11/0.38 % 135:2:2:INP:TopTop: -> p7(x0),ren24(x1,x0)
% 0.11/0.38 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren24(x2,x0)
% 0.11/0.38 % 137:2:2:INP:TopTop: p6(x0) -> ren24(x1,x0)
% 0.11/0.38 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.11/0.38 % 139:2:2:INP:TopTop: p7(skf10(x0)) -> ren24(x1,x0)
% 0.11/0.38 % 283:2:2:INP:TopTop: -> p1(x0),ren48(x1,x0)
% 0.11/0.38 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p6(x1),ren24(x2,x0)
% 0.11/0.38 % 142:2:2:INP:TopTop: -> p6(skf10(x0)),ren24(x1,x0)
% 0.11/0.38 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.11/0.38 % 327:1:2:[147.0,144.0]:TopTop: -> ren25(x0,x1)
% 0.11/0.38 % 282:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren48(x2,x0)
% 0.11/0.38 % 328:1:2:[150.0,146.0]:TopTop: -> ren25(x0,x1)
% 0.11/0.38 % 280:2:2:INP:TopTop: p2(x0) -> ren48(x1,x0)
% 0.11/0.38 % 279:2:2:INP:TopTop: p1(skf19(x0)) -> ren48(x1,x0)
% 0.11/0.38 % 278:3:3:INP:TopTopTop: r1(skf19(x0),x1) -> p2(x1),ren48(x2,x0)
% 0.11/0.38 % 277:2:2:INP:TopTop: -> p2(skf19(x0)),ren48(x1,x0)
% 0.11/0.38 % 151:2:2:INP:TopTop: -> r1(x0,x1),ren26(x0,x1)
% 0.11/0.38 % 152:2:2:INP:TopTop: p6(x0) -> ren26(x1,x0)
% 0.11/0.38 % 153:2:2:INP:TopTop: -> r1(x0,x1),ren27(x0,x1)
% 0.11/0.38 % 154:2:2:INP:TopTop: p5(x0) -> ren27(x1,x0)
% 0.11/0.38 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren28(x0,x1)
% 0.11/0.38 % 156:2:2:INP:TopTop: -> r1(x0,skf11(x0)),ren28(x1,x0)
% 0.11/0.38 % 157:2:2:INP:TopTop: -> p6(skf11(x0)),ren28(x1,x0)
% 0.11/0.38 % 158:3:3:INP:TopTopTop: r1(skf11(x0),x1) -> p6(x1),ren28(x2,x0)
% 0.11/0.38 % 159:2:2:INP:TopTop: p5(skf11(x0)) -> ren28(x1,x0)
% 0.11/0.38 % 160:2:2:INP:TopTop: p6(x0) -> ren28(x1,x0)
% 0.11/0.38 % 276:2:2:INP:TopTop: -> r1(x0,skf19(x0)),ren48(x1,x0)
% 0.11/0.38 % 162:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren28(x2,x0)
% 0.11/0.38 % 163:2:2:INP:TopTop: -> p5(x0),ren28(x1,x0)
% 0.11/0.38 % 164:2:2:INP:TopTop: -> r1(x0,x1),ren29(x0,x1)
% 0.11/0.38 % 165:2:2:INP:TopTop: -> p6(x0),ren29(x1,x0)
% 0.11/0.38 % 166:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren29(x2,x0)
% 0.11/0.38 % 167:2:2:INP:TopTop: p5(x0) -> ren29(x1,x0)
% 0.11/0.38 % 168:2:2:INP:TopTop: -> r1(x0,skf12(x0)),ren29(x1,x0)
% 0.11/0.38 % 169:2:2:INP:TopTop: p6(skf12(x0)) -> ren29(x1,x0)
% 0.11/0.38 % 275:2:2:INP:TopTop: -> r1(x0,x1),ren48(x0,x1)
% 0.11/0.38 % 171:3:3:INP:TopTopTop: r1(skf12(x0),x1) -> p5(x1),ren29(x2,x0)
% 0.11/0.38 % 172:2:2:INP:TopTop: -> p5(skf12(x0)),ren29(x1,x0)
% 0.11/0.38 % 173:2:2:INP:TopTop: -> r1(x0,x1),ren30(x0,x1)
% 0.11/0.38 % 329:1:2:[177.0,174.0]:TopTop: -> ren30(x0,x1)
% 0.11/0.38 % 274:2:2:INP:TopTop: p1(x0) -> ren47(x1,x0)
% 0.11/0.38 % 330:1:2:[180.0,176.0]:TopTop: -> ren30(x0,x1)
% 0.11/0.38 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren47(x0,x1)
% 0.11/0.38 % 272:2:2:INP:TopTop: p2(x0) -> ren46(x1,x0)
% 0.11/0.38 % 271:2:2:INP:TopTop: -> r1(x0,x1),ren46(x0,x1)
% 0.11/0.38 % 336:1:2:[268.0,266.0]:TopTop: -> ren45(x0,x1)
% 0.11/0.38 % 181:2:2:INP:TopTop: -> r1(x0,x1),ren31(x0,x1)
% 0.11/0.38 % 182:2:2:INP:TopTop: p5(x0) -> ren31(x1,x0)
% 0.11/0.38 % 183:2:2:INP:TopTop: -> r1(x0,x1),ren32(x0,x1)
% 0.11/0.38 % 184:2:2:INP:TopTop: p4(x0) -> ren32(x1,x0)
% 0.11/0.38 % 185:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1)
% 0.11/0.38 % 186:2:2:INP:TopTop: -> r1(x0,skf13(x0)),ren33(x1,x0)
% 0.11/0.38 % 187:2:2:INP:TopTop: -> p5(skf13(x0)),ren33(x1,x0)
% 0.11/0.38 % 188:3:3:INP:TopTopTop: r1(skf13(x0),x1) -> p5(x1),ren33(x2,x0)
% 0.11/0.38 % 189:2:2:INP:TopTop: p4(skf13(x0)) -> ren33(x1,x0)
% 0.11/0.38 % 190:2:2:INP:TopTop: p5(x0) -> ren33(x1,x0)
% 0.11/0.38 % 335:1:2:[267.0,264.0]:TopTop: -> ren45(x0,x1)
% 0.11/0.38 % 192:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren33(x2,x0)
% 0.11/0.38 % 193:2:2:INP:TopTop: -> p4(x0),ren33(x1,x0)
% 0.11/0.38 % 194:2:2:INP:TopTop: -> r1(x0,x1),ren34(x0,x1)
% 0.11/0.38 % 195:2:2:INP:TopTop: -> p5(x0),ren34(x1,x0)
% 0.11/0.38 % 196:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren34(x2,x0)
% 0.11/0.38 % 197:2:2:INP:TopTop: p4(x0) -> ren34(x1,x0)
% 0.11/0.38 % 198:2:2:INP:TopTop: -> r1(x0,skf14(x0)),ren34(x1,x0)
% 0.11/0.38 % 199:2:2:INP:TopTop: p5(skf14(x0)) -> ren34(x1,x0)
% 0.11/0.38 % 263:2:2:INP:TopTop: -> r1(x0,x1),ren45(x0,x1)
% 0.11/0.38 % 201:3:3:INP:TopTopTop: r1(skf14(x0),x1) -> p4(x1),ren34(x2,x0)
% 0.11/0.38 % 202:2:2:INP:TopTop: -> p4(skf14(x0)),ren34(x1,x0)
% 0.11/0.38 % 203:2:2:INP:TopTop: -> r1(x0,x1),ren35(x0,x1)
% 0.11/0.38 % 331:1:2:[207.0,204.0]:TopTop: -> ren35(x0,x1)
% 0.11/0.38 % 262:2:2:INP:TopTop: -> p2(skf18(x0)),ren44(x1,x0)
% 0.11/0.38 % 332:1:2:[210.0,206.0]:TopTop: -> ren35(x0,x1)
% 0.11/0.38 % 261:3:3:INP:TopTopTop: r1(skf18(x0),x1) -> p2(x1),ren44(x2,x0)
% 0.11/0.38 % 259:2:2:INP:TopTop: p3(skf18(x0)) -> ren44(x1,x0)
% 0.11/0.38 % 258:2:2:INP:TopTop: -> r1(x0,skf18(x0)),ren44(x1,x0)
% 0.11/0.38 % 257:2:2:INP:TopTop: p2(x0) -> ren44(x1,x0)
% 0.11/0.38 % 211:2:2:INP:TopTop: -> r1(x0,x1),ren36(x0,x1)
% 0.11/0.38 % 212:2:2:INP:TopTop: p4(x0) -> ren36(x1,x0)
% 0.11/0.38 % 213:2:2:INP:TopTop: -> r1(x0,x1),ren37(x0,x1)
% 0.11/0.38 % 214:2:2:INP:TopTop: p3(x0) -> ren37(x1,x0)
% 0.11/0.38 % 215:2:2:INP:TopTop: -> r1(x0,x1),ren38(x0,x1)
% 0.11/0.38 % 216:2:2:INP:TopTop: -> r1(x0,skf15(x0)),ren38(x1,x0)
% 0.11/0.38 % 217:2:2:INP:TopTop: -> p4(skf15(x0)),ren38(x1,x0)
% 0.11/0.38 % 218:3:3:INP:TopTopTop: r1(skf15(x0),x1) -> p4(x1),ren38(x2,x0)
% 0.11/0.38 % 219:2:2:INP:TopTop: p3(skf15(x0)) -> ren38(x1,x0)
% 0.11/0.38 % 220:2:2:INP:TopTop: p4(x0) -> ren38(x1,x0)
% 0.11/0.38 % 256:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren44(x2,x0)
% 0.11/0.38 % 222:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren38(x2,x0)
% 0.11/0.38 % 223:2:2:INP:TopTop: -> p3(x0),ren38(x1,x0)
% 0.11/0.38 % 224:2:2:INP:TopTop: -> r1(x0,x1),ren39(x0,x1)
% 0.11/0.38 % 225:2:2:INP:TopTop: -> p4(x0),ren39(x1,x0)
% 0.11/0.38 % 226:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren39(x2,x0)
% 0.11/0.38 % 227:2:2:INP:TopTop: p3(x0) -> ren39(x1,x0)
% 0.11/0.38 % 228:2:2:INP:TopTop: -> r1(x0,skf16(x0)),ren39(x1,x0)
% 0.11/0.38 % 229:2:2:INP:TopTop: p4(skf16(x0)) -> ren39(x1,x0)
% 0.11/0.38 % 255:2:2:INP:TopTop: -> p3(x0),ren44(x1,x0)
% 0.11/0.38 % 231:3:3:INP:TopTopTop: r1(skf16(x0),x1) -> p3(x1),ren39(x2,x0)
% 0.11/0.38 % 232:2:2:INP:TopTop: -> p3(skf16(x0)),ren39(x1,x0)
% 0.11/0.38 % 233:2:2:INP:TopTop: -> r1(x0,x1),ren40(x0,x1)
% 0.11/0.38 % 333:1:2:[237.0,234.0]:TopTop: -> ren40(x0,x1)
% 0.11/0.38 % 254:2:2:INP:TopTop: -> r1(x0,x1),ren44(x0,x1)
% 0.11/0.38 % 334:1:2:[238.0,236.0]:TopTop: -> ren40(x0,x1)
% 0.11/0.38 % 253:2:2:INP:TopTop: -> p2(x0),ren43(x1,x0)
% 0.11/0.38 % 252:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren43(x2,x0)
% 0.11/0.38 % 250:2:2:INP:TopTop: p3(x0) -> ren43(x1,x0)
% 0.11/0.38 % 249:2:2:INP:TopTop: p2(skf17(x0)) -> ren43(x1,x0)
% 0.11/0.38 % 241:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1)
% 0.11/0.38 % 242:2:2:INP:TopTop: p3(x0) -> ren41(x1,x0)
% 0.11/0.38 % 243:2:2:INP:TopTop: -> r1(x0,x1),ren42(x0,x1)
% 0.11/0.38 % 244:2:2:INP:TopTop: p2(x0) -> ren42(x1,x0)
% 0.11/0.38 % 245:2:2:INP:TopTop: -> r1(x0,x1),ren43(x0,x1)
% 0.11/0.38 % 246:2:2:INP:TopTop: -> r1(x0,skf17(x0)),ren43(x1,x0)
% 0.11/0.38 % 247:2:2:INP:TopTop: -> p3(skf17(x0)),ren43(x1,x0)
% 0.11/0.38 % 248:3:3:INP:TopTopTop: r1(skf17(x0),x1) -> p3(x1),ren43(x2,x0)
% 0.11/0.38
% 0.11/0.38 % Reduced Input Conjecture Clauses:
% 0.11/0.38 % 350:10:2:[338.1,318.8]:TopTop: r1(skc21,x0),p2(x0),ren46(x0,skf69(x0)),r1(skc21,x1),ren47(x1,skf70(x1)),p1(x1),ren48(skc21,skc71),ren49(skc21,skc72) -> p1(x0),p2(x1)
% 0.11/0.38 % 349:10:2:[336.1,317.8]:TopTop: r1(skc21,x0),p3(x0),ren41(x0,skf64(x0)),r1(skc21,x1),ren42(x1,skf65(x1)),p2(x1),ren43(skc21,skc66),ren44(skc21,skc67) -> p2(x0),p3(x1)
% 0.11/0.38 % 348:10:2:[333.1,316.8]:TopTop: r1(skc21,x0),p4(x0),ren36(x0,skf59(x0)),r1(skc21,x1),ren37(x1,skf60(x1)),p3(x1),ren38(skc21,skc61),ren39(skc21,skc62) -> p3(x0),p4(x1)
% 0.11/0.38 % 315:1:0:INP:: -> p10(skc58)
% 0.11/0.38 % 314:2:1:INP:Top: r1(skc58,x0) -> p10(x0)
% 0.11/0.38 % 347:0:0:[315.0,313.0]:: ->
% 0.11/0.38 % 312:1:0:INP:: -> r1(skc21,skc58)
% 0.11/0.38 % 311:1:0:INP:: -> p10(skc57)
% 0.11/0.38 % 310:2:1:INP:Top: r1(skc57,x0) -> p10(x0)
% 0.11/0.38 % 346:0:0:[311.0,309.0]:: ->
% 0.11/0.38 % 308:1:0:INP:: -> r1(skc21,skc57)
% 0.11/0.38 % 345:10:2:[331.1,307.8]:TopTop: r1(skc21,x0),p5(x0),ren31(x0,skf52(x0)),r1(skc21,x1),ren32(x1,skf53(x1)),p4(x1),ren33(skc21,skc54),ren34(skc21,skc55) -> p4(x0),p5(x1)
% 0.11/0.38 % 344:10:2:[330.1,306.8]:TopTop: r1(skc21,x0),p6(x0),ren26(x0,skf47(x0)),r1(skc21,x1),ren27(x1,skf48(x1)),p5(x1),ren28(skc21,skc49),ren29(skc21,skc50) -> p5(x0),p6(x1)
% 0.11/0.38 % 343:10:2:[327.1,305.8]:TopTop: r1(skc21,x0),p7(x0),ren21(x0,skf42(x0)),r1(skc21,x1),ren22(x1,skf43(x1)),p6(x1),ren23(skc21,skc44),ren24(skc21,skc45) -> p6(x0),p7(x1)
% 0.11/0.38 % 342:10:2:[326.1,304.8]:TopTop: r1(skc21,x0),p8(x0),ren16(x0,skf37(x0)),r1(skc21,x1),ren17(x1,skf38(x1)),p7(x1),ren18(skc21,skc39),ren19(skc21,skc40) -> p7(x0),p8(x1)
% 0.11/0.38 % 341:10:2:[324.1,303.8]:TopTop: r1(skc21,x0),p9(x0),ren11(x0,skf32(x0)),r1(skc21,x1),ren12(x1,skf33(x1)),p8(x1),ren13(skc21,skc34),ren14(skc21,skc35) -> p8(x0),p9(x1)
% 0.11/0.38 % 340:10:2:[321.1,302.8]:TopTop: r1(skc21,x0),p10(x0),ren6(x0,skf27(x0)),r1(skc21,x1),ren7(x1,skf28(x1)),p9(x1),ren8(skc21,skc29),ren9(skc21,skc30) -> p9(x0),p10(x1)
% 0.11/0.38 % 339:10:2:[320.1,301.8]:TopTop: r1(skc21,x0),p11(x0),ren1(x0,skf22(x0)),r1(skc21,x1),ren2(x1,skf23(x1)),p10(x1),ren3(skc21,skc24),ren4(skc21,skc25) -> p10(x0),p11(x1)
% 0.11/0.38
% 0.11/0.38 % SZS status Theorem
% 0.11/0.38
% 0.11/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.11/0.38 % SZS output start Proof for theBenchmark
% See solution above
% 0.11/0.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.11/0.39
% 0.11/0.39 % Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.39
% 0.11/0.39 % SPASS-SCL-FOL Statistics:
% 0.11/0.39 % Number of learned clauses: 0
% 0.11/0.39 % Number of propagations: 0
% 0.11/0.39 % Number of decisions: 0
% 0.11/0.39 % Number of resolutions: 0
% 0.11/0.39 % Number of condensations: 0
% 0.11/0.39 % Number of sub resolutions: 32
% 0.11/0.39
% 0.11/0.39 % Needed: 0:00:00.01
% 0.11/0.39
% 0.11/0.39 % ###
% 0.11/0.39 % ### Pagesize: 8192
% 0.11/0.39 % ### Marksize: 0
% 0.11/0.39 % ### Memory demanded: 1065 KBytes
% 0.11/0.39 % ### Memory freed: 1065 KBytes
% 0.11/0.39 % ### Memory remaining: 0 Bytes
% 0.11/0.39 % ### Pages allocated: 179 Pages
% 0.11/0.39 % ###
%------------------------------------------------------------------------------