%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS196+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 : n015.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:27 PM UTC 2026
% Result : Theorem 95.26s 12.57s
% Output : Proof 95.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 26
% Syntax : Number of formulae : 129 ( 53 unt; 0 def)
% Number of atoms : 419 ( 39 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 486 ( 196 ~; 138 |; 129 &)
% ( 15 <=>; 6 =>; 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 : 62 ( 62 usr; 28 con; 0-4 aty)
% Number of variables : 335 ( 25 sgn 168 !; 82 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f20,axiom,
! [S1,S2] :
( ! [Ax,C] :
( status(Ax,C,S1)
=> status(Ax,C,S2) )
<=> isa(S1,S2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',isa) ).
fof(f20_nnf,plain,
! [S1,S2] :
( ( ~ isa(S1,S2)
| ! [Ax,C] :
( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) )
& ( isa(S1,S2)
| ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) ) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [S1,S2,Ax,C] :
( ( ~ isa(S1,S2)
| status(Ax,C,S2)
| ~ status(Ax,C,S1) )
& ( isa(S1,S2)
| ( ~ status(sk43(S1,S2),sk44(S1,S2),S2)
& status(sk43(S1,S2),sk44(S1,S2),S1) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk43,sk44])],[f20_nnf]) ).
cnf(c83,plain,
( isa(X0,X1)
| ~ status(sk43(X0,X1),sk44(X0,X1),X1) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t204,plain,
ifeq(status(sk43(X1,X2),sk44(X1,X2),X2),true,isa(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(t1563,plain,
ifeq(status(sk43(X1,X2),sk44(X1,X2),X2),true,isa(X1,X2),true) = true,
inference(orient,[status(thm)],[t204]) ).
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(c15,plain,
( status(X0,X1,thm)
| model(sk9(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t158,plain,
or(model(sk9(X1,X2),X1),status(X1,X2,thm)) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t1599,plain,
or(model(sk9(X1,X2),X1),status(X1,X2,thm)) = true,
inference(orient,[status(thm)],[t158]) ).
cnf(t108,plain,
ifeq(notq(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1388,plain,
ifeq(notq(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t108]) ).
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(t163,plain,
or(notq(model(X1,X2)),notq(status(X2,X3,wca))) = true,
inference(equality_encoding,[status(esa)],[c65]) ).
cnf(t1670,plain,
or(notq(model(X1,X2)),notq(status(X2,X3,wca))) = true,
inference(orient,[status(thm)],[t163]) ).
cnf(c82,plain,
( isa(X0,X1)
| status(sk43(X0,X1),sk44(X0,X1),X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t189,plain,
or(status(sk43(X1,X2),sk44(X1,X2),X1),isa(X1,X2)) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(t1726,plain,
or(status(sk43(X1,X2),sk44(X1,X2),X1),isa(X1,X2)) = true,
inference(orient,[status(thm)],[t189]) ).
fof(f32,conjecture,
isa(wca,thm),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',isa_wca_thm) ).
fof(f32_neg,negated_conjecture,
~ isa(wca,thm),
inference(negated_conjecture,[status(cth)],[f32]) ).
fof(f32_nnf,plain,
~ isa(wca,thm),
inference(nnf_transformation,[status(thm)],[f32_neg]) ).
fof(f32_sk,plain,
~ isa(wca,thm),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c118,plain,
~ isa(wca,thm),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(t2,plain,
isa(wca,thm) = false,
inference(equality_encoding,[status(esa)],[c118]) ).
cnf(t1789,plain,
isa(wca,thm) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t1790,plain,
true = or(status(sk43(wca,thm),sk44(wca,thm),wca),false),
inference(cp,[status(thm)],[t1726,t1789]) ).
cnf(t52,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t257,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t52]) ).
cnf(t18423,plain,
true = status(sk43(wca,thm),sk44(wca,thm),wca),
inference(step,[status(thm)],[t1790,t257]) ).
cnf(t16977,plain,
status(sk43(wca,thm),sk44(wca,thm),wca) = true,
inference(orient,[status(thm)],[t18423]) ).
cnf(t16978,plain,
true = or(notq(model(X1,sk43(wca,thm))),notq(true)),
inference(cp,[status(thm)],[t1670,t16977]) ).
cnf(t1,plain,
notq(true) = false,
introduced(definition) ).
cnf(t1787,plain,
notq(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t18424,plain,
true = or(notq(model(X1,sk43(wca,thm))),false),
inference(step,[status(thm)],[t16978,t1787]) ).
cnf(t18425,plain,
true = notq(model(X1,sk43(wca,thm))),
inference(step,[status(thm)],[t18424,t257]) ).
cnf(t16999,plain,
notq(model(X1,sk43(wca,thm))) = true,
inference(orient,[status(thm)],[t18425]) ).
cnf(t17000,plain,
false = ifeq(true,true,model(X1,sk43(wca,thm)),false),
inference(cp,[status(thm)],[t1388,t16999]) ).
cnf(t85,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t256,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t85]) ).
cnf(t18426,plain,
false = model(X1,sk43(wca,thm)),
inference(step,[status(thm)],[t17000,t256]) ).
cnf(t17001,plain,
model(X1,sk43(wca,thm)) = false,
inference(orient,[status(thm)],[t18426]) ).
cnf(t17013,plain,
true = or(false,status(sk43(wca,thm),X1,thm)),
inference(cp,[status(thm)],[t1599,t17001]) ).
cnf(t54,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t258,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t54]) ).
cnf(t18427,plain,
true = status(sk43(wca,thm),X1,thm),
inference(step,[status(thm)],[t17013,t258]) ).
cnf(t17140,plain,
status(sk43(wca,thm),X1,thm) = true,
inference(orient,[status(thm)],[t18427]) ).
cnf(t17141,plain,
true = ifeq(true,true,isa(wca,thm),true),
inference(cp,[status(thm)],[t1563,t17140]) ).
cnf(t18429,plain,
true = isa(wca,thm),
inference(step,[status(thm)],[t17141,t256]) ).
cnf(t18430,plain,
true = false,
inference(step,[status(thm)],[t18429,t1789]) ).
cnf(t17306,plain,
false = true,
inference(orient,[status(thm)],[t18430]) ).
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]) ).
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,t17306]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS196+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 19:43:12 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 95.26/12.57 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 95.26/12.57 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------