%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL656+1.005 : 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 : n031.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:59 PM UTC 2026
% Result : Theorem 0.15s 0.41s
% Output : Proof 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 42 ( 8 unt; 12 def)
% Number of atoms : 693 ( 0 equ)
% Maximal formula atoms : 129 ( 16 avg)
% Number of connectives : 1209 ( 558 ~; 373 |; 266 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-1 aty)
% Number of variables : 203 ( 0 sgn 168 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,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)
| ~ 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) )
& ( 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)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) ) ) ) ) )
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,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)
| ~ 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) )
& ( 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)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| p3(X6) ) ) ) ) )
| ~ ( ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ( ( ( ~ ! [X12] :
( ~ r1(X11,X12)
| ~ ( ~ p6(X12)
& ~ p106(X12)
& p105(X12) ) )
& ~ ! [X13] :
( ~ r1(X11,X13)
| ~ ( p6(X13)
& ~ p106(X13)
& p105(X13) ) ) )
| ~ ( ~ p105(X11)
& p104(X11) ) )
& ( ( ~ ! [X14] :
( ~ r1(X11,X14)
| ~ ( ~ p5(X14)
& ~ p105(X14)
& p104(X14) ) )
& ~ ! [X15] :
( ~ r1(X11,X15)
| ~ ( p5(X15)
& ~ p105(X15)
& p104(X15) ) ) )
| ~ ( ~ p104(X11)
& p103(X11) ) )
& ( ( ~ ! [X16] :
( ~ r1(X11,X16)
| ~ ( ~ p4(X16)
& ~ p104(X16)
& p103(X16) ) )
& ~ ! [X17] :
( ~ r1(X11,X17)
| ~ ( p4(X17)
& ~ p104(X17)
& p103(X17) ) ) )
| ~ ( ~ p103(X11)
& p102(X11) ) )
& ( ( ~ ! [X18] :
( ~ r1(X11,X18)
| ~ ( ~ p3(X18)
& ~ p103(X18)
& p102(X18) ) )
& ~ ! [X19] :
( ~ r1(X11,X19)
| ~ ( p3(X19)
& ~ p103(X19)
& p102(X19) ) ) )
| ~ ( ~ p102(X11)
& p101(X11) ) )
& ( ( ~ ! [X20] :
( ~ r1(X11,X20)
| ~ ( ~ p2(X20)
& ~ p102(X20)
& p101(X20) ) )
& ~ ! [X21] :
( ~ r1(X11,X21)
| ~ ( p2(X21)
& ~ p102(X21)
& p101(X21) ) ) )
| ~ ( ~ p101(X11)
& p100(X11) ) )
& ( ( ( ! [X22] :
( ~ r1(X11,X22)
| ~ p6(X22)
| ~ p105(X22) )
| p6(X11) )
& ( ! [X23] :
( ~ r1(X11,X23)
| p6(X23)
| ~ p105(X23) )
| ~ p6(X11) ) )
| ~ p105(X11) )
& ( ( ( ! [X24] :
( ~ r1(X11,X24)
| ~ p5(X24)
| ~ p104(X24) )
| p5(X11) )
& ( ! [X25] :
( ~ r1(X11,X25)
| p5(X25)
| ~ p104(X25) )
| ~ p5(X11) ) )
| ~ p104(X11) )
& ( ( ( ! [X26] :
( ~ r1(X11,X26)
| ~ p4(X26)
| ~ p103(X26) )
| p4(X11) )
& ( ! [X27] :
( ~ r1(X11,X27)
| p4(X27)
| ~ p103(X27) )
| ~ p4(X11) ) )
| ~ p103(X11) )
& ( ( ( ! [X28] :
( ~ r1(X11,X28)
| ~ p3(X28)
| ~ p102(X28) )
| p3(X11) )
& ( ! [X29] :
( ~ r1(X11,X29)
| p3(X29)
| ~ p102(X29) )
| ~ p3(X11) ) )
| ~ p102(X11) )
& ( ( ( ! [X30] :
( ~ r1(X11,X30)
| ~ p2(X30)
| ~ p101(X30) )
| p2(X11) )
& ( ! [X31] :
( ~ r1(X11,X31)
| p2(X31)
| ~ p101(X31) )
| ~ p2(X11) ) )
| ~ p101(X11) )
& ( ( ( ! [X32] :
( ~ r1(X11,X32)
| ~ p1(X32)
| ~ p100(X32) )
| p1(X11) )
& ( ! [X33] :
( ~ r1(X11,X33)
| p1(X33)
| ~ p100(X33) )
| ~ p1(X11) ) )
| ~ p100(X11) )
& ( p105(X11)
| ~ p106(X11) )
& ( p104(X11)
| ~ p105(X11) )
& ( p103(X11)
| ~ p104(X11) )
& ( p102(X11)
| ~ p103(X11) )
& ( p101(X11)
| ~ p102(X11) )
& ( p100(X11)
| ~ p101(X11) ) ) ) ) ) ) )
& ~ p101(X1)
& p100(X1) ) ),
inference(elimTB,[status(thm)],[inference(variable_rename,[status(thm)],[main_nc])]) ).
% FOF INTRODUCE RENAMING
fof(ren1_defn,definition,
! [X11] :
( ren1(X11)
=> ( ~ ! [X12] :
( ~ r1(X11,X12)
| ~ ( ~ p6(X12)
& ~ p106(X12)
& p105(X12) ) )
& ~ ! [X13] :
( ~ r1(X11,X13)
| ~ ( p6(X13)
& ~ p106(X13)
& p105(X13) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren1])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren2_defn,definition,
! [X11] :
( ren2(X11)
=> ( ~ ! [X14] :
( ~ r1(X11,X14)
| ~ ( ~ p5(X14)
& ~ p105(X14)
& p104(X14) ) )
& ~ ! [X15] :
( ~ r1(X11,X15)
| ~ ( p5(X15)
& ~ p105(X15)
& p104(X15) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren2])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren3_defn,definition,
! [X11] :
( ren3(X11)
=> ( ~ ! [X16] :
( ~ r1(X11,X16)
| ~ ( ~ p4(X16)
& ~ p104(X16)
& p103(X16) ) )
& ~ ! [X17] :
( ~ r1(X11,X17)
| ~ ( p4(X17)
& ~ p104(X17)
& p103(X17) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren3])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren4_defn,definition,
! [X11] :
( ren4(X11)
=> ( ~ ! [X18] :
( ~ r1(X11,X18)
| ~ ( ~ p3(X18)
& ~ p103(X18)
& p102(X18) ) )
& ~ ! [X19] :
( ~ r1(X11,X19)
| ~ ( p3(X19)
& ~ p103(X19)
& p102(X19) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren4])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren5_defn,definition,
! [X11] :
( ren5(X11)
=> ( ~ ! [X20] :
( ~ r1(X11,X20)
| ~ ( ~ p2(X20)
& ~ p102(X20)
& p101(X20) ) )
& ~ ! [X21] :
( ~ r1(X11,X21)
| ~ ( p2(X21)
& ~ p102(X21)
& p101(X21) ) ) ) ),
introduced(definition,[new_symbols(definition,[ren5])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren6_defn,definition,
! [X11] :
( ren6(X11)
=> ( ( ! [X22] :
( ~ r1(X11,X22)
| ~ p6(X22)
| ~ p105(X22) )
| p6(X11) )
& ( ! [X23] :
( ~ r1(X11,X23)
| p6(X23)
| ~ p105(X23) )
| ~ p6(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren6])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren7_defn,definition,
! [X11] :
( ren7(X11)
=> ( ( ! [X24] :
( ~ r1(X11,X24)
| ~ p5(X24)
| ~ p104(X24) )
| p5(X11) )
& ( ! [X25] :
( ~ r1(X11,X25)
| p5(X25)
| ~ p104(X25) )
| ~ p5(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren7])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren8_defn,definition,
! [X11] :
( ren8(X11)
=> ( ( ! [X26] :
( ~ r1(X11,X26)
| ~ p4(X26)
| ~ p103(X26) )
| p4(X11) )
& ( ! [X27] :
( ~ r1(X11,X27)
| p4(X27)
| ~ p103(X27) )
| ~ p4(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren8])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren9_defn,definition,
! [X11] :
( ren9(X11)
=> ( ( ! [X28] :
( ~ r1(X11,X28)
| ~ p3(X28)
| ~ p102(X28) )
| p3(X11) )
& ( ! [X29] :
( ~ r1(X11,X29)
| p3(X29)
| ~ p102(X29) )
| ~ p3(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren9])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren10_defn,definition,
! [X11] :
( ren10(X11)
=> ( ( ! [X30] :
( ~ r1(X11,X30)
| ~ p2(X30)
| ~ p101(X30) )
| p2(X11) )
& ( ! [X31] :
( ~ r1(X11,X31)
| p2(X31)
| ~ p101(X31) )
| ~ p2(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren10])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren11_defn,definition,
! [X11] :
( ren11(X11)
=> ( ( ! [X32] :
( ~ r1(X11,X32)
| ~ p1(X32)
| ~ p100(X32) )
| p1(X11) )
& ( ! [X33] :
( ~ r1(X11,X33)
| p1(X33)
| ~ p100(X33) )
| ~ p1(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren11])],[main_nc_elimTB]) ).
% FOF INTRODUCE RENAMING
fof(ren12_defn,definition,
! [X11] :
( ren12(X11)
=> ( ( ren1(X11)
| ~ ( ~ p105(X11)
& p104(X11) ) )
& ( ren2(X11)
| ~ ( ~ p104(X11)
& p103(X11) ) )
& ( ren3(X11)
| ~ ( ~ p103(X11)
& p102(X11) ) )
& ( ren4(X11)
| ~ ( ~ p102(X11)
& p101(X11) ) )
& ( ren5(X11)
| ~ ( ~ p101(X11)
& p100(X11) ) )
& ( ren6(X11)
| ~ p105(X11) )
& ( ren7(X11)
| ~ p104(X11) )
& ( ren8(X11)
| ~ p103(X11) )
& ( ren9(X11)
| ~ p102(X11) )
& ( ren10(X11)
| ~ p101(X11) )
& ( ren11(X11)
| ~ p100(X11) )
& ( p105(X11)
| ~ p106(X11) )
& ( p104(X11)
| ~ p105(X11) )
& ( p103(X11)
| ~ p104(X11) )
& ( p102(X11)
| ~ p103(X11) )
& ( p101(X11)
| ~ p102(X11) )
& ( p100(X11)
| ~ p101(X11) ) ) ),
introduced(definition,[new_symbols(definition,[ren12])],[main_nc_elimTB]) ).
% FOF RENAMING INFERENCE
fof(main_nc_renObv,negated_conjecture,
? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| p3(X6) ) ) ) ) )
| ~ ( ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ren12(X11) ) ) ) ) )
& ~ 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]) ).
% FOF SIMPLE INFERENCE
fof(main_nc_elimImpEquivPushNegMiniScope,negated_conjecture,
? [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| p3(X6) ) ) ) ) )
& ! [X7] :
( ~ r1(X1,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ren12(X11) ) ) ) ) )
& ~ p101(X1)
& p100(X1) ),
inference(elimImpEquivPushNegMiniScope,[status(thm)],[main_nc_renObv]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(main_nc_skol,negated_conjecture,
( ! [X2] :
( ~ r1(skc11,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| p3(X6) ) ) ) ) )
& ! [X7] :
( ~ r1(skc11,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ren12(X11) ) ) ) ) )
& ~ p101(skc11)
& p100(skc11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skc11]),skolemize(X1,skc11)],[main_nc_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_72,plain,
( ~ r1(skc11,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ren12(X4) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren12_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren12(X1)
| ( ( ren1(X1)
| p105(X1)
| ~ p104(X1) )
& ( ren2(X1)
| p104(X1)
| ~ p103(X1) )
& ( ren3(X1)
| p103(X1)
| ~ p102(X1) )
& ( ren4(X1)
| p102(X1)
| ~ p101(X1) )
& ( ren5(X1)
| p101(X1)
| ~ p100(X1) )
& ( ren6(X1)
| ~ p105(X1) )
& ( ren7(X1)
| ~ p104(X1) )
& ( ren8(X1)
| ~ p103(X1) )
& ( ren9(X1)
| ~ p102(X1) )
& ( ren10(X1)
| ~ p101(X1) )
& ( ren11(X1)
| ~ p100(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)],[ren12_defn]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_58,plain,
( ~ ren12(X0)
| ~ p100(X0)
| ren5(X0)
| p101(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren12_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_57,plain,
( ~ ren12(X0)
| ~ p101(X0)
| ren4(X0)
| p102(X0) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren12_elimImpEquivPushNegMiniScope])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_71,plain,
( ~ r1(skc11,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p3(X4) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF SIMPLE INFERENCE
fof(ren4_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren4(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)],[ren4_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren4_skol,plain,
! [X1] :
( ~ ren4(X1)
| ( r1(X1,skf7(X1))
& ~ p3(skf7(X1))
& ~ p103(skf7(X1))
& p102(skf7(X1))
& r1(X1,skf8(X1))
& p3(skf8(X1))
& ~ p103(skf8(X1))
& p102(skf8(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf7,skf8]),skolemize(X2,skf7(X1)),skolemize(X3,skf8(X1))],[ren4_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_27,plain,
( ~ ren4(X0)
| ~ p3(skf7(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_26,plain,
( ~ ren4(X0)
| r1(X0,skf7(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren4_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_96,plain,
( ~ r1(skc11,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ ren4(X3) ),
inference(resolution,[status(thm)],[c_71,c_27,c_26]) ).
% FOF SIMPLE INFERENCE
fof(ren5_elimImpEquivPushNegMiniScope,plain,
! [X1] :
( ~ ren5(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)],[ren5_defn]) ).
% FOF SKOLEM INFERENCE. WIP!!
fof(ren5_skol,plain,
! [X1] :
( ~ ren5(X1)
| ( r1(X1,skf9(X1))
& ~ p2(skf9(X1))
& ~ p102(skf9(X1))
& p101(skf9(X1))
& r1(X1,skf10(X1))
& p2(skf10(X1))
& ~ p102(skf10(X1))
& p101(skf10(X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[skf9,skf10]),skolemize(X2,skf9(X1)),skolemize(X3,skf10(X1))],[ren5_elimImpEquivPushNegMiniScope]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_36,plain,
( ~ ren5(X0)
| ~ p102(skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_37,plain,
( ~ ren5(X0)
| p101(skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_34,plain,
( ~ ren5(X0)
| r1(X0,skf9(X0)) ),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[ren5_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_88,plain,
( ~ r1(skc11,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ ren5(X3)
| ren12(skf9(X3)) ),
inference(resolution,[status(thm)],[c_72,c_34]) ).
% 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])]) ).
% CNF SPASS RESOLUTION.
cnf(c_97,plain,
~ ren5(skc11),
inference(resolution,[status(thm)],[c_57,c_96,c_36,c_37,c_34,c_88,c_1]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_73,plain,
~ p101(skc11),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% FOF PUSH DISJ SPLITTING.
cnf(c_74,plain,
p100(skc11),
inference(split_conjunct,[status(thm)],[inference(push_disj,[status(thm)],[main_nc_skol])]) ).
% CNF SPASS RESOLUTION.
cnf(c_99,plain,
$false,
inference(byPropositionalAbstraction,[status(thm)],[c_72,c_58,c_97,c_73,c_74,c_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n031.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 5 17:29:10 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36
% 0.10/0.36 % Input Clauses:
% 0.10/0.36 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.10/0.36 % 2:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.10/0.36 % 3:2:1:INP:Top: ren1(x0),p6(skf1(x0)) ->
% 0.10/0.36 % 4:2:1:INP:Top: ren1(x0),p106(skf1(x0)) ->
% 0.10/0.36 % 5:2:1:INP:Top: ren1(x0) -> p105(skf1(x0))
% 0.10/0.36 % 6:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.10/0.36 % 7:2:1:INP:Top: ren1(x0) -> p6(skf2(x0))
% 0.10/0.36 % 8:2:1:INP:Top: ren1(x0),p106(skf2(x0)) ->
% 0.10/0.36 % 9:2:1:INP:Top: ren1(x0) -> p105(skf2(x0))
% 0.10/0.36 % 10:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.10/0.36 % 11:2:1:INP:Top: ren2(x0),p5(skf3(x0)) ->
% 0.10/0.36 % 12:2:1:INP:Top: ren2(x0),p105(skf3(x0)) ->
% 0.10/0.36 % 13:2:1:INP:Top: ren2(x0) -> p104(skf3(x0))
% 0.10/0.36 % 14:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.10/0.36 % 15:2:1:INP:Top: ren2(x0) -> p5(skf4(x0))
% 0.10/0.36 % 16:2:1:INP:Top: ren2(x0),p105(skf4(x0)) ->
% 0.10/0.36 % 17:2:1:INP:Top: ren2(x0) -> p104(skf4(x0))
% 0.10/0.36 % 18:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.10/0.36 % 19:2:1:INP:Top: ren3(x0),p4(skf5(x0)) ->
% 0.10/0.36 % 20:2:1:INP:Top: ren3(x0),p104(skf5(x0)) ->
% 0.10/0.36 % 21:2:1:INP:Top: ren3(x0) -> p103(skf5(x0))
% 0.10/0.36 % 22:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.10/0.36 % 23:2:1:INP:Top: ren3(x0) -> p4(skf6(x0))
% 0.10/0.36 % 24:2:1:INP:Top: ren3(x0),p104(skf6(x0)) ->
% 0.10/0.36 % 25:2:1:INP:Top: ren3(x0) -> p103(skf6(x0))
% 0.10/0.36 % 26:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.10/0.36 % 27:2:1:INP:Top: ren4(x0),p3(skf7(x0)) ->
% 0.10/0.36 % 28:2:1:INP:Top: ren4(x0),p103(skf7(x0)) ->
% 0.10/0.36 % 29:2:1:INP:Top: ren4(x0) -> p102(skf7(x0))
% 0.10/0.36 % 30:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.10/0.36 % 31:2:1:INP:Top: ren4(x0) -> p3(skf8(x0))
% 0.10/0.36 % 32:2:1:INP:Top: ren4(x0),p103(skf8(x0)) ->
% 0.10/0.36 % 33:2:1:INP:Top: ren4(x0) -> p102(skf8(x0))
% 0.10/0.36 % 34:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.10/0.36 % 35:2:1:INP:Top: ren5(x0),p2(skf9(x0)) ->
% 0.10/0.36 % 36:2:1:INP:Top: ren5(x0),p102(skf9(x0)) ->
% 0.10/0.36 % 37:2:1:INP:Top: ren5(x0) -> p101(skf9(x0))
% 0.10/0.36 % 38:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.10/0.36 % 39:2:1:INP:Top: ren5(x0) -> p2(skf10(x0))
% 0.10/0.36 % 40:2:1:INP:Top: ren5(x0),p102(skf10(x0)) ->
% 0.10/0.36 % 41:2:1:INP:Top: ren5(x0) -> p101(skf10(x0))
% 0.10/0.36 % 42:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.10/0.36 % 43:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.10/0.36 % 44:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.10/0.36 % 45:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 0.10/0.36 % 46:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 0.10/0.36 % 47:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 0.10/0.36 % 48:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 0.10/0.36 % 49:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 0.10/0.36 % 50:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.10/0.36 % 51:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.10/0.36 % 52:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.10/0.36 % 53:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.10/0.36 % 54:4:1:INP:Top: ren12(x0),p104(x0) -> ren1(x0),p105(x0)
% 0.10/0.36 % 55:4:1:INP:Top: ren12(x0),p103(x0) -> ren2(x0),p104(x0)
% 0.10/0.36 % 56:4:1:INP:Top: ren12(x0),p102(x0) -> ren3(x0),p103(x0)
% 0.10/0.36 % 57:4:1:INP:Top: ren12(x0),p101(x0) -> ren4(x0),p102(x0)
% 0.10/0.36 % 58:4:1:INP:Top: ren12(x0),p100(x0) -> ren5(x0),p101(x0)
% 0.10/0.36 % 59:3:1:INP:Top: ren12(x0),p105(x0) -> ren6(x0)
% 0.10/0.36 % 60:3:1:INP:Top: ren12(x0),p104(x0) -> ren7(x0)
% 0.10/0.36 % 61:3:1:INP:Top: ren12(x0),p103(x0) -> ren8(x0)
% 0.10/0.36 % 62:3:1:INP:Top: ren12(x0),p102(x0) -> ren9(x0)
% 0.10/0.36 % 63:3:1:INP:Top: ren12(x0),p101(x0) -> ren10(x0)
% 0.10/0.36 % 64:3:1:INP:Top: ren12(x0),p100(x0) -> ren11(x0)
% 0.10/0.36 % 65:3:1:INP:Top: ren12(x0),p106(x0) -> p105(x0)
% 0.10/0.36 % 66:3:1:INP:Top: ren12(x0),p105(x0) -> p104(x0)
% 0.10/0.36 % 67:3:1:INP:Top: ren12(x0),p104(x0) -> p103(x0)
% 0.10/0.36 % 68:3:1:INP:Top: ren12(x0),p103(x0) -> p102(x0)
% 0.10/0.36 % 69:3:1:INP:Top: ren12(x0),p102(x0) -> p101(x0)
% 0.10/0.36 % 70:3:1:INP:Top: ren12(x0),p101(x0) -> p100(x0)
% 0.10/0.36 % 71:6:5:INP:TopTopTopTopTop: r1(skc11,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4) -> p3(x4)
% 0.10/0.36 % 72:6:5:INP:TopTopTopTopTop: r1(skc11,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4) -> ren12(x4)
% 0.10/0.36 % 73:1:0:INP:: p101(skc11) ->
% 0.10/0.36 % 74:1:0:INP:: -> p100(skc11)
% 0.10/0.36
% 0.10/0.36 % Predicates: r1 p3 p6 p106 p105 p104 p5 p103 p4 p102 p101 p2 p100 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12
% 0.10/0.36 % Fol Constants: skc11
% 0.10/0.36 % Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10
% 0.10/0.36 % Problem Properties:
% 0.10/0.36 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.15/0.41
% 0.15/0.41
% 0.15/0.41 % Reduced Input Axiom Clauses:
% 0.15/0.41 % 1:1:1:INP:Top: -> r1(x0,x0)
% 0.15/0.41 % 2:2:1:INP:Top: ren1(x0) -> r1(x0,skf1(x0))
% 0.15/0.41 % 3:2:1:INP:Top: ren1(x0),p6(skf1(x0)) ->
% 0.15/0.41 % 4:2:1:INP:Top: ren1(x0),p106(skf1(x0)) ->
% 0.15/0.41 % 5:2:1:INP:Top: ren1(x0) -> p105(skf1(x0))
% 0.15/0.41 % 6:2:1:INP:Top: ren1(x0) -> r1(x0,skf2(x0))
% 0.15/0.41 % 7:2:1:INP:Top: ren1(x0) -> p6(skf2(x0))
% 0.15/0.41 % 8:2:1:INP:Top: ren1(x0),p106(skf2(x0)) ->
% 0.15/0.41 % 9:2:1:INP:Top: ren1(x0) -> p105(skf2(x0))
% 0.15/0.41 % 10:2:1:INP:Top: ren2(x0) -> r1(x0,skf3(x0))
% 0.15/0.41 % 11:2:1:INP:Top: ren2(x0),p5(skf3(x0)) ->
% 0.15/0.41 % 12:2:1:INP:Top: ren2(x0),p105(skf3(x0)) ->
% 0.15/0.41 % 13:2:1:INP:Top: ren2(x0) -> p104(skf3(x0))
% 0.15/0.41 % 14:2:1:INP:Top: ren2(x0) -> r1(x0,skf4(x0))
% 0.15/0.41 % 15:2:1:INP:Top: ren2(x0) -> p5(skf4(x0))
% 0.15/0.41 % 16:2:1:INP:Top: ren2(x0),p105(skf4(x0)) ->
% 0.15/0.41 % 17:2:1:INP:Top: ren2(x0) -> p104(skf4(x0))
% 0.15/0.41 % 18:2:1:INP:Top: ren3(x0) -> r1(x0,skf5(x0))
% 0.15/0.41 % 19:2:1:INP:Top: ren3(x0),p4(skf5(x0)) ->
% 0.15/0.41 % 20:2:1:INP:Top: ren3(x0),p104(skf5(x0)) ->
% 0.15/0.41 % 21:2:1:INP:Top: ren3(x0) -> p103(skf5(x0))
% 0.15/0.41 % 22:2:1:INP:Top: ren3(x0) -> r1(x0,skf6(x0))
% 0.15/0.41 % 23:2:1:INP:Top: ren3(x0) -> p4(skf6(x0))
% 0.15/0.41 % 24:2:1:INP:Top: ren3(x0),p104(skf6(x0)) ->
% 0.15/0.41 % 25:2:1:INP:Top: ren3(x0) -> p103(skf6(x0))
% 0.15/0.41 % 26:2:1:INP:Top: ren4(x0) -> r1(x0,skf7(x0))
% 0.15/0.41 % 27:2:1:INP:Top: ren4(x0),p3(skf7(x0)) ->
% 0.15/0.41 % 28:2:1:INP:Top: ren4(x0),p103(skf7(x0)) ->
% 0.15/0.41 % 29:2:1:INP:Top: ren4(x0) -> p102(skf7(x0))
% 0.15/0.41 % 30:2:1:INP:Top: ren4(x0) -> r1(x0,skf8(x0))
% 0.15/0.41 % 31:2:1:INP:Top: ren4(x0) -> p3(skf8(x0))
% 0.15/0.41 % 32:2:1:INP:Top: ren4(x0),p103(skf8(x0)) ->
% 0.15/0.41 % 33:2:1:INP:Top: ren4(x0) -> p102(skf8(x0))
% 0.15/0.41 % 34:2:1:INP:Top: ren5(x0) -> r1(x0,skf9(x0))
% 0.15/0.41 % 35:2:1:INP:Top: ren5(x0),p2(skf9(x0)) ->
% 0.15/0.41 % 36:2:1:INP:Top: ren5(x0),p102(skf9(x0)) ->
% 0.15/0.41 % 37:2:1:INP:Top: ren5(x0) -> p101(skf9(x0))
% 0.15/0.41 % 38:2:1:INP:Top: ren5(x0) -> r1(x0,skf10(x0))
% 0.15/0.41 % 39:2:1:INP:Top: ren5(x0) -> p2(skf10(x0))
% 0.15/0.41 % 40:2:1:INP:Top: ren5(x0),p102(skf10(x0)) ->
% 0.15/0.41 % 41:2:1:INP:Top: ren5(x0) -> p101(skf10(x0))
% 0.15/0.41 % 42:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p6(x1),p105(x1) -> p6(x0)
% 0.15/0.41 % 43:5:2:INP:TopTop: ren6(x0),r1(x0,x1),p105(x1),p6(x0) -> p6(x1)
% 0.15/0.41 % 44:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p5(x1),p104(x1) -> p5(x0)
% 0.15/0.41 % 45:5:2:INP:TopTop: ren7(x0),r1(x0,x1),p104(x1),p5(x0) -> p5(x1)
% 0.15/0.41 % 46:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p4(x1),p103(x1) -> p4(x0)
% 0.15/0.41 % 47:5:2:INP:TopTop: ren8(x0),r1(x0,x1),p103(x1),p4(x0) -> p4(x1)
% 0.15/0.41 % 48:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p3(x1),p102(x1) -> p3(x0)
% 0.15/0.41 % 49:5:2:INP:TopTop: ren9(x0),r1(x0,x1),p102(x1),p3(x0) -> p3(x1)
% 0.15/0.41 % 50:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p2(x1),p101(x1) -> p2(x0)
% 0.15/0.41 % 51:5:2:INP:TopTop: ren10(x0),r1(x0,x1),p101(x1),p2(x0) -> p2(x1)
% 0.15/0.41 % 52:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p1(x1),p100(x1) -> p1(x0)
% 0.15/0.41 % 53:5:2:INP:TopTop: ren11(x0),r1(x0,x1),p100(x1),p1(x0) -> p1(x1)
% 0.15/0.41 % 54:4:1:INP:Top: ren12(x0),p104(x0) -> ren1(x0),p105(x0)
% 0.15/0.41 % 55:4:1:INP:Top: ren12(x0),p103(x0) -> ren2(x0),p104(x0)
% 0.15/0.41 % 56:4:1:INP:Top: ren12(x0),p102(x0) -> ren3(x0),p103(x0)
% 0.15/0.41 % 57:4:1:INP:Top: ren12(x0),p101(x0) -> ren4(x0),p102(x0)
% 0.15/0.41 % 58:4:1:INP:Top: ren12(x0),p100(x0) -> ren5(x0),p101(x0)
% 0.15/0.41 % 59:3:1:INP:Top: ren12(x0),p105(x0) -> ren6(x0)
% 0.15/0.41 % 60:3:1:INP:Top: ren12(x0),p104(x0) -> ren7(x0)
% 0.15/0.41 % 61:3:1:INP:Top: ren12(x0),p103(x0) -> ren8(x0)
% 0.15/0.41 % 62:3:1:INP:Top: ren12(x0),p102(x0) -> ren9(x0)
% 0.15/0.41 % 63:3:1:INP:Top: ren12(x0),p101(x0) -> ren10(x0)
% 0.15/0.41 % 64:3:1:INP:Top: ren12(x0),p100(x0) -> ren11(x0)
% 0.15/0.41 % 65:3:1:INP:Top: ren12(x0),p106(x0) -> p105(x0)
% 0.15/0.41 % 66:3:1:INP:Top: ren12(x0),p105(x0) -> p104(x0)
% 0.15/0.41 % 67:3:1:INP:Top: ren12(x0),p104(x0) -> p103(x0)
% 0.15/0.41 % 68:3:1:INP:Top: ren12(x0),p103(x0) -> p102(x0)
% 0.15/0.41 % 69:3:1:INP:Top: ren12(x0),p102(x0) -> p101(x0)
% 0.15/0.41 % 70:3:1:INP:Top: ren12(x0),p101(x0) -> p100(x0)
% 0.15/0.41
% 0.15/0.41 % Reduced Input Conjecture Clauses:
% 0.15/0.41 % 71:6:5:INP:TopTopTopTopTop: r1(skc11,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4) -> p3(x4)
% 0.15/0.41 % 72:6:5:INP:TopTopTopTopTop: r1(skc11,x0),r1(x0,x1),r1(x1,x2),r1(x2,x3),r1(x3,x4) -> ren12(x4)
% 0.15/0.41 % 73:1:0:INP:: p101(skc11) ->
% 0.15/0.41 % 74:1:0:INP:: -> p100(skc11)
% 0.15/0.41
% 0.15/0.41
% 0.15/0.41 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 196 atoms initially. Used heuristic: lmodel_grow ===
% 0.15/0.41
% 0.15/0.41 %
% 0.15/0.41
% 0.15/0.41 % === SAT Conflict found: 99:0:0:[72.0,58.0,97.0,73.0,74.0,1.0]:: ->
% 0.15/0.41
% 0.15/0.41 % SZS status Theorem
% 0.15/0.41 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41
% 0.15/0.41 % SPASS-SCL-FOL Statistics:
% 0.15/0.41 % Number of learned clauses: 23
% 0.15/0.41 % Number of propagations: 192
% 0.15/0.41 % Number of decisions: 545
% 0.15/0.41 % Number of resolutions: 39
% 0.15/0.41 % Number of condensations: 0
% 0.15/0.41 % Number of sub resolutions: 1
% 0.15/0.41
% 0.15/0.41 % Solver is done. Empty clause found
% 0.15/0.41
% 0.15/0.41 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.15/0.41 % SZS output start Proof for theBenchmark
% See solution above
% 0.15/0.42 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.15/0.42
% 0.15/0.42
% 0.15/0.42 % Needed: 0:00:00.06
% 0.15/0.42
% 0.15/0.42 % ###
% 0.15/0.42 % ### Pagesize: 8192
% 0.15/0.42 % ### Marksize: 0
% 0.15/0.42 % ### Memory demanded: 2441 KBytes
% 0.15/0.42 % ### Memory freed: 2441 KBytes
% 0.15/0.42 % ### Memory remaining: 0 Bytes
% 0.15/0.42 % ### Pages allocated: 358 Pages
% 0.15/0.42 % ###
%------------------------------------------------------------------------------