%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS259+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:32 PM UTC 2026
% Result : Theorem 16.28s 2.74s
% Output : Proof 16.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 23
% Syntax : Number of formulae : 109 ( 30 unt; 0 def)
% Number of atoms : 413 ( 12 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 510 ( 206 ~; 146 |; 135 &)
% ( 16 <=>; 5 =>; 0 <=; 2 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 64 ( 64 usr; 30 con; 0-4 aty)
% Number of variables : 329 ( 14 sgn 180 !; 89 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [Ax,C] :
( ! [I1] :
( model(I1,Ax)
=> model(I1,C) )
<=> status(Ax,C,thm) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm) ).
fof(f4_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,thm)
| ! [I1] :
( model(I1,C)
| ~ model(I1,Ax) ) )
& ( status(Ax,C,thm)
| ? [I1] :
( ~ model(I1,C)
& model(I1,Ax) ) ) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [Ax,C,I1] :
( ( ~ status(Ax,C,thm)
| model(I1,C)
| ~ model(I1,Ax) )
& ( status(Ax,C,thm)
| ( ~ model(sk9(Ax,C),C)
& model(sk9(Ax,C),Ax) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f4_nnf]) ).
cnf(c16,plain,
( status(X0,X1,thm)
| ~ model(sk9(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi16,axiom,
ifeq(model(sk9(X0,X1),X1),true,status(X0,X1,thm),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
fof(f26,axiom,
? [F] :
! [I] : model(I,F),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tautology) ).
fof(f26_nnf,plain,
? [F] :
! [I] : model(I,F),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [I] : model(I,sk51),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk51])],[f26_nnf]) ).
cnf(c103,plain,
model(X1,sk51),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(hi80,axiom,
model(X0,sk51) = true,
inference(equality_encoding,[status(esa)],[c103]) ).
cnf(h13,plain,
status(V0,sk51,thm) = true,
inference(hyper_resolution,[status(thm)],[hi16,hi80]) ).
fof(f6,axiom,
! [Ax,C] :
( ( ! [I2] : model(I2,C)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,tac) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tac) ).
fof(f6_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,tac)
| ( ! [I2] : model(I2,C)
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,tac)
| ? [I2] : ~ model(I2,C)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [I1,Ax,C,I2] :
( ( ~ status(Ax,C,tac)
| ( model(I2,C)
& model(sk13(Ax,C),Ax) ) )
& ( status(Ax,C,tac)
| ~ model(sk12(Ax,C),C)
| ~ model(I1,Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13])],[f6_nnf]) ).
cnf(c25,plain,
( status(X0,X1,tac)
| ~ model(sk12(X0,X1),X1)
| ~ model(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi23,axiom,
ifeq(model(X0,X1),true,ifeq(model(sk12(X1,X2),X2),true,status(X1,X2,tac),true),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(h10,plain,
status(sk51,sk51,tac) = true,
inference(hyper_resolution,[status(thm)],[hi23,hi80,hi80]) ).
fof(f19,axiom,
! [S1,S2] :
( ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) )
<=> mighta(S1,S2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mighta) ).
fof(f19_nnf,plain,
! [S1,S2] :
( ( ~ mighta(S1,S2)
| ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) ) )
& ( mighta(S1,S2)
| ! [Ax,C] :
( ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [Ax,C,S1,S2] :
( ( ~ mighta(S1,S2)
| ( status(sk41(S1,S2),sk42(S1,S2),S2)
& status(sk41(S1,S2),sk42(S1,S2),S1) ) )
& ( mighta(S1,S2)
| ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk41,sk42])],[f19_nnf]) ).
cnf(c79,plain,
( mighta(X0,X1)
| ~ status(X2,X3,X1)
| ~ status(X2,X3,X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi65,axiom,
ifeq(status(X0,X1,X2),true,ifeq(status(X0,X1,X3),true,mighta(X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c79]) ).
cnf(h358,plain,
mighta(tac,thm) = true,
inference(hyper_resolution,[status(thm)],[hi65,h10,h13]) ).
fof(f32,conjecture,
mighta(tac,thm),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mighta_tac_thm) ).
fof(f32_neg,negated_conjecture,
~ mighta(tac,thm),
inference(negated_conjecture,[status(cth)],[f32]) ).
fof(f32_nnf,plain,
~ mighta(tac,thm),
inference(nnf_transformation,[status(thm)],[f32_neg]) ).
fof(f32_sk,plain,
~ mighta(tac,thm),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c118,plain,
~ mighta(tac,thm),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(hi110,negated_conjecture,
ifeq(mighta(tac,thm),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi110,h358]) ).
cnf(t1682,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f7,axiom,
! [Ax,C] :
( ( ? [I3] :
( ~ model(I3,Ax)
& model(I3,C) )
& ! [I2] :
( model(I2,Ax)
=> model(I2,C) )
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wec) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wec) ).
fof(f7_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,wec)
| ( ? [I3] :
( ~ model(I3,Ax)
& model(I3,C) )
& ! [I2] :
( model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,wec)
| ! [I3] :
( model(I3,Ax)
| ~ model(I3,C) )
| ? [I2] :
( ~ model(I2,C)
& model(I2,Ax) )
| ! [I1] : ~ model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [I1,Ax,C,I3,I2] :
( ( ~ status(Ax,C,wec)
| ( ~ model(sk16(Ax,C),Ax)
& model(sk16(Ax,C),C)
& ( model(I2,C)
| ~ model(I2,Ax) )
& model(sk15(Ax,C),Ax) ) )
& ( status(Ax,C,wec)
| model(I3,Ax)
| ~ model(I3,C)
| ( ~ model(sk14(Ax,C),C)
& model(sk14(Ax,C),Ax) )
| ~ model(I1,Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14,sk15,sk16])],[f7_nnf]) ).
cnf(c33,plain,
( ~ status(X0,X1,wec)
| ~ model(sk16(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f8,axiom,
! [Ax,C] :
( ( ! [I3] :
( model(I3,Ax)
<=> model(I3,C) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,eth) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',eth) ).
fof(f8_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,eth)
| ( ! [I3] :
( ( ~ model(I3,C)
| model(I3,Ax) )
& ( model(I3,C)
| ~ model(I3,Ax) ) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,eth)
| ? [I3] :
( ( model(I3,C)
& ~ model(I3,Ax) )
| ( ~ model(I3,C)
& model(I3,Ax) ) )
| ! [I2] : model(I2,Ax)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [I1,Ax,I2,C,I3] :
( ( ~ status(Ax,C,eth)
| ( ( ~ model(I3,C)
| model(I3,Ax) )
& ( model(I3,C)
| ~ model(I3,Ax) )
& ~ model(sk19(Ax,C),Ax)
& model(sk18(Ax,C),Ax) ) )
& ( status(Ax,C,eth)
| ( model(sk17(Ax,C),C)
& ~ model(sk17(Ax,C),Ax) )
| ( ~ model(sk17(Ax,C),C)
& model(sk17(Ax,C),Ax) )
| model(I2,Ax)
| ~ model(I1,Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17,sk18,sk19])],[f8_nnf]) ).
cnf(c39,plain,
( ~ status(X0,X1,eth)
| ~ model(sk19(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
fof(f10,axiom,
! [Ax,C] :
( ( ! [I3] : model(I3,C)
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wtc) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wtc) ).
fof(f10_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,wtc)
| ( ! [I3] : model(I3,C)
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,wtc)
| ? [I3] : ~ model(I3,C)
| ! [I2] : model(I2,Ax)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [I1,Ax,I2,C,I3] :
( ( ~ status(Ax,C,wtc)
| ( model(I3,C)
& ~ model(sk23(Ax,C),Ax)
& model(sk22(Ax,C),Ax) ) )
& ( status(Ax,C,wtc)
| ~ model(sk21(Ax,C),C)
| model(I2,Ax)
| ~ model(I1,Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk21,sk22,sk23])],[f10_nnf]) ).
cnf(c47,plain,
( ~ status(X0,X1,wtc)
| ~ model(sk23(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f11,axiom,
! [Ax,C] :
( ( ? [I4] : ~ model(I4,C)
& ? [I3] :
( ~ model(I3,Ax)
& model(I3,C) )
& ! [I2] :
( model(I2,Ax)
=> model(I2,C) )
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wth) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wth) ).
fof(f11_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,wth)
| ( ? [I4] : ~ model(I4,C)
& ? [I3] :
( ~ model(I3,Ax)
& model(I3,C) )
& ! [I2] :
( model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] : model(I1,Ax) ) )
& ( status(Ax,C,wth)
| ! [I4] : model(I4,C)
| ! [I3] :
( model(I3,Ax)
| ~ model(I3,C) )
| ? [I2] :
( ~ model(I2,C)
& model(I2,Ax) )
| ! [I1] : ~ model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [I1,Ax,C,I3,I4,I2] :
( ( ~ status(Ax,C,wth)
| ( ~ model(sk27(Ax,C),C)
& ~ model(sk26(Ax,C),Ax)
& model(sk26(Ax,C),C)
& ( model(I2,C)
| ~ model(I2,Ax) )
& model(sk25(Ax,C),Ax) ) )
& ( status(Ax,C,wth)
| model(I4,C)
| model(I3,Ax)
| ~ model(I3,C)
| ( ~ model(sk24(Ax,C),C)
& model(sk24(Ax,C),Ax) )
| ~ model(I1,Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk24,sk25,sk26,sk27])],[f11_nnf]) ).
cnf(c54,plain,
( ~ status(X0,X1,wth)
| ~ model(sk26(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(c55,plain,
( ~ status(X0,X1,wth)
| ~ model(sk27(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f12,axiom,
! [Ax,C] :
( ~ ? [I1] : model(I1,Ax)
<=> status(Ax,C,cax) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cax) ).
fof(f12_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,cax)
| ! [I1] : ~ model(I1,Ax) )
& ( status(Ax,C,cax)
| ? [I1] : model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Ax,C,I1] :
( ( ~ status(Ax,C,cax)
| ~ model(I1,Ax) )
& ( status(Ax,C,cax)
| model(sk28(Ax,C),Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk28])],[f12_nnf]) ).
cnf(c57,plain,
( ~ status(X0,X1,cax)
| ~ model(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f13,axiom,
! [Ax,C] :
( ( ? [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,sca) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sca) ).
fof(f13_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,sca)
| ( ? [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) ) )
& ( status(Ax,C,sca)
| ! [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [Ax,C,I2,I1] :
( ( ~ status(Ax,C,sca)
| ( model(sk30(Ax,C),C)
& ~ model(I1,Ax) ) )
& ( status(Ax,C,sca)
| ~ model(I2,C)
| model(sk29(Ax,C),Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk29,sk30])],[f13_nnf]) ).
cnf(c59,plain,
( ~ status(X0,X1,sca)
| ~ model(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f14,axiom,
! [Ax,C] :
( ( ! [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,tca) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tca) ).
fof(f14_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,tca)
| ( ! [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) ) )
& ( status(Ax,C,tca)
| ? [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Ax,C,I1,I2] :
( ( ~ status(Ax,C,tca)
| ( model(I2,C)
& ~ model(I1,Ax) ) )
& ( status(Ax,C,tca)
| ~ model(sk32(Ax,C),C)
| model(sk31(Ax,C),Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk31,sk32])],[f14_nnf]) ).
cnf(c62,plain,
( ~ status(X0,X1,tca)
| ~ model(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
fof(f15,axiom,
! [Ax,C] :
( ( ? [I3] : ~ model(I3,C)
& ? [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wca) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wca) ).
fof(f15_nnf,plain,
! [Ax,C] :
( ( ~ status(Ax,C,wca)
| ( ? [I3] : ~ model(I3,C)
& ? [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) ) )
& ( status(Ax,C,wca)
| ! [I3] : model(I3,C)
| ! [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Ax,C,I2,I3,I1] :
( ( ~ status(Ax,C,wca)
| ( ~ model(sk35(Ax,C),C)
& model(sk34(Ax,C),C)
& ~ model(I1,Ax) ) )
& ( status(Ax,C,wca)
| model(I3,C)
| ~ model(I2,C)
| model(sk33(Ax,C),Ax) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk33,sk34,sk35])],[f15_nnf]) ).
cnf(c65,plain,
( ~ status(X0,X1,wca)
| ~ model(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(c67,plain,
( ~ status(X0,X1,wca)
| ~ model(sk35(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
fof(f21,axiom,
! [S1,S2] :
( ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) )
<=> nota(S1,S2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nota) ).
fof(f21_nnf,plain,
! [S1,S2] :
( ( ~ nota(S1,S2)
| ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) )
& ( nota(S1,S2)
| ! [Ax,C] :
( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [Ax,C,S1,S2] :
( ( ~ nota(S1,S2)
| ( ~ status(sk45(S1,S2),sk46(S1,S2),S2)
& status(sk45(S1,S2),sk46(S1,S2),S1) ) )
& ( nota(S1,S2)
| status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk45,sk46])],[f21_nnf]) ).
cnf(c87,plain,
( ~ nota(X0,X1)
| ~ status(sk45(X0,X1),sk46(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
fof(f22,axiom,
! [S1,S2] :
( ! [Ax,C] :
( status(Ax,C,S1)
=> ~ status(Ax,C,S2) )
<=> nevera(S1,S2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nevera) ).
fof(f22_nnf,plain,
! [S1,S2] :
( ( ~ nevera(S1,S2)
| ! [Ax,C] :
( ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) ) )
& ( nevera(S1,S2)
| ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) ) ) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [S1,S2,Ax,C] :
( ( ~ nevera(S1,S2)
| ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) )
& ( nevera(S1,S2)
| ( status(sk47(S1,S2),sk48(S1,S2),S2)
& status(sk47(S1,S2),sk48(S1,S2),S1) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47,sk48])],[f22_nnf]) ).
cnf(c90,plain,
( ~ nevera(X0,X1)
| ~ status(X2,X3,X1)
| ~ status(X2,X3,X0) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f23,axiom,
! [S1,S2] :
( ! [Ax,C] :
( status(Ax,C,S1)
<~> status(Ax,C,S2) )
<=> xora(S1,S2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',xora) ).
fof(f23_nnf,plain,
! [S1,S2] :
( ( ~ xora(S1,S2)
| ! [Ax,C] :
( ( status(Ax,C,S2)
& ~ status(Ax,C,S1) )
| ( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) ) )
& ( xora(S1,S2)
| ? [Ax,C] :
( ( ~ status(Ax,C,S2)
| status(Ax,C,S1) )
& ( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ) ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [S1,S2,Ax,C] :
( ( ~ xora(S1,S2)
| ( status(Ax,C,S2)
& ~ status(Ax,C,S1) )
| ( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) )
& ( xora(S1,S2)
| ( ( ~ status(sk49(S1,S2),sk50(S1,S2),S2)
| status(sk49(S1,S2),sk50(S1,S2),S1) )
& ( status(sk49(S1,S2),sk50(S1,S2),S2)
| ~ status(sk49(S1,S2),sk50(S1,S2),S1) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk49,sk50])],[f23_nnf]) ).
cnf(c95,plain,
( ~ xora(X0,X1)
| ~ status(X2,X3,X0)
| ~ status(X2,X3,X1) ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
fof(f24,axiom,
! [I,F] :
( model(I,F)
<~> model(I,not(F)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',completeness) ).
fof(f24_nnf,plain,
! [I,F] :
( ( model(I,not(F))
& ~ model(I,F) )
| ( ~ model(I,not(F))
& model(I,F) ) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [I,F] :
( ( model(I,not(F))
& ~ model(I,F) )
| ( ~ model(I,not(F))
& model(I,F) ) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c99,plain,
( ~ model(X0,X1)
| ~ model(X0,not(X1)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f25,axiom,
! [I,F] :
( model(I,F)
<=> ~ model(I,not(F)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not) ).
fof(f25_nnf,plain,
! [I,F] :
( ( model(I,not(F))
| model(I,F) )
& ( ~ model(I,not(F))
| ~ model(I,F) ) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [I,F] :
( ( model(I,not(F))
| model(I,F) )
& ( ~ model(I,not(F))
| ~ model(I,F) ) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c101,plain,
( ~ model(X0,not(X1))
| ~ model(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f27,axiom,
? [F] :
( ? [I2] : ~ model(I2,F)
& ? [I1] : model(I1,F) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',satisfiable) ).
fof(f27_nnf,plain,
? [F] :
( ? [I2] : ~ model(I2,F)
& ? [I1] : model(I1,F) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
( ~ model(sk54,sk52)
& model(sk53,sk52) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk52,sk53,sk54])],[f27_nnf]) ).
cnf(c105,plain,
~ model(sk54,sk52),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f28,axiom,
? [F] :
! [I] : ~ model(I,F),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',contradiction) ).
fof(f28_nnf,plain,
? [F] :
! [I] : ~ model(I,F),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [I] : ~ model(I,sk55),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk55])],[f28_nnf]) ).
cnf(c106,plain,
~ model(X1,sk55),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
fof(f29,axiom,
? [Ax,C] :
( ? [I2] :
( ~ model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sat_non_taut_pair) ).
fof(f29_nnf,plain,
? [Ax,C] :
( ? [I2] :
( ~ model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
( ( ~ model(sk59,sk57)
| ~ model(sk59,sk56) )
& model(sk58,sk57)
& model(sk58,sk56) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk56,sk57,sk58,sk59])],[f29_nnf]) ).
cnf(c109,plain,
( ~ model(sk59,sk57)
| ~ model(sk59,sk56) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f30,axiom,
? [Ax,C] :
( ? [I4] : ~ model(I4,C)
& ? [I3] :
( model(I3,C)
& ~ model(I3,Ax) )
& ! [I2] :
( model(I2,Ax)
=> model(I2,C) )
& ? [I1] : model(I1,Ax) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mixed_pair) ).
fof(f30_nnf,plain,
? [Ax,C] :
( ? [I4] : ~ model(I4,C)
& ? [I3] :
( model(I3,C)
& ~ model(I3,Ax) )
& ! [I2] :
( model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] : model(I1,Ax) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [I2] :
( ~ model(sk64,sk61)
& model(sk63,sk61)
& ~ model(sk63,sk60)
& ( model(I2,sk61)
| ~ model(I2,sk60) )
& model(sk62,sk60) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk60,sk61,sk62,sk63,sk64])],[f30_nnf]) ).
cnf(c112,plain,
~ model(sk63,sk60),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(c114,plain,
~ model(sk64,sk61),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f31,axiom,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_thm_spt) ).
fof(f31_nnf,plain,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
( model(sk68,sk67)
& ~ model(sk65,sk67)
& model(sk65,sk66) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk65,sk66,sk67,sk68])],[f31_nnf]) ).
cnf(c116,plain,
~ model(sk65,sk67),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c33,c39,c47,c54,c55,c57,c59,c62,c65,c67,c87,c90,c95,c99,c101,c105,c106,c109,c112,c114,c116,c118]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1682]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KRS259+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.06/0.65 % Computer : n016.cluster.edu
% 0.06/0.65 % Model : x86_64 x86_64
% 0.06/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.65 % Memory : 8046.5625MB
% 0.06/0.65 % OS : Linux 6.8.0-71-generic
% 0.06/0.65 % CPULimit : 300
% 0.06/0.65 % WCLimit : 300
% 0.06/0.65 % DateTime : Wed Sep 23 19:55:27 UTC 2026
% 0.06/0.65 % CPUTime :
% 0.06/0.65 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.28/2.74 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.28/2.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------