%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL674+1.010 : 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 : n029.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:10:07 PM UTC 2026
% Result : Theorem 7.25s 7.55s
% Output : Proof 7.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 25
% Syntax : Number of formulae : 89 ( 13 unt; 22 def)
% Number of atoms : 1227 ( 0 equ)
% Maximal formula atoms : 226 ( 13 avg)
% Number of connectives : 2093 ( 955 ~; 603 |; 511 &)
% ( 0 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 42 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 47 ( 46 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 1 con; 0-1 aty)
% Number of variables : 272 ( 0 sgn 223 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ( ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p11(X1)
& ~ p111(X1)
& p110(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p11(X1)
& ~ p111(X1)
& p110(X1) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p10(X1)
& ~ p110(X1)
& p109(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p10(X1)
& ~ p110(X1)
& p109(X1) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p9(X1)
& ~ p109(X1)
& p108(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p9(X1)
& ~ p109(X1)
& p108(X1) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p8(X1)
& ~ p108(X1)
& p107(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p8(X1)
& ~ p108(X1)
& p107(X1) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p7(X1)
& ~ p107(X1)
& p106(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p7(X1)
& ~ p107(X1)
& p106(X1) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p6(X1)
& ~ p106(X1)
& p105(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ~ p106(X1)
& p105(X1) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p5(X1)
& ~ p105(X1)
& p104(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ~ p105(X1)
& p104(X1) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p4(X1)
& ~ p104(X1)
& p103(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ~ p104(X1)
& p103(X1) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p3(X1)
& ~ p103(X1)
& p102(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ~ p103(X1)
& p102(X1) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p2(X1)
& ~ p102(X1)
& p101(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ~ p102(X1)
& p101(X1) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p11(X1)
| ~ p110(X1) )
| p11(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p11(X1)
| ~ p110(X1) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p10(X1)
| ~ p109(X1) )
| p10(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1)
| ~ p109(X1) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p9(X1)
| ~ p108(X1) )
| p9(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p9(X1)
| ~ p108(X1) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p8(X1)
| ~ p107(X1) )
| p8(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p8(X1)
| ~ p107(X1) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p7(X1)
| ~ p106(X1) )
| p7(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p7(X1)
| ~ p106(X1) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p6(X1)
| ~ p105(X1) )
| p6(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ p105(X1) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p5(X1)
| ~ p104(X1) )
| p5(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ p104(X1) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p4(X1)
| ~ p103(X1) )
| p4(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ p103(X1) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p3(X1)
| ~ p102(X1) )
| p3(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ p102(X1) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1)
| ~ p101(X1) )
| p2(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ p101(X1) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1)
| ~ p100(X1) )
| p1(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1)
| ~ p100(X1) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
file('theBenchmark.p',main) ).
% NEGATING CONJECTURE
fof(main_nc,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ( ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p11(X1)
& ~ p111(X1)
& p110(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p11(X1)
& ~ p111(X1)
& p110(X1) ) ) )
| ~ ( ~ p110(X2)
& p109(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p10(X1)
& ~ p110(X1)
& p109(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p10(X1)
& ~ p110(X1)
& p109(X1) ) ) )
| ~ ( ~ p109(X2)
& p108(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p9(X1)
& ~ p109(X1)
& p108(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p9(X1)
& ~ p109(X1)
& p108(X1) ) ) )
| ~ ( ~ p108(X2)
& p107(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p8(X1)
& ~ p108(X1)
& p107(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p8(X1)
& ~ p108(X1)
& p107(X1) ) ) )
| ~ ( ~ p107(X2)
& p106(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p7(X1)
& ~ p107(X1)
& p106(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p7(X1)
& ~ p107(X1)
& p106(X1) ) ) )
| ~ ( ~ p106(X2)
& p105(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p6(X1)
& ~ p106(X1)
& p105(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p6(X1)
& ~ p106(X1)
& p105(X1) ) ) )
| ~ ( ~ p105(X2)
& p104(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p5(X1)
& ~ p105(X1)
& p104(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p5(X1)
& ~ p105(X1)
& p104(X1) ) ) )
| ~ ( ~ p104(X2)
& p103(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p4(X1)
& ~ p104(X1)
& p103(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p4(X1)
& ~ p104(X1)
& p103(X1) ) ) )
| ~ ( ~ p103(X2)
& p102(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p3(X1)
& ~ p103(X1)
& p102(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p3(X1)
& ~ p103(X1)
& p102(X1) ) ) )
| ~ ( ~ p102(X2)
& p101(X2) ) )
& ( ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ p2(X1)
& ~ p102(X1)
& p101(X1) ) )
& ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( p2(X1)
& ~ p102(X1)
& p101(X1) ) ) )
| ~ ( ~ p101(X2)
& p100(X2) ) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p11(X1)
| ~ p110(X1) )
| p11(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p11(X1)
| ~ p110(X1) )
| ~ p11(X2) ) )
| ~ p110(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p10(X1)
| ~ p109(X1) )
| p10(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p10(X1)
| ~ p109(X1) )
| ~ p10(X2) ) )
| ~ p109(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p9(X1)
| ~ p108(X1) )
| p9(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p9(X1)
| ~ p108(X1) )
| ~ p9(X2) ) )
| ~ p108(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p8(X1)
| ~ p107(X1) )
| p8(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p8(X1)
| ~ p107(X1) )
| ~ p8(X2) ) )
| ~ p107(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p7(X1)
| ~ p106(X1) )
| p7(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p7(X1)
| ~ p106(X1) )
| ~ p7(X2) ) )
| ~ p106(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p6(X1)
| ~ p105(X1) )
| p6(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1)
| ~ p105(X1) )
| ~ p6(X2) ) )
| ~ p105(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p5(X1)
| ~ p104(X1) )
| p5(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1)
| ~ p104(X1) )
| ~ p5(X2) ) )
| ~ p104(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p4(X1)
| ~ p103(X1) )
| p4(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1)
| ~ p103(X1) )
| ~ p4(X2) ) )
| ~ p103(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p3(X1)
| ~ p102(X1) )
| p3(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1)
| ~ p102(X1) )
| ~ p3(X2) ) )
| ~ p102(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1)
| ~ p101(X1) )
| p2(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1)
| ~ p101(X1) )
| ~ p2(X2) ) )
| ~ p101(X2) )
& ( ( ( ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1)
| ~ p100(X1) )
| p1(X2) )
& ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1)
| ~ p100(X1) )
| ~ p1(X2) ) )
| ~ p100(X2) )
& ( p110(X2)
| ~ p111(X2) )
& ( p109(X2)
| ~ p110(X2) )
& ( p108(X2)
| ~ p109(X2) )
& ( p107(X2)
| ~ p108(X2) )
& ( p106(X2)
| ~ p107(X2) )
& ( p105(X2)
| ~ p106(X2) )
& ( p104(X2)
| ~ p105(X2) )
& ( p103(X2)
| ~ p104(X2) )
& ( p102(X2)
| ~ p103(X2) )
& ( p101(X2)
| ~ p102(X2) )
& ( p100(X2)
| ~ p101(X2) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
inference(negating_conjecture,[status(cth)],[main]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimTB,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ( ! [X3] :
( ~ r1(X1,X3)
| ( ( ( ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ( ~ p11(X4)
& ~ p111(X4)
& p110(X4) ) )
& ~ ! [X5] :
( ~ r1(X3,X5)
| ~ ( p11(X5)
& ~ p111(X5)
& p110(X5) ) ) )
| ~ ( ~ p110(X3)
& p109(X3) ) )
& ( ( ~ ! [X6] :
( ~ r1(X3,X6)
| ~ ( ~ p10(X6)
& ~ p110(X6)
& p109(X6) ) )
& ~ ! [X7] :
( ~ r1(X3,X7)
| ~ ( p10(X7)
& ~ p110(X7)
& p109(X7) ) ) )
| ~ ( ~ p109(X3)
& p108(X3) ) )
& ( ( ~ ! [X8] :
( ~ r1(X3,X8)
| ~ ( ~ p9(X8)
& ~ p109(X8)
& p108(X8) ) )
& ~ ! [X9] :
( ~ r1(X3,X9)
| ~ ( p9(X9)
& ~ p109(X9)
& p108(X9) ) ) )
| ~ ( ~ p108(X3)
& p107(X3) ) )
& ( ( ~ ! [X10] :
( ~ r1(X3,X10)
| ~ ( ~ p8(X10)
& ~ p108(X10)
& p107(X10) ) )
& ~ ! [X11] :
( ~ r1(X3,X11)
| ~ ( p8(X11)
& ~ p108(X11)
& p107(X11) ) ) )
| ~ ( ~ p107(X3)
& p106(X3) ) )
& ( ( ~ ! [X12] :
( ~ r1(X3,X12)
| ~ ( ~ p7(X12)
& ~ p107(X12)
& p106(X12) ) )
& ~ ! [X13] :
( ~ r1(X3,X13)
| ~ ( p7(X13)
& ~ p107(X13)
& p106(X13) ) ) )
| ~ ( ~ p106(X3)
& p105(X3) ) )
& ( ( ~ ! [X14] :
( ~ r1(X3,X14)
| ~ ( ~ p6(X14)
& ~ p106(X14)
& p105(X14) ) )
& ~ ! [X15] :
( ~ r1(X3,X15)
| ~ ( p6(X15)
& ~ p106(X15)
& p105(X15) ) ) )
| ~ ( ~ p105(X3)
& p104(X3) ) )
& ( ( ~ ! [X16] :
( ~ r1(X3,X16)
| ~ ( ~ p5(X16)
& ~ p105(X16)
& p104(X16) ) )
& ~ ! [X17] :
( ~ r1(X3,X17)
| ~ ( p5(X17)
& ~ p105(X17)
& p104(X17) ) ) )
| ~ ( ~ p104(X3)
& p103(X3) ) )
& ( ( ~ ! [X18] :
( ~ r1(X3,X18)
| ~ ( ~ p4(X18)
& ~ p104(X18)
& p103(X18) ) )
& ~ ! [X19] :
( ~ r1(X3,X19)
| ~ ( p4(X19)
& ~ p104(X19)
& p103(X19) ) ) )
| ~ ( ~ p103(X3)
& p102(X3) ) )
& ( ( ~ ! [X20] :
( ~ r1(X3,X20)
| ~ ( ~ p3(X20)
& ~ p103(X20)
& p102(X20) ) )
& ~ ! [X21] :
( ~ r1(X3,X21)
| ~ ( p3(X21)
& ~ p103(X21)
& p102(X21) ) ) )
| ~ ( ~ p102(X3)
& p101(X3) ) )
& ( ( ~ ! [X22] :
( ~ r1(X3,X22)
| ~ ( ~ p2(X22)
& ~ p102(X22)
& p101(X22) ) )
& ~ ! [X23] :
( ~ r1(X3,X23)
| ~ ( p2(X23)
& ~ p102(X23)
& p101(X23) ) ) )
| ~ ( ~ p101(X3)
& p100(X3) ) )
& ( ( ( ! [X24] :
( ~ r1(X3,X24)
| ~ p11(X24)
| ~ p110(X24) )
| p11(X3) )
& ( ! [X25] :
( ~ r1(X3,X25)
| p11(X25)
| ~ p110(X25) )
| ~ p11(X3) ) )
| ~ p110(X3) )
& ( ( ( ! [X26] :
( ~ r1(X3,X26)
| ~ p10(X26)
| ~ p109(X26) )
| p10(X3) )
& ( ! [X27] :
( ~ r1(X3,X27)
| p10(X27)
| ~ p109(X27) )
| ~ p10(X3) ) )
| ~ p109(X3) )
& ( ( ( ! [X28] :
( ~ r1(X3,X28)
| ~ p9(X28)
| ~ p108(X28) )
| p9(X3) )
& ( ! [X29] :
( ~ r1(X3,X29)
| p9(X29)
| ~ p108(X29) )
| ~ p9(X3) ) )
| ~ p108(X3) )
& ( ( ( ! [X30] :
( ~ r1(X3,X30)
| ~ p8(X30)
| ~ p107(X30) )
| p8(X3) )
& ( ! [X31] :
( ~ r1(X3,X31)
| p8(X31)
| ~ p107(X31) )
| ~ p8(X3) ) )
| ~ p107(X3) )
& ( ( ( ! [X32] :
( ~ r1(X3,X32)
| ~ p7(X32)
| ~ p106(X32) )
| p7(X3) )
& ( ! [X33] :
( ~ r1(X3,X33)
| p7(X33)
| ~ p106(X33) )
| ~ p7(X3) ) )
| ~ p106(X3) )
& ( ( ( ! [X34] :
( ~ r1(X3,X34)
| ~ p6(X34)
| ~ p105(X34) )
| p6(X3) )
& ( ! [X35] :
( ~ r1(X3,X35)
| p6(X35)
| ~ p105(X35) )
| ~ p6(X3) ) )
| ~ p105(X3) )
& ( ( ( ! [X36] :
( ~ r1(X3,X36)
| ~ p5(X36)
| ~ p104(X36) )
| p5(X3) )
& ( ! [X37] :
( ~ r1(X3,X37)
| p5(X37)
| ~ p104(X37) )
| ~ p5(X3) ) )
| ~ p104(X3) )
& ( ( ( ! [X38] :
( ~ r1(X3,X38)
| ~ p4(X38)
| ~ p103(X38) )
| p4(X3) )
& ( ! [X39] :
( ~ r1(X3,X39)
| p4(X39)
| ~ p103(X39) )
| ~ p4(X3) ) )
| ~ p103(X3) )
& ( ( ( ! [X40] :
( ~ r1(X3,X40)
| ~ p3(X40)
| ~ p102(X40) )
| p3(X3) )
& ( ! [X41] :
( ~ r1(X3,X41)
| p3(X41)
| ~ p102(X41) )
| ~ p3(X3) ) )
| ~ p102(X3) )
& ( ( ( ! [X42] :
( ~ r1(X3,X42)
| ~ p2(X42)
| ~ p101(X42) )
| p2(X3) )
& ( ! [X43] :
( ~ r1(X3,X43)
| p2(X43)
| ~ p101(X43) )
| ~ p2(X3) ) )
| ~ p101(X3) )
& ( ( ( ! [X44] :
( ~ r1(X3,X44)
| ~ p1(X44)
| ~ p100(X44) )
| p1(X3) )
& ( ! [X45] :
( ~ r1(X3,X45)
| p1(X45)
| ~ p100(X45) )
| ~ p1(X3) ) )
| ~ p100(X3) )
& ( p110(X3)
| ~ p111(X3) )
& ( p109(X3)
| ~ p110(X3) )
& ( p108(X3)
| ~ p109(X3) )
& ( p107(X3)
| ~ p108(X3) )
& ( p106(X3)
| ~ p107(X3) )
& ( p105(X3)
| ~ p106(X3) )
& ( p104(X3)
| ~ p105(X3) )
& ( p103(X3)
| ~ p104(X3) )
& ( p102(X3)
| ~ p103(X3) )
& ( p101(X3)
| ~ p102(X3) )
& ( p100(X3)
| ~ p101(X3) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X3] :
( ren9(X3)
=> ( ~ ! [X20] :
( ~ r1(X3,X20)
| ~ ( ~ p3(X20)
& ~ p103(X20)
& p102(X20) ) )
& ~ ! [X21] :
( ~ r1(X3,X21)
| ~ ( p3(X21)
& ~ p103(X21)
& p102(X21) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF SIMPLE INFERENCE
fof(ren9_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren9(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p3(X2)
& ~ p103(X2)
& p102(X2) )
& ? [X3] :
( r1(X1,X3)
& p3(X3)
& ~ p103(X3)
& p102(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren9_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren9_skol,plain,
! [X1] :
( ~ ren9(X1)
| ( r1(X1,skf17(X1))
& ~ p3(skf17(X1))
& ~ p103(skf17(X1))
& p102(skf17(X1))
& r1(X1,skf18(X1))
& p3(skf18(X1))
& ~ p103(skf18(X1))
& p102(skf18(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf17,skf18]),skolemize(X2,skf17(X1)),skolemize(X3,skf18(X1))],[ren9_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_71,plain,
( ~ ren9(X0)
| r1(X0,skf18(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren9_skol])]) ).
% FILE RECORD
fof(transitivity,axiom,
! [X1,X2,X3] :
( ( r1(X1,X2)
& r1(X2,X3) )
=> r1(X1,X3) ),
file('theBenchmark.p',transitivity) ).
% FOF SIMPLE INFERENCE
fof(transitivity_elimTB,axiom,
! [X1,X2,X3] :
( ( r1(X1,X2)
& r1(X2,X3) )
=> r1(X1,X3) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[transitivity])]) ).
% FOF SIMPLE INFERENCE
fof(transitivity_elimImpEquivPushNegMiniScope,axiom,
! [X1,X2,X3] :
( ~ r1(X1,X2)
| ~ r1(X2,X3)
| r1(X1,X3) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[transitivity_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_2,plain,
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X0,X2) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[transitivity_elimImpEquivPushNegMiniScope])]) ).
% CNF SPASS RESOLUTION.
cnf(c_305,plain,
( ~ ren9(X0)
| ~ r1(X1,X0)
| r1(X1,skf18(X0)) ),
inference(resolution,[status(thm)],[c_71,c_2]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X3] :
( ren1(X3)
=> ( ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ( ~ p11(X4)
& ~ p111(X4)
& p110(X4) ) )
& ~ ! [X5] :
( ~ r1(X3,X5)
| ~ ( p11(X5)
& ~ p111(X5)
& p110(X5) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X3] :
( ren2(X3)
=> ( ~ ! [X6] :
( ~ r1(X3,X6)
| ~ ( ~ p10(X6)
& ~ p110(X6)
& p109(X6) ) )
& ~ ! [X7] :
( ~ r1(X3,X7)
| ~ ( p10(X7)
& ~ p110(X7)
& p109(X7) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X3] :
( ren3(X3)
=> ( ~ ! [X8] :
( ~ r1(X3,X8)
| ~ ( ~ p9(X8)
& ~ p109(X8)
& p108(X8) ) )
& ~ ! [X9] :
( ~ r1(X3,X9)
| ~ ( p9(X9)
& ~ p109(X9)
& p108(X9) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X3] :
( ren4(X3)
=> ( ~ ! [X10] :
( ~ r1(X3,X10)
| ~ ( ~ p8(X10)
& ~ p108(X10)
& p107(X10) ) )
& ~ ! [X11] :
( ~ r1(X3,X11)
| ~ ( p8(X11)
& ~ p108(X11)
& p107(X11) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X3] :
( ren5(X3)
=> ( ~ ! [X12] :
( ~ r1(X3,X12)
| ~ ( ~ p7(X12)
& ~ p107(X12)
& p106(X12) ) )
& ~ ! [X13] :
( ~ r1(X3,X13)
| ~ ( p7(X13)
& ~ p107(X13)
& p106(X13) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X3] :
( ren6(X3)
=> ( ~ ! [X14] :
( ~ r1(X3,X14)
| ~ ( ~ p6(X14)
& ~ p106(X14)
& p105(X14) ) )
& ~ ! [X15] :
( ~ r1(X3,X15)
| ~ ( p6(X15)
& ~ p106(X15)
& p105(X15) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X3] :
( ren7(X3)
=> ( ~ ! [X16] :
( ~ r1(X3,X16)
| ~ ( ~ p5(X16)
& ~ p105(X16)
& p104(X16) ) )
& ~ ! [X17] :
( ~ r1(X3,X17)
| ~ ( p5(X17)
& ~ p105(X17)
& p104(X17) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X3] :
( ren8(X3)
=> ( ~ ! [X18] :
( ~ r1(X3,X18)
| ~ ( ~ p4(X18)
& ~ p104(X18)
& p103(X18) ) )
& ~ ! [X19] :
( ~ r1(X3,X19)
| ~ ( p4(X19)
& ~ p104(X19)
& p103(X19) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X3] :
( ren10(X3)
=> ( ~ ! [X22] :
( ~ r1(X3,X22)
| ~ ( ~ p2(X22)
& ~ p102(X22)
& p101(X22) ) )
& ~ ! [X23] :
( ~ r1(X3,X23)
| ~ ( p2(X23)
& ~ p102(X23)
& p101(X23) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X3] :
( ren11(X3)
=> ( ( ! [X24] :
( ~ r1(X3,X24)
| ~ p11(X24)
| ~ p110(X24) )
| p11(X3) )
& ( ! [X25] :
( ~ r1(X3,X25)
| p11(X25)
| ~ p110(X25) )
| ~ p11(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X3] :
( ren12(X3)
=> ( ( ! [X26] :
( ~ r1(X3,X26)
| ~ p10(X26)
| ~ p109(X26) )
| p10(X3) )
& ( ! [X27] :
( ~ r1(X3,X27)
| p10(X27)
| ~ p109(X27) )
| ~ p10(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren13_defn,definition,
! [X3] :
( ren13(X3)
=> ( ( ! [X28] :
( ~ r1(X3,X28)
| ~ p9(X28)
| ~ p108(X28) )
| p9(X3) )
& ( ! [X29] :
( ~ r1(X3,X29)
| p9(X29)
| ~ p108(X29) )
| ~ p9(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren13])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren14_defn,definition,
! [X3] :
( ren14(X3)
=> ( ( ! [X30] :
( ~ r1(X3,X30)
| ~ p8(X30)
| ~ p107(X30) )
| p8(X3) )
& ( ! [X31] :
( ~ r1(X3,X31)
| p8(X31)
| ~ p107(X31) )
| ~ p8(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren14])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren15_defn,definition,
! [X3] :
( ren15(X3)
=> ( ( ! [X32] :
( ~ r1(X3,X32)
| ~ p7(X32)
| ~ p106(X32) )
| p7(X3) )
& ( ! [X33] :
( ~ r1(X3,X33)
| p7(X33)
| ~ p106(X33) )
| ~ p7(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren15])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren16_defn,definition,
! [X3] :
( ren16(X3)
=> ( ( ! [X34] :
( ~ r1(X3,X34)
| ~ p6(X34)
| ~ p105(X34) )
| p6(X3) )
& ( ! [X35] :
( ~ r1(X3,X35)
| p6(X35)
| ~ p105(X35) )
| ~ p6(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren16])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren17_defn,definition,
! [X3] :
( ren17(X3)
=> ( ( ! [X36] :
( ~ r1(X3,X36)
| ~ p5(X36)
| ~ p104(X36) )
| p5(X3) )
& ( ! [X37] :
( ~ r1(X3,X37)
| p5(X37)
| ~ p104(X37) )
| ~ p5(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren17])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren18_defn,definition,
! [X3] :
( ren18(X3)
=> ( ( ! [X38] :
( ~ r1(X3,X38)
| ~ p4(X38)
| ~ p103(X38) )
| p4(X3) )
& ( ! [X39] :
( ~ r1(X3,X39)
| p4(X39)
| ~ p103(X39) )
| ~ p4(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren18])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren19_defn,definition,
! [X3] :
( ren19(X3)
=> ( ( ! [X40] :
( ~ r1(X3,X40)
| ~ p3(X40)
| ~ p102(X40) )
| p3(X3) )
& ( ! [X41] :
( ~ r1(X3,X41)
| p3(X41)
| ~ p102(X41) )
| ~ p3(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren19])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren20_defn,definition,
! [X3] :
( ren20(X3)
=> ( ( ! [X42] :
( ~ r1(X3,X42)
| ~ p2(X42)
| ~ p101(X42) )
| p2(X3) )
& ( ! [X43] :
( ~ r1(X3,X43)
| p2(X43)
| ~ p101(X43) )
| ~ p2(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren20])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren21_defn,definition,
! [X3] :
( ren21(X3)
=> ( ( ! [X44] :
( ~ r1(X3,X44)
| ~ p1(X44)
| ~ p100(X44) )
| p1(X3) )
& ( ! [X45] :
( ~ r1(X3,X45)
| p1(X45)
| ~ p100(X45) )
| ~ p1(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren21])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren22_defn,definition,
! [X3] :
( ren22(X3)
=> ( ( ren1(X3)
| ~ ( ~ p110(X3)
& p109(X3) ) )
& ( ren2(X3)
| ~ ( ~ p109(X3)
& p108(X3) ) )
& ( ren3(X3)
| ~ ( ~ p108(X3)
& p107(X3) ) )
& ( ren4(X3)
| ~ ( ~ p107(X3)
& p106(X3) ) )
& ( ren5(X3)
| ~ ( ~ p106(X3)
& p105(X3) ) )
& ( ren6(X3)
| ~ ( ~ p105(X3)
& p104(X3) ) )
& ( ren7(X3)
| ~ ( ~ p104(X3)
& p103(X3) ) )
& ( ren8(X3)
| ~ ( ~ p103(X3)
& p102(X3) ) )
& ( ren9(X3)
| ~ ( ~ p102(X3)
& p101(X3) ) )
& ( ren10(X3)
| ~ ( ~ p101(X3)
& p100(X3) ) )
& ( ren11(X3)
| ~ p110(X3) )
& ( ren12(X3)
| ~ p109(X3) )
& ( ren13(X3)
| ~ p108(X3) )
& ( ren14(X3)
| ~ p107(X3) )
& ( ren15(X3)
| ~ p106(X3) )
& ( ren16(X3)
| ~ p105(X3) )
& ( ren17(X3)
| ~ p104(X3) )
& ( ren18(X3)
| ~ p103(X3) )
& ( ren19(X3)
| ~ p102(X3) )
& ( ren20(X3)
| ~ p101(X3) )
& ( ren21(X3)
| ~ p100(X3) )
& ( p110(X3)
| ~ p111(X3) )
& ( p109(X3)
| ~ p110(X3) )
& ( p108(X3)
| ~ p109(X3) )
& ( p107(X3)
| ~ p108(X3) )
& ( p106(X3)
| ~ p107(X3) )
& ( p105(X3)
| ~ p106(X3) )
& ( p104(X3)
| ~ p105(X3) )
& ( p103(X3)
| ~ p104(X3) )
& ( p102(X3)
| ~ p103(X3) )
& ( p101(X3)
| ~ p102(X3) )
& ( p100(X3)
| ~ p101(X3) ) ) ),
introduced(definition,[new_symbols(definition,[ren22])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ~ ( ! [X3] :
( ~ r1(X1,X3)
| ren22(X3) )
& ~ p101(X1)
& p100(X1) ) ),
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]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ! [X3] :
( ~ r1(X1,X3)
| ren22(X3) )
& ~ p101(X1)
& p100(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ! [X2] :
( ~ r1(skc21,X2)
| p5(X2) )
& ! [X3] :
( ~ r1(skc21,X3)
| ren22(X3) )
& ~ p101(skc21)
& p100(skc21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc21]),skolemize(X1,skc21)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_138,plain,
( ~ r1(skc21,X0)
| ren22(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren10_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren10(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ~ p102(X2)
& p101(X2) )
& ? [X3] :
( r1(X1,X3)
& p2(X3)
& ~ p102(X3)
& p101(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren10_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren10_skol,plain,
! [X1] :
( ~ ren10(X1)
| ( r1(X1,skf19(X1))
& ~ p2(skf19(X1))
& ~ p102(skf19(X1))
& p101(skf19(X1))
& r1(X1,skf20(X1))
& p2(skf20(X1))
& ~ p102(skf20(X1))
& p101(skf20(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf19,skf20]),skolemize(X2,skf19(X1)),skolemize(X3,skf20(X1))],[ren10_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_79,plain,
( ~ ren10(X0)
| r1(X0,skf20(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren10_skol])]) ).
% FILE RECORD
fof(reflexivity,axiom,
! [X1] : r1(X1,X1),
file('theBenchmark.p',reflexivity) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimTB,axiom,
! [X1] : r1(X1,X1),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[reflexivity])]) ).
% FOF SIMPLE INFERENCE
fof(reflexivity_elimImpEquivPushNegMiniScope,axiom,
! [X1] : r1(X1,X1),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[reflexivity_elimTB]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_1,plain,
r1(X0,X0),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[reflexivity_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_139,plain,
~ p101(skc21),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren22_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren22(X1)
| ( ( ren1(X1)
| p110(X1)
| ~ p109(X1) )
& ( ren2(X1)
| p109(X1)
| ~ p108(X1) )
& ( ren3(X1)
| p108(X1)
| ~ p107(X1) )
& ( ren4(X1)
| p107(X1)
| ~ p106(X1) )
& ( ren5(X1)
| p106(X1)
| ~ p105(X1) )
& ( ren6(X1)
| p105(X1)
| ~ p104(X1) )
& ( ren7(X1)
| p104(X1)
| ~ p103(X1) )
& ( ren8(X1)
| p103(X1)
| ~ p102(X1) )
& ( ren9(X1)
| p102(X1)
| ~ p101(X1) )
& ( ren10(X1)
| p101(X1)
| ~ p100(X1) )
& ( ren11(X1)
| ~ p110(X1) )
& ( ren12(X1)
| ~ p109(X1) )
& ( ren13(X1)
| ~ p108(X1) )
& ( ren14(X1)
| ~ p107(X1) )
& ( ren15(X1)
| ~ p106(X1) )
& ( ren16(X1)
| ~ p105(X1) )
& ( ren17(X1)
| ~ p104(X1) )
& ( ren18(X1)
| ~ p103(X1) )
& ( ren19(X1)
| ~ p102(X1) )
& ( ren20(X1)
| ~ p101(X1) )
& ( ren21(X1)
| ~ p100(X1) )
& ( p110(X1)
| ~ p111(X1) )
& ( p109(X1)
| ~ p110(X1) )
& ( p108(X1)
| ~ p109(X1) )
& ( p107(X1)
| ~ p108(X1) )
& ( p106(X1)
| ~ p107(X1) )
& ( p105(X1)
| ~ p106(X1) )
& ( p104(X1)
| ~ p105(X1) )
& ( p103(X1)
| ~ p104(X1) )
& ( p102(X1)
| ~ p103(X1) )
& ( p101(X1)
| ~ p102(X1) )
& ( p100(X1)
| ~ p101(X1) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren22_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_114,plain,
( ~ ren22(X0)
| ~ p100(X0)
| ren10(X0)
| p101(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren22_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_140,plain,
p100(skc21),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_307,plain,
( ~ ren22(skc21)
| ren10(skc21)
| p101(skc21) ),
inference(resolution,[status(thm)],[c_114,c_140]) ).
% CNF SPASS RESOLUTION.
cnf(c_308,plain,
( ~ ren22(skc21)
| ren10(skc21) ),
inference(resolution,[status(thm)],[c_139,c_307]) ).
% CNF SPASS RESOLUTION.
cnf(c_311,plain,
ren10(skc21),
inference(resolution,[status(thm)],[c_1,c_138,c_308]) ).
% CNF SPASS RESOLUTION.
cnf(c_317,plain,
r1(skc21,skf20(skc21)),
inference(resolution,[status(thm)],[c_79,c_311]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_81,plain,
( ~ ren10(X0)
| ~ p102(skf20(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren10_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_113,plain,
( ~ ren22(X0)
| ~ p101(X0)
| ren9(X0)
| p102(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren22_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_82,plain,
( ~ ren10(X0)
| p101(skf20(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren10_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_221,plain,
( ~ ren22(skf20(X0))
| ~ ren10(X0)
| ren9(skf20(X0))
| p102(skf20(X0)) ),
inference(resolution,[status(thm)],[c_113,c_82]) ).
% CNF SPASS RESOLUTION.
cnf(c_222,plain,
( ~ ren22(skf20(X0))
| ~ ren10(X0)
| ren9(skf20(X0)) ),
inference(resolution,[status(thm)],[c_81,c_221]) ).
% CNF SPASS RESOLUTION.
cnf(c_306,plain,
( ~ ren10(X0)
| ~ r1(skc21,skf20(X0))
| ren9(skf20(X0)) ),
inference(resolution,[status(thm)],[c_222,c_138]) ).
% CNF SPASS RESOLUTION.
cnf(c_310,plain,
( ~ r1(skc21,skf20(skc21))
| ren9(skf20(skc21)) ),
inference(resolution,[status(thm)],[c_1,c_138,c_308,c_306]) ).
% CNF SPASS RESOLUTION.
cnf(c_318,plain,
ren9(skf20(skc21)),
inference(resolution,[status(thm)],[c_1,c_138,c_308,c_306,c_317,c_310]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_74,plain,
( ~ ren9(X0)
| p102(skf18(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren9_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_112,plain,
( ~ ren22(X0)
| ~ p102(X0)
| ren8(X0)
| p103(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren22_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_73,plain,
( ~ ren9(X0)
| ~ p103(skf18(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren9_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_243,plain,
( ~ ren22(skf18(X0))
| ~ p102(skf18(X0))
| ~ ren9(X0)
| ren8(skf18(X0)) ),
inference(resolution,[status(thm)],[c_112,c_73]) ).
% CNF SPASS RESOLUTION.
cnf(c_244,plain,
( ~ ren22(skf18(X0))
| ~ ren9(X0)
| ren8(skf18(X0)) ),
inference(resolution,[status(thm)],[c_74,c_243]) ).
% CNF SPASS RESOLUTION.
cnf(c_330,plain,
( ~ ren22(skf18(skf20(skc21)))
| ren8(skf18(skf20(skc21))) ),
inference(resolution,[status(thm)],[c_244,c_318]) ).
% CNF SPASS RESOLUTION.
cnf(c_334,plain,
ren8(skf18(skf20(skc21))),
inference(resolution,[status(thm)],[c_305,c_138,c_317,c_318,c_330]) ).
% FOF SIMPLE INFERENCE
fof(ren8_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren8(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p4(X2)
& ~ p104(X2)
& p103(X2) )
& ? [X3] :
( r1(X1,X3)
& p4(X3)
& ~ p104(X3)
& p103(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren8_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren8_skol,plain,
! [X1] :
( ~ ren8(X1)
| ( r1(X1,skf15(X1))
& ~ p4(skf15(X1))
& ~ p104(skf15(X1))
& p103(skf15(X1))
& r1(X1,skf16(X1))
& p4(skf16(X1))
& ~ p104(skf16(X1))
& p103(skf16(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf15,skf16]),skolemize(X2,skf15(X1)),skolemize(X3,skf16(X1))],[ren8_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_66,plain,
( ~ ren8(X0)
| p103(skf16(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren8_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_137,plain,
( ~ r1(skc21,X0)
| p5(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren7_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren7(X1)
| ( ? [X2] :
( r1(X1,X2)
& ~ p5(X2)
& ~ p105(X2)
& p104(X2) )
& ? [X3] :
( r1(X1,X3)
& p5(X3)
& ~ p105(X3)
& p104(X3) ) ) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[ren7_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren7_skol,plain,
! [X1] :
( ~ ren7(X1)
| ( r1(X1,skf13(X1))
& ~ p5(skf13(X1))
& ~ p105(skf13(X1))
& p104(skf13(X1))
& r1(X1,skf14(X1))
& p5(skf14(X1))
& ~ p105(skf14(X1))
& p104(skf14(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf13,skf14]),skolemize(X2,skf13(X1)),skolemize(X3,skf14(X1))],[ren7_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_52,plain,
( ~ ren7(X0)
| ~ p5(skf13(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren7_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_285,plain,
( ~ r1(skc21,skf13(X0))
| ~ ren7(X0) ),
inference(resolution,[status(thm)],[c_137,c_52]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_51,plain,
( ~ ren7(X0)
| r1(X0,skf13(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren7_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_287,plain,
( ~ r1(X0,X1)
| ~ ren7(X1)
| r1(X0,skf13(X1)) ),
inference(resolution,[status(thm)],[c_2,c_51]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_111,plain,
( ~ ren22(X0)
| ~ p103(X0)
| ren7(X0)
| p104(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren22_elimImpEquivPushNegMiniScope])]) ).
% CNF SPASS RESOLUTION.
cnf(c_288,plain,
( ~ r1(skc21,X0)
| ~ ren22(X0)
| ~ p103(X0)
| p104(X0) ),
inference(resolution,[status(thm)],[c_285,c_287,c_111]) ).
% CNF SPASS RESOLUTION.
cnf(c_289,plain,
( ~ r1(skc21,X0)
| ~ p103(X0)
| p104(X0) ),
inference(resolution,[status(thm)],[c_138,c_288]) ).
% CNF SPASS RESOLUTION.
cnf(c_302,plain,
( ~ p103(X0)
| ~ r1(skc21,X1)
| ~ r1(X1,X0)
| p104(X0) ),
inference(resolution,[status(thm)],[c_289,c_2]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_65,plain,
( ~ ren8(X0)
| ~ p104(skf16(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren8_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_63,plain,
( ~ ren8(X0)
| r1(X0,skf16(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren8_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_338,plain,
r1(skf18(skf20(skc21)),skf16(skf18(skf20(skc21)))),
inference(resolution,[status(thm)],[c_63,c_334]) ).
% CNF SPASS RESOLUTION.
cnf(c_380,plain,
( ~ p103(skf16(skf18(skf20(skc21))))
| ~ r1(skc21,skf18(skf20(skc21)))
| ~ ren8(skf18(skf20(skc21))) ),
inference(resolution,[status(thm)],[c_302,c_65,c_338]) ).
% CNF SPASS RESOLUTION.
cnf(c_381,plain,
( ~ r1(skc21,skf18(skf20(skc21)))
| ~ ren8(skf18(skf20(skc21))) ),
inference(resolution,[status(thm)],[c_66,c_380]) ).
% CNF SPASS RESOLUTION.
cnf(c_382,plain,
~ r1(skc21,skf18(skf20(skc21))),
inference(resolution,[status(thm)],[c_334,c_381]) ).
% CNF SPASS RESOLUTION.
cnf(c_309,plain,
( ~ r1(skc21,skf20(skc21))
| ~ r1(X0,skf20(skc21))
| r1(X0,skf18(skf20(skc21))) ),
inference(resolution,[status(thm)],[c_1,c_138,c_308,c_306,c_305]) ).
% CNF SPASS RESOLUTION.
cnf(c_383,plain,
$false,
inference(byPropositionalAbstraction,[status(thm)],[c_382,c_309]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.010 : 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.36 % Computer : n029.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 21:14:10 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.36
% 0.13/0.36 % Input Clauses:
% 0.13/0.36 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.13/0.36 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.13/0.36 % 3:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.13/0.36 % 4:2:1:INP:Top: ren1(x0),p11(skf1(x0)) ->
% 0.13/0.36 % 5:2:1:INP:Top: ren1(x0),p111(skf1(x0)) ->
% 0.13/0.36 % 6:2:1:INP:Top: ren1(x0) -> p110(skf1(x0))
% 0.13/0.36 % 7:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.13/0.36 % 8:2:1:INP:Top: ren1(x0) -> p11(skf2(x0))
% 0.13/0.36 % 9:2:1:INP:Top: ren1(x0),p111(skf2(x0)) ->
% 0.13/0.36 % 10:2:1:INP:Top: ren1(x0) -> p110(skf2(x0))
% 0.13/0.36 % 11:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.13/0.36 % 12:2:1:INP:Top: ren2(x0),p10(skf3(x0)) ->
% 0.13/0.36 % 13:2:1:INP:Top: ren2(x0),p110(skf3(x0)) ->
% 0.13/0.36 % 14:2:1:INP:Top: ren2(x0) -> p109(skf3(x0))
% 0.13/0.36 % 15:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.13/0.36 % 16:2:1:INP:Top: ren2(x0) -> p10(skf4(x0))
% 0.13/0.36 % 17:2:1:INP:Top: ren2(x0),p110(skf4(x0)) ->
% 0.13/0.36 % 18:2:1:INP:Top: ren2(x0) -> p109(skf4(x0))
% 0.13/0.36 % 19:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.13/0.36 % 20:2:1:INP:Top: ren3(x0),p9(skf5(x0)) ->
% 0.13/0.36 % 21:2:1:INP:Top: ren3(x0),p109(skf5(x0)) ->
% 0.13/0.36 % 22:2:1:INP:Top: ren3(x0) -> p108(skf5(x0))
% 0.13/0.36 % 23:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.13/0.36 % 24:2:1:INP:Top: ren3(x0) -> p9(skf6(x0))
% 0.13/0.36 % 25:2:1:INP:Top: ren3(x0),p109(skf6(x0)) ->
% 0.13/0.36 % 26:2:1:INP:Top: ren3(x0) -> p108(skf6(x0))
% 0.13/0.36 % 27:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.13/0.36 % 28:2:1:INP:Top: ren4(x0),p8(skf7(x0)) ->
% 0.13/0.36 % 29:2:1:INP:Top: ren4(x0),p108(skf7(x0)) ->
% 0.13/0.36 % 30:2:1:INP:Top: ren4(x0) -> p107(skf7(x0))
% 0.13/0.36 % 31:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.13/0.36 % 32:2:1:INP:Top: ren4(x0) -> p8(skf8(x0))
% 0.13/0.36 % 33:2:1:INP:Top: ren4(x0),p108(skf8(x0)) ->
% 0.13/0.36 % 34:2:1:INP:Top: ren4(x0) -> p107(skf8(x0))
% 0.13/0.36 % 35:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.13/0.36 % 36:2:1:INP:Top: ren5(x0),p7(skf9(x0)) ->
% 0.13/0.36 % 37:2:1:INP:Top: ren5(x0),p107(skf9(x0)) ->
% 0.13/0.36 % 38:2:1:INP:Top: ren5(x0) -> p106(skf9(x0))
% 0.13/0.36 % 39:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.13/0.36 % 40:2:1:INP:Top: ren5(x0) -> p7(skf10(x0))
% 0.13/0.36 % 41:2:1:INP:Top: ren5(x0),p107(skf10(x0)) ->
% 0.13/0.36 % 42:2:1:INP:Top: ren5(x0) -> p106(skf10(x0))
% 0.13/0.36 % 43:2:1:INP:Top: ren6(x0) -> r1(x0,skf11(x0))
% 0.13/0.36 % 44:2:1:INP:Top: ren6(x0),p6(skf11(x0)) ->
% 0.13/0.36 % 45:2:1:INP:Top: ren6(x0),p106(skf11(x0)) ->
% 0.13/0.36 % 46:2:1:INP:Top: ren6(x0) -> p105(skf11(x0))
% 0.13/0.36 % 47:2:1:INP:Top: ren6(x0) -> r1(x0,skf12(x0))
% 0.13/0.36 % 48:2:1:INP:Top: ren6(x0) -> p6(skf12(x0))
% 0.13/0.36 % 49:2:1:INP:Top: ren6(x0),p106(skf12(x0)) ->
% 0.13/0.36 % 50:2:1:INP:Top: ren6(x0) -> p105(skf12(x0))
% 0.13/0.36 % 51:2:1:INP:Top: ren7(x0) -> r1(x0,skf13(x0))
% 0.13/0.36 % 52:2:1:INP:Top: ren7(x0),p5(skf13(x0)) ->
% 0.13/0.36 % 53:2:1:INP:Top: ren7(x0),p105(skf13(x0)) ->
% 0.13/0.36 % 54:2:1:INP:Top: ren7(x0) -> p104(skf13(x0))
% 0.13/0.36 % 55:2:1:INP:Top: ren7(x0) -> r1(x0,skf14(x0))
% 0.13/0.36 % 56:2:1:INP:Top: ren7(x0) -> p5(skf14(x0))
% 0.13/0.36 % 57:2:1:INP:Top: ren7(x0),p105(skf14(x0)) ->
% 0.13/0.36 % 58:2:1:INP:Top: ren7(x0) -> p104(skf14(x0))
% 0.13/0.36 % 59:2:1:INP:Top: ren8(x0) -> r1(x0,skf15(x0))
% 0.13/0.36 % 60:2:1:INP:Top: ren8(x0),p4(skf15(x0)) ->
% 0.13/0.36 % 61:2:1:INP:Top: ren8(x0),p104(skf15(x0)) ->
% 0.13/0.36 % 62:2:1:INP:Top: ren8(x0) -> p103(skf15(x0))
% 0.13/0.36 % 63:2:1:INP:Top: ren8(x0) -> r1(x0,skf16(x0))
% 0.13/0.36 % 64:2:1:INP:Top: ren8(x0) -> p4(skf16(x0))
% 0.13/0.36 % 65:2:1:INP:Top: ren8(x0),p104(skf16(x0)) ->
% 0.13/0.36 % 66:2:1:INP:Top: ren8(x0) -> p103(skf16(x0))
% 0.13/0.36 % 67:2:1:INP:Top: ren9(x0) -> r1(x0,skf17(x0))
% 0.13/0.36 % 68:2:1:INP:Top: ren9(x0),p3(skf17(x0)) ->
% 0.13/0.36 % 69:2:1:INP:Top: ren9(x0),p103(skf17(x0)) ->
% 0.13/0.36 % 70:2:1:INP:Top: ren9(x0) -> p102(skf17(x0))
% 0.13/0.36 % 71:2:1:INP:Top: ren9(x0) -> r1(x0,skf18(x0))
% 0.13/0.36 % 72:2:1:INP:Top: ren9(x0) -> p3(skf18(x0))
% 0.13/0.36 % 73:2:1:INP:Top: ren9(x0),p103(skf18(x0)) ->
% 0.13/0.36 % 74:2:1:INP:Top: ren9(x0) -> p102(skf18(x0))
% 0.13/0.36 % 75:2:1:INP:Top: ren10(x0) -> r1(x0,skf19(x0))
% 0.13/0.36 % 76:2:1:INP:Top: ren10(x0),p2(skf19(x0)) ->
% 0.13/0.36 % 77:2:1:INP:Top: ren10(x0),p102(skf19(x0)) ->
% 0.13/0.36 % 78:2:1:INP:Top: ren10(x0) -> p101(skf19(x0))
% 0.13/0.36 % 79:2:1:INP:Top: ren10(x0) -> r1(x0,skf20(x0))
% 0.13/0.36 % 80:2:1:INP:Top: ren10(x0) -> p2(skf20(x0))
% 0.13/0.36 % 81:2:1:INP:Top: ren10(x0),p102(skf20(x0)) ->
% 0.13/0.36 % 82:2:1:INP:Top: ren10(x0) -> p101(skf20(x0))
% 0.13/0.36 % 83:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p11(x1),p110(x1) -> p11(x0)
% 0.13/0.36 % 84:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p110(x1),p11(x0) -> p11(x1)
% 0.13/0.36 % 85:5:2:INP:TopTop: ren12(x0),r1(x0,x1),p10(x1),p109(x1) -> p10(x0)
% 0.13/0.36 % 86:5:2:INP:TopTop: ren12(x0),r1(x0,x1),p109(x1),p10(x0) -> p10(x1)
% 0.13/0.36 % 87:5:2:INP:TopTop: ren13(x0),r1(x0,x1),p9(x1),p108(x1) -> p9(x0)
% 0.13/0.36 % 88:5:2:INP:TopTop: ren13(x0),r1(x0,x1),p108(x1),p9(x0) -> p9(x1)
% 0.13/0.36 % 89:5:2:INP:TopTop: ren14(x0),r1(x0,x1),p8(x1),p107(x1) -> p8(x0)
% 0.13/0.36 % 90:5:2:INP:TopTop: ren14(x0),r1(x0,x1),p107(x1),p8(x0) -> p8(x1)
% 0.13/0.36 % 91:5:2:INP:TopTop: ren15(x0),r1(x0,x1),p7(x1),p106(x1) -> p7(x0)
% 0.13/0.36 % 92:5:2:INP:TopTop: ren15(x0),r1(x0,x1),p106(x1),p7(x0) -> p7(x1)
% 0.13/0.36 % 93:5:2:INP:TopTop: ren16(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.13/0.36 % 94:5:2:INP:TopTop: ren16(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.13/0.36 % 95:5:2:INP:TopTop: ren17(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.13/0.36 % 96:5:2:INP:TopTop: ren17(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 0.13/0.36 % 97:5:2:INP:TopTop: ren18(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 0.13/0.36 % 98:5:2:INP:TopTop: ren18(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 0.13/0.36 % 99:5:2:INP:TopTop: ren19(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 0.13/0.36 % 100:5:2:INP:TopTop: ren19(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 0.13/0.36 % 101:5:2:INP:TopTop: ren20(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.13/0.36 % 102:5:2:INP:TopTop: ren20(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.13/0.36 % 103:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.13/0.36 % 104:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.13/0.36 % 105:4:1:INP:Top: ren22(x0),p109(x0) -> ren1(x0),p110(x0)
% 0.13/0.36 % 106:4:1:INP:Top: ren22(x0),p108(x0) -> ren2(x0),p109(x0)
% 0.13/0.36 % 107:4:1:INP:Top: ren22(x0),p107(x0) -> ren3(x0),p108(x0)
% 0.13/0.36 % 108:4:1:INP:Top: ren22(x0),p106(x0) -> ren4(x0),p107(x0)
% 0.13/0.36 % 109:4:1:INP:Top: ren22(x0),p105(x0) -> ren5(x0),p106(x0)
% 0.13/0.36 % 110:4:1:INP:Top: ren22(x0),p104(x0) -> ren6(x0),p105(x0)
% 0.13/0.36 % 111:4:1:INP:Top: ren22(x0),p103(x0) -> ren7(x0),p104(x0)
% 0.13/0.36 % 112:4:1:INP:Top: ren22(x0),p102(x0) -> ren8(x0),p103(x0)
% 0.13/0.36 % 113:4:1:INP:Top: ren22(x0),p101(x0) -> ren9(x0),p102(x0)
% 0.13/0.36 % 114:4:1:INP:Top: ren22(x0),p100(x0) -> ren10(x0),p101(x0)
% 0.13/0.36 % 115:3:1:INP:Top: ren22(x0),p110(x0) -> ren11(x0)
% 0.13/0.36 % 116:3:1:INP:Top: ren22(x0),p109(x0) -> ren12(x0)
% 0.13/0.36 % 117:3:1:INP:Top: ren22(x0),p108(x0) -> ren13(x0)
% 0.13/0.36 % 118:3:1:INP:Top: ren22(x0),p107(x0) -> ren14(x0)
% 0.13/0.36 % 119:3:1:INP:Top: ren22(x0),p106(x0) -> ren15(x0)
% 0.13/0.36 % 120:3:1:INP:Top: ren22(x0),p105(x0) -> ren16(x0)
% 0.13/0.36 % 121:3:1:INP:Top: ren22(x0),p104(x0) -> ren17(x0)
% 0.13/0.36 % 122:3:1:INP:Top: ren22(x0),p103(x0) -> ren18(x0)
% 0.13/0.36 % 123:3:1:INP:Top: ren22(x0),p102(x0) -> ren19(x0)
% 0.13/0.36 % 124:3:1:INP:Top: ren22(x0),p101(x0) -> ren20(x0)
% 0.13/0.36 % 125:3:1:INP:Top: ren22(x0),p100(x0) -> ren21(x0)
% 0.13/0.36 % 126:3:1:INP:Top: ren22(x0),p111(x0) -> p110(x0)
% 0.13/0.36 % 127:3:1:INP:Top: ren22(x0),p110(x0) -> p109(x0)
% 0.13/0.36 % 128:3:1:INP:Top: ren22(x0),p109(x0) -> p108(x0)
% 0.13/0.36 % 129:3:1:INP:Top: ren22(x0),p108(x0) -> p107(x0)
% 0.13/0.36 % 130:3:1:INP:Top: ren22(x0),p107(x0) -> p106(x0)
% 0.13/0.36 % 131:3:1:INP:Top: ren22(x0),p106(x0) -> p105(x0)
% 0.13/0.36 % 132:3:1:INP:Top: ren22(x0),p105(x0) -> p104(x0)
% 0.13/0.36 % 133:3:1:INP:Top: ren22(x0),p104(x0) -> p103(x0)
% 0.13/0.36 % 134:3:1:INP:Top: ren22(x0),p103(x0) -> p102(x0)
% 0.13/0.36 % 135:3:1:INP:Top: ren22(x0),p102(x0) -> p101(x0)
% 0.13/0.36 % 136:3:1:INP:Top: ren22(x0),p101(x0) -> p100(x0)
% 0.13/0.36 % 137:2:1:INP:Top: r1(skc21,x0) -> p5(x0)
% 0.13/0.36 % 138:2:1:INP:Top: r1(skc21,x0) -> ren22(x0)
% 0.13/0.36 % 139:1:0:INP:: p101(skc21) ->
% 0.13/0.36 % 140:1:0:INP:: -> p100(skc21)
% 0.13/0.36
% 0.13/0.36 % Predicates: r1 p5 p11 p111 p110 p109 p10 p108 p9 p107 p8 p106 p7 p105 p6 p104 p103 p4 p102 p3 p101 p2 p100 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22
% 0.13/0.36 % Fol Constants: skc21
% 0.13/0.36 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20
% 0.13/0.36 % Problem Properties:
% 0.13/0.36 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.13/0.36
% 0.13/0.36
% 0.13/0.36 % Reduced Input Axiom Clauses:
% 0.13/0.36 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.13/0.36 % 2:3:3:INP:TopTopTop: r1(x0,x1),r1(x1,x2) -> r1(x0,x2)
% 0.13/0.36 % 3:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.13/0.36 % 4:2:1:INP:Top: ren1(x0),p11(skf1(x0)) ->
% 0.13/0.36 % 5:2:1:INP:Top: ren1(x0),p111(skf1(x0)) ->
% 0.13/0.36 % 6:2:1:INP:Top: ren1(x0) -> p110(skf1(x0))
% 0.13/0.36 % 7:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.13/0.36 % 8:2:1:INP:Top: ren1(x0) -> p11(skf2(x0))
% 0.13/0.36 % 9:2:1:INP:Top: ren1(x0),p111(skf2(x0)) ->
% 0.13/0.36 % 10:2:1:INP:Top: ren1(x0) -> p110(skf2(x0))
% 0.13/0.36 % 11:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.13/0.36 % 12:2:1:INP:Top: ren2(x0),p10(skf3(x0)) ->
% 0.13/0.36 % 13:2:1:INP:Top: ren2(x0),p110(skf3(x0)) ->
% 0.13/0.36 % 14:2:1:INP:Top: ren2(x0) -> p109(skf3(x0))
% 0.13/0.36 % 15:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.13/0.36 % 16:2:1:INP:Top: ren2(x0) -> p10(skf4(x0))
% 0.13/0.36 % 17:2:1:INP:Top: ren2(x0),p110(skf4(x0)) ->
% 0.13/0.36 % 18:2:1:INP:Top: ren2(x0) -> p109(skf4(x0))
% 0.13/0.36 % 19:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.13/0.36 % 20:2:1:INP:Top: ren3(x0),p9(skf5(x0)) ->
% 0.13/0.36 % 21:2:1:INP:Top: ren3(x0),p109(skf5(x0)) ->
% 0.13/0.36 % 22:2:1:INP:Top: ren3(x0) -> p108(skf5(x0))
% 0.13/0.36 % 23:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.13/0.36 % 24:2:1:INP:Top: ren3(x0) -> p9(skf6(x0))
% 0.13/0.36 % 25:2:1:INP:Top: ren3(x0),p109(skf6(x0)) ->
% 0.13/0.36 % 26:2:1:INP:Top: ren3(x0) -> p108(skf6(x0))
% 0.13/0.36 % 27:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.13/0.36 % 28:2:1:INP:Top: ren4(x0),p8(skf7(x0)) ->
% 0.13/0.36 % 29:2:1:INP:Top: ren4(x0),p108(skf7(x0)) ->
% 0.13/0.36 % 30:2:1:INP:Top: ren4(x0) -> p107(skf7(x0))
% 0.13/0.36 % 31:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.13/0.36 % 32:2:1:INP:Top: ren4(x0) -> p8(skf8(x0))
% 0.13/0.36 % 33:2:1:INP:Top: ren4(x0),p108(skf8(x0)) ->
% 0.13/0.36 % 34:2:1:INP:Top: ren4(x0) -> p107(skf8(x0))
% 0.13/0.36 % 35:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.13/0.36 % 36:2:1:INP:Top: ren5(x0),p7(skf9(x0)) ->
% 0.13/0.36 % 37:2:1:INP:Top: ren5(x0),p107(skf9(x0)) ->
% 0.13/0.36 % 38:2:1:INP:Top: ren5(x0) -> p106(skf9(x0))
% 0.13/0.36 % 39:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.13/0.36 % 40:2:1:INP:Top: ren5(x0) -> p7(skf10(x0))
% 0.13/0.36 % 41:2:1:INP:Top: ren5(x0),p107(skf10(x0)) ->
% 0.13/0.36 % 42:2:1:INP:Top: ren5(x0) -> p106(skf10(x0))
% 0.13/0.36 % 43:2:1:INP:Top: ren6(x0) -> r1(x0,skf11(x0))
% 0.13/0.36 % 44:2:1:INP:Top: ren6(x0),p6(skf11(x0)) ->
% 0.13/0.36 % 45:2:1:INP:Top: ren6(x0),p106(skf11(x0)) ->
% 0.13/0.36 % 46:2:1:INP:Top: ren6(x0) -> p105(skf11(x0))
% 0.13/0.36 % 47:2:1:INP:Top: ren6(x0) -> r1(x0,skf12(x0))
% 0.13/0.36 % 48:2:1:INP:Top: ren6(x0) -> p6(skf12(x0))
% 0.13/0.36 % 49:2:1:INP:Top: ren6(x0),p106(skf12(x0)) ->
% 0.13/0.36 % 50:2:1:INP:Top: ren6(x0) -> p105(skf12(x0))
% 0.13/0.36 % 51:2:1:INP:Top: ren7(x0) -> r1(x0,skf13(x0))
% 0.13/0.36 % 52:2:1:INP:Top: ren7(x0),p5(skf13(x0)) ->
% 0.13/0.36 % 53:2:1:INP:Top: ren7(x0),p105(skf13(x0)) ->
% 0.13/0.36 % 54:2:1:INP:Top: ren7(x0) -> p104(skf13(x0))
% 0.13/0.36 % 55:2:1:INP:Top: ren7(x0) -> r1(x0,skf14(x0))
% 0.13/0.36 % 56:2:1:INP:Top: ren7(x0) -> p5(skf14(x0))
% 0.13/0.36 % 57:2:1:INP:Top: ren7(x0),p105(skf14(x0)) ->
% 0.13/0.36 % 58:2:1:INP:Top: ren7(x0) -> p104(skf14(x0))
% 0.13/0.36 % 59:2:1:INP:Top: ren8(x0) -> r1(x0,skf15(x0))
% 0.13/0.36 % 60:2:1:INP:Top: ren8(x0),p4(skf15(x0)) ->
% 0.13/0.36 % 61:2:1:INP:Top: ren8(x0),p104(skf15(x0)) ->
% 0.13/0.36 % 62:2:1:INP:Top: ren8(x0) -> p103(skf15(x0))
% 0.13/0.36 % 63:2:1:INP:Top: ren8(x0) -> r1(x0,skf16(x0))
% 0.13/0.36 % 64:2:1:INP:Top: ren8(x0) -> p4(skf16(x0))
% 0.13/0.36 % 65:2:1:INP:Top: ren8(x0),p104(skf16(x0)) ->
% 0.13/0.36 % 66:2:1:INP:Top: ren8(x0) -> p103(skf16(x0))
% 0.13/0.36 % 67:2:1:INP:Top: ren9(x0) -> r1(x0,skf17(x0))
% 0.13/0.36 % 68:2:1:INP:Top: ren9(x0),p3(skf17(x0)) ->
% 0.13/0.36 % 69:2:1:INP:Top: ren9(x0),p103(skf17(x0)) ->
% 0.13/0.36 % 70:2:1:INP:Top: ren9(x0) -> p102(skf17(x0))
% 0.13/0.36 % 71:2:1:INP:Top: ren9(x0) -> r1(x0,skf18(x0))
% 0.13/0.36 % 72:2:1:INP:Top: ren9(x0) -> p3(skf18(x0))
% 0.13/0.36 % 73:2:1:INP:Top: ren9(x0),p103(skf18(x0)) ->
% 0.13/0.36 % 74:2:1:INP:Top: ren9(x0) -> p102(skf18(x0))
% 0.13/0.36 % 75:2:1:INP:Top: ren10(x0) -> r1(x0,skf19(x0))
% 0.13/0.36 % 76:2:1:INP:Top: ren10(x0),p2(skf19(x0)) ->
% 0.13/0.36 % 77:2:1:INP:Top: ren10(x0),p102(skf19(x0)) ->
% 0.13/0.36 % 78:2:1:INP:Top: ren10(x0) -> p101(skf19(x0))
% 0.13/0.36 % 79:2:1:INP:Top: ren10(x0) -> r1(x0,skf20(x0))
% 0.13/0.36 % 80:2:1:INP:Top: ren10(x0) -> p2(skf20(x0))
% 0.13/0.36 % 81:2:1:INP:Top: ren10(x0),p102(skf20(x0)) ->
% 0.13/0.36 % 82:2:1:INP:Top: ren10(x0) -> p101(skf20(x0))
% 0.13/0.36 % 83:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p11(x1),p110(x1) -> p11(x0)
% 0.13/0.36 % 84:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p110(x1),p11(x0) -> p11(x1)
% 0.13/0.36 % 85:5:2:INP:TopTop: ren12(x0),r1(x0,x1),p10(x1),p109(x1) -> p10(x0)
% 0.13/0.36 % 86:5:2:INP:TopTop: ren12(x0),r1(x0,x1),p109(x1),p10(x0) -> p10(x1)
% 0.13/0.36 % 87:5:2:INP:TopTop: ren13(x0),r1(x0,x1),p9(x1),p108(x1) -> p9(x0)
% 0.13/0.36 % 88:5:2:INP:TopTop: ren13(x0),r1(x0,x1),p108(x1),p9(x0) -> p9(x1)
% 0.13/0.36 % 89:5:2:INP:TopTop: ren14(x0),r1(x0,x1),p8(x1),p107(x1) -> p8(x0)
% 0.13/0.36 % 90:5:2:INP:TopTop: ren14(x0),r1(x0,x1),p107(x1),p8(x0) -> p8(x1)
% 0.13/0.36 % 91:5:2:INP:TopTop: ren15(x0),r1(x0,x1),p7(x1),p106(x1) -> p7(x0)
% 0.13/0.36 % 92:5:2:INP:TopTop: ren15(x0),r1(x0,x1),p106(x1),p7(x0) -> p7(x1)
% 0.13/0.36 % 93:5:2:INP:TopTop: ren16(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.13/0.36 % 94:5:2:INP:TopTop: ren16(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.13/0.36 % 95:5:2:INP:TopTop: ren17(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.13/0.36 % 96:5:2:INP:TopTop: ren17(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 7.25/7.55 % 97:5:2:INP:TopTop: ren18(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 7.25/7.55 % 98:5:2:INP:TopTop: ren18(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 7.25/7.55 % 99:5:2:INP:TopTop: ren19(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 7.25/7.55 % 100:5:2:INP:TopTop: ren19(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 7.25/7.55 % 101:5:2:INP:TopTop: ren20(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 7.25/7.55 % 102:5:2:INP:TopTop: ren20(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 7.25/7.55 % 103:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 7.25/7.55 % 104:5:2:INP:TopTop: ren21(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 7.25/7.55 % 105:4:1:INP:Top: ren22(x0),p109(x0) -> ren1(x0),p110(x0)
% 7.25/7.55 % 106:4:1:INP:Top: ren22(x0),p108(x0) -> ren2(x0),p109(x0)
% 7.25/7.55 % 107:4:1:INP:Top: ren22(x0),p107(x0) -> ren3(x0),p108(x0)
% 7.25/7.55 % 108:4:1:INP:Top: ren22(x0),p106(x0) -> ren4(x0),p107(x0)
% 7.25/7.55 % 109:4:1:INP:Top: ren22(x0),p105(x0) -> ren5(x0),p106(x0)
% 7.25/7.55 % 110:4:1:INP:Top: ren22(x0),p104(x0) -> ren6(x0),p105(x0)
% 7.25/7.55 % 111:4:1:INP:Top: ren22(x0),p103(x0) -> ren7(x0),p104(x0)
% 7.25/7.55 % 112:4:1:INP:Top: ren22(x0),p102(x0) -> ren8(x0),p103(x0)
% 7.25/7.55 % 113:4:1:INP:Top: ren22(x0),p101(x0) -> ren9(x0),p102(x0)
% 7.25/7.55 % 114:4:1:INP:Top: ren22(x0),p100(x0) -> ren10(x0),p101(x0)
% 7.25/7.55 % 115:3:1:INP:Top: ren22(x0),p110(x0) -> ren11(x0)
% 7.25/7.55 % 116:3:1:INP:Top: ren22(x0),p109(x0) -> ren12(x0)
% 7.25/7.55 % 117:3:1:INP:Top: ren22(x0),p108(x0) -> ren13(x0)
% 7.25/7.55 % 118:3:1:INP:Top: ren22(x0),p107(x0) -> ren14(x0)
% 7.25/7.55 % 119:3:1:INP:Top: ren22(x0),p106(x0) -> ren15(x0)
% 7.25/7.55 % 120:3:1:INP:Top: ren22(x0),p105(x0) -> ren16(x0)
% 7.25/7.55 % 121:3:1:INP:Top: ren22(x0),p104(x0) -> ren17(x0)
% 7.25/7.55 % 122:3:1:INP:Top: ren22(x0),p103(x0) -> ren18(x0)
% 7.25/7.55 % 123:3:1:INP:Top: ren22(x0),p102(x0) -> ren19(x0)
% 7.25/7.55 % 124:3:1:INP:Top: ren22(x0),p101(x0) -> ren20(x0)
% 7.25/7.55 % 125:3:1:INP:Top: ren22(x0),p100(x0) -> ren21(x0)
% 7.25/7.55 % 126:3:1:INP:Top: ren22(x0),p111(x0) -> p110(x0)
% 7.25/7.55 % 127:3:1:INP:Top: ren22(x0),p110(x0) -> p109(x0)
% 7.25/7.55 % 128:3:1:INP:Top: ren22(x0),p109(x0) -> p108(x0)
% 7.25/7.55 % 129:3:1:INP:Top: ren22(x0),p108(x0) -> p107(x0)
% 7.25/7.55 % 130:3:1:INP:Top: ren22(x0),p107(x0) -> p106(x0)
% 7.25/7.55 % 131:3:1:INP:Top: ren22(x0),p106(x0) -> p105(x0)
% 7.25/7.55 % 132:3:1:INP:Top: ren22(x0),p105(x0) -> p104(x0)
% 7.25/7.55 % 133:3:1:INP:Top: ren22(x0),p104(x0) -> p103(x0)
% 7.25/7.55 % 134:3:1:INP:Top: ren22(x0),p103(x0) -> p102(x0)
% 7.25/7.55 % 135:3:1:INP:Top: ren22(x0),p102(x0) -> p101(x0)
% 7.25/7.55 % 136:3:1:INP:Top: ren22(x0),p101(x0) -> p100(x0)
% 7.25/7.55
% 7.25/7.55 % Reduced Input Conjecture Clauses:
% 7.25/7.55 % 137:2:1:INP:Top: r1(skc21,x0) -> p5(x0)
% 7.25/7.55 % 138:2:1:INP:Top: r1(skc21,x0) -> ren22(x0)
% 7.25/7.55 % 139:1:0:INP:: p101(skc21) ->
% 7.25/7.55 % 140:1:0:INP:: -> p100(skc21)
% 7.25/7.55
% 7.25/7.55
% 7.25/7.55 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 387 atoms initially. Used heuristic: lmodel_grow ===
% 7.25/7.55
% 7.25/7.55 %
% 7.25/7.55
% 7.25/7.55 % === SAT Conflict found: 383:0:0:[382.0,309.0]:: ->
% 7.25/7.55
% 7.25/7.55 % SZS status Theorem
% 7.25/7.55 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.25/7.55
% 7.25/7.55 % SPASS-SCL-FOL Statistics:
% 7.25/7.55 % Number of learned clauses: 198
% 7.25/7.55 % Number of propagations: 51431
% 7.25/7.55 % Number of decisions: 25498
% 7.25/7.55 % Number of resolutions: 305
% 7.25/7.55 % Number of condensations: 0
% 7.25/7.55 % Number of sub resolutions: 44
% 7.25/7.55
% 7.25/7.55 % Solver is done. Empty clause found
% 7.25/7.55
% 7.25/7.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 7.25/7.55 % SZS output start Proof for theBenchmark
% See solution above
% 7.25/7.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 7.25/7.56
% 7.25/7.56
% 7.25/7.56 % Needed: 0:00:07.19
% 7.25/7.56
% 7.25/7.56 % ###
% 7.25/7.56 % ### Pagesize: 8192
% 7.25/7.56 % ### Marksize: 0
% 7.25/7.56 % ### Memory demanded: 254015 KBytes
% 7.25/7.56 % ### Memory freed: 254015 KBytes
% 7.25/7.56 % ### Memory remaining: 0 Bytes
% 7.25/7.56 % ### Pages allocated: 8524 Pages
% 7.25/7.56 % ###
%------------------------------------------------------------------------------