%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:09:53 PM UTC 2026
% Result : Theorem 0.12s 0.37s
% Output : Proof 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 76
% Syntax : Number of formulae : 84 ( 3 unt; 75 def)
% Number of atoms : 3153 ( 0 equ)
% Maximal formula atoms : 655 ( 37 avg)
% Number of connectives : 4907 (1838 ~;2102 |; 892 &)
% ( 0 <=>; 0 =>; 75 <=; 0 <~>)
% Maximal formula depth : 39 ( 12 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 93 ( 92 usr; 1 prp; 0-2 aty)
% Number of functors : 78 ( 78 usr; 48 con; 0-1 aty)
% Number of variables : 1212 ( 0 sgn1130 !; 82 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p16(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p16(X2) ) )
| p15(X1) )
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p16(X1)
| ~ ( p15(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
& p15(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2)
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p15(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p15(X2) ) )
| p14(X1) )
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p15(X1)
| ~ ( p14(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p14(X2) )
& p14(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2)
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p14(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p14(X2) ) )
| p13(X1) )
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p14(X1)
| ~ ( p13(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p13(X2) )
& p13(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2)
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p13(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p13(X2) ) )
| p12(X1) )
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p13(X1)
| ~ ( p12(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p12(X2) )
& p12(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2)
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p12(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p12(X2) ) )
| p11(X1) )
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p12(X1)
| ~ ( p11(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p11(X2) )
& p11(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2)
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) ) ) )
| ~ ( ! [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)
| p15(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(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)
| ~ ( 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)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p16(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p16(X2) ) )
| p15(X1) )
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p16(X1)
| ~ ( p15(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
& p15(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p16(X1) ) )
| p15(X2)
| p16(X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p15(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p15(X2) ) )
| p14(X1) )
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p15(X1)
| ~ ( p14(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p14(X2) )
& p14(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p15(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p15(X1) ) )
| p14(X2)
| p15(X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) )
& p14(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p14(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p14(X2) ) )
| p13(X1) )
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p14(X1)
| ~ ( p13(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p13(X2) )
& p13(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p14(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p14(X1) ) )
| p13(X2)
| p14(X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) )
& p13(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p13(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p13(X2) ) )
| p12(X1) )
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p13(X1)
| ~ ( p12(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p12(X2) )
& p12(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p13(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p13(X1) ) )
| p12(X2)
| p13(X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) )
& p12(X2) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( p12(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p12(X2) ) )
| p11(X1) )
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2)
| ! [X1] :
( ~ r1(X2,X1)
| p12(X1)
| ~ ( p11(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p11(X2) )
& p11(X1) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ( p12(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p12(X1) ) )
| p11(X2)
| p12(X2)
| ~ ( p11(X2)
& ! [X1] :
( ~ r1(X2,X1)
| p11(X1) )
& p11(X2) ) ) ) )
| ~ ( ! [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)
| p15(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p15(X1) )
& p15(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)
| ~ ( 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)
| ~ ( p16(X2)
& ! [X3] :
( ~ r1(X2,X3)
| p16(X3) ) )
| p15(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p16(X4)
| ~ ( p15(X4)
& ! [X5] :
( ~ r1(X4,X5)
| p15(X5) )
& p15(X4) ) )
| ~ ( ! [X6] :
( ~ r1(X1,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ~ ( p16(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p16(X8) ) )
| p15(X7) )
| p16(X6)
| ~ ( p15(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p15(X9) )
& p15(X6) ) )
& ! [X10] :
( ~ r1(X1,X10)
| ~ ( p16(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p16(X11) ) )
| p15(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p16(X12)
| ~ ( p15(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p15(X13) )
& p15(X12) ) ) )
& ! [X14] :
( ~ r1(X1,X14)
| ~ ( p16(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p16(X15) ) )
| p15(X14)
| p16(X14)
| ~ ( p15(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p15(X16) )
& p15(X14) ) ) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p15(X17)
& ! [X18] :
( ~ r1(X17,X18)
| p15(X18) ) )
| p14(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p15(X19)
| ~ ( p14(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p14(X20) )
& p14(X19) ) )
| ~ ( ! [X21] :
( ~ r1(X1,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ~ ( p15(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p15(X23) ) )
| p14(X22) )
| p15(X21)
| ~ ( p14(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p14(X24) )
& p14(X21) ) )
& ! [X25] :
( ~ r1(X1,X25)
| ~ ( p15(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p15(X26) ) )
| p14(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p15(X27)
| ~ ( p14(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p14(X28) )
& p14(X27) ) ) )
& ! [X29] :
( ~ r1(X1,X29)
| ~ ( p15(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p15(X30) ) )
| p14(X29)
| p15(X29)
| ~ ( p14(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p14(X31) )
& p14(X29) ) ) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p14(X32)
& ! [X33] :
( ~ r1(X32,X33)
| p14(X33) ) )
| p13(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p14(X34)
| ~ ( p13(X34)
& ! [X35] :
( ~ r1(X34,X35)
| p13(X35) )
& p13(X34) ) )
| ~ ( ! [X36] :
( ~ r1(X1,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ( p14(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p14(X38) ) )
| p13(X37) )
| p14(X36)
| ~ ( p13(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p13(X39) )
& p13(X36) ) )
& ! [X40] :
( ~ r1(X1,X40)
| ~ ( p14(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p14(X41) ) )
| p13(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p14(X42)
| ~ ( p13(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p13(X43) )
& p13(X42) ) ) )
& ! [X44] :
( ~ r1(X1,X44)
| ~ ( p14(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p14(X45) ) )
| p13(X44)
| p14(X44)
| ~ ( p13(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p13(X46) )
& p13(X44) ) ) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p13(X47)
& ! [X48] :
( ~ r1(X47,X48)
| p13(X48) ) )
| p12(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p13(X49)
| ~ ( p12(X49)
& ! [X50] :
( ~ r1(X49,X50)
| p12(X50) )
& p12(X49) ) )
| ~ ( ! [X51] :
( ~ r1(X1,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ( p13(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p13(X53) ) )
| p12(X52) )
| p13(X51)
| ~ ( p12(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p12(X54) )
& p12(X51) ) )
& ! [X55] :
( ~ r1(X1,X55)
| ~ ( p13(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p13(X56) ) )
| p12(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p13(X57)
| ~ ( p12(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p12(X58) )
& p12(X57) ) ) )
& ! [X59] :
( ~ r1(X1,X59)
| ~ ( p13(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p13(X60) ) )
| p12(X59)
| p13(X59)
| ~ ( p12(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p12(X61) )
& p12(X59) ) ) ) )
| ~ ( ! [X62] :
( ~ r1(X1,X62)
| ~ ( p12(X62)
& ! [X63] :
( ~ r1(X62,X63)
| p12(X63) ) )
| p11(X62) )
| ! [X64] :
( ~ r1(X1,X64)
| p12(X64)
| ~ ( p11(X64)
& ! [X65] :
( ~ r1(X64,X65)
| p11(X65) )
& p11(X64) ) )
| ~ ( ! [X66] :
( ~ r1(X1,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ~ ( p12(X67)
& ! [X68] :
( ~ r1(X67,X68)
| p12(X68) ) )
| p11(X67) )
| p12(X66)
| ~ ( p11(X66)
& ! [X69] :
( ~ r1(X66,X69)
| p11(X69) )
& p11(X66) ) )
& ! [X70] :
( ~ r1(X1,X70)
| ~ ( p12(X70)
& ! [X71] :
( ~ r1(X70,X71)
| p12(X71) ) )
| p11(X70)
| ! [X72] :
( ~ r1(X70,X72)
| p12(X72)
| ~ ( p11(X72)
& ! [X73] :
( ~ r1(X72,X73)
| p11(X73) )
& p11(X72) ) ) )
& ! [X74] :
( ~ r1(X1,X74)
| ~ ( p12(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p12(X75) ) )
| p11(X74)
| p12(X74)
| ~ ( p11(X74)
& ! [X76] :
( ~ r1(X74,X76)
| p11(X76) )
& p11(X74) ) ) ) )
| ~ ( ! [X77] :
( ~ r1(X1,X77)
| ~ ( p11(X77)
& ! [X78] :
( ~ r1(X77,X78)
| p11(X78) ) )
| p10(X77) )
| ! [X79] :
( ~ r1(X1,X79)
| p11(X79)
| ~ ( p10(X79)
& ! [X80] :
( ~ r1(X79,X80)
| p10(X80) )
& p10(X79) ) )
| ~ ( ! [X81] :
( ~ r1(X1,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ~ ( p11(X82)
& ! [X83] :
( ~ r1(X82,X83)
| p11(X83) ) )
| p10(X82) )
| p11(X81)
| ~ ( p10(X81)
& ! [X84] :
( ~ r1(X81,X84)
| p10(X84) )
& p10(X81) ) )
& ! [X85] :
( ~ r1(X1,X85)
| ~ ( p11(X85)
& ! [X86] :
( ~ r1(X85,X86)
| p11(X86) ) )
| p10(X85)
| ! [X87] :
( ~ r1(X85,X87)
| p11(X87)
| ~ ( p10(X87)
& ! [X88] :
( ~ r1(X87,X88)
| p10(X88) )
& p10(X87) ) ) )
& ! [X89] :
( ~ r1(X1,X89)
| ~ ( p11(X89)
& ! [X90] :
( ~ r1(X89,X90)
| p11(X90) ) )
| p10(X89)
| p11(X89)
| ~ ( p10(X89)
& ! [X91] :
( ~ r1(X89,X91)
| p10(X91) )
& p10(X89) ) ) ) )
| ~ ( ! [X92] :
( ~ r1(X1,X92)
| ~ ( p10(X92)
& ! [X93] :
( ~ r1(X92,X93)
| p10(X93) ) )
| p9(X92) )
| ! [X94] :
( ~ r1(X1,X94)
| p10(X94)
| ~ ( p9(X94)
& ! [X95] :
( ~ r1(X94,X95)
| p9(X95) )
& p9(X94) ) )
| ~ ( ! [X96] :
( ~ r1(X1,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ~ ( p10(X97)
& ! [X98] :
( ~ r1(X97,X98)
| p10(X98) ) )
| p9(X97) )
| p10(X96)
| ~ ( p9(X96)
& ! [X99] :
( ~ r1(X96,X99)
| p9(X99) )
& p9(X96) ) )
& ! [X100] :
( ~ r1(X1,X100)
| ~ ( p10(X100)
& ! [X101] :
( ~ r1(X100,X101)
| p10(X101) ) )
| p9(X100)
| ! [X102] :
( ~ r1(X100,X102)
| p10(X102)
| ~ ( p9(X102)
& ! [X103] :
( ~ r1(X102,X103)
| p9(X103) )
& p9(X102) ) ) )
& ! [X104] :
( ~ r1(X1,X104)
| ~ ( p10(X104)
& ! [X105] :
( ~ r1(X104,X105)
| p10(X105) ) )
| p9(X104)
| p10(X104)
| ~ ( p9(X104)
& ! [X106] :
( ~ r1(X104,X106)
| p9(X106) )
& p9(X104) ) ) ) )
| ~ ( ! [X107] :
( ~ r1(X1,X107)
| ~ ( p9(X107)
& ! [X108] :
( ~ r1(X107,X108)
| p9(X108) ) )
| p8(X107) )
| ! [X109] :
( ~ r1(X1,X109)
| p9(X109)
| ~ ( p8(X109)
& ! [X110] :
( ~ r1(X109,X110)
| p8(X110) )
& p8(X109) ) )
| ~ ( ! [X111] :
( ~ r1(X1,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ ( p9(X112)
& ! [X113] :
( ~ r1(X112,X113)
| p9(X113) ) )
| p8(X112) )
| p9(X111)
| ~ ( p8(X111)
& ! [X114] :
( ~ r1(X111,X114)
| p8(X114) )
& p8(X111) ) )
& ! [X115] :
( ~ r1(X1,X115)
| ~ ( p9(X115)
& ! [X116] :
( ~ r1(X115,X116)
| p9(X116) ) )
| p8(X115)
| ! [X117] :
( ~ r1(X115,X117)
| p9(X117)
| ~ ( p8(X117)
& ! [X118] :
( ~ r1(X117,X118)
| p8(X118) )
& p8(X117) ) ) )
& ! [X119] :
( ~ r1(X1,X119)
| ~ ( p9(X119)
& ! [X120] :
( ~ r1(X119,X120)
| p9(X120) ) )
| p8(X119)
| p9(X119)
| ~ ( p8(X119)
& ! [X121] :
( ~ r1(X119,X121)
| p8(X121) )
& p8(X119) ) ) ) )
| ~ ( ! [X122] :
( ~ r1(X1,X122)
| ~ ( p8(X122)
& ! [X123] :
( ~ r1(X122,X123)
| p8(X123) ) )
| p7(X122) )
| ! [X124] :
( ~ r1(X1,X124)
| p8(X124)
| ~ ( p7(X124)
& ! [X125] :
( ~ r1(X124,X125)
| p7(X125) )
& p7(X124) ) )
| ~ ( ! [X126] :
( ~ r1(X1,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ~ ( p8(X127)
& ! [X128] :
( ~ r1(X127,X128)
| p8(X128) ) )
| p7(X127) )
| p8(X126)
| ~ ( p7(X126)
& ! [X129] :
( ~ r1(X126,X129)
| p7(X129) )
& p7(X126) ) )
& ! [X130] :
( ~ r1(X1,X130)
| ~ ( p8(X130)
& ! [X131] :
( ~ r1(X130,X131)
| p8(X131) ) )
| p7(X130)
| ! [X132] :
( ~ r1(X130,X132)
| p8(X132)
| ~ ( p7(X132)
& ! [X133] :
( ~ r1(X132,X133)
| p7(X133) )
& p7(X132) ) ) )
& ! [X134] :
( ~ r1(X1,X134)
| ~ ( p8(X134)
& ! [X135] :
( ~ r1(X134,X135)
| p8(X135) ) )
| p7(X134)
| p8(X134)
| ~ ( p7(X134)
& ! [X136] :
( ~ r1(X134,X136)
| p7(X136) )
& p7(X134) ) ) ) )
| ~ ( ! [X137] :
( ~ r1(X1,X137)
| ~ ( p7(X137)
& ! [X138] :
( ~ r1(X137,X138)
| p7(X138) ) )
| p6(X137) )
| ! [X139] :
( ~ r1(X1,X139)
| p7(X139)
| ~ ( p6(X139)
& ! [X140] :
( ~ r1(X139,X140)
| p6(X140) )
& p6(X139) ) )
| ~ ( ! [X141] :
( ~ r1(X1,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ~ ( p7(X142)
& ! [X143] :
( ~ r1(X142,X143)
| p7(X143) ) )
| p6(X142) )
| p7(X141)
| ~ ( p6(X141)
& ! [X144] :
( ~ r1(X141,X144)
| p6(X144) )
& p6(X141) ) )
& ! [X145] :
( ~ r1(X1,X145)
| ~ ( p7(X145)
& ! [X146] :
( ~ r1(X145,X146)
| p7(X146) ) )
| p6(X145)
| ! [X147] :
( ~ r1(X145,X147)
| p7(X147)
| ~ ( p6(X147)
& ! [X148] :
( ~ r1(X147,X148)
| p6(X148) )
& p6(X147) ) ) )
& ! [X149] :
( ~ r1(X1,X149)
| ~ ( p7(X149)
& ! [X150] :
( ~ r1(X149,X150)
| p7(X150) ) )
| p6(X149)
| p7(X149)
| ~ ( p6(X149)
& ! [X151] :
( ~ r1(X149,X151)
| p6(X151) )
& p6(X149) ) ) ) )
| ! [X152] :
( ~ r1(X1,X152)
| p15(X152)
| ~ ( ! [X153] :
( ~ r1(X152,X153)
| p15(X153) )
& p15(X152) ) )
| ! [X154] :
( ~ r1(X1,X154)
| p15(X154)
| ~ ( ! [X155] :
( ~ r1(X154,X155)
| p15(X155) )
& p15(X154) ) )
| ~ ( ! [X156] :
( ~ r1(X1,X156)
| ~ ( p6(X156)
& ! [X157] :
( ~ r1(X156,X157)
| p6(X157) ) )
| p5(X156) )
| ! [X158] :
( ~ r1(X1,X158)
| p6(X158)
| ~ ( p5(X158)
& ! [X159] :
( ~ r1(X158,X159)
| p5(X159) )
& p5(X158) ) )
| ~ ( ! [X160] :
( ~ r1(X1,X160)
| ! [X161] :
( ~ r1(X160,X161)
| ~ ( p6(X161)
& ! [X162] :
( ~ r1(X161,X162)
| p6(X162) ) )
| p5(X161) )
| p6(X160)
| ~ ( p5(X160)
& ! [X163] :
( ~ r1(X160,X163)
| p5(X163) )
& p5(X160) ) )
& ! [X164] :
( ~ r1(X1,X164)
| ~ ( p6(X164)
& ! [X165] :
( ~ r1(X164,X165)
| p6(X165) ) )
| p5(X164)
| ! [X166] :
( ~ r1(X164,X166)
| p6(X166)
| ~ ( p5(X166)
& ! [X167] :
( ~ r1(X166,X167)
| p5(X167) )
& p5(X166) ) ) )
& ! [X168] :
( ~ r1(X1,X168)
| ~ ( p6(X168)
& ! [X169] :
( ~ r1(X168,X169)
| p6(X169) ) )
| p5(X168)
| p6(X168)
| ~ ( p5(X168)
& ! [X170] :
( ~ r1(X168,X170)
| p5(X170) )
& p5(X168) ) ) ) )
| ~ ( ! [X171] :
( ~ r1(X1,X171)
| ~ ( p5(X171)
& ! [X172] :
( ~ r1(X171,X172)
| p5(X172) ) )
| p4(X171) )
| ! [X173] :
( ~ r1(X1,X173)
| p5(X173)
| ~ ( p4(X173)
& ! [X174] :
( ~ r1(X173,X174)
| p4(X174) )
& p4(X173) ) )
| ~ ( ! [X175] :
( ~ r1(X1,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ ( p5(X176)
& ! [X177] :
( ~ r1(X176,X177)
| p5(X177) ) )
| p4(X176) )
| p5(X175)
| ~ ( p4(X175)
& ! [X178] :
( ~ r1(X175,X178)
| p4(X178) )
& p4(X175) ) )
& ! [X179] :
( ~ r1(X1,X179)
| ~ ( p5(X179)
& ! [X180] :
( ~ r1(X179,X180)
| p5(X180) ) )
| p4(X179)
| ! [X181] :
( ~ r1(X179,X181)
| p5(X181)
| ~ ( p4(X181)
& ! [X182] :
( ~ r1(X181,X182)
| p4(X182) )
& p4(X181) ) ) )
& ! [X183] :
( ~ r1(X1,X183)
| ~ ( p5(X183)
& ! [X184] :
( ~ r1(X183,X184)
| p5(X184) ) )
| p4(X183)
| p5(X183)
| ~ ( p4(X183)
& ! [X185] :
( ~ r1(X183,X185)
| p4(X185) )
& p4(X183) ) ) ) )
| ~ ( ! [X186] :
( ~ r1(X1,X186)
| ~ ( p4(X186)
& ! [X187] :
( ~ r1(X186,X187)
| p4(X187) ) )
| p3(X186) )
| ! [X188] :
( ~ r1(X1,X188)
| p4(X188)
| ~ ( p3(X188)
& ! [X189] :
( ~ r1(X188,X189)
| p3(X189) )
& p3(X188) ) )
| ~ ( ! [X190] :
( ~ r1(X1,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ~ ( p4(X191)
& ! [X192] :
( ~ r1(X191,X192)
| p4(X192) ) )
| p3(X191) )
| p4(X190)
| ~ ( p3(X190)
& ! [X193] :
( ~ r1(X190,X193)
| p3(X193) )
& p3(X190) ) )
& ! [X194] :
( ~ r1(X1,X194)
| ~ ( p4(X194)
& ! [X195] :
( ~ r1(X194,X195)
| p4(X195) ) )
| p3(X194)
| ! [X196] :
( ~ r1(X194,X196)
| p4(X196)
| ~ ( p3(X196)
& ! [X197] :
( ~ r1(X196,X197)
| p3(X197) )
& p3(X196) ) ) )
& ! [X198] :
( ~ r1(X1,X198)
| ~ ( p4(X198)
& ! [X199] :
( ~ r1(X198,X199)
| p4(X199) ) )
| p3(X198)
| p4(X198)
| ~ ( p3(X198)
& ! [X200] :
( ~ r1(X198,X200)
| p3(X200) )
& p3(X198) ) ) ) )
| ~ ( ! [X201] :
( ~ r1(X1,X201)
| ~ ( p3(X201)
& ! [X202] :
( ~ r1(X201,X202)
| p3(X202) ) )
| p2(X201) )
| ! [X203] :
( ~ r1(X1,X203)
| p3(X203)
| ~ ( p2(X203)
& ! [X204] :
( ~ r1(X203,X204)
| p2(X204) )
& p2(X203) ) )
| ~ ( ! [X205] :
( ~ r1(X1,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ~ ( p3(X206)
& ! [X207] :
( ~ r1(X206,X207)
| p3(X207) ) )
| p2(X206) )
| p3(X205)
| ~ ( p2(X205)
& ! [X208] :
( ~ r1(X205,X208)
| p2(X208) )
& p2(X205) ) )
& ! [X209] :
( ~ r1(X1,X209)
| ~ ( p3(X209)
& ! [X210] :
( ~ r1(X209,X210)
| p3(X210) ) )
| p2(X209)
| ! [X211] :
( ~ r1(X209,X211)
| p3(X211)
| ~ ( p2(X211)
& ! [X212] :
( ~ r1(X211,X212)
| p2(X212) )
& p2(X211) ) ) )
& ! [X213] :
( ~ r1(X1,X213)
| ~ ( p3(X213)
& ! [X214] :
( ~ r1(X213,X214)
| p3(X214) ) )
| p2(X213)
| p3(X213)
| ~ ( p2(X213)
& ! [X215] :
( ~ r1(X213,X215)
| p2(X215) )
& p2(X213) ) ) ) )
| ~ ( ! [X216] :
( ~ r1(X1,X216)
| ~ ( p2(X216)
& ! [X217] :
( ~ r1(X216,X217)
| p2(X217) ) )
| p1(X216) )
| ! [X218] :
( ~ r1(X1,X218)
| p2(X218)
| ~ ( p1(X218)
& ! [X219] :
( ~ r1(X218,X219)
| p1(X219) )
& p1(X218) ) )
| ~ ( ! [X220] :
( ~ r1(X1,X220)
| ! [X221] :
( ~ r1(X220,X221)
| ~ ( p2(X221)
& ! [X222] :
( ~ r1(X221,X222)
| p2(X222) ) )
| p1(X221) )
| p2(X220)
| ~ ( p1(X220)
& ! [X223] :
( ~ r1(X220,X223)
| p1(X223) )
& p1(X220) ) )
& ! [X224] :
( ~ r1(X1,X224)
| ~ ( p2(X224)
& ! [X225] :
( ~ r1(X224,X225)
| p2(X225) ) )
| p1(X224)
| ! [X226] :
( ~ r1(X224,X226)
| p2(X226)
| ~ ( p1(X226)
& ! [X227] :
( ~ r1(X226,X227)
| p1(X227) )
& p1(X226) ) ) )
& ! [X228] :
( ~ r1(X1,X228)
| ~ ( p2(X228)
& ! [X229] :
( ~ r1(X228,X229)
| p2(X229) ) )
| p1(X228)
| p2(X228)
| ~ ( p1(X228)
& ! [X230] :
( ~ r1(X228,X230)
| p1(X230) )
& p1(X228) ) ) ) ) ),
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)
| p16(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)
| p15(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)
| ~ ( p16(X7)
& ! [X8] :
( ~ r1(X7,X8)
| p16(X8) ) )
| p15(X7) )
| p16(X6)
| ~ ( p15(X6)
& ! [X9] :
( ~ r1(X6,X9)
| p15(X9) )
& p15(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)
| ~ ( p16(X10)
& ! [X11] :
( ~ r1(X10,X11)
| p16(X11) ) )
| p15(X10)
| ! [X12] :
( ~ r1(X10,X12)
| p16(X12)
| ~ ( p15(X12)
& ! [X13] :
( ~ r1(X12,X13)
| p15(X13) )
& p15(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)
| ~ ( p16(X14)
& ! [X15] :
( ~ r1(X14,X15)
| p16(X15) ) )
| p15(X14)
| p16(X14)
| ~ ( p15(X14)
& ! [X16] :
( ~ r1(X14,X16)
| p15(X16) )
& p15(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)
| p15(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)
| p14(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)
| ~ ( p15(X22)
& ! [X23] :
( ~ r1(X22,X23)
| p15(X23) ) )
| p14(X22) )
| p15(X21)
| ~ ( p14(X21)
& ! [X24] :
( ~ r1(X21,X24)
| p14(X24) )
& p14(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)
| ~ ( p15(X25)
& ! [X26] :
( ~ r1(X25,X26)
| p15(X26) ) )
| p14(X25)
| ! [X27] :
( ~ r1(X25,X27)
| p15(X27)
| ~ ( p14(X27)
& ! [X28] :
( ~ r1(X27,X28)
| p14(X28) )
& p14(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)
| ~ ( p15(X29)
& ! [X30] :
( ~ r1(X29,X30)
| p15(X30) ) )
| p14(X29)
| p15(X29)
| ~ ( p14(X29)
& ! [X31] :
( ~ r1(X29,X31)
| p14(X31) )
& p14(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)
| p14(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)
| p13(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)
| ~ ( p14(X37)
& ! [X38] :
( ~ r1(X37,X38)
| p14(X38) ) )
| p13(X37) )
| p14(X36)
| ~ ( p13(X36)
& ! [X39] :
( ~ r1(X36,X39)
| p13(X39) )
& p13(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)
| ~ ( p14(X40)
& ! [X41] :
( ~ r1(X40,X41)
| p14(X41) ) )
| p13(X40)
| ! [X42] :
( ~ r1(X40,X42)
| p14(X42)
| ~ ( p13(X42)
& ! [X43] :
( ~ r1(X42,X43)
| p13(X43) )
& p13(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)
| ~ ( p14(X44)
& ! [X45] :
( ~ r1(X44,X45)
| p14(X45) ) )
| p13(X44)
| p14(X44)
| ~ ( p13(X44)
& ! [X46] :
( ~ r1(X44,X46)
| p13(X46) )
& p13(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)
| p13(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)
| p12(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)
| ~ ( p13(X52)
& ! [X53] :
( ~ r1(X52,X53)
| p13(X53) ) )
| p12(X52) )
| p13(X51)
| ~ ( p12(X51)
& ! [X54] :
( ~ r1(X51,X54)
| p12(X54) )
& p12(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)
| ~ ( p13(X55)
& ! [X56] :
( ~ r1(X55,X56)
| p13(X56) ) )
| p12(X55)
| ! [X57] :
( ~ r1(X55,X57)
| p13(X57)
| ~ ( p12(X57)
& ! [X58] :
( ~ r1(X57,X58)
| p12(X58) )
& p12(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)
| ~ ( p13(X59)
& ! [X60] :
( ~ r1(X59,X60)
| p13(X60) ) )
| p12(X59)
| p13(X59)
| ~ ( p12(X59)
& ! [X61] :
( ~ r1(X59,X61)
| p12(X61) )
& p12(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)
| p12(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)
| p11(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)
| ~ ( p12(X67)
& ! [X68] :
( ~ r1(X67,X68)
| p12(X68) ) )
| p11(X67) )
| p12(X66)
| ~ ( p11(X66)
& ! [X69] :
( ~ r1(X66,X69)
| p11(X69) )
& p11(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)
| ~ ( p12(X70)
& ! [X71] :
( ~ r1(X70,X71)
| p12(X71) ) )
| p11(X70)
| ! [X72] :
( ~ r1(X70,X72)
| p12(X72)
| ~ ( p11(X72)
& ! [X73] :
( ~ r1(X72,X73)
| p11(X73) )
& p11(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)
| ~ ( p12(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p12(X75) ) )
| p11(X74)
| p12(X74)
| ~ ( p11(X74)
& ! [X76] :
( ~ r1(X74,X76)
| p11(X76) )
& p11(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)
| p11(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)
| p10(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)
| ~ ( p11(X82)
& ! [X83] :
( ~ r1(X82,X83)
| p11(X83) ) )
| p10(X82) )
| p11(X81)
| ~ ( p10(X81)
& ! [X84] :
( ~ r1(X81,X84)
| p10(X84) )
& p10(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)
| ~ ( p11(X85)
& ! [X86] :
( ~ r1(X85,X86)
| p11(X86) ) )
| p10(X85)
| ! [X87] :
( ~ r1(X85,X87)
| p11(X87)
| ~ ( p10(X87)
& ! [X88] :
( ~ r1(X87,X88)
| p10(X88) )
& p10(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)
| ~ ( p11(X89)
& ! [X90] :
( ~ r1(X89,X90)
| p11(X90) ) )
| p10(X89)
| p11(X89)
| ~ ( p10(X89)
& ! [X91] :
( ~ r1(X89,X91)
| p10(X91) )
& p10(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)
| p10(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)
| p9(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)
| ~ ( p10(X97)
& ! [X98] :
( ~ r1(X97,X98)
| p10(X98) ) )
| p9(X97) )
| p10(X96)
| ~ ( p9(X96)
& ! [X99] :
( ~ r1(X96,X99)
| p9(X99) )
& p9(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)
| ~ ( p10(X100)
& ! [X101] :
( ~ r1(X100,X101)
| p10(X101) ) )
| p9(X100)
| ! [X102] :
( ~ r1(X100,X102)
| p10(X102)
| ~ ( p9(X102)
& ! [X103] :
( ~ r1(X102,X103)
| p9(X103) )
& p9(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)
| ~ ( p10(X104)
& ! [X105] :
( ~ r1(X104,X105)
| p10(X105) ) )
| p9(X104)
| p10(X104)
| ~ ( p9(X104)
& ! [X106] :
( ~ r1(X104,X106)
| p9(X106) )
& p9(X104) ) ) ),
introduced(definition,[new_symbols(definition,[ren35])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren36_defn,definition,
! [X107,X108] :
( ren36(X107,X108)
<= ( ~ r1(X107,X108)
| p9(X108) ) ),
introduced(definition,[new_symbols(definition,[ren36])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren37_defn,definition,
! [X109,X110] :
( ren37(X109,X110)
<= ( ~ r1(X109,X110)
| p8(X110) ) ),
introduced(definition,[new_symbols(definition,[ren37])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren38_defn,definition,
! [X1,X111] :
( ren38(X1,X111)
<= ( ~ r1(X1,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ~ ( p9(X112)
& ! [X113] :
( ~ r1(X112,X113)
| p9(X113) ) )
| p8(X112) )
| p9(X111)
| ~ ( p8(X111)
& ! [X114] :
( ~ r1(X111,X114)
| p8(X114) )
& p8(X111) ) ) ),
introduced(definition,[new_symbols(definition,[ren38])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren39_defn,definition,
! [X1,X115] :
( ren39(X1,X115)
<= ( ~ r1(X1,X115)
| ~ ( p9(X115)
& ! [X116] :
( ~ r1(X115,X116)
| p9(X116) ) )
| p8(X115)
| ! [X117] :
( ~ r1(X115,X117)
| p9(X117)
| ~ ( p8(X117)
& ! [X118] :
( ~ r1(X117,X118)
| p8(X118) )
& p8(X117) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren39])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren40_defn,definition,
! [X1,X119] :
( ren40(X1,X119)
<= ( ~ r1(X1,X119)
| ~ ( p9(X119)
& ! [X120] :
( ~ r1(X119,X120)
| p9(X120) ) )
| p8(X119)
| p9(X119)
| ~ ( p8(X119)
& ! [X121] :
( ~ r1(X119,X121)
| p8(X121) )
& p8(X119) ) ) ),
introduced(definition,[new_symbols(definition,[ren40])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren41_defn,definition,
! [X122,X123] :
( ren41(X122,X123)
<= ( ~ r1(X122,X123)
| p8(X123) ) ),
introduced(definition,[new_symbols(definition,[ren41])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren42_defn,definition,
! [X124,X125] :
( ren42(X124,X125)
<= ( ~ r1(X124,X125)
| p7(X125) ) ),
introduced(definition,[new_symbols(definition,[ren42])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren43_defn,definition,
! [X1,X126] :
( ren43(X1,X126)
<= ( ~ r1(X1,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ~ ( p8(X127)
& ! [X128] :
( ~ r1(X127,X128)
| p8(X128) ) )
| p7(X127) )
| p8(X126)
| ~ ( p7(X126)
& ! [X129] :
( ~ r1(X126,X129)
| p7(X129) )
& p7(X126) ) ) ),
introduced(definition,[new_symbols(definition,[ren43])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren44_defn,definition,
! [X1,X130] :
( ren44(X1,X130)
<= ( ~ r1(X1,X130)
| ~ ( p8(X130)
& ! [X131] :
( ~ r1(X130,X131)
| p8(X131) ) )
| p7(X130)
| ! [X132] :
( ~ r1(X130,X132)
| p8(X132)
| ~ ( p7(X132)
& ! [X133] :
( ~ r1(X132,X133)
| p7(X133) )
& p7(X132) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren44])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren45_defn,definition,
! [X1,X134] :
( ren45(X1,X134)
<= ( ~ r1(X1,X134)
| ~ ( p8(X134)
& ! [X135] :
( ~ r1(X134,X135)
| p8(X135) ) )
| p7(X134)
| p8(X134)
| ~ ( p7(X134)
& ! [X136] :
( ~ r1(X134,X136)
| p7(X136) )
& p7(X134) ) ) ),
introduced(definition,[new_symbols(definition,[ren45])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren46_defn,definition,
! [X137,X138] :
( ren46(X137,X138)
<= ( ~ r1(X137,X138)
| p7(X138) ) ),
introduced(definition,[new_symbols(definition,[ren46])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren47_defn,definition,
! [X139,X140] :
( ren47(X139,X140)
<= ( ~ r1(X139,X140)
| p6(X140) ) ),
introduced(definition,[new_symbols(definition,[ren47])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren48_defn,definition,
! [X1,X141] :
( ren48(X1,X141)
<= ( ~ r1(X1,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ~ ( p7(X142)
& ! [X143] :
( ~ r1(X142,X143)
| p7(X143) ) )
| p6(X142) )
| p7(X141)
| ~ ( p6(X141)
& ! [X144] :
( ~ r1(X141,X144)
| p6(X144) )
& p6(X141) ) ) ),
introduced(definition,[new_symbols(definition,[ren48])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren49_defn,definition,
! [X1,X145] :
( ren49(X1,X145)
<= ( ~ r1(X1,X145)
| ~ ( p7(X145)
& ! [X146] :
( ~ r1(X145,X146)
| p7(X146) ) )
| p6(X145)
| ! [X147] :
( ~ r1(X145,X147)
| p7(X147)
| ~ ( p6(X147)
& ! [X148] :
( ~ r1(X147,X148)
| p6(X148) )
& p6(X147) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren49])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren50_defn,definition,
! [X1,X149] :
( ren50(X1,X149)
<= ( ~ r1(X1,X149)
| ~ ( p7(X149)
& ! [X150] :
( ~ r1(X149,X150)
| p7(X150) ) )
| p6(X149)
| p7(X149)
| ~ ( p6(X149)
& ! [X151] :
( ~ r1(X149,X151)
| p6(X151) )
& p6(X149) ) ) ),
introduced(definition,[new_symbols(definition,[ren50])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren51_defn,definition,
! [X156,X157] :
( ren51(X156,X157)
<= ( ~ r1(X156,X157)
| p6(X157) ) ),
introduced(definition,[new_symbols(definition,[ren51])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren52_defn,definition,
! [X158,X159] :
( ren52(X158,X159)
<= ( ~ r1(X158,X159)
| p5(X159) ) ),
introduced(definition,[new_symbols(definition,[ren52])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren53_defn,definition,
! [X1,X160] :
( ren53(X1,X160)
<= ( ~ r1(X1,X160)
| ! [X161] :
( ~ r1(X160,X161)
| ~ ( p6(X161)
& ! [X162] :
( ~ r1(X161,X162)
| p6(X162) ) )
| p5(X161) )
| p6(X160)
| ~ ( p5(X160)
& ! [X163] :
( ~ r1(X160,X163)
| p5(X163) )
& p5(X160) ) ) ),
introduced(definition,[new_symbols(definition,[ren53])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren54_defn,definition,
! [X1,X164] :
( ren54(X1,X164)
<= ( ~ r1(X1,X164)
| ~ ( p6(X164)
& ! [X165] :
( ~ r1(X164,X165)
| p6(X165) ) )
| p5(X164)
| ! [X166] :
( ~ r1(X164,X166)
| p6(X166)
| ~ ( p5(X166)
& ! [X167] :
( ~ r1(X166,X167)
| p5(X167) )
& p5(X166) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren54])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren55_defn,definition,
! [X1,X168] :
( ren55(X1,X168)
<= ( ~ r1(X1,X168)
| ~ ( p6(X168)
& ! [X169] :
( ~ r1(X168,X169)
| p6(X169) ) )
| p5(X168)
| p6(X168)
| ~ ( p5(X168)
& ! [X170] :
( ~ r1(X168,X170)
| p5(X170) )
& p5(X168) ) ) ),
introduced(definition,[new_symbols(definition,[ren55])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren56_defn,definition,
! [X171,X172] :
( ren56(X171,X172)
<= ( ~ r1(X171,X172)
| p5(X172) ) ),
introduced(definition,[new_symbols(definition,[ren56])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren57_defn,definition,
! [X173,X174] :
( ren57(X173,X174)
<= ( ~ r1(X173,X174)
| p4(X174) ) ),
introduced(definition,[new_symbols(definition,[ren57])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren58_defn,definition,
! [X1,X175] :
( ren58(X1,X175)
<= ( ~ r1(X1,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ ( p5(X176)
& ! [X177] :
( ~ r1(X176,X177)
| p5(X177) ) )
| p4(X176) )
| p5(X175)
| ~ ( p4(X175)
& ! [X178] :
( ~ r1(X175,X178)
| p4(X178) )
& p4(X175) ) ) ),
introduced(definition,[new_symbols(definition,[ren58])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren59_defn,definition,
! [X1,X179] :
( ren59(X1,X179)
<= ( ~ r1(X1,X179)
| ~ ( p5(X179)
& ! [X180] :
( ~ r1(X179,X180)
| p5(X180) ) )
| p4(X179)
| ! [X181] :
( ~ r1(X179,X181)
| p5(X181)
| ~ ( p4(X181)
& ! [X182] :
( ~ r1(X181,X182)
| p4(X182) )
& p4(X181) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren59])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren60_defn,definition,
! [X1,X183] :
( ren60(X1,X183)
<= ( ~ r1(X1,X183)
| ~ ( p5(X183)
& ! [X184] :
( ~ r1(X183,X184)
| p5(X184) ) )
| p4(X183)
| p5(X183)
| ~ ( p4(X183)
& ! [X185] :
( ~ r1(X183,X185)
| p4(X185) )
& p4(X183) ) ) ),
introduced(definition,[new_symbols(definition,[ren60])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren61_defn,definition,
! [X186,X187] :
( ren61(X186,X187)
<= ( ~ r1(X186,X187)
| p4(X187) ) ),
introduced(definition,[new_symbols(definition,[ren61])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren62_defn,definition,
! [X188,X189] :
( ren62(X188,X189)
<= ( ~ r1(X188,X189)
| p3(X189) ) ),
introduced(definition,[new_symbols(definition,[ren62])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren63_defn,definition,
! [X1,X190] :
( ren63(X1,X190)
<= ( ~ r1(X1,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ~ ( p4(X191)
& ! [X192] :
( ~ r1(X191,X192)
| p4(X192) ) )
| p3(X191) )
| p4(X190)
| ~ ( p3(X190)
& ! [X193] :
( ~ r1(X190,X193)
| p3(X193) )
& p3(X190) ) ) ),
introduced(definition,[new_symbols(definition,[ren63])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren64_defn,definition,
! [X1,X194] :
( ren64(X1,X194)
<= ( ~ r1(X1,X194)
| ~ ( p4(X194)
& ! [X195] :
( ~ r1(X194,X195)
| p4(X195) ) )
| p3(X194)
| ! [X196] :
( ~ r1(X194,X196)
| p4(X196)
| ~ ( p3(X196)
& ! [X197] :
( ~ r1(X196,X197)
| p3(X197) )
& p3(X196) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren64])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren65_defn,definition,
! [X1,X198] :
( ren65(X1,X198)
<= ( ~ r1(X1,X198)
| ~ ( p4(X198)
& ! [X199] :
( ~ r1(X198,X199)
| p4(X199) ) )
| p3(X198)
| p4(X198)
| ~ ( p3(X198)
& ! [X200] :
( ~ r1(X198,X200)
| p3(X200) )
& p3(X198) ) ) ),
introduced(definition,[new_symbols(definition,[ren65])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren66_defn,definition,
! [X201,X202] :
( ren66(X201,X202)
<= ( ~ r1(X201,X202)
| p3(X202) ) ),
introduced(definition,[new_symbols(definition,[ren66])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren67_defn,definition,
! [X203,X204] :
( ren67(X203,X204)
<= ( ~ r1(X203,X204)
| p2(X204) ) ),
introduced(definition,[new_symbols(definition,[ren67])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren68_defn,definition,
! [X1,X205] :
( ren68(X1,X205)
<= ( ~ r1(X1,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ~ ( p3(X206)
& ! [X207] :
( ~ r1(X206,X207)
| p3(X207) ) )
| p2(X206) )
| p3(X205)
| ~ ( p2(X205)
& ! [X208] :
( ~ r1(X205,X208)
| p2(X208) )
& p2(X205) ) ) ),
introduced(definition,[new_symbols(definition,[ren68])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren69_defn,definition,
! [X1,X209] :
( ren69(X1,X209)
<= ( ~ r1(X1,X209)
| ~ ( p3(X209)
& ! [X210] :
( ~ r1(X209,X210)
| p3(X210) ) )
| p2(X209)
| ! [X211] :
( ~ r1(X209,X211)
| p3(X211)
| ~ ( p2(X211)
& ! [X212] :
( ~ r1(X211,X212)
| p2(X212) )
& p2(X211) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren69])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren70_defn,definition,
! [X1,X213] :
( ren70(X1,X213)
<= ( ~ r1(X1,X213)
| ~ ( p3(X213)
& ! [X214] :
( ~ r1(X213,X214)
| p3(X214) ) )
| p2(X213)
| p3(X213)
| ~ ( p2(X213)
& ! [X215] :
( ~ r1(X213,X215)
| p2(X215) )
& p2(X213) ) ) ),
introduced(definition,[new_symbols(definition,[ren70])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren71_defn,definition,
! [X216,X217] :
( ren71(X216,X217)
<= ( ~ r1(X216,X217)
| p2(X217) ) ),
introduced(definition,[new_symbols(definition,[ren71])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren72_defn,definition,
! [X218,X219] :
( ren72(X218,X219)
<= ( ~ r1(X218,X219)
| p1(X219) ) ),
introduced(definition,[new_symbols(definition,[ren72])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren73_defn,definition,
! [X1,X220] :
( ren73(X1,X220)
<= ( ~ r1(X1,X220)
| ! [X221] :
( ~ r1(X220,X221)
| ~ ( p2(X221)
& ! [X222] :
( ~ r1(X221,X222)
| p2(X222) ) )
| p1(X221) )
| p2(X220)
| ~ ( p1(X220)
& ! [X223] :
( ~ r1(X220,X223)
| p1(X223) )
& p1(X220) ) ) ),
introduced(definition,[new_symbols(definition,[ren73])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren74_defn,definition,
! [X1,X224] :
( ren74(X1,X224)
<= ( ~ r1(X1,X224)
| ~ ( p2(X224)
& ! [X225] :
( ~ r1(X224,X225)
| p2(X225) ) )
| p1(X224)
| ! [X226] :
( ~ r1(X224,X226)
| p2(X226)
| ~ ( p1(X226)
& ! [X227] :
( ~ r1(X226,X227)
| p1(X227) )
& p1(X226) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren74])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren75_defn,definition,
! [X1,X228] :
( ren75(X1,X228)
<= ( ~ r1(X1,X228)
| ~ ( p2(X228)
& ! [X229] :
( ~ r1(X228,X229)
| p2(X229) ) )
| p1(X228)
| p2(X228)
| ~ ( p1(X228)
& ! [X230] :
( ~ r1(X228,X230)
| p1(X230) )
& p1(X228) ) ) ),
introduced(definition,[new_symbols(definition,[ren75])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ( p16(X2)
& ! [X3] : ren1(X2,X3) )
| p15(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p16(X4)
| ~ ( p15(X4)
& ! [X5] : ren2(X4,X5)
& p15(X4) ) )
| ~ ( ! [X6] : ren3(X1,X6)
& ! [X10] : ren4(X1,X10)
& ! [X14] : ren5(X1,X14) ) )
| ~ ( ! [X17] :
( ~ r1(X1,X17)
| ~ ( p15(X17)
& ! [X18] : ren6(X17,X18) )
| p14(X17) )
| ! [X19] :
( ~ r1(X1,X19)
| p15(X19)
| ~ ( p14(X19)
& ! [X20] : ren7(X19,X20)
& p14(X19) ) )
| ~ ( ! [X21] : ren8(X1,X21)
& ! [X25] : ren9(X1,X25)
& ! [X29] : ren10(X1,X29) ) )
| ~ ( ! [X32] :
( ~ r1(X1,X32)
| ~ ( p14(X32)
& ! [X33] : ren11(X32,X33) )
| p13(X32) )
| ! [X34] :
( ~ r1(X1,X34)
| p14(X34)
| ~ ( p13(X34)
& ! [X35] : ren12(X34,X35)
& p13(X34) ) )
| ~ ( ! [X36] : ren13(X1,X36)
& ! [X40] : ren14(X1,X40)
& ! [X44] : ren15(X1,X44) ) )
| ~ ( ! [X47] :
( ~ r1(X1,X47)
| ~ ( p13(X47)
& ! [X48] : ren16(X47,X48) )
| p12(X47) )
| ! [X49] :
( ~ r1(X1,X49)
| p13(X49)
| ~ ( p12(X49)
& ! [X50] : ren17(X49,X50)
& p12(X49) ) )
| ~ ( ! [X51] : ren18(X1,X51)
& ! [X55] : ren19(X1,X55)
& ! [X59] : ren20(X1,X59) ) )
| ~ ( ! [X62] :
( ~ r1(X1,X62)
| ~ ( p12(X62)
& ! [X63] : ren21(X62,X63) )
| p11(X62) )
| ! [X64] :
( ~ r1(X1,X64)
| p12(X64)
| ~ ( p11(X64)
& ! [X65] : ren22(X64,X65)
& p11(X64) ) )
| ~ ( ! [X66] : ren23(X1,X66)
& ! [X70] : ren24(X1,X70)
& ! [X74] : ren25(X1,X74) ) )
| ~ ( ! [X77] :
( ~ r1(X1,X77)
| ~ ( p11(X77)
& ! [X78] : ren26(X77,X78) )
| p10(X77) )
| ! [X79] :
( ~ r1(X1,X79)
| p11(X79)
| ~ ( p10(X79)
& ! [X80] : ren27(X79,X80)
& p10(X79) ) )
| ~ ( ! [X81] : ren28(X1,X81)
& ! [X85] : ren29(X1,X85)
& ! [X89] : ren30(X1,X89) ) )
| ~ ( ! [X92] :
( ~ r1(X1,X92)
| ~ ( p10(X92)
& ! [X93] : ren31(X92,X93) )
| p9(X92) )
| ! [X94] :
( ~ r1(X1,X94)
| p10(X94)
| ~ ( p9(X94)
& ! [X95] : ren32(X94,X95)
& p9(X94) ) )
| ~ ( ! [X96] : ren33(X1,X96)
& ! [X100] : ren34(X1,X100)
& ! [X104] : ren35(X1,X104) ) )
| ~ ( ! [X107] :
( ~ r1(X1,X107)
| ~ ( p9(X107)
& ! [X108] : ren36(X107,X108) )
| p8(X107) )
| ! [X109] :
( ~ r1(X1,X109)
| p9(X109)
| ~ ( p8(X109)
& ! [X110] : ren37(X109,X110)
& p8(X109) ) )
| ~ ( ! [X111] : ren38(X1,X111)
& ! [X115] : ren39(X1,X115)
& ! [X119] : ren40(X1,X119) ) )
| ~ ( ! [X122] :
( ~ r1(X1,X122)
| ~ ( p8(X122)
& ! [X123] : ren41(X122,X123) )
| p7(X122) )
| ! [X124] :
( ~ r1(X1,X124)
| p8(X124)
| ~ ( p7(X124)
& ! [X125] : ren42(X124,X125)
& p7(X124) ) )
| ~ ( ! [X126] : ren43(X1,X126)
& ! [X130] : ren44(X1,X130)
& ! [X134] : ren45(X1,X134) ) )
| ~ ( ! [X137] :
( ~ r1(X1,X137)
| ~ ( p7(X137)
& ! [X138] : ren46(X137,X138) )
| p6(X137) )
| ! [X139] :
( ~ r1(X1,X139)
| p7(X139)
| ~ ( p6(X139)
& ! [X140] : ren47(X139,X140)
& p6(X139) ) )
| ~ ( ! [X141] : ren48(X1,X141)
& ! [X145] : ren49(X1,X145)
& ! [X149] : ren50(X1,X149) ) )
| ! [X152] :
( ~ r1(X1,X152)
| p15(X152)
| ~ ( ! [X153] :
( ~ r1(X152,X153)
| p15(X153) )
& p15(X152) ) )
| ! [X154] :
( ~ r1(X1,X154)
| p15(X154)
| ~ ( ! [X155] :
( ~ r1(X154,X155)
| p15(X155) )
& p15(X154) ) )
| ~ ( ! [X156] :
( ~ r1(X1,X156)
| ~ ( p6(X156)
& ! [X157] : ren51(X156,X157) )
| p5(X156) )
| ! [X158] :
( ~ r1(X1,X158)
| p6(X158)
| ~ ( p5(X158)
& ! [X159] : ren52(X158,X159)
& p5(X158) ) )
| ~ ( ! [X160] : ren53(X1,X160)
& ! [X164] : ren54(X1,X164)
& ! [X168] : ren55(X1,X168) ) )
| ~ ( ! [X171] :
( ~ r1(X1,X171)
| ~ ( p5(X171)
& ! [X172] : ren56(X171,X172) )
| p4(X171) )
| ! [X173] :
( ~ r1(X1,X173)
| p5(X173)
| ~ ( p4(X173)
& ! [X174] : ren57(X173,X174)
& p4(X173) ) )
| ~ ( ! [X175] : ren58(X1,X175)
& ! [X179] : ren59(X1,X179)
& ! [X183] : ren60(X1,X183) ) )
| ~ ( ! [X186] :
( ~ r1(X1,X186)
| ~ ( p4(X186)
& ! [X187] : ren61(X186,X187) )
| p3(X186) )
| ! [X188] :
( ~ r1(X1,X188)
| p4(X188)
| ~ ( p3(X188)
& ! [X189] : ren62(X188,X189)
& p3(X188) ) )
| ~ ( ! [X190] : ren63(X1,X190)
& ! [X194] : ren64(X1,X194)
& ! [X198] : ren65(X1,X198) ) )
| ~ ( ! [X201] :
( ~ r1(X1,X201)
| ~ ( p3(X201)
& ! [X202] : ren66(X201,X202) )
| p2(X201) )
| ! [X203] :
( ~ r1(X1,X203)
| p3(X203)
| ~ ( p2(X203)
& ! [X204] : ren67(X203,X204)
& p2(X203) ) )
| ~ ( ! [X205] : ren68(X1,X205)
& ! [X209] : ren69(X1,X209)
& ! [X213] : ren70(X1,X213) ) )
| ~ ( ! [X216] :
( ~ r1(X1,X216)
| ~ ( p2(X216)
& ! [X217] : ren71(X216,X217) )
| p1(X216) )
| ! [X218] :
( ~ r1(X1,X218)
| p2(X218)
| ~ ( p1(X218)
& ! [X219] : ren72(X218,X219)
& p1(X218) ) )
| ~ ( ! [X220] : ren73(X1,X220)
& ! [X224] : ren74(X1,X224)
& ! [X228] : ren75(X1,X228) ) ) ),
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,ren51_defn,ren52_defn,ren53_defn,ren54_defn,ren55_defn,ren56_defn,ren57_defn,ren58_defn,ren59_defn,ren60_defn,ren61_defn,ren62_defn,ren63_defn,ren64_defn,ren65_defn,ren66_defn,ren67_defn,ren68_defn,ren69_defn,ren70_defn,ren71_defn,ren72_defn,ren73_defn,ren74_defn,ren75_defn]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ( ! [X2] :
( ~ r1(X1,X2)
| ~ p16(X2)
| ? [X3] : ~ ren1(X2,X3)
| p15(X2) )
| ! [X4] :
( ~ r1(X1,X4)
| p16(X4)
| ~ p15(X4)
| ? [X5] : ~ ren2(X4,X5)
| ~ p15(X4) )
| ? [X6] : ~ ren3(X1,X6)
| ? [X7] : ~ ren4(X1,X7)
| ? [X8] : ~ ren5(X1,X8) )
& ( ! [X9] :
( ~ r1(X1,X9)
| ~ p15(X9)
| ? [X10] : ~ ren6(X9,X10)
| p14(X9) )
| ! [X11] :
( ~ r1(X1,X11)
| p15(X11)
| ~ p14(X11)
| ? [X12] : ~ ren7(X11,X12)
| ~ p14(X11) )
| ? [X13] : ~ ren8(X1,X13)
| ? [X14] : ~ ren9(X1,X14)
| ? [X15] : ~ ren10(X1,X15) )
& ( ! [X16] :
( ~ r1(X1,X16)
| ~ p14(X16)
| ? [X17] : ~ ren11(X16,X17)
| p13(X16) )
| ! [X18] :
( ~ r1(X1,X18)
| p14(X18)
| ~ p13(X18)
| ? [X19] : ~ ren12(X18,X19)
| ~ p13(X18) )
| ? [X20] : ~ ren13(X1,X20)
| ? [X21] : ~ ren14(X1,X21)
| ? [X22] : ~ ren15(X1,X22) )
& ( ! [X23] :
( ~ r1(X1,X23)
| ~ p13(X23)
| ? [X24] : ~ ren16(X23,X24)
| p12(X23) )
| ! [X25] :
( ~ r1(X1,X25)
| p13(X25)
| ~ p12(X25)
| ? [X26] : ~ ren17(X25,X26)
| ~ p12(X25) )
| ? [X27] : ~ ren18(X1,X27)
| ? [X28] : ~ ren19(X1,X28)
| ? [X29] : ~ ren20(X1,X29) )
& ( ! [X30] :
( ~ r1(X1,X30)
| ~ p12(X30)
| ? [X31] : ~ ren21(X30,X31)
| p11(X30) )
| ! [X32] :
( ~ r1(X1,X32)
| p12(X32)
| ~ p11(X32)
| ? [X33] : ~ ren22(X32,X33)
| ~ p11(X32) )
| ? [X34] : ~ ren23(X1,X34)
| ? [X35] : ~ ren24(X1,X35)
| ? [X36] : ~ ren25(X1,X36) )
& ( ! [X37] :
( ~ r1(X1,X37)
| ~ p11(X37)
| ? [X38] : ~ ren26(X37,X38)
| p10(X37) )
| ! [X39] :
( ~ r1(X1,X39)
| p11(X39)
| ~ p10(X39)
| ? [X40] : ~ ren27(X39,X40)
| ~ p10(X39) )
| ? [X41] : ~ ren28(X1,X41)
| ? [X42] : ~ ren29(X1,X42)
| ? [X43] : ~ ren30(X1,X43) )
& ( ! [X44] :
( ~ r1(X1,X44)
| ~ p10(X44)
| ? [X45] : ~ ren31(X44,X45)
| p9(X44) )
| ! [X46] :
( ~ r1(X1,X46)
| p10(X46)
| ~ p9(X46)
| ? [X47] : ~ ren32(X46,X47)
| ~ p9(X46) )
| ? [X48] : ~ ren33(X1,X48)
| ? [X49] : ~ ren34(X1,X49)
| ? [X50] : ~ ren35(X1,X50) )
& ( ! [X51] :
( ~ r1(X1,X51)
| ~ p9(X51)
| ? [X52] : ~ ren36(X51,X52)
| p8(X51) )
| ! [X53] :
( ~ r1(X1,X53)
| p9(X53)
| ~ p8(X53)
| ? [X54] : ~ ren37(X53,X54)
| ~ p8(X53) )
| ? [X55] : ~ ren38(X1,X55)
| ? [X56] : ~ ren39(X1,X56)
| ? [X57] : ~ ren40(X1,X57) )
& ( ! [X58] :
( ~ r1(X1,X58)
| ~ p8(X58)
| ? [X59] : ~ ren41(X58,X59)
| p7(X58) )
| ! [X60] :
( ~ r1(X1,X60)
| p8(X60)
| ~ p7(X60)
| ? [X61] : ~ ren42(X60,X61)
| ~ p7(X60) )
| ? [X62] : ~ ren43(X1,X62)
| ? [X63] : ~ ren44(X1,X63)
| ? [X64] : ~ ren45(X1,X64) )
& ( ! [X65] :
( ~ r1(X1,X65)
| ~ p7(X65)
| ? [X66] : ~ ren46(X65,X66)
| p6(X65) )
| ! [X67] :
( ~ r1(X1,X67)
| p7(X67)
| ~ p6(X67)
| ? [X68] : ~ ren47(X67,X68)
| ~ p6(X67) )
| ? [X69] : ~ ren48(X1,X69)
| ? [X70] : ~ ren49(X1,X70)
| ? [X71] : ~ ren50(X1,X71) )
& ? [X72] :
( r1(X1,X72)
& ~ p15(X72)
& ! [X73] :
( ~ r1(X72,X73)
| p15(X73) )
& p15(X72) )
& ? [X74] :
( r1(X1,X74)
& ~ p15(X74)
& ! [X75] :
( ~ r1(X74,X75)
| p15(X75) )
& p15(X74) )
& ( ! [X76] :
( ~ r1(X1,X76)
| ~ p6(X76)
| ? [X77] : ~ ren51(X76,X77)
| p5(X76) )
| ! [X78] :
( ~ r1(X1,X78)
| p6(X78)
| ~ p5(X78)
| ? [X79] : ~ ren52(X78,X79)
| ~ p5(X78) )
| ? [X80] : ~ ren53(X1,X80)
| ? [X81] : ~ ren54(X1,X81)
| ? [X82] : ~ ren55(X1,X82) )
& ( ! [X83] :
( ~ r1(X1,X83)
| ~ p5(X83)
| ? [X84] : ~ ren56(X83,X84)
| p4(X83) )
| ! [X85] :
( ~ r1(X1,X85)
| p5(X85)
| ~ p4(X85)
| ? [X86] : ~ ren57(X85,X86)
| ~ p4(X85) )
| ? [X87] : ~ ren58(X1,X87)
| ? [X88] : ~ ren59(X1,X88)
| ? [X89] : ~ ren60(X1,X89) )
& ( ! [X90] :
( ~ r1(X1,X90)
| ~ p4(X90)
| ? [X91] : ~ ren61(X90,X91)
| p3(X90) )
| ! [X92] :
( ~ r1(X1,X92)
| p4(X92)
| ~ p3(X92)
| ? [X93] : ~ ren62(X92,X93)
| ~ p3(X92) )
| ? [X94] : ~ ren63(X1,X94)
| ? [X95] : ~ ren64(X1,X95)
| ? [X96] : ~ ren65(X1,X96) )
& ( ! [X97] :
( ~ r1(X1,X97)
| ~ p3(X97)
| ? [X98] : ~ ren66(X97,X98)
| p2(X97) )
| ! [X99] :
( ~ r1(X1,X99)
| p3(X99)
| ~ p2(X99)
| ? [X100] : ~ ren67(X99,X100)
| ~ p2(X99) )
| ? [X101] : ~ ren68(X1,X101)
| ? [X102] : ~ ren69(X1,X102)
| ? [X103] : ~ ren70(X1,X103) )
& ( ! [X104] :
( ~ r1(X1,X104)
| ~ p2(X104)
| ? [X105] : ~ ren71(X104,X105)
| p1(X104) )
| ! [X106] :
( ~ r1(X1,X106)
| p2(X106)
| ~ p1(X106)
| ? [X107] : ~ ren72(X106,X107)
| ~ p1(X106) )
| ? [X108] : ~ ren73(X1,X108)
| ? [X109] : ~ ren74(X1,X109)
| ? [X110] : ~ ren75(X1,X110) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ( ! [X2] :
( ~ r1(skc31,X2)
| ~ p16(X2)
| ~ ren1(X2,skf32(X2))
| p15(X2) )
| ! [X4] :
( ~ r1(skc31,X4)
| p16(X4)
| ~ p15(X4)
| ~ ren2(X4,skf33(X4))
| ~ p15(X4) )
| ~ ren3(skc31,skc34)
| ~ ren4(skc31,skc35)
| ~ ren5(skc31,skc36) )
& ( ! [X9] :
( ~ r1(skc31,X9)
| ~ p15(X9)
| ~ ren6(X9,skf37(X9))
| p14(X9) )
| ! [X11] :
( ~ r1(skc31,X11)
| p15(X11)
| ~ p14(X11)
| ~ ren7(X11,skf38(X11))
| ~ p14(X11) )
| ~ ren8(skc31,skc39)
| ~ ren9(skc31,skc40)
| ~ ren10(skc31,skc41) )
& ( ! [X16] :
( ~ r1(skc31,X16)
| ~ p14(X16)
| ~ ren11(X16,skf42(X16))
| p13(X16) )
| ! [X18] :
( ~ r1(skc31,X18)
| p14(X18)
| ~ p13(X18)
| ~ ren12(X18,skf43(X18))
| ~ p13(X18) )
| ~ ren13(skc31,skc44)
| ~ ren14(skc31,skc45)
| ~ ren15(skc31,skc46) )
& ( ! [X23] :
( ~ r1(skc31,X23)
| ~ p13(X23)
| ~ ren16(X23,skf47(X23))
| p12(X23) )
| ! [X25] :
( ~ r1(skc31,X25)
| p13(X25)
| ~ p12(X25)
| ~ ren17(X25,skf48(X25))
| ~ p12(X25) )
| ~ ren18(skc31,skc49)
| ~ ren19(skc31,skc50)
| ~ ren20(skc31,skc51) )
& ( ! [X30] :
( ~ r1(skc31,X30)
| ~ p12(X30)
| ~ ren21(X30,skf52(X30))
| p11(X30) )
| ! [X32] :
( ~ r1(skc31,X32)
| p12(X32)
| ~ p11(X32)
| ~ ren22(X32,skf53(X32))
| ~ p11(X32) )
| ~ ren23(skc31,skc54)
| ~ ren24(skc31,skc55)
| ~ ren25(skc31,skc56) )
& ( ! [X37] :
( ~ r1(skc31,X37)
| ~ p11(X37)
| ~ ren26(X37,skf57(X37))
| p10(X37) )
| ! [X39] :
( ~ r1(skc31,X39)
| p11(X39)
| ~ p10(X39)
| ~ ren27(X39,skf58(X39))
| ~ p10(X39) )
| ~ ren28(skc31,skc59)
| ~ ren29(skc31,skc60)
| ~ ren30(skc31,skc61) )
& ( ! [X44] :
( ~ r1(skc31,X44)
| ~ p10(X44)
| ~ ren31(X44,skf62(X44))
| p9(X44) )
| ! [X46] :
( ~ r1(skc31,X46)
| p10(X46)
| ~ p9(X46)
| ~ ren32(X46,skf63(X46))
| ~ p9(X46) )
| ~ ren33(skc31,skc64)
| ~ ren34(skc31,skc65)
| ~ ren35(skc31,skc66) )
& ( ! [X51] :
( ~ r1(skc31,X51)
| ~ p9(X51)
| ~ ren36(X51,skf67(X51))
| p8(X51) )
| ! [X53] :
( ~ r1(skc31,X53)
| p9(X53)
| ~ p8(X53)
| ~ ren37(X53,skf68(X53))
| ~ p8(X53) )
| ~ ren38(skc31,skc69)
| ~ ren39(skc31,skc70)
| ~ ren40(skc31,skc71) )
& ( ! [X58] :
( ~ r1(skc31,X58)
| ~ p8(X58)
| ~ ren41(X58,skf72(X58))
| p7(X58) )
| ! [X60] :
( ~ r1(skc31,X60)
| p8(X60)
| ~ p7(X60)
| ~ ren42(X60,skf73(X60))
| ~ p7(X60) )
| ~ ren43(skc31,skc74)
| ~ ren44(skc31,skc75)
| ~ ren45(skc31,skc76) )
& ( ! [X65] :
( ~ r1(skc31,X65)
| ~ p7(X65)
| ~ ren46(X65,skf77(X65))
| p6(X65) )
| ! [X67] :
( ~ r1(skc31,X67)
| p7(X67)
| ~ p6(X67)
| ~ ren47(X67,skf78(X67))
| ~ p6(X67) )
| ~ ren48(skc31,skc79)
| ~ ren49(skc31,skc80)
| ~ ren50(skc31,skc81) )
& r1(skc31,skc82)
& ~ p15(skc82)
& ! [X73] :
( ~ r1(skc82,X73)
| p15(X73) )
& p15(skc82)
& r1(skc31,skc83)
& ~ p15(skc83)
& ! [X75] :
( ~ r1(skc83,X75)
| p15(X75) )
& p15(skc83)
& ( ! [X76] :
( ~ r1(skc31,X76)
| ~ p6(X76)
| ~ ren51(X76,skf84(X76))
| p5(X76) )
| ! [X78] :
( ~ r1(skc31,X78)
| p6(X78)
| ~ p5(X78)
| ~ ren52(X78,skf85(X78))
| ~ p5(X78) )
| ~ ren53(skc31,skc86)
| ~ ren54(skc31,skc87)
| ~ ren55(skc31,skc88) )
& ( ! [X83] :
( ~ r1(skc31,X83)
| ~ p5(X83)
| ~ ren56(X83,skf89(X83))
| p4(X83) )
| ! [X85] :
( ~ r1(skc31,X85)
| p5(X85)
| ~ p4(X85)
| ~ ren57(X85,skf90(X85))
| ~ p4(X85) )
| ~ ren58(skc31,skc91)
| ~ ren59(skc31,skc92)
| ~ ren60(skc31,skc93) )
& ( ! [X90] :
( ~ r1(skc31,X90)
| ~ p4(X90)
| ~ ren61(X90,skf94(X90))
| p3(X90) )
| ! [X92] :
( ~ r1(skc31,X92)
| p4(X92)
| ~ p3(X92)
| ~ ren62(X92,skf95(X92))
| ~ p3(X92) )
| ~ ren63(skc31,skc96)
| ~ ren64(skc31,skc97)
| ~ ren65(skc31,skc98) )
& ( ! [X97] :
( ~ r1(skc31,X97)
| ~ p3(X97)
| ~ ren66(X97,skf99(X97))
| p2(X97) )
| ! [X99] :
( ~ r1(skc31,X99)
| p3(X99)
| ~ p2(X99)
| ~ ren67(X99,skf100(X99))
| ~ p2(X99) )
| ~ ren68(skc31,skc101)
| ~ ren69(skc31,skc102)
| ~ ren70(skc31,skc103) )
& ( ! [X104] :
( ~ r1(skc31,X104)
| ~ p2(X104)
| ~ ren71(X104,skf104(X104))
| p1(X104) )
| ! [X106] :
( ~ r1(skc31,X106)
| p2(X106)
| ~ p1(X106)
| ~ ren72(X106,skf105(X106))
| ~ p1(X106) )
| ~ ren73(skc31,skc106)
| ~ ren74(skc31,skc107)
| ~ ren75(skc31,skc108) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[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,skf57,skf58,skc59,skc60,skc61,skf62,skf63,skc64,skc65,skc66,skf67,skf68,skc69,skc70,skc71,skf72,skf73,skc74,skc75,skc76,skf77,skf78,skc79,skc80,skc81,skc82,skc83,skf84,skf85,skc86,skc87,skc88,skf89,skf90,skc91,skc92,skc93,skf94,skf95,skc96,skc97,skc98,skf99,skf100,skc101,skc102,skc103,skf104,skf105,skc106,skc107,skc108]),skolemize(X1,skc31),skolemize(X3,skf32(X2)),skolemize(X5,skf33(X4)),skolemize(X6,skc34),skolemize(X7,skc35),skolemize(X8,skc36),skolemize(X10,skf37(X9)),skolemize(X12,skf38(X11)),skolemize(X13,skc39),skolemize(X14,skc40),skolemize(X15,skc41),skolemize(X17,skf42(X16)),skolemize(X19,skf43(X18)),skolemize(X20,skc44),skolemize(X21,skc45),skolemize(X22,skc46),skolemize(X24,skf47(X23)),skolemize(X26,skf48(X25)),skolemize(X27,skc49),skolemize(X28,skc50),skolemize(X29,skc51),skolemize(X31,skf52(X30)),skolemize(X33,skf53(X32)),skolemize(X34,skc54),skolemize(X35,skc55),skolemize(X36,skc56),skolemize(X38,skf57(X37)),skolemize(X40,skf58(X39)),skolemize(X41,skc59),skolemize(X42,skc60),skolemize(X43,skc61),skolemize(X45,skf62(X44)),skolemize(X47,skf63(X46)),skolemize(X48,skc64),skolemize(X49,skc65),skolemize(X50,skc66),skolemize(X52,skf67(X51)),skolemize(X54,skf68(X53)),skolemize(X55,skc69),skolemize(X56,skc70),skolemize(X57,skc71),skolemize(X59,skf72(X58)),skolemize(X61,skf73(X60)),skolemize(X62,skc74),skolemize(X63,skc75),skolemize(X64,skc76),skolemize(X66,skf77(X65)),skolemize(X68,skf78(X67)),skolemize(X69,skc79),skolemize(X70,skc80),skolemize(X71,skc81),skolemize(X72,skc82),skolemize(X74,skc83),skolemize(X77,skf84(X76)),skolemize(X79,skf85(X78)),skolemize(X80,skc86),skolemize(X81,skc87),skolemize(X82,skc88),skolemize(X84,skf89(X83)),skolemize(X86,skf90(X85)),skolemize(X87,skc91),skolemize(X88,skc92),skolemize(X89,skc93),skolemize(X91,skf94(X90)),skolemize(X93,skf95(X92)),skolemize(X94,skc96),skolemize(X95,skc97),skolemize(X96,skc98),skolemize(X98,skf99(X97)),skolemize(X100,skf100(X99)),skolemize(X101,skc101),skolemize(X102,skc102),skolemize(X103,skc103),skolemize(X105,skf104(X104)),skolemize(X107,skf105(X106)),skolemize(X108,skc106),skolemize(X109,skc107),skolemize(X110,skc108)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_468,plain,
p15(skc83),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_466,plain,
~ p15(skc83),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_515,plain,
$false,
inference(resolution,[status(thm)],[c_468,c_466]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n014.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 23:03:57 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36
% 0.12/0.36 % Input Clauses:
% 0.12/0.36 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.12/0.36 % 2:2:2:INP:TopTop: p16(x0) -> ren1(x1,x0)
% 0.12/0.36 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.12/0.36 % 4:2:2:INP:TopTop: p15(x0) -> ren2(x1,x0)
% 0.12/0.36 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.12/0.36 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.12/0.36 % 7:2:2:INP:TopTop: -> p16(skf1(x0)),ren3(x1,x0)
% 0.12/0.36 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p16(x1),ren3(x2,x0)
% 0.12/0.36 % 9:2:2:INP:TopTop: p15(skf1(x0)) -> ren3(x1,x0)
% 0.12/0.36 % 10:2:2:INP:TopTop: p16(x0) -> ren3(x1,x0)
% 0.12/0.36 % 11:2:2:INP:TopTop: -> p15(x0),ren3(x1,x0)
% 0.12/0.36 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren3(x2,x0)
% 0.12/0.36 % 13:2:2:INP:TopTop: -> p15(x0),ren3(x1,x0)
% 0.12/0.36 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.12/0.36 % 15:2:2:INP:TopTop: -> p16(x0),ren4(x1,x0)
% 0.12/0.36 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p16(x1),ren4(x2,x0)
% 0.12/0.36 % 17:2:2:INP:TopTop: p15(x0) -> ren4(x1,x0)
% 0.12/0.36 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.12/0.36 % 19:2:2:INP:TopTop: p16(skf2(x0)) -> ren4(x1,x0)
% 0.12/0.36 % 20:2:2:INP:TopTop: -> p15(skf2(x0)),ren4(x1,x0)
% 0.12/0.36 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p15(x1),ren4(x2,x0)
% 0.12/0.36 % 22:2:2:INP:TopTop: -> p15(skf2(x0)),ren4(x1,x0)
% 0.12/0.36 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.12/0.36 % 24:2:2:INP:TopTop: -> p16(x0),ren5(x1,x0)
% 0.12/0.36 % 25:3:3:INP:TopTopTop: r1(x0,x1) -> p16(x1),ren5(x2,x0)
% 0.12/0.36 % 26:2:2:INP:TopTop: p15(x0) -> ren5(x1,x0)
% 0.12/0.36 % 27:2:2:INP:TopTop: p16(x0) -> ren5(x1,x0)
% 0.12/0.36 % 28:2:2:INP:TopTop: -> p15(x0),ren5(x1,x0)
% 0.12/0.36 % 29:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren5(x2,x0)
% 0.12/0.36 % 30:2:2:INP:TopTop: -> p15(x0),ren5(x1,x0)
% 0.12/0.36 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.12/0.36 % 32:2:2:INP:TopTop: p15(x0) -> ren6(x1,x0)
% 0.12/0.36 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.12/0.36 % 34:2:2:INP:TopTop: p14(x0) -> ren7(x1,x0)
% 0.12/0.36 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.12/0.36 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.12/0.36 % 37:2:2:INP:TopTop: -> p15(skf3(x0)),ren8(x1,x0)
% 0.12/0.36 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p15(x1),ren8(x2,x0)
% 0.12/0.36 % 39:2:2:INP:TopTop: p14(skf3(x0)) -> ren8(x1,x0)
% 0.12/0.36 % 40:2:2:INP:TopTop: p15(x0) -> ren8(x1,x0)
% 0.12/0.36 % 41:2:2:INP:TopTop: -> p14(x0),ren8(x1,x0)
% 0.12/0.36 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren8(x2,x0)
% 0.12/0.36 % 43:2:2:INP:TopTop: -> p14(x0),ren8(x1,x0)
% 0.12/0.36 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.12/0.36 % 45:2:2:INP:TopTop: -> p15(x0),ren9(x1,x0)
% 0.12/0.36 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren9(x2,x0)
% 0.12/0.36 % 47:2:2:INP:TopTop: p14(x0) -> ren9(x1,x0)
% 0.12/0.36 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.12/0.36 % 49:2:2:INP:TopTop: p15(skf4(x0)) -> ren9(x1,x0)
% 0.12/0.36 % 50:2:2:INP:TopTop: -> p14(skf4(x0)),ren9(x1,x0)
% 0.12/0.36 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p14(x1),ren9(x2,x0)
% 0.12/0.36 % 52:2:2:INP:TopTop: -> p14(skf4(x0)),ren9(x1,x0)
% 0.12/0.36 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.12/0.36 % 54:2:2:INP:TopTop: -> p15(x0),ren10(x1,x0)
% 0.12/0.36 % 55:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren10(x2,x0)
% 0.12/0.36 % 56:2:2:INP:TopTop: p14(x0) -> ren10(x1,x0)
% 0.12/0.36 % 57:2:2:INP:TopTop: p15(x0) -> ren10(x1,x0)
% 0.12/0.36 % 58:2:2:INP:TopTop: -> p14(x0),ren10(x1,x0)
% 0.12/0.36 % 59:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren10(x2,x0)
% 0.12/0.36 % 60:2:2:INP:TopTop: -> p14(x0),ren10(x1,x0)
% 0.12/0.36 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.12/0.36 % 62:2:2:INP:TopTop: p14(x0) -> ren11(x1,x0)
% 0.12/0.36 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.12/0.36 % 64:2:2:INP:TopTop: p13(x0) -> ren12(x1,x0)
% 0.12/0.36 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.12/0.36 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.12/0.36 % 67:2:2:INP:TopTop: -> p14(skf5(x0)),ren13(x1,x0)
% 0.12/0.36 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p14(x1),ren13(x2,x0)
% 0.12/0.36 % 69:2:2:INP:TopTop: p13(skf5(x0)) -> ren13(x1,x0)
% 0.12/0.36 % 70:2:2:INP:TopTop: p14(x0) -> ren13(x1,x0)
% 0.12/0.36 % 71:2:2:INP:TopTop: -> p13(x0),ren13(x1,x0)
% 0.12/0.36 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren13(x2,x0)
% 0.12/0.36 % 73:2:2:INP:TopTop: -> p13(x0),ren13(x1,x0)
% 0.12/0.36 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.12/0.36 % 75:2:2:INP:TopTop: -> p14(x0),ren14(x1,x0)
% 0.12/0.36 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren14(x2,x0)
% 0.12/0.36 % 77:2:2:INP:TopTop: p13(x0) -> ren14(x1,x0)
% 0.12/0.36 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.12/0.36 % 79:2:2:INP:TopTop: p14(skf6(x0)) -> ren14(x1,x0)
% 0.12/0.36 % 80:2:2:INP:TopTop: -> p13(skf6(x0)),ren14(x1,x0)
% 0.12/0.36 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p13(x1),ren14(x2,x0)
% 0.12/0.36 % 82:2:2:INP:TopTop: -> p13(skf6(x0)),ren14(x1,x0)
% 0.12/0.36 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.12/0.36 % 84:2:2:INP:TopTop: -> p14(x0),ren15(x1,x0)
% 0.12/0.36 % 85:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren15(x2,x0)
% 0.12/0.36 % 86:2:2:INP:TopTop: p13(x0) -> ren15(x1,x0)
% 0.12/0.36 % 87:2:2:INP:TopTop: p14(x0) -> ren15(x1,x0)
% 0.12/0.36 % 88:2:2:INP:TopTop: -> p13(x0),ren15(x1,x0)
% 0.12/0.36 % 89:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren15(x2,x0)
% 0.12/0.36 % 90:2:2:INP:TopTop: -> p13(x0),ren15(x1,x0)
% 0.12/0.36 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.12/0.36 % 92:2:2:INP:TopTop: p13(x0) -> ren16(x1,x0)
% 0.12/0.36 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.12/0.36 % 94:2:2:INP:TopTop: p12(x0) -> ren17(x1,x0)
% 0.12/0.36 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.12/0.36 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.12/0.36 % 97:2:2:INP:TopTop: -> p13(skf7(x0)),ren18(x1,x0)
% 0.12/0.36 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p13(x1),ren18(x2,x0)
% 0.12/0.36 % 99:2:2:INP:TopTop: p12(skf7(x0)) -> ren18(x1,x0)
% 0.12/0.36 % 100:2:2:INP:TopTop: p13(x0) -> ren18(x1,x0)
% 0.12/0.36 % 101:2:2:INP:TopTop: -> p12(x0),ren18(x1,x0)
% 0.12/0.36 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren18(x2,x0)
% 0.12/0.36 % 103:2:2:INP:TopTop: -> p12(x0),ren18(x1,x0)
% 0.12/0.36 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.12/0.36 % 105:2:2:INP:TopTop: -> p13(x0),ren19(x1,x0)
% 0.12/0.36 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren19(x2,x0)
% 0.12/0.36 % 107:2:2:INP:TopTop: p12(x0) -> ren19(x1,x0)
% 0.12/0.36 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.12/0.36 % 109:2:2:INP:TopTop: p13(skf8(x0)) -> ren19(x1,x0)
% 0.12/0.36 % 110:2:2:INP:TopTop: -> p12(skf8(x0)),ren19(x1,x0)
% 0.12/0.36 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p12(x1),ren19(x2,x0)
% 0.12/0.36 % 112:2:2:INP:TopTop: -> p12(skf8(x0)),ren19(x1,x0)
% 0.12/0.36 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.12/0.36 % 114:2:2:INP:TopTop: -> p13(x0),ren20(x1,x0)
% 0.12/0.36 % 115:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren20(x2,x0)
% 0.12/0.36 % 116:2:2:INP:TopTop: p12(x0) -> ren20(x1,x0)
% 0.12/0.36 % 117:2:2:INP:TopTop: p13(x0) -> ren20(x1,x0)
% 0.12/0.36 % 118:2:2:INP:TopTop: -> p12(x0),ren20(x1,x0)
% 0.12/0.36 % 119:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren20(x2,x0)
% 0.12/0.36 % 120:2:2:INP:TopTop: -> p12(x0),ren20(x1,x0)
% 0.12/0.36 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.12/0.36 % 122:2:2:INP:TopTop: p12(x0) -> ren21(x1,x0)
% 0.12/0.36 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.12/0.36 % 124:2:2:INP:TopTop: p11(x0) -> ren22(x1,x0)
% 0.12/0.36 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.12/0.36 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.12/0.36 % 127:2:2:INP:TopTop: -> p12(skf9(x0)),ren23(x1,x0)
% 0.12/0.36 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p12(x1),ren23(x2,x0)
% 0.12/0.36 % 129:2:2:INP:TopTop: p11(skf9(x0)) -> ren23(x1,x0)
% 0.12/0.36 % 130:2:2:INP:TopTop: p12(x0) -> ren23(x1,x0)
% 0.12/0.36 % 131:2:2:INP:TopTop: -> p11(x0),ren23(x1,x0)
% 0.12/0.36 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren23(x2,x0)
% 0.12/0.36 % 133:2:2:INP:TopTop: -> p11(x0),ren23(x1,x0)
% 0.12/0.36 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.12/0.36 % 135:2:2:INP:TopTop: -> p12(x0),ren24(x1,x0)
% 0.12/0.36 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren24(x2,x0)
% 0.12/0.36 % 137:2:2:INP:TopTop: p11(x0) -> ren24(x1,x0)
% 0.12/0.36 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.12/0.36 % 139:2:2:INP:TopTop: p12(skf10(x0)) -> ren24(x1,x0)
% 0.12/0.36 % 140:2:2:INP:TopTop: -> p11(skf10(x0)),ren24(x1,x0)
% 0.12/0.36 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p11(x1),ren24(x2,x0)
% 0.12/0.36 % 142:2:2:INP:TopTop: -> p11(skf10(x0)),ren24(x1,x0)
% 0.12/0.36 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.12/0.36 % 144:2:2:INP:TopTop: -> p12(x0),ren25(x1,x0)
% 0.12/0.36 % 145:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren25(x2,x0)
% 0.12/0.36 % 146:2:2:INP:TopTop: p11(x0) -> ren25(x1,x0)
% 0.12/0.36 % 147:2:2:INP:TopTop: p12(x0) -> ren25(x1,x0)
% 0.12/0.36 % 148:2:2:INP:TopTop: -> p11(x0),ren25(x1,x0)
% 0.12/0.36 % 149:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren25(x2,x0)
% 0.12/0.36 % 150:2:2:INP:TopTop: -> p11(x0),ren25(x1,x0)
% 0.12/0.36 % 151:2:2:INP:TopTop: -> r1(x0,x1),ren26(x0,x1)
% 0.12/0.36 % 152:2:2:INP:TopTop: p11(x0) -> ren26(x1,x0)
% 0.12/0.36 % 153:2:2:INP:TopTop: -> r1(x0,x1),ren27(x0,x1)
% 0.12/0.36 % 154:2:2:INP:TopTop: p10(x0) -> ren27(x1,x0)
% 0.12/0.36 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren28(x0,x1)
% 0.12/0.36 % 156:2:2:INP:TopTop: -> r1(x0,skf11(x0)),ren28(x1,x0)
% 0.12/0.36 % 157:2:2:INP:TopTop: -> p11(skf11(x0)),ren28(x1,x0)
% 0.12/0.36 % 158:3:3:INP:TopTopTop: r1(skf11(x0),x1) -> p11(x1),ren28(x2,x0)
% 0.12/0.36 % 159:2:2:INP:TopTop: p10(skf11(x0)) -> ren28(x1,x0)
% 0.12/0.36 % 160:2:2:INP:TopTop: p11(x0) -> ren28(x1,x0)
% 0.12/0.36 % 161:2:2:INP:TopTop: -> p10(x0),ren28(x1,x0)
% 0.12/0.36 % 162:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren28(x2,x0)
% 0.12/0.36 % 163:2:2:INP:TopTop: -> p10(x0),ren28(x1,x0)
% 0.12/0.36 % 164:2:2:INP:TopTop: -> r1(x0,x1),ren29(x0,x1)
% 0.12/0.36 % 165:2:2:INP:TopTop: -> p11(x0),ren29(x1,x0)
% 0.12/0.36 % 166:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren29(x2,x0)
% 0.12/0.36 % 167:2:2:INP:TopTop: p10(x0) -> ren29(x1,x0)
% 0.12/0.36 % 168:2:2:INP:TopTop: -> r1(x0,skf12(x0)),ren29(x1,x0)
% 0.12/0.36 % 169:2:2:INP:TopTop: p11(skf12(x0)) -> ren29(x1,x0)
% 0.12/0.36 % 170:2:2:INP:TopTop: -> p10(skf12(x0)),ren29(x1,x0)
% 0.12/0.36 % 171:3:3:INP:TopTopTop: r1(skf12(x0),x1) -> p10(x1),ren29(x2,x0)
% 0.12/0.36 % 172:2:2:INP:TopTop: -> p10(skf12(x0)),ren29(x1,x0)
% 0.12/0.36 % 173:2:2:INP:TopTop: -> r1(x0,x1),ren30(x0,x1)
% 0.12/0.36 % 174:2:2:INP:TopTop: -> p11(x0),ren30(x1,x0)
% 0.12/0.36 % 175:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren30(x2,x0)
% 0.12/0.36 % 176:2:2:INP:TopTop: p10(x0) -> ren30(x1,x0)
% 0.12/0.36 % 177:2:2:INP:TopTop: p11(x0) -> ren30(x1,x0)
% 0.12/0.36 % 178:2:2:INP:TopTop: -> p10(x0),ren30(x1,x0)
% 0.12/0.36 % 179:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren30(x2,x0)
% 0.12/0.36 % 180:2:2:INP:TopTop: -> p10(x0),ren30(x1,x0)
% 0.12/0.36 % 181:2:2:INP:TopTop: -> r1(x0,x1),ren31(x0,x1)
% 0.12/0.36 % 182:2:2:INP:TopTop: p10(x0) -> ren31(x1,x0)
% 0.12/0.36 % 183:2:2:INP:TopTop: -> r1(x0,x1),ren32(x0,x1)
% 0.12/0.36 % 184:2:2:INP:TopTop: p9(x0) -> ren32(x1,x0)
% 0.12/0.36 % 185:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1)
% 0.12/0.36 % 186:2:2:INP:TopTop: -> r1(x0,skf13(x0)),ren33(x1,x0)
% 0.12/0.36 % 187:2:2:INP:TopTop: -> p10(skf13(x0)),ren33(x1,x0)
% 0.12/0.36 % 188:3:3:INP:TopTopTop: r1(skf13(x0),x1) -> p10(x1),ren33(x2,x0)
% 0.12/0.36 % 189:2:2:INP:TopTop: p9(skf13(x0)) -> ren33(x1,x0)
% 0.12/0.36 % 190:2:2:INP:TopTop: p10(x0) -> ren33(x1,x0)
% 0.12/0.36 % 191:2:2:INP:TopTop: -> p9(x0),ren33(x1,x0)
% 0.12/0.36 % 192:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren33(x2,x0)
% 0.12/0.36 % 193:2:2:INP:TopTop: -> p9(x0),ren33(x1,x0)
% 0.12/0.36 % 194:2:2:INP:TopTop: -> r1(x0,x1),ren34(x0,x1)
% 0.12/0.36 % 195:2:2:INP:TopTop: -> p10(x0),ren34(x1,x0)
% 0.12/0.36 % 196:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren34(x2,x0)
% 0.12/0.36 % 197:2:2:INP:TopTop: p9(x0) -> ren34(x1,x0)
% 0.12/0.36 % 198:2:2:INP:TopTop: -> r1(x0,skf14(x0)),ren34(x1,x0)
% 0.12/0.36 % 199:2:2:INP:TopTop: p10(skf14(x0)) -> ren34(x1,x0)
% 0.12/0.36 % 200:2:2:INP:TopTop: -> p9(skf14(x0)),ren34(x1,x0)
% 0.12/0.36 % 201:3:3:INP:TopTopTop: r1(skf14(x0),x1) -> p9(x1),ren34(x2,x0)
% 0.12/0.36 % 202:2:2:INP:TopTop: -> p9(skf14(x0)),ren34(x1,x0)
% 0.12/0.36 % 203:2:2:INP:TopTop: -> r1(x0,x1),ren35(x0,x1)
% 0.12/0.36 % 204:2:2:INP:TopTop: -> p10(x0),ren35(x1,x0)
% 0.12/0.36 % 205:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren35(x2,x0)
% 0.12/0.36 % 206:2:2:INP:TopTop: p9(x0) -> ren35(x1,x0)
% 0.12/0.36 % 207:2:2:INP:TopTop: p10(x0) -> ren35(x1,x0)
% 0.12/0.36 % 208:2:2:INP:TopTop: -> p9(x0),ren35(x1,x0)
% 0.12/0.36 % 209:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren35(x2,x0)
% 0.12/0.36 % 210:2:2:INP:TopTop: -> p9(x0),ren35(x1,x0)
% 0.12/0.36 % 211:2:2:INP:TopTop: -> r1(x0,x1),ren36(x0,x1)
% 0.12/0.36 % 212:2:2:INP:TopTop: p9(x0) -> ren36(x1,x0)
% 0.12/0.36 % 213:2:2:INP:TopTop: -> r1(x0,x1),ren37(x0,x1)
% 0.12/0.36 % 214:2:2:INP:TopTop: p8(x0) -> ren37(x1,x0)
% 0.12/0.36 % 215:2:2:INP:TopTop: -> r1(x0,x1),ren38(x0,x1)
% 0.12/0.36 % 216:2:2:INP:TopTop: -> r1(x0,skf15(x0)),ren38(x1,x0)
% 0.12/0.36 % 217:2:2:INP:TopTop: -> p9(skf15(x0)),ren38(x1,x0)
% 0.12/0.36 % 218:3:3:INP:TopTopTop: r1(skf15(x0),x1) -> p9(x1),ren38(x2,x0)
% 0.12/0.36 % 219:2:2:INP:TopTop: p8(skf15(x0)) -> ren38(x1,x0)
% 0.12/0.36 % 220:2:2:INP:TopTop: p9(x0) -> ren38(x1,x0)
% 0.12/0.36 % 221:2:2:INP:TopTop: -> p8(x0),ren38(x1,x0)
% 0.12/0.36 % 222:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren38(x2,x0)
% 0.12/0.36 % 223:2:2:INP:TopTop: -> p8(x0),ren38(x1,x0)
% 0.12/0.36 % 224:2:2:INP:TopTop: -> r1(x0,x1),ren39(x0,x1)
% 0.12/0.36 % 225:2:2:INP:TopTop: -> p9(x0),ren39(x1,x0)
% 0.12/0.36 % 226:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren39(x2,x0)
% 0.12/0.36 % 227:2:2:INP:TopTop: p8(x0) -> ren39(x1,x0)
% 0.12/0.36 % 228:2:2:INP:TopTop: -> r1(x0,skf16(x0)),ren39(x1,x0)
% 0.12/0.36 % 229:2:2:INP:TopTop: p9(skf16(x0)) -> ren39(x1,x0)
% 0.12/0.36 % 230:2:2:INP:TopTop: -> p8(skf16(x0)),ren39(x1,x0)
% 0.12/0.36 % 231:3:3:INP:TopTopTop: r1(skf16(x0),x1) -> p8(x1),ren39(x2,x0)
% 0.12/0.36 % 232:2:2:INP:TopTop: -> p8(skf16(x0)),ren39(x1,x0)
% 0.12/0.36 % 233:2:2:INP:TopTop: -> r1(x0,x1),ren40(x0,x1)
% 0.12/0.36 % 234:2:2:INP:TopTop: -> p9(x0),ren40(x1,x0)
% 0.12/0.36 % 235:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren40(x2,x0)
% 0.12/0.36 % 236:2:2:INP:TopTop: p8(x0) -> ren40(x1,x0)
% 0.12/0.36 % 237:2:2:INP:TopTop: p9(x0) -> ren40(x1,x0)
% 0.12/0.36 % 238:2:2:INP:TopTop: -> p8(x0),ren40(x1,x0)
% 0.12/0.36 % 239:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren40(x2,x0)
% 0.12/0.36 % 240:2:2:INP:TopTop: -> p8(x0),ren40(x1,x0)
% 0.12/0.36 % 241:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1)
% 0.12/0.36 % 242:2:2:INP:TopTop: p8(x0) -> ren41(x1,x0)
% 0.12/0.36 % 243:2:2:INP:TopTop: -> r1(x0,x1),ren42(x0,x1)
% 0.12/0.36 % 244:2:2:INP:TopTop: p7(x0) -> ren42(x1,x0)
% 0.12/0.36 % 245:2:2:INP:TopTop: -> r1(x0,x1),ren43(x0,x1)
% 0.12/0.36 % 246:2:2:INP:TopTop: -> r1(x0,skf17(x0)),ren43(x1,x0)
% 0.12/0.36 % 247:2:2:INP:TopTop: -> p8(skf17(x0)),ren43(x1,x0)
% 0.12/0.36 % 248:3:3:INP:TopTopTop: r1(skf17(x0),x1) -> p8(x1),ren43(x2,x0)
% 0.12/0.36 % 249:2:2:INP:TopTop: p7(skf17(x0)) -> ren43(x1,x0)
% 0.12/0.36 % 250:2:2:INP:TopTop: p8(x0) -> ren43(x1,x0)
% 0.12/0.36 % 251:2:2:INP:TopTop: -> p7(x0),ren43(x1,x0)
% 0.12/0.36 % 252:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren43(x2,x0)
% 0.12/0.36 % 253:2:2:INP:TopTop: -> p7(x0),ren43(x1,x0)
% 0.12/0.36 % 254:2:2:INP:TopTop: -> r1(x0,x1),ren44(x0,x1)
% 0.12/0.36 % 255:2:2:INP:TopTop: -> p8(x0),ren44(x1,x0)
% 0.12/0.36 % 256:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren44(x2,x0)
% 0.12/0.36 % 257:2:2:INP:TopTop: p7(x0) -> ren44(x1,x0)
% 0.12/0.36 % 258:2:2:INP:TopTop: -> r1(x0,skf18(x0)),ren44(x1,x0)
% 0.12/0.36 % 259:2:2:INP:TopTop: p8(skf18(x0)) -> ren44(x1,x0)
% 0.12/0.36 % 260:2:2:INP:TopTop: -> p7(skf18(x0)),ren44(x1,x0)
% 0.12/0.36 % 261:3:3:INP:TopTopTop: r1(skf18(x0),x1) -> p7(x1),ren44(x2,x0)
% 0.12/0.36 % 262:2:2:INP:TopTop: -> p7(skf18(x0)),ren44(x1,x0)
% 0.12/0.36 % 263:2:2:INP:TopTop: -> r1(x0,x1),ren45(x0,x1)
% 0.12/0.36 % 264:2:2:INP:TopTop: -> p8(x0),ren45(x1,x0)
% 0.12/0.36 % 265:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren45(x2,x0)
% 0.12/0.36 % 266:2:2:INP:TopTop: p7(x0) -> ren45(x1,x0)
% 0.12/0.36 % 267:2:2:INP:TopTop: p8(x0) -> ren45(x1,x0)
% 0.12/0.36 % 268:2:2:INP:TopTop: -> p7(x0),ren45(x1,x0)
% 0.12/0.36 % 269:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren45(x2,x0)
% 0.12/0.36 % 270:2:2:INP:TopTop: -> p7(x0),ren45(x1,x0)
% 0.12/0.36 % 271:2:2:INP:TopTop: -> r1(x0,x1),ren46(x0,x1)
% 0.12/0.36 % 272:2:2:INP:TopTop: p7(x0) -> ren46(x1,x0)
% 0.12/0.36 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren47(x0,x1)
% 0.12/0.36 % 274:2:2:INP:TopTop: p6(x0) -> ren47(x1,x0)
% 0.12/0.36 % 275:2:2:INP:TopTop: -> r1(x0,x1),ren48(x0,x1)
% 0.12/0.36 % 276:2:2:INP:TopTop: -> r1(x0,skf19(x0)),ren48(x1,x0)
% 0.12/0.36 % 277:2:2:INP:TopTop: -> p7(skf19(x0)),ren48(x1,x0)
% 0.12/0.36 % 278:3:3:INP:TopTopTop: r1(skf19(x0),x1) -> p7(x1),ren48(x2,x0)
% 0.12/0.36 % 279:2:2:INP:TopTop: p6(skf19(x0)) -> ren48(x1,x0)
% 0.12/0.36 % 280:2:2:INP:TopTop: p7(x0) -> ren48(x1,x0)
% 0.12/0.36 % 281:2:2:INP:TopTop: -> p6(x0),ren48(x1,x0)
% 0.12/0.36 % 282:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren48(x2,x0)
% 0.12/0.36 % 283:2:2:INP:TopTop: -> p6(x0),ren48(x1,x0)
% 0.12/0.36 % 284:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1)
% 0.12/0.36 % 285:2:2:INP:TopTop: -> p7(x0),ren49(x1,x0)
% 0.12/0.36 % 286:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren49(x2,x0)
% 0.12/0.36 % 287:2:2:INP:TopTop: p6(x0) -> ren49(x1,x0)
% 0.12/0.36 % 288:2:2:INP:TopTop: -> r1(x0,skf20(x0)),ren49(x1,x0)
% 0.12/0.36 % 289:2:2:INP:TopTop: p7(skf20(x0)) -> ren49(x1,x0)
% 0.12/0.36 % 290:2:2:INP:TopTop: -> p6(skf20(x0)),ren49(x1,x0)
% 0.12/0.36 % 291:3:3:INP:TopTopTop: r1(skf20(x0),x1) -> p6(x1),ren49(x2,x0)
% 0.12/0.36 % 292:2:2:INP:TopTop: -> p6(skf20(x0)),ren49(x1,x0)
% 0.12/0.36 % 293:2:2:INP:TopTop: -> r1(x0,x1),ren50(x0,x1)
% 0.12/0.36 % 294:2:2:INP:TopTop: -> p7(x0),ren50(x1,x0)
% 0.12/0.36 % 295:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren50(x2,x0)
% 0.12/0.36 % 296:2:2:INP:TopTop: p6(x0) -> ren50(x1,x0)
% 0.12/0.36 % 297:2:2:INP:TopTop: p7(x0) -> ren50(x1,x0)
% 0.12/0.36 % 298:2:2:INP:TopTop: -> p6(x0),ren50(x1,x0)
% 0.12/0.36 % 299:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren50(x2,x0)
% 0.12/0.36 % 300:2:2:INP:TopTop: -> p6(x0),ren50(x1,x0)
% 0.12/0.36 % 301:2:2:INP:TopTop: -> r1(x0,x1),ren51(x0,x1)
% 0.12/0.36 % 302:2:2:INP:TopTop: p6(x0) -> ren51(x1,x0)
% 0.12/0.36 % 303:2:2:INP:TopTop: -> r1(x0,x1),ren52(x0,x1)
% 0.12/0.36 % 304:2:2:INP:TopTop: p5(x0) -> ren52(x1,x0)
% 0.12/0.36 % 305:2:2:INP:TopTop: -> r1(x0,x1),ren53(x0,x1)
% 0.12/0.36 % 306:2:2:INP:TopTop: -> r1(x0,skf21(x0)),ren53(x1,x0)
% 0.12/0.36 % 307:2:2:INP:TopTop: -> p6(skf21(x0)),ren53(x1,x0)
% 0.12/0.36 % 308:3:3:INP:TopTopTop: r1(skf21(x0),x1) -> p6(x1),ren53(x2,x0)
% 0.12/0.36 % 309:2:2:INP:TopTop: p5(skf21(x0)) -> ren53(x1,x0)
% 0.12/0.36 % 310:2:2:INP:TopTop: p6(x0) -> ren53(x1,x0)
% 0.12/0.36 % 311:2:2:INP:TopTop: -> p5(x0),ren53(x1,x0)
% 0.12/0.36 % 312:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren53(x2,x0)
% 0.12/0.36 % 313:2:2:INP:TopTop: -> p5(x0),ren53(x1,x0)
% 0.12/0.36 % 314:2:2:INP:TopTop: -> r1(x0,x1),ren54(x0,x1)
% 0.12/0.36 % 315:2:2:INP:TopTop: -> p6(x0),ren54(x1,x0)
% 0.12/0.36 % 316:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren54(x2,x0)
% 0.12/0.36 % 317:2:2:INP:TopTop: p5(x0) -> ren54(x1,x0)
% 0.12/0.36 % 318:2:2:INP:TopTop: -> r1(x0,skf22(x0)),ren54(x1,x0)
% 0.12/0.36 % 319:2:2:INP:TopTop: p6(skf22(x0)) -> ren54(x1,x0)
% 0.12/0.36 % 320:2:2:INP:TopTop: -> p5(skf22(x0)),ren54(x1,x0)
% 0.12/0.36 % 321:3:3:INP:TopTopTop: r1(skf22(x0),x1) -> p5(x1),ren54(x2,x0)
% 0.12/0.36 % 322:2:2:INP:TopTop: -> p5(skf22(x0)),ren54(x1,x0)
% 0.12/0.36 % 323:2:2:INP:TopTop: -> r1(x0,x1),ren55(x0,x1)
% 0.12/0.36 % 324:2:2:INP:TopTop: -> p6(x0),ren55(x1,x0)
% 0.12/0.36 % 325:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren55(x2,x0)
% 0.12/0.36 % 326:2:2:INP:TopTop: p5(x0) -> ren55(x1,x0)
% 0.12/0.36 % 327:2:2:INP:TopTop: p6(x0) -> ren55(x1,x0)
% 0.12/0.36 % 328:2:2:INP:TopTop: -> p5(x0),ren55(x1,x0)
% 0.12/0.36 % 329:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren55(x2,x0)
% 0.12/0.36 % 330:2:2:INP:TopTop: -> p5(x0),ren55(x1,x0)
% 0.12/0.36 % 331:2:2:INP:TopTop: -> r1(x0,x1),ren56(x0,x1)
% 0.12/0.36 % 332:2:2:INP:TopTop: p5(x0) -> ren56(x1,x0)
% 0.12/0.36 % 333:2:2:INP:TopTop: -> r1(x0,x1),ren57(x0,x1)
% 0.12/0.36 % 334:2:2:INP:TopTop: p4(x0) -> ren57(x1,x0)
% 0.12/0.36 % 335:2:2:INP:TopTop: -> r1(x0,x1),ren58(x0,x1)
% 0.12/0.36 % 336:2:2:INP:TopTop: -> r1(x0,skf23(x0)),ren58(x1,x0)
% 0.12/0.36 % 337:2:2:INP:TopTop: -> p5(skf23(x0)),ren58(x1,x0)
% 0.12/0.36 % 338:3:3:INP:TopTopTop: r1(skf23(x0),x1) -> p5(x1),ren58(x2,x0)
% 0.12/0.36 % 339:2:2:INP:TopTop: p4(skf23(x0)) -> ren58(x1,x0)
% 0.12/0.36 % 340:2:2:INP:TopTop: p5(x0) -> ren58(x1,x0)
% 0.12/0.36 % 341:2:2:INP:TopTop: -> p4(x0),ren58(x1,x0)
% 0.12/0.36 % 342:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren58(x2,x0)
% 0.12/0.36 % 343:2:2:INP:TopTop: -> p4(x0),ren58(x1,x0)
% 0.12/0.36 % 344:2:2:INP:TopTop: -> r1(x0,x1),ren59(x0,x1)
% 0.12/0.36 % 345:2:2:INP:TopTop: -> p5(x0),ren59(x1,x0)
% 0.12/0.36 % 346:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren59(x2,x0)
% 0.12/0.36 % 347:2:2:INP:TopTop: p4(x0) -> ren59(x1,x0)
% 0.12/0.36 % 348:2:2:INP:TopTop: -> r1(x0,skf24(x0)),ren59(x1,x0)
% 0.12/0.36 % 349:2:2:INP:TopTop: p5(skf24(x0)) -> ren59(x1,x0)
% 0.12/0.36 % 350:2:2:INP:TopTop: -> p4(skf24(x0)),ren59(x1,x0)
% 0.12/0.36 % 351:3:3:INP:TopTopTop: r1(skf24(x0),x1) -> p4(x1),ren59(x2,x0)
% 0.12/0.36 % 352:2:2:INP:TopTop: -> p4(skf24(x0)),ren59(x1,x0)
% 0.12/0.36 % 353:2:2:INP:TopTop: -> r1(x0,x1),ren60(x0,x1)
% 0.12/0.36 % 354:2:2:INP:TopTop: -> p5(x0),ren60(x1,x0)
% 0.12/0.36 % 355:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren60(x2,x0)
% 0.12/0.36 % 356:2:2:INP:TopTop: p4(x0) -> ren60(x1,x0)
% 0.12/0.36 % 357:2:2:INP:TopTop: p5(x0) -> ren60(x1,x0)
% 0.12/0.36 % 358:2:2:INP:TopTop: -> p4(x0),ren60(x1,x0)
% 0.12/0.36 % 359:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren60(x2,x0)
% 0.12/0.36 % 360:2:2:INP:TopTop: -> p4(x0),ren60(x1,x0)
% 0.12/0.36 % 361:2:2:INP:TopTop: -> r1(x0,x1),ren61(x0,x1)
% 0.12/0.36 % 362:2:2:INP:TopTop: p4(x0) -> ren61(x1,x0)
% 0.12/0.36 % 363:2:2:INP:TopTop: -> r1(x0,x1),ren62(x0,x1)
% 0.12/0.36 % 364:2:2:INP:TopTop: p3(x0) -> ren62(x1,x0)
% 0.12/0.36 % 365:2:2:INP:TopTop: -> r1(x0,x1),ren63(x0,x1)
% 0.12/0.36 % 366:2:2:INP:TopTop: -> r1(x0,skf25(x0)),ren63(x1,x0)
% 0.12/0.36 % 367:2:2:INP:TopTop: -> p4(skf25(x0)),ren63(x1,x0)
% 0.12/0.36 % 368:3:3:INP:TopTopTop: r1(skf25(x0),x1) -> p4(x1),ren63(x2,x0)
% 0.12/0.36 % 369:2:2:INP:TopTop: p3(skf25(x0)) -> ren63(x1,x0)
% 0.12/0.36 % 370:2:2:INP:TopTop: p4(x0) -> ren63(x1,x0)
% 0.12/0.36 % 371:2:2:INP:TopTop: -> p3(x0),ren63(x1,x0)
% 0.12/0.36 % 372:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren63(x2,x0)
% 0.12/0.36 % 373:2:2:INP:TopTop: -> p3(x0),ren63(x1,x0)
% 0.12/0.36 % 374:2:2:INP:TopTop: -> r1(x0,x1),ren64(x0,x1)
% 0.12/0.36 % 375:2:2:INP:TopTop: -> p4(x0),ren64(x1,x0)
% 0.12/0.36 % 376:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren64(x2,x0)
% 0.12/0.36 % 377:2:2:INP:TopTop: p3(x0) -> ren64(x1,x0)
% 0.12/0.36 % 378:2:2:INP:TopTop: -> r1(x0,skf26(x0)),ren64(x1,x0)
% 0.12/0.36 % 379:2:2:INP:TopTop: p4(skf26(x0)) -> ren64(x1,x0)
% 0.12/0.36 % 380:2:2:INP:TopTop: -> p3(skf26(x0)),ren64(x1,x0)
% 0.12/0.36 % 381:3:3:INP:TopTopTop: r1(skf26(x0),x1) -> p3(x1),ren64(x2,x0)
% 0.12/0.36 % 382:2:2:INP:TopTop: -> p3(skf26(x0)),ren64(x1,x0)
% 0.12/0.36 % 383:2:2:INP:TopTop: -> r1(x0,x1),ren65(x0,x1)
% 0.12/0.36 % 384:2:2:INP:TopTop: -> p4(x0),ren65(x1,x0)
% 0.12/0.36 % 385:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren65(x2,x0)
% 0.12/0.36 % 386:2:2:INP:TopTop: p3(x0) -> ren65(x1,x0)
% 0.12/0.36 % 387:2:2:INP:TopTop: p4(x0) -> ren65(x1,x0)
% 0.12/0.36 % 388:2:2:INP:TopTop: -> p3(x0),ren65(x1,x0)
% 0.12/0.36 % 389:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren65(x2,x0)
% 0.12/0.36 % 390:2:2:INP:TopTop: -> p3(x0),ren65(x1,x0)
% 0.12/0.36 % 391:2:2:INP:TopTop: -> r1(x0,x1),ren66(x0,x1)
% 0.12/0.36 % 392:2:2:INP:TopTop: p3(x0) -> ren66(x1,x0)
% 0.12/0.36 % 393:2:2:INP:TopTop: -> r1(x0,x1),ren67(x0,x1)
% 0.12/0.36 % 394:2:2:INP:TopTop: p2(x0) -> ren67(x1,x0)
% 0.12/0.36 % 395:2:2:INP:TopTop: -> r1(x0,x1),ren68(x0,x1)
% 0.12/0.36 % 396:2:2:INP:TopTop: -> r1(x0,skf27(x0)),ren68(x1,x0)
% 0.12/0.36 % 397:2:2:INP:TopTop: -> p3(skf27(x0)),ren68(x1,x0)
% 0.12/0.36 % 398:3:3:INP:TopTopTop: r1(skf27(x0),x1) -> p3(x1),ren68(x2,x0)
% 0.12/0.36 % 399:2:2:INP:TopTop: p2(skf27(x0)) -> ren68(x1,x0)
% 0.12/0.36 % 400:2:2:INP:TopTop: p3(x0) -> ren68(x1,x0)
% 0.12/0.36 % 401:2:2:INP:TopTop: -> p2(x0),ren68(x1,x0)
% 0.12/0.36 % 402:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren68(x2,x0)
% 0.12/0.36 % 403:2:2:INP:TopTop: -> p2(x0),ren68(x1,x0)
% 0.12/0.36 % 404:2:2:INP:TopTop: -> r1(x0,x1),ren69(x0,x1)
% 0.12/0.36 % 405:2:2:INP:TopTop: -> p3(x0),ren69(x1,x0)
% 0.12/0.36 % 406:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren69(x2,x0)
% 0.12/0.36 % 407:2:2:INP:TopTop: p2(x0) -> ren69(x1,x0)
% 0.12/0.36 % 408:2:2:INP:TopTop: -> r1(x0,skf28(x0)),ren69(x1,x0)
% 0.12/0.36 % 409:2:2:INP:TopTop: p3(skf28(x0)) -> ren69(x1,x0)
% 0.12/0.36 % 410:2:2:INP:TopTop: -> p2(skf28(x0)),ren69(x1,x0)
% 0.12/0.36 % 411:3:3:INP:TopTopTop: r1(skf28(x0),x1) -> p2(x1),ren69(x2,x0)
% 0.12/0.36 % 412:2:2:INP:TopTop: -> p2(skf28(x0)),ren69(x1,x0)
% 0.12/0.36 % 413:2:2:INP:TopTop: -> r1(x0,x1),ren70(x0,x1)
% 0.12/0.36 % 414:2:2:INP:TopTop: -> p3(x0),ren70(x1,x0)
% 0.12/0.36 % 415:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren70(x2,x0)
% 0.12/0.36 % 416:2:2:INP:TopTop: p2(x0) -> ren70(x1,x0)
% 0.12/0.36 % 417:2:2:INP:TopTop: p3(x0) -> ren70(x1,x0)
% 0.12/0.36 % 418:2:2:INP:TopTop: -> p2(x0),ren70(x1,x0)
% 0.12/0.36 % 419:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren70(x2,x0)
% 0.12/0.36 % 420:2:2:INP:TopTop: -> p2(x0),ren70(x1,x0)
% 0.12/0.36 % 421:2:2:INP:TopTop: -> r1(x0,x1),ren71(x0,x1)
% 0.12/0.36 % 422:2:2:INP:TopTop: p2(x0) -> ren71(x1,x0)
% 0.12/0.36 % 423:2:2:INP:TopTop: -> r1(x0,x1),ren72(x0,x1)
% 0.12/0.36 % 424:2:2:INP:TopTop: p1(x0) -> ren72(x1,x0)
% 0.12/0.36 % 425:2:2:INP:TopTop: -> r1(x0,x1),ren73(x0,x1)
% 0.12/0.36 % 426:2:2:INP:TopTop: -> r1(x0,skf29(x0)),ren73(x1,x0)
% 0.12/0.36 % 427:2:2:INP:TopTop: -> p2(skf29(x0)),ren73(x1,x0)
% 0.12/0.36 % 428:3:3:INP:TopTopTop: r1(skf29(x0),x1) -> p2(x1),ren73(x2,x0)
% 0.12/0.36 % 429:2:2:INP:TopTop: p1(skf29(x0)) -> ren73(x1,x0)
% 0.12/0.36 % 430:2:2:INP:TopTop: p2(x0) -> ren73(x1,x0)
% 0.12/0.36 % 431:2:2:INP:TopTop: -> p1(x0),ren73(x1,x0)
% 0.12/0.36 % 432:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren73(x2,x0)
% 0.12/0.36 % 433:2:2:INP:TopTop: -> p1(x0),ren73(x1,x0)
% 0.12/0.36 % 434:2:2:INP:TopTop: -> r1(x0,x1),ren74(x0,x1)
% 0.12/0.36 % 435:2:2:INP:TopTop: -> p2(x0),ren74(x1,x0)
% 0.12/0.36 % 436:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren74(x2,x0)
% 0.12/0.36 % 437:2:2:INP:TopTop: p1(x0) -> ren74(x1,x0)
% 0.12/0.36 % 438:2:2:INP:TopTop: -> r1(x0,skf30(x0)),ren74(x1,x0)
% 0.12/0.36 % 439:2:2:INP:TopTop: p2(skf30(x0)) -> ren74(x1,x0)
% 0.12/0.36 % 440:2:2:INP:TopTop: -> p1(skf30(x0)),ren74(x1,x0)
% 0.12/0.36 % 441:3:3:INP:TopTopTop: r1(skf30(x0),x1) -> p1(x1),ren74(x2,x0)
% 0.12/0.36 % 442:2:2:INP:TopTop: -> p1(skf30(x0)),ren74(x1,x0)
% 0.12/0.36 % 443:2:2:INP:TopTop: -> r1(x0,x1),ren75(x0,x1)
% 0.12/0.36 % 444:2:2:INP:TopTop: -> p2(x0),ren75(x1,x0)
% 0.12/0.36 % 445:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren75(x2,x0)
% 0.12/0.36 % 446:2:2:INP:TopTop: p1(x0) -> ren75(x1,x0)
% 0.12/0.36 % 447:2:2:INP:TopTop: p2(x0) -> ren75(x1,x0)
% 0.12/0.36 % 448:2:2:INP:TopTop: -> p1(x0),ren75(x1,x0)
% 0.12/0.36 % 449:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren75(x2,x0)
% 0.12/0.36 % 450:2:2:INP:TopTop: -> p1(x0),ren75(x1,x0)
% 0.12/0.36 % 451:12:2:INP:TopTop: r1(skc31,x0),p16(x0),ren1(x0,skf32(x0)),r1(skc31,x1),p15(x1),ren2(x1,skf33(x1)),p15(x1),ren3(skc31,skc34),ren4(skc31,skc35),ren5(skc31,skc36) -> p15(x0),p16(x1)
% 0.12/0.36 % 452:12:2:INP:TopTop: r1(skc31,x0),p15(x0),ren6(x0,skf37(x0)),r1(skc31,x1),p14(x1),ren7(x1,skf38(x1)),p14(x1),ren8(skc31,skc39),ren9(skc31,skc40),ren10(skc31,skc41) -> p14(x0),p15(x1)
% 0.12/0.36 % 453:12:2:INP:TopTop: r1(skc31,x0),p14(x0),ren11(x0,skf42(x0)),r1(skc31,x1),p13(x1),ren12(x1,skf43(x1)),p13(x1),ren13(skc31,skc44),ren14(skc31,skc45),ren15(skc31,skc46) -> p13(x0),p14(x1)
% 0.12/0.36 % 454:12:2:INP:TopTop: r1(skc31,x0),p13(x0),ren16(x0,skf47(x0)),r1(skc31,x1),p12(x1),ren17(x1,skf48(x1)),p12(x1),ren18(skc31,skc49),ren19(skc31,skc50),ren20(skc31,skc51) -> p12(x0),p13(x1)
% 0.12/0.36 % 455:12:2:INP:TopTop: r1(skc31,x0),p12(x0),ren21(x0,skf52(x0)),r1(skc31,x1),p11(x1),ren22(x1,skf53(x1)),p11(x1),ren23(skc31,skc54),ren24(skc31,skc55),ren25(skc31,skc56) -> p11(x0),p12(x1)
% 0.12/0.36 % 456:12:2:INP:TopTop: r1(skc31,x0),p11(x0),ren26(x0,skf57(x0)),r1(skc31,x1),p10(x1),ren27(x1,skf58(x1)),p10(x1),ren28(skc31,skc59),ren29(skc31,skc60),ren30(skc31,skc61) -> p10(x0),p11(x1)
% 0.12/0.36 % 457:12:2:INP:TopTop: r1(skc31,x0),p10(x0),ren31(x0,skf62(x0)),r1(skc31,x1),p9(x1),ren32(x1,skf63(x1)),p9(x1),ren33(skc31,skc64),ren34(skc31,skc65),ren35(skc31,skc66) -> p9(x0),p10(x1)
% 0.12/0.36 % 458:12:2:INP:TopTop: r1(skc31,x0),p9(x0),ren36(x0,skf67(x0)),r1(skc31,x1),p8(x1),ren37(x1,skf68(x1)),p8(x1),ren38(skc31,skc69),ren39(skc31,skc70),ren40(skc31,skc71) -> p8(x0),p9(x1)
% 0.12/0.36 % 459:12:2:INP:TopTop: r1(skc31,x0),p8(x0),ren41(x0,skf72(x0)),r1(skc31,x1),p7(x1),ren42(x1,skf73(x1)),p7(x1),ren43(skc31,skc74),ren44(skc31,skc75),ren45(skc31,skc76) -> p7(x0),p8(x1)
% 0.12/0.36 % 460:12:2:INP:TopTop: r1(skc31,x0),p7(x0),ren46(x0,skf77(x0)),r1(skc31,x1),p6(x1),ren47(x1,skf78(x1)),p6(x1),ren48(skc31,skc79),ren49(skc31,skc80),ren50(skc31,skc81) -> p6(x0),p7(x1)
% 0.12/0.37 % 461:1:0:INP:: -> r1(skc31,skc82)
% 0.12/0.37 % 462:1:0:INP:: p15(skc82) ->
% 0.12/0.37 % 463:2:1:INP:Top: r1(skc82,x0) -> p15(x0)
% 0.12/0.37 % 464:1:0:INP:: -> p15(skc82)
% 0.12/0.37 % 465:1:0:INP:: -> r1(skc31,skc83)
% 0.12/0.37 % 466:1:0:INP:: p15(skc83) ->
% 0.12/0.37 % 467:2:1:INP:Top: r1(skc83,x0) -> p15(x0)
% 0.12/0.37 % 468:1:0:INP:: -> p15(skc83)
% 0.12/0.37 % 469:12:2:INP:TopTop: r1(skc31,x0),p6(x0),ren51(x0,skf84(x0)),r1(skc31,x1),p5(x1),ren52(x1,skf85(x1)),p5(x1),ren53(skc31,skc86),ren54(skc31,skc87),ren55(skc31,skc88) -> p5(x0),p6(x1)
% 0.12/0.37 % 470:12:2:INP:TopTop: r1(skc31,x0),p5(x0),ren56(x0,skf89(x0)),r1(skc31,x1),p4(x1),ren57(x1,skf90(x1)),p4(x1),ren58(skc31,skc91),ren59(skc31,skc92),ren60(skc31,skc93) -> p4(x0),p5(x1)
% 0.12/0.37 % 471:12:2:INP:TopTop: r1(skc31,x0),p4(x0),ren61(x0,skf94(x0)),r1(skc31,x1),p3(x1),ren62(x1,skf95(x1)),p3(x1),ren63(skc31,skc96),ren64(skc31,skc97),ren65(skc31,skc98) -> p3(x0),p4(x1)
% 0.12/0.37 % 472:12:2:INP:TopTop: r1(skc31,x0),p3(x0),ren66(x0,skf99(x0)),r1(skc31,x1),p2(x1),ren67(x1,skf100(x1)),p2(x1),ren68(skc31,skc101),ren69(skc31,skc102),ren70(skc31,skc103) -> p2(x0),p3(x1)
% 0.12/0.37 % 473:12:2:INP:TopTop: r1(skc31,x0),p2(x0),ren71(x0,skf104(x0)),r1(skc31,x1),p1(x1),ren72(x1,skf105(x1)),p1(x1),ren73(skc31,skc106),ren74(skc31,skc107),ren75(skc31,skc108) -> p1(x0),p2(x1)
% 0.12/0.37
% 0.12/0.37 % Predicates: r1 p16 p15 p14 p13 p12 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 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75
% 0.12/0.37 % Fol Constants: skc31 skc34 skc35 skc36 skc39 skc40 skc41 skc44 skc45 skc46 skc49 skc50 skc51 skc54 skc55 skc56 skc59 skc60 skc61 skc64 skc65 skc66 skc69 skc70 skc71 skc74 skc75 skc76 skc79 skc80 skc81 skc82 skc83 skc86 skc87 skc88 skc91 skc92 skc93 skc96 skc97 skc98 skc101 skc102 skc103 skc106 skc107 skc108
% 0.12/0.37 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf28 skf29 skf30 skf32 skf33 skf37 skf38 skf42 skf43 skf47 skf48 skf52 skf53 skf57 skf58 skf62 skf63 skf67 skf68 skf72 skf73 skf77 skf78 skf84 skf85 skf89 skf90 skf94 skf95 skf99 skf100 skf104 skf105
% 0.12/0.37 % Problem Properties:
% 0.12/0.37 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.12/0.37
% 0.12/0.37
% 0.12/0.37 % Reduced Input Axiom Clauses:
% 0.12/0.37 % 1:2:2:INP:TopTop: -> r1(x0,x1),ren1(x0,x1)
% 0.12/0.37 % 2:2:2:INP:TopTop: p16(x0) -> ren1(x1,x0)
% 0.12/0.37 % 3:2:2:INP:TopTop: -> r1(x0,x1),ren2(x0,x1)
% 0.12/0.37 % 4:2:2:INP:TopTop: p15(x0) -> ren2(x1,x0)
% 0.12/0.37 % 5:2:2:INP:TopTop: -> r1(x0,x1),ren3(x0,x1)
% 0.12/0.37 % 6:2:2:INP:TopTop: -> r1(x0,skf1(x0)),ren3(x1,x0)
% 0.12/0.37 % 7:2:2:INP:TopTop: -> p16(skf1(x0)),ren3(x1,x0)
% 0.12/0.37 % 8:3:3:INP:TopTopTop: r1(skf1(x0),x1) -> p16(x1),ren3(x2,x0)
% 0.12/0.37 % 9:2:2:INP:TopTop: p15(skf1(x0)) -> ren3(x1,x0)
% 0.12/0.37 % 10:2:2:INP:TopTop: p16(x0) -> ren3(x1,x0)
% 0.12/0.37 % 12:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren3(x2,x0)
% 0.12/0.37 % 13:2:2:INP:TopTop: -> p15(x0),ren3(x1,x0)
% 0.12/0.37 % 14:2:2:INP:TopTop: -> r1(x0,x1),ren4(x0,x1)
% 0.12/0.37 % 15:2:2:INP:TopTop: -> p16(x0),ren4(x1,x0)
% 0.12/0.37 % 16:3:3:INP:TopTopTop: r1(x0,x1) -> p16(x1),ren4(x2,x0)
% 0.12/0.37 % 17:2:2:INP:TopTop: p15(x0) -> ren4(x1,x0)
% 0.12/0.37 % 18:2:2:INP:TopTop: -> r1(x0,skf2(x0)),ren4(x1,x0)
% 0.12/0.37 % 19:2:2:INP:TopTop: p16(skf2(x0)) -> ren4(x1,x0)
% 0.12/0.37 % 21:3:3:INP:TopTopTop: r1(skf2(x0),x1) -> p15(x1),ren4(x2,x0)
% 0.12/0.37 % 22:2:2:INP:TopTop: -> p15(skf2(x0)),ren4(x1,x0)
% 0.12/0.37 % 23:2:2:INP:TopTop: -> r1(x0,x1),ren5(x0,x1)
% 0.12/0.37 % 474:1:2:[27.0,24.0]:TopTop: -> ren5(x0,x1)
% 0.12/0.37 % 475:1:2:[28.0,26.0]:TopTop: -> ren5(x0,x1)
% 0.12/0.37 % 31:2:2:INP:TopTop: -> r1(x0,x1),ren6(x0,x1)
% 0.12/0.37 % 32:2:2:INP:TopTop: p15(x0) -> ren6(x1,x0)
% 0.12/0.37 % 33:2:2:INP:TopTop: -> r1(x0,x1),ren7(x0,x1)
% 0.12/0.37 % 34:2:2:INP:TopTop: p14(x0) -> ren7(x1,x0)
% 0.12/0.37 % 35:2:2:INP:TopTop: -> r1(x0,x1),ren8(x0,x1)
% 0.12/0.37 % 36:2:2:INP:TopTop: -> r1(x0,skf3(x0)),ren8(x1,x0)
% 0.12/0.37 % 37:2:2:INP:TopTop: -> p15(skf3(x0)),ren8(x1,x0)
% 0.12/0.37 % 38:3:3:INP:TopTopTop: r1(skf3(x0),x1) -> p15(x1),ren8(x2,x0)
% 0.12/0.37 % 39:2:2:INP:TopTop: p14(skf3(x0)) -> ren8(x1,x0)
% 0.12/0.37 % 40:2:2:INP:TopTop: p15(x0) -> ren8(x1,x0)
% 0.12/0.37 % 42:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren8(x2,x0)
% 0.12/0.37 % 43:2:2:INP:TopTop: -> p14(x0),ren8(x1,x0)
% 0.12/0.37 % 44:2:2:INP:TopTop: -> r1(x0,x1),ren9(x0,x1)
% 0.12/0.37 % 45:2:2:INP:TopTop: -> p15(x0),ren9(x1,x0)
% 0.12/0.37 % 46:3:3:INP:TopTopTop: r1(x0,x1) -> p15(x1),ren9(x2,x0)
% 0.12/0.37 % 47:2:2:INP:TopTop: p14(x0) -> ren9(x1,x0)
% 0.12/0.37 % 48:2:2:INP:TopTop: -> r1(x0,skf4(x0)),ren9(x1,x0)
% 0.12/0.37 % 49:2:2:INP:TopTop: p15(skf4(x0)) -> ren9(x1,x0)
% 0.12/0.37 % 51:3:3:INP:TopTopTop: r1(skf4(x0),x1) -> p14(x1),ren9(x2,x0)
% 0.12/0.37 % 52:2:2:INP:TopTop: -> p14(skf4(x0)),ren9(x1,x0)
% 0.12/0.37 % 53:2:2:INP:TopTop: -> r1(x0,x1),ren10(x0,x1)
% 0.12/0.37 % 476:1:2:[57.0,54.0]:TopTop: -> ren10(x0,x1)
% 0.12/0.37 % 477:1:2:[58.0,56.0]:TopTop: -> ren10(x0,x1)
% 0.12/0.37 % 61:2:2:INP:TopTop: -> r1(x0,x1),ren11(x0,x1)
% 0.12/0.37 % 62:2:2:INP:TopTop: p14(x0) -> ren11(x1,x0)
% 0.12/0.37 % 63:2:2:INP:TopTop: -> r1(x0,x1),ren12(x0,x1)
% 0.12/0.37 % 64:2:2:INP:TopTop: p13(x0) -> ren12(x1,x0)
% 0.12/0.37 % 65:2:2:INP:TopTop: -> r1(x0,x1),ren13(x0,x1)
% 0.12/0.37 % 66:2:2:INP:TopTop: -> r1(x0,skf5(x0)),ren13(x1,x0)
% 0.12/0.37 % 67:2:2:INP:TopTop: -> p14(skf5(x0)),ren13(x1,x0)
% 0.12/0.37 % 68:3:3:INP:TopTopTop: r1(skf5(x0),x1) -> p14(x1),ren13(x2,x0)
% 0.12/0.37 % 69:2:2:INP:TopTop: p13(skf5(x0)) -> ren13(x1,x0)
% 0.12/0.37 % 70:2:2:INP:TopTop: p14(x0) -> ren13(x1,x0)
% 0.12/0.37 % 72:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren13(x2,x0)
% 0.12/0.37 % 73:2:2:INP:TopTop: -> p13(x0),ren13(x1,x0)
% 0.12/0.37 % 74:2:2:INP:TopTop: -> r1(x0,x1),ren14(x0,x1)
% 0.12/0.37 % 75:2:2:INP:TopTop: -> p14(x0),ren14(x1,x0)
% 0.12/0.37 % 76:3:3:INP:TopTopTop: r1(x0,x1) -> p14(x1),ren14(x2,x0)
% 0.12/0.37 % 77:2:2:INP:TopTop: p13(x0) -> ren14(x1,x0)
% 0.12/0.37 % 78:2:2:INP:TopTop: -> r1(x0,skf6(x0)),ren14(x1,x0)
% 0.12/0.37 % 79:2:2:INP:TopTop: p14(skf6(x0)) -> ren14(x1,x0)
% 0.12/0.37 % 81:3:3:INP:TopTopTop: r1(skf6(x0),x1) -> p13(x1),ren14(x2,x0)
% 0.12/0.37 % 82:2:2:INP:TopTop: -> p13(skf6(x0)),ren14(x1,x0)
% 0.12/0.37 % 83:2:2:INP:TopTop: -> r1(x0,x1),ren15(x0,x1)
% 0.12/0.37 % 478:1:2:[87.0,84.0]:TopTop: -> ren15(x0,x1)
% 0.12/0.37 % 479:1:2:[88.0,86.0]:TopTop: -> ren15(x0,x1)
% 0.12/0.37 % 91:2:2:INP:TopTop: -> r1(x0,x1),ren16(x0,x1)
% 0.12/0.37 % 92:2:2:INP:TopTop: p13(x0) -> ren16(x1,x0)
% 0.12/0.37 % 93:2:2:INP:TopTop: -> r1(x0,x1),ren17(x0,x1)
% 0.12/0.37 % 94:2:2:INP:TopTop: p12(x0) -> ren17(x1,x0)
% 0.12/0.37 % 95:2:2:INP:TopTop: -> r1(x0,x1),ren18(x0,x1)
% 0.12/0.37 % 96:2:2:INP:TopTop: -> r1(x0,skf7(x0)),ren18(x1,x0)
% 0.12/0.37 % 97:2:2:INP:TopTop: -> p13(skf7(x0)),ren18(x1,x0)
% 0.12/0.37 % 98:3:3:INP:TopTopTop: r1(skf7(x0),x1) -> p13(x1),ren18(x2,x0)
% 0.12/0.37 % 99:2:2:INP:TopTop: p12(skf7(x0)) -> ren18(x1,x0)
% 0.12/0.37 % 100:2:2:INP:TopTop: p13(x0) -> ren18(x1,x0)
% 0.12/0.37 % 102:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren18(x2,x0)
% 0.12/0.37 % 103:2:2:INP:TopTop: -> p12(x0),ren18(x1,x0)
% 0.12/0.37 % 104:2:2:INP:TopTop: -> r1(x0,x1),ren19(x0,x1)
% 0.12/0.37 % 105:2:2:INP:TopTop: -> p13(x0),ren19(x1,x0)
% 0.12/0.37 % 106:3:3:INP:TopTopTop: r1(x0,x1) -> p13(x1),ren19(x2,x0)
% 0.12/0.37 % 107:2:2:INP:TopTop: p12(x0) -> ren19(x1,x0)
% 0.12/0.37 % 108:2:2:INP:TopTop: -> r1(x0,skf8(x0)),ren19(x1,x0)
% 0.12/0.37 % 109:2:2:INP:TopTop: p13(skf8(x0)) -> ren19(x1,x0)
% 0.12/0.37 % 111:3:3:INP:TopTopTop: r1(skf8(x0),x1) -> p12(x1),ren19(x2,x0)
% 0.12/0.37 % 112:2:2:INP:TopTop: -> p12(skf8(x0)),ren19(x1,x0)
% 0.12/0.37 % 113:2:2:INP:TopTop: -> r1(x0,x1),ren20(x0,x1)
% 0.12/0.37 % 480:1:2:[117.0,114.0]:TopTop: -> ren20(x0,x1)
% 0.12/0.37 % 503:1:2:[450.0,446.0]:TopTop: -> ren75(x0,x1)
% 0.12/0.37 % 481:1:2:[120.0,116.0]:TopTop: -> ren20(x0,x1)
% 0.12/0.37 % 502:1:2:[447.0,444.0]:TopTop: -> ren75(x0,x1)
% 0.12/0.37 % 443:2:2:INP:TopTop: -> r1(x0,x1),ren75(x0,x1)
% 0.12/0.37 % 442:2:2:INP:TopTop: -> p1(skf30(x0)),ren74(x1,x0)
% 0.12/0.37 % 441:3:3:INP:TopTopTop: r1(skf30(x0),x1) -> p1(x1),ren74(x2,x0)
% 0.12/0.37 % 121:2:2:INP:TopTop: -> r1(x0,x1),ren21(x0,x1)
% 0.12/0.37 % 122:2:2:INP:TopTop: p12(x0) -> ren21(x1,x0)
% 0.12/0.37 % 123:2:2:INP:TopTop: -> r1(x0,x1),ren22(x0,x1)
% 0.12/0.37 % 124:2:2:INP:TopTop: p11(x0) -> ren22(x1,x0)
% 0.12/0.37 % 125:2:2:INP:TopTop: -> r1(x0,x1),ren23(x0,x1)
% 0.12/0.37 % 126:2:2:INP:TopTop: -> r1(x0,skf9(x0)),ren23(x1,x0)
% 0.12/0.37 % 127:2:2:INP:TopTop: -> p12(skf9(x0)),ren23(x1,x0)
% 0.12/0.37 % 128:3:3:INP:TopTopTop: r1(skf9(x0),x1) -> p12(x1),ren23(x2,x0)
% 0.12/0.37 % 129:2:2:INP:TopTop: p11(skf9(x0)) -> ren23(x1,x0)
% 0.12/0.37 % 130:2:2:INP:TopTop: p12(x0) -> ren23(x1,x0)
% 0.12/0.37 % 439:2:2:INP:TopTop: p2(skf30(x0)) -> ren74(x1,x0)
% 0.12/0.37 % 132:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren23(x2,x0)
% 0.12/0.37 % 133:2:2:INP:TopTop: -> p11(x0),ren23(x1,x0)
% 0.12/0.37 % 134:2:2:INP:TopTop: -> r1(x0,x1),ren24(x0,x1)
% 0.12/0.37 % 135:2:2:INP:TopTop: -> p12(x0),ren24(x1,x0)
% 0.12/0.37 % 136:3:3:INP:TopTopTop: r1(x0,x1) -> p12(x1),ren24(x2,x0)
% 0.12/0.37 % 137:2:2:INP:TopTop: p11(x0) -> ren24(x1,x0)
% 0.12/0.37 % 138:2:2:INP:TopTop: -> r1(x0,skf10(x0)),ren24(x1,x0)
% 0.12/0.37 % 139:2:2:INP:TopTop: p12(skf10(x0)) -> ren24(x1,x0)
% 0.12/0.37 % 438:2:2:INP:TopTop: -> r1(x0,skf30(x0)),ren74(x1,x0)
% 0.12/0.37 % 141:3:3:INP:TopTopTop: r1(skf10(x0),x1) -> p11(x1),ren24(x2,x0)
% 0.12/0.37 % 142:2:2:INP:TopTop: -> p11(skf10(x0)),ren24(x1,x0)
% 0.12/0.37 % 143:2:2:INP:TopTop: -> r1(x0,x1),ren25(x0,x1)
% 0.12/0.37 % 482:1:2:[147.0,144.0]:TopTop: -> ren25(x0,x1)
% 0.12/0.37 % 437:2:2:INP:TopTop: p1(x0) -> ren74(x1,x0)
% 0.12/0.37 % 483:1:2:[150.0,146.0]:TopTop: -> ren25(x0,x1)
% 0.12/0.37 % 436:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren74(x2,x0)
% 0.12/0.37 % 435:2:2:INP:TopTop: -> p2(x0),ren74(x1,x0)
% 0.12/0.37 % 434:2:2:INP:TopTop: -> r1(x0,x1),ren74(x0,x1)
% 0.12/0.37 % 433:2:2:INP:TopTop: -> p1(x0),ren73(x1,x0)
% 0.12/0.37 % 151:2:2:INP:TopTop: -> r1(x0,x1),ren26(x0,x1)
% 0.12/0.37 % 152:2:2:INP:TopTop: p11(x0) -> ren26(x1,x0)
% 0.12/0.37 % 153:2:2:INP:TopTop: -> r1(x0,x1),ren27(x0,x1)
% 0.12/0.37 % 154:2:2:INP:TopTop: p10(x0) -> ren27(x1,x0)
% 0.12/0.37 % 155:2:2:INP:TopTop: -> r1(x0,x1),ren28(x0,x1)
% 0.12/0.37 % 156:2:2:INP:TopTop: -> r1(x0,skf11(x0)),ren28(x1,x0)
% 0.12/0.37 % 157:2:2:INP:TopTop: -> p11(skf11(x0)),ren28(x1,x0)
% 0.12/0.37 % 158:3:3:INP:TopTopTop: r1(skf11(x0),x1) -> p11(x1),ren28(x2,x0)
% 0.12/0.37 % 159:2:2:INP:TopTop: p10(skf11(x0)) -> ren28(x1,x0)
% 0.12/0.37 % 160:2:2:INP:TopTop: p11(x0) -> ren28(x1,x0)
% 0.12/0.37 % 432:3:3:INP:TopTopTop: r1(x0,x1) -> p1(x1),ren73(x2,x0)
% 0.12/0.37 % 162:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren28(x2,x0)
% 0.12/0.37 % 163:2:2:INP:TopTop: -> p10(x0),ren28(x1,x0)
% 0.12/0.37 % 164:2:2:INP:TopTop: -> r1(x0,x1),ren29(x0,x1)
% 0.12/0.37 % 165:2:2:INP:TopTop: -> p11(x0),ren29(x1,x0)
% 0.12/0.37 % 166:3:3:INP:TopTopTop: r1(x0,x1) -> p11(x1),ren29(x2,x0)
% 0.12/0.37 % 167:2:2:INP:TopTop: p10(x0) -> ren29(x1,x0)
% 0.12/0.37 % 168:2:2:INP:TopTop: -> r1(x0,skf12(x0)),ren29(x1,x0)
% 0.12/0.37 % 169:2:2:INP:TopTop: p11(skf12(x0)) -> ren29(x1,x0)
% 0.12/0.37 % 430:2:2:INP:TopTop: p2(x0) -> ren73(x1,x0)
% 0.12/0.37 % 171:3:3:INP:TopTopTop: r1(skf12(x0),x1) -> p10(x1),ren29(x2,x0)
% 0.12/0.37 % 172:2:2:INP:TopTop: -> p10(skf12(x0)),ren29(x1,x0)
% 0.12/0.37 % 173:2:2:INP:TopTop: -> r1(x0,x1),ren30(x0,x1)
% 0.12/0.37 % 484:1:2:[177.0,174.0]:TopTop: -> ren30(x0,x1)
% 0.12/0.37 % 429:2:2:INP:TopTop: p1(skf29(x0)) -> ren73(x1,x0)
% 0.12/0.37 % 485:1:2:[180.0,176.0]:TopTop: -> ren30(x0,x1)
% 0.12/0.37 % 428:3:3:INP:TopTopTop: r1(skf29(x0),x1) -> p2(x1),ren73(x2,x0)
% 0.12/0.37 % 427:2:2:INP:TopTop: -> p2(skf29(x0)),ren73(x1,x0)
% 0.12/0.37 % 426:2:2:INP:TopTop: -> r1(x0,skf29(x0)),ren73(x1,x0)
% 0.12/0.37 % 425:2:2:INP:TopTop: -> r1(x0,x1),ren73(x0,x1)
% 0.12/0.37 % 181:2:2:INP:TopTop: -> r1(x0,x1),ren31(x0,x1)
% 0.12/0.37 % 182:2:2:INP:TopTop: p10(x0) -> ren31(x1,x0)
% 0.12/0.37 % 183:2:2:INP:TopTop: -> r1(x0,x1),ren32(x0,x1)
% 0.12/0.37 % 184:2:2:INP:TopTop: p9(x0) -> ren32(x1,x0)
% 0.12/0.37 % 185:2:2:INP:TopTop: -> r1(x0,x1),ren33(x0,x1)
% 0.12/0.37 % 186:2:2:INP:TopTop: -> r1(x0,skf13(x0)),ren33(x1,x0)
% 0.12/0.37 % 187:2:2:INP:TopTop: -> p10(skf13(x0)),ren33(x1,x0)
% 0.12/0.37 % 188:3:3:INP:TopTopTop: r1(skf13(x0),x1) -> p10(x1),ren33(x2,x0)
% 0.12/0.37 % 189:2:2:INP:TopTop: p9(skf13(x0)) -> ren33(x1,x0)
% 0.12/0.37 % 190:2:2:INP:TopTop: p10(x0) -> ren33(x1,x0)
% 0.12/0.37 % 424:2:2:INP:TopTop: p1(x0) -> ren72(x1,x0)
% 0.12/0.37 % 192:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren33(x2,x0)
% 0.12/0.37 % 193:2:2:INP:TopTop: -> p9(x0),ren33(x1,x0)
% 0.12/0.37 % 194:2:2:INP:TopTop: -> r1(x0,x1),ren34(x0,x1)
% 0.12/0.37 % 195:2:2:INP:TopTop: -> p10(x0),ren34(x1,x0)
% 0.12/0.37 % 196:3:3:INP:TopTopTop: r1(x0,x1) -> p10(x1),ren34(x2,x0)
% 0.12/0.37 % 197:2:2:INP:TopTop: p9(x0) -> ren34(x1,x0)
% 0.12/0.37 % 198:2:2:INP:TopTop: -> r1(x0,skf14(x0)),ren34(x1,x0)
% 0.12/0.37 % 199:2:2:INP:TopTop: p10(skf14(x0)) -> ren34(x1,x0)
% 0.12/0.37 % 423:2:2:INP:TopTop: -> r1(x0,x1),ren72(x0,x1)
% 0.12/0.37 % 201:3:3:INP:TopTopTop: r1(skf14(x0),x1) -> p9(x1),ren34(x2,x0)
% 0.12/0.37 % 202:2:2:INP:TopTop: -> p9(skf14(x0)),ren34(x1,x0)
% 0.12/0.37 % 203:2:2:INP:TopTop: -> r1(x0,x1),ren35(x0,x1)
% 0.12/0.37 % 486:1:2:[207.0,204.0]:TopTop: -> ren35(x0,x1)
% 0.12/0.37 % 422:2:2:INP:TopTop: p2(x0) -> ren71(x1,x0)
% 0.12/0.37 % 487:1:2:[210.0,206.0]:TopTop: -> ren35(x0,x1)
% 0.12/0.37 % 421:2:2:INP:TopTop: -> r1(x0,x1),ren71(x0,x1)
% 0.12/0.37 % 501:1:2:[420.0,416.0]:TopTop: -> ren70(x0,x1)
% 0.12/0.37 % 500:1:2:[417.0,414.0]:TopTop: -> ren70(x0,x1)
% 0.12/0.37 % 413:2:2:INP:TopTop: -> r1(x0,x1),ren70(x0,x1)
% 0.12/0.37 % 211:2:2:INP:TopTop: -> r1(x0,x1),ren36(x0,x1)
% 0.12/0.37 % 212:2:2:INP:TopTop: p9(x0) -> ren36(x1,x0)
% 0.12/0.37 % 213:2:2:INP:TopTop: -> r1(x0,x1),ren37(x0,x1)
% 0.12/0.37 % 214:2:2:INP:TopTop: p8(x0) -> ren37(x1,x0)
% 0.12/0.37 % 215:2:2:INP:TopTop: -> r1(x0,x1),ren38(x0,x1)
% 0.12/0.37 % 216:2:2:INP:TopTop: -> r1(x0,skf15(x0)),ren38(x1,x0)
% 0.12/0.37 % 217:2:2:INP:TopTop: -> p9(skf15(x0)),ren38(x1,x0)
% 0.12/0.37 % 218:3:3:INP:TopTopTop: r1(skf15(x0),x1) -> p9(x1),ren38(x2,x0)
% 0.12/0.37 % 219:2:2:INP:TopTop: p8(skf15(x0)) -> ren38(x1,x0)
% 0.12/0.37 % 220:2:2:INP:TopTop: p9(x0) -> ren38(x1,x0)
% 0.12/0.37 % 412:2:2:INP:TopTop: -> p2(skf28(x0)),ren69(x1,x0)
% 0.12/0.37 % 222:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren38(x2,x0)
% 0.12/0.37 % 223:2:2:INP:TopTop: -> p8(x0),ren38(x1,x0)
% 0.12/0.37 % 224:2:2:INP:TopTop: -> r1(x0,x1),ren39(x0,x1)
% 0.12/0.37 % 225:2:2:INP:TopTop: -> p9(x0),ren39(x1,x0)
% 0.12/0.37 % 226:3:3:INP:TopTopTop: r1(x0,x1) -> p9(x1),ren39(x2,x0)
% 0.12/0.37 % 227:2:2:INP:TopTop: p8(x0) -> ren39(x1,x0)
% 0.12/0.37 % 228:2:2:INP:TopTop: -> r1(x0,skf16(x0)),ren39(x1,x0)
% 0.12/0.37 % 229:2:2:INP:TopTop: p9(skf16(x0)) -> ren39(x1,x0)
% 0.12/0.37 % 411:3:3:INP:TopTopTop: r1(skf28(x0),x1) -> p2(x1),ren69(x2,x0)
% 0.12/0.37 % 231:3:3:INP:TopTopTop: r1(skf16(x0),x1) -> p8(x1),ren39(x2,x0)
% 0.12/0.37 % 232:2:2:INP:TopTop: -> p8(skf16(x0)),ren39(x1,x0)
% 0.12/0.37 % 233:2:2:INP:TopTop: -> r1(x0,x1),ren40(x0,x1)
% 0.12/0.37 % 488:1:2:[237.0,234.0]:TopTop: -> ren40(x0,x1)
% 0.12/0.37 % 409:2:2:INP:TopTop: p3(skf28(x0)) -> ren69(x1,x0)
% 0.12/0.37 % 489:1:2:[238.0,236.0]:TopTop: -> ren40(x0,x1)
% 0.12/0.37 % 408:2:2:INP:TopTop: -> r1(x0,skf28(x0)),ren69(x1,x0)
% 0.12/0.37 % 407:2:2:INP:TopTop: p2(x0) -> ren69(x1,x0)
% 0.12/0.37 % 406:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren69(x2,x0)
% 0.12/0.37 % 405:2:2:INP:TopTop: -> p3(x0),ren69(x1,x0)
% 0.12/0.37 % 241:2:2:INP:TopTop: -> r1(x0,x1),ren41(x0,x1)
% 0.12/0.37 % 242:2:2:INP:TopTop: p8(x0) -> ren41(x1,x0)
% 0.12/0.37 % 243:2:2:INP:TopTop: -> r1(x0,x1),ren42(x0,x1)
% 0.12/0.37 % 244:2:2:INP:TopTop: p7(x0) -> ren42(x1,x0)
% 0.12/0.37 % 245:2:2:INP:TopTop: -> r1(x0,x1),ren43(x0,x1)
% 0.12/0.37 % 246:2:2:INP:TopTop: -> r1(x0,skf17(x0)),ren43(x1,x0)
% 0.12/0.37 % 247:2:2:INP:TopTop: -> p8(skf17(x0)),ren43(x1,x0)
% 0.12/0.37 % 248:3:3:INP:TopTopTop: r1(skf17(x0),x1) -> p8(x1),ren43(x2,x0)
% 0.12/0.37 % 249:2:2:INP:TopTop: p7(skf17(x0)) -> ren43(x1,x0)
% 0.12/0.37 % 250:2:2:INP:TopTop: p8(x0) -> ren43(x1,x0)
% 0.12/0.37 % 404:2:2:INP:TopTop: -> r1(x0,x1),ren69(x0,x1)
% 0.12/0.37 % 252:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren43(x2,x0)
% 0.12/0.37 % 253:2:2:INP:TopTop: -> p7(x0),ren43(x1,x0)
% 0.12/0.37 % 254:2:2:INP:TopTop: -> r1(x0,x1),ren44(x0,x1)
% 0.12/0.37 % 255:2:2:INP:TopTop: -> p8(x0),ren44(x1,x0)
% 0.12/0.37 % 256:3:3:INP:TopTopTop: r1(x0,x1) -> p8(x1),ren44(x2,x0)
% 0.12/0.37 % 257:2:2:INP:TopTop: p7(x0) -> ren44(x1,x0)
% 0.12/0.37 % 258:2:2:INP:TopTop: -> r1(x0,skf18(x0)),ren44(x1,x0)
% 0.12/0.37 % 259:2:2:INP:TopTop: p8(skf18(x0)) -> ren44(x1,x0)
% 0.12/0.37 % 403:2:2:INP:TopTop: -> p2(x0),ren68(x1,x0)
% 0.12/0.37 % 261:3:3:INP:TopTopTop: r1(skf18(x0),x1) -> p7(x1),ren44(x2,x0)
% 0.12/0.37 % 262:2:2:INP:TopTop: -> p7(skf18(x0)),ren44(x1,x0)
% 0.12/0.37 % 263:2:2:INP:TopTop: -> r1(x0,x1),ren45(x0,x1)
% 0.12/0.37 % 490:1:2:[267.0,264.0]:TopTop: -> ren45(x0,x1)
% 0.12/0.37 % 402:3:3:INP:TopTopTop: r1(x0,x1) -> p2(x1),ren68(x2,x0)
% 0.12/0.37 % 491:1:2:[268.0,266.0]:TopTop: -> ren45(x0,x1)
% 0.12/0.37 % 400:2:2:INP:TopTop: p3(x0) -> ren68(x1,x0)
% 0.12/0.37 % 399:2:2:INP:TopTop: p2(skf27(x0)) -> ren68(x1,x0)
% 0.12/0.37 % 398:3:3:INP:TopTopTop: r1(skf27(x0),x1) -> p3(x1),ren68(x2,x0)
% 0.12/0.37 % 397:2:2:INP:TopTop: -> p3(skf27(x0)),ren68(x1,x0)
% 0.12/0.37 % 271:2:2:INP:TopTop: -> r1(x0,x1),ren46(x0,x1)
% 0.12/0.37 % 272:2:2:INP:TopTop: p7(x0) -> ren46(x1,x0)
% 0.12/0.37 % 273:2:2:INP:TopTop: -> r1(x0,x1),ren47(x0,x1)
% 0.12/0.37 % 274:2:2:INP:TopTop: p6(x0) -> ren47(x1,x0)
% 0.12/0.37 % 275:2:2:INP:TopTop: -> r1(x0,x1),ren48(x0,x1)
% 0.12/0.37 % 276:2:2:INP:TopTop: -> r1(x0,skf19(x0)),ren48(x1,x0)
% 0.12/0.37 % 277:2:2:INP:TopTop: -> p7(skf19(x0)),ren48(x1,x0)
% 0.12/0.37 % 278:3:3:INP:TopTopTop: r1(skf19(x0),x1) -> p7(x1),ren48(x2,x0)
% 0.12/0.37 % 279:2:2:INP:TopTop: p6(skf19(x0)) -> ren48(x1,x0)
% 0.12/0.37 % 280:2:2:INP:TopTop: p7(x0) -> ren48(x1,x0)
% 0.12/0.37 % 396:2:2:INP:TopTop: -> r1(x0,skf27(x0)),ren68(x1,x0)
% 0.12/0.37 % 282:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren48(x2,x0)
% 0.12/0.37 % 283:2:2:INP:TopTop: -> p6(x0),ren48(x1,x0)
% 0.12/0.37 % 284:2:2:INP:TopTop: -> r1(x0,x1),ren49(x0,x1)
% 0.12/0.37 % 285:2:2:INP:TopTop: -> p7(x0),ren49(x1,x0)
% 0.12/0.37 % 286:3:3:INP:TopTopTop: r1(x0,x1) -> p7(x1),ren49(x2,x0)
% 0.12/0.37 % 287:2:2:INP:TopTop: p6(x0) -> ren49(x1,x0)
% 0.12/0.37 % 288:2:2:INP:TopTop: -> r1(x0,skf20(x0)),ren49(x1,x0)
% 0.12/0.37 % 289:2:2:INP:TopTop: p7(skf20(x0)) -> ren49(x1,x0)
% 0.12/0.37 % 395:2:2:INP:TopTop: -> r1(x0,x1),ren68(x0,x1)
% 0.12/0.37 % 291:3:3:INP:TopTopTop: r1(skf20(x0),x1) -> p6(x1),ren49(x2,x0)
% 0.12/0.37 % 292:2:2:INP:TopTop: -> p6(skf20(x0)),ren49(x1,x0)
% 0.12/0.37 % 293:2:2:INP:TopTop: -> r1(x0,x1),ren50(x0,x1)
% 0.12/0.37 % 492:1:2:[297.0,294.0]:TopTop: -> ren50(x0,x1)
% 0.12/0.37 % 394:2:2:INP:TopTop: p2(x0) -> ren67(x1,x0)
% 0.12/0.37 % 493:1:2:[298.0,296.0]:TopTop: -> ren50(x0,x1)
% 0.12/0.37 % 393:2:2:INP:TopTop: -> r1(x0,x1),ren67(x0,x1)
% 0.12/0.37 % 392:2:2:INP:TopTop: p3(x0) -> ren66(x1,x0)
% 0.12/0.37 % 391:2:2:INP:TopTop: -> r1(x0,x1),ren66(x0,x1)
% 0.12/0.37 % 499:1:2:[390.0,386.0]:TopTop: -> ren65(x0,x1)
% 0.12/0.37 % 301:2:2:INP:TopTop: -> r1(x0,x1),ren51(x0,x1)
% 0.12/0.37 % 302:2:2:INP:TopTop: p6(x0) -> ren51(x1,x0)
% 0.12/0.37 % 303:2:2:INP:TopTop: -> r1(x0,x1),ren52(x0,x1)
% 0.12/0.37 % 304:2:2:INP:TopTop: p5(x0) -> ren52(x1,x0)
% 0.12/0.37 % 305:2:2:INP:TopTop: -> r1(x0,x1),ren53(x0,x1)
% 0.12/0.37 % 306:2:2:INP:TopTop: -> r1(x0,skf21(x0)),ren53(x1,x0)
% 0.12/0.37 % 307:2:2:INP:TopTop: -> p6(skf21(x0)),ren53(x1,x0)
% 0.12/0.37 % 308:3:3:INP:TopTopTop: r1(skf21(x0),x1) -> p6(x1),ren53(x2,x0)
% 0.12/0.37 % 309:2:2:INP:TopTop: p5(skf21(x0)) -> ren53(x1,x0)
% 0.12/0.37 % 310:2:2:INP:TopTop: p6(x0) -> ren53(x1,x0)
% 0.12/0.37 % 498:1:2:[387.0,384.0]:TopTop: -> ren65(x0,x1)
% 0.12/0.37 % 312:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren53(x2,x0)
% 0.12/0.37 % 313:2:2:INP:TopTop: -> p5(x0),ren53(x1,x0)
% 0.12/0.37 % 314:2:2:INP:TopTop: -> r1(x0,x1),ren54(x0,x1)
% 0.12/0.37 % 315:2:2:INP:TopTop: -> p6(x0),ren54(x1,x0)
% 0.12/0.37 % 316:3:3:INP:TopTopTop: r1(x0,x1) -> p6(x1),ren54(x2,x0)
% 0.12/0.37 % 317:2:2:INP:TopTop: p5(x0) -> ren54(x1,x0)
% 0.12/0.37 % 318:2:2:INP:TopTop: -> r1(x0,skf22(x0)),ren54(x1,x0)
% 0.12/0.37 % 319:2:2:INP:TopTop: p6(skf22(x0)) -> ren54(x1,x0)
% 0.12/0.37 % 383:2:2:INP:TopTop: -> r1(x0,x1),ren65(x0,x1)
% 0.12/0.37 % 321:3:3:INP:TopTopTop: r1(skf22(x0),x1) -> p5(x1),ren54(x2,x0)
% 0.12/0.37 % 322:2:2:INP:TopTop: -> p5(skf22(x0)),ren54(x1,x0)
% 0.12/0.37 % 323:2:2:INP:TopTop: -> r1(x0,x1),ren55(x0,x1)
% 0.12/0.37 % 494:1:2:[327.0,324.0]:TopTop: -> ren55(x0,x1)
% 0.12/0.37 % 382:2:2:INP:TopTop: -> p3(skf26(x0)),ren64(x1,x0)
% 0.12/0.37 % 495:1:2:[328.0,326.0]:TopTop: -> ren55(x0,x1)
% 0.12/0.37 % 381:3:3:INP:TopTopTop: r1(skf26(x0),x1) -> p3(x1),ren64(x2,x0)
% 0.12/0.37 % 379:2:2:INP:TopTop: p4(skf26(x0)) -> ren64(x1,x0)
% 0.12/0.37 % 378:2:2:INP:TopTop: -> r1(x0,skf26(x0)),ren64(x1,x0)
% 0.12/0.37 % 377:2:2:INP:TopTop: p3(x0) -> ren64(x1,x0)
% 0.12/0.37 % 331:2:2:INP:TopTop: -> r1(x0,x1),ren56(x0,x1)
% 0.12/0.37 % 332:2:2:INP:TopTop: p5(x0) -> ren56(x1,x0)
% 0.12/0.37 % 333:2:2:INP:TopTop: -> r1(x0,x1),ren57(x0,x1)
% 0.12/0.37 % 334:2:2:INP:TopTop: p4(x0) -> ren57(x1,x0)
% 0.12/0.37 % 335:2:2:INP:TopTop: -> r1(x0,x1),ren58(x0,x1)
% 0.12/0.37 % 336:2:2:INP:TopTop: -> r1(x0,skf23(x0)),ren58(x1,x0)
% 0.12/0.37 % 337:2:2:INP:TopTop: -> p5(skf23(x0)),ren58(x1,x0)
% 0.12/0.37 % 338:3:3:INP:TopTopTop: r1(skf23(x0),x1) -> p5(x1),ren58(x2,x0)
% 0.12/0.37 % 339:2:2:INP:TopTop: p4(skf23(x0)) -> ren58(x1,x0)
% 0.12/0.37 % 340:2:2:INP:TopTop: p5(x0) -> ren58(x1,x0)
% 0.12/0.37 % 376:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren64(x2,x0)
% 0.12/0.37 % 342:3:3:INP:TopTopTop: r1(x0,x1) -> p4(x1),ren58(x2,x0)
% 0.12/0.37 % 343:2:2:INP:TopTop: -> p4(x0),ren58(x1,x0)
% 0.12/0.37 % 344:2:2:INP:TopTop: -> r1(x0,x1),ren59(x0,x1)
% 0.12/0.37 % 345:2:2:INP:TopTop: -> p5(x0),ren59(x1,x0)
% 0.12/0.37 % 346:3:3:INP:TopTopTop: r1(x0,x1) -> p5(x1),ren59(x2,x0)
% 0.12/0.37 % 347:2:2:INP:TopTop: p4(x0) -> ren59(x1,x0)
% 0.12/0.37 % 348:2:2:INP:TopTop: -> r1(x0,skf24(x0)),ren59(x1,x0)
% 0.12/0.37 % 349:2:2:INP:TopTop: p5(skf24(x0)) -> ren59(x1,x0)
% 0.12/0.37 % 375:2:2:INP:TopTop: -> p4(x0),ren64(x1,x0)
% 0.12/0.37 % 351:3:3:INP:TopTopTop: r1(skf24(x0),x1) -> p4(x1),ren59(x2,x0)
% 0.12/0.37 % 352:2:2:INP:TopTop: -> p4(skf24(x0)),ren59(x1,x0)
% 0.12/0.37 % 353:2:2:INP:TopTop: -> r1(x0,x1),ren60(x0,x1)
% 0.12/0.37 % 496:1:2:[357.0,354.0]:TopTop: -> ren60(x0,x1)
% 0.12/0.37 % 374:2:2:INP:TopTop: -> r1(x0,x1),ren64(x0,x1)
% 0.12/0.37 % 497:1:2:[360.0,356.0]:TopTop: -> ren60(x0,x1)
% 0.12/0.37 % 373:2:2:INP:TopTop: -> p3(x0),ren63(x1,x0)
% 0.12/0.37 % 372:3:3:INP:TopTopTop: r1(x0,x1) -> p3(x1),ren63(x2,x0)
% 0.12/0.37 % 370:2:2:INP:TopTop: p4(x0) -> ren63(x1,x0)
% 0.12/0.37 % 369:2:2:INP:TopTop: p3(skf25(x0)) -> ren63(x1,x0)
% 0.12/0.37 % 361:2:2:INP:TopTop: -> r1(x0,x1),ren61(x0,x1)
% 0.12/0.37 % 362:2:2:INP:TopTop: p4(x0) -> ren61(x1,x0)
% 0.12/0.37 % 363:2:2:INP:TopTop: -> r1(x0,x1),ren62(x0,x1)
% 0.12/0.37 % 364:2:2:INP:TopTop: p3(x0) -> ren62(x1,x0)
% 0.12/0.37 % 365:2:2:INP:TopTop: -> r1(x0,x1),ren63(x0,x1)
% 0.12/0.37 % 366:2:2:INP:TopTop: -> r1(x0,skf25(x0)),ren63(x1,x0)
% 0.12/0.37 % 367:2:2:INP:TopTop: -> p4(skf25(x0)),ren63(x1,x0)
% 0.12/0.37 % 368:3:3:INP:TopTopTop: r1(skf25(x0),x1) -> p4(x1),ren63(x2,x0)
% 0.12/0.37
% 0.12/0.37 % Reduced Input Conjecture Clauses:
% 0.12/0.37 % 520:10:2:[503.1,473.8]:TopTop: r1(skc31,x0),p2(x0),ren71(x0,skf104(x0)),r1(skc31,x1),ren72(x1,skf105(x1)),p1(x1),ren73(skc31,skc106),ren74(skc31,skc107) -> p1(x0),p2(x1)
% 0.12/0.37 % 519:10:2:[501.1,472.8]:TopTop: r1(skc31,x0),p3(x0),ren66(x0,skf99(x0)),r1(skc31,x1),ren67(x1,skf100(x1)),p2(x1),ren68(skc31,skc101),ren69(skc31,skc102) -> p2(x0),p3(x1)
% 0.12/0.37 % 518:10:2:[499.1,471.8]:TopTop: r1(skc31,x0),p4(x0),ren61(x0,skf94(x0)),r1(skc31,x1),ren62(x1,skf95(x1)),p3(x1),ren63(skc31,skc96),ren64(skc31,skc97) -> p3(x0),p4(x1)
% 0.12/0.37 % 517:10:2:[496.1,470.8]:TopTop: r1(skc31,x0),p5(x0),ren56(x0,skf89(x0)),r1(skc31,x1),ren57(x1,skf90(x1)),p4(x1),ren58(skc31,skc91),ren59(skc31,skc92) -> p4(x0),p5(x1)
% 0.12/0.37 % 516:10:2:[495.1,469.8]:TopTop: r1(skc31,x0),p6(x0),ren51(x0,skf84(x0)),r1(skc31,x1),ren52(x1,skf85(x1)),p5(x1),ren53(skc31,skc86),ren54(skc31,skc87) -> p5(x0),p6(x1)
% 0.12/0.37 % 468:1:0:INP:: -> p15(skc83)
% 0.12/0.37 % 467:2:1:INP:Top: r1(skc83,x0) -> p15(x0)
% 0.12/0.37 % 515:0:0:[468.0,466.0]:: ->
% 0.12/0.37 % 465:1:0:INP:: -> r1(skc31,skc83)
% 0.12/0.37 % 464:1:0:INP:: -> p15(skc82)
% 0.12/0.37 % 463:2:1:INP:Top: r1(skc82,x0) -> p15(x0)
% 0.12/0.37 % 514:0:0:[464.0,462.0]:: ->
% 0.12/0.37 % 461:1:0:INP:: -> r1(skc31,skc82)
% 0.12/0.37 % 513:10:2:[493.1,460.8]:TopTop: r1(skc31,x0),p7(x0),ren46(x0,skf77(x0)),r1(skc31,x1),ren47(x1,skf78(x1)),p6(x1),ren48(skc31,skc79),ren49(skc31,skc80) -> p6(x0),p7(x1)
% 0.12/0.37 % 512:10:2:[491.1,459.8]:TopTop: r1(skc31,x0),p8(x0),ren41(x0,skf72(x0)),r1(skc31,x1),ren42(x1,skf73(x1)),p7(x1),ren43(skc31,skc74),ren44(skc31,skc75) -> p7(x0),p8(x1)
% 0.12/0.37 % 511:10:2:[488.1,458.8]:TopTop: r1(skc31,x0),p9(x0),ren36(x0,skf67(x0)),r1(skc31,x1),ren37(x1,skf68(x1)),p8(x1),ren38(skc31,skc69),ren39(skc31,skc70) -> p8(x0),p9(x1)
% 0.12/0.37 % 510:10:2:[486.1,457.8]:TopTop: r1(skc31,x0),p10(x0),ren31(x0,skf62(x0)),r1(skc31,x1),ren32(x1,skf63(x1)),p9(x1),ren33(skc31,skc64),ren34(skc31,skc65) -> p9(x0),p10(x1)
% 0.12/0.37 % 509:10:2:[485.1,456.8]:TopTop: r1(skc31,x0),p11(x0),ren26(x0,skf57(x0)),r1(skc31,x1),ren27(x1,skf58(x1)),p10(x1),ren28(skc31,skc59),ren29(skc31,skc60) -> p10(x0),p11(x1)
% 0.12/0.37 % 508:10:2:[482.1,455.8]:TopTop: r1(skc31,x0),p12(x0),ren21(x0,skf52(x0)),r1(skc31,x1),ren22(x1,skf53(x1)),p11(x1),ren23(skc31,skc54),ren24(skc31,skc55) -> p11(x0),p12(x1)
% 0.12/0.37 % 507:10:2:[481.1,454.8]:TopTop: r1(skc31,x0),p13(x0),ren16(x0,skf47(x0)),r1(skc31,x1),ren17(x1,skf48(x1)),p12(x1),ren18(skc31,skc49),ren19(skc31,skc50) -> p12(x0),p13(x1)
% 0.12/0.37 % 506:10:2:[479.1,453.8]:TopTop: r1(skc31,x0),p14(x0),ren11(x0,skf42(x0)),r1(skc31,x1),ren12(x1,skf43(x1)),p13(x1),ren13(skc31,skc44),ren14(skc31,skc45) -> p13(x0),p14(x1)
% 0.12/0.37 % 505:10:2:[476.1,452.8]:TopTop: r1(skc31,x0),p15(x0),ren6(x0,skf37(x0)),r1(skc31,x1),ren7(x1,skf38(x1)),p14(x1),ren8(skc31,skc39),ren9(skc31,skc40) -> p14(x0),p15(x1)
% 0.12/0.37 % 504:10:2:[475.1,451.8]:TopTop: r1(skc31,x0),p16(x0),ren1(x0,skf32(x0)),r1(skc31,x1),ren2(x1,skf33(x1)),p15(x1),ren3(skc31,skc34),ren4(skc31,skc35) -> p15(x0),p16(x1)
% 0.12/0.37
% 0.12/0.37 % SZS status Theorem
% 0.12/0.37
% 0.12/0.37 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.12/0.37 % SZS output start Proof for theBenchmark
% See solution above
% 0.12/0.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.12/0.40
% 0.12/0.40 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % SPASS-SCL-FOL Statistics:
% 0.12/0.40 % Number of learned clauses: 0
% 0.12/0.40 % Number of propagations: 0
% 0.12/0.40 % Number of decisions: 0
% 0.12/0.40 % Number of resolutions: 0
% 0.12/0.40 % Number of condensations: 0
% 0.12/0.40 % Number of sub resolutions: 47
% 0.12/0.40
% 0.12/0.40 % Needed: 0:00:00.03
% 0.12/0.40
% 0.12/0.40 % ###
% 0.12/0.40 % ### Pagesize: 8192
% 0.12/0.40 % ### Marksize: 0
% 0.12/0.40 % ### Memory demanded: 1517 KBytes
% 0.12/0.40 % ### Memory freed: 1517 KBytes
% 0.12/0.40 % ### Memory remaining: 0 Bytes
% 0.12/0.40 % ### Pages allocated: 230 Pages
% 0.12/0.40 % ###
%------------------------------------------------------------------------------