%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : KRS188+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 08:47:28 AM UTC 2026
% Result : Theorem 36.35s 36.67s
% Output : Proof 36.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(unp,axiom,
! [Ax,C] :
( ( ~ ? [I1] : model(I1,Ax)
=> ~ ? [I2] : model(I2,C) )
<=> status(Ax,C,unp) ),
file('KRS001+0.ax',unp) ).
fof(sap,axiom,
! [Ax,C] :
( ( ? [I1] : model(I1,Ax)
=> ? [I2] : model(I2,C) )
<=> status(Ax,C,sap) ),
file('KRS001+0.ax',sap) ).
fof(esa,axiom,
! [Ax,C] :
( ( ? [I1] : model(I1,Ax)
<=> ? [I2] : model(I2,C) )
<=> status(Ax,C,esa) ),
file('KRS001+0.ax',esa) ).
fof(sat,axiom,
! [Ax,C] :
( ? [I1] :
( model(I1,C)
& model(I1,Ax) )
<=> status(Ax,C,sat) ),
file('KRS001+0.ax',sat) ).
fof(thm,axiom,
! [Ax,C] :
( ! [I1] :
( model(I1,Ax)
=> model(I1,C) )
<=> status(Ax,C,thm) ),
file('KRS001+0.ax',thm) ).
fof(eqv,axiom,
! [Ax,C] :
( ( ! [I2] :
( model(I2,Ax)
<=> model(I2,C) )
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,eqv) ),
file('KRS001+0.ax',eqv) ).
fof(tac,axiom,
! [Ax,C] :
( ( ! [I2] : model(I2,C)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,tac) ),
file('KRS001+0.ax',tac) ).
fof(wec,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('KRS001+0.ax',wec) ).
fof(eth,axiom,
! [Ax,C] :
( ( ! [I3] :
( model(I3,Ax)
<=> model(I3,C) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,eth) ),
file('KRS001+0.ax',eth) ).
fof(tau,axiom,
! [Ax,C] :
( ! [I1] :
( model(I1,C)
& model(I1,Ax) )
<=> status(Ax,C,tau) ),
file('KRS001+0.ax',tau) ).
fof(wtc,axiom,
! [Ax,C] :
( ( ! [I3] : model(I3,C)
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wtc) ),
file('KRS001+0.ax',wtc) ).
fof(wth,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('KRS001+0.ax',wth) ).
fof(cax,axiom,
! [Ax,C] :
( ~ ? [I1] : model(I1,Ax)
<=> status(Ax,C,cax) ),
file('KRS001+0.ax',cax) ).
fof(sca,axiom,
! [Ax,C] :
( ( ? [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,sca) ),
file('KRS001+0.ax',sca) ).
fof(tca,axiom,
! [Ax,C] :
( ( ! [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,tca) ),
file('KRS001+0.ax',tca) ).
fof(wca,axiom,
! [Ax,C] :
( ( ? [I3] : ~ model(I3,C)
& ? [I2] : model(I2,C)
& ~ ? [I1] : model(I1,Ax) )
<=> status(Ax,C,wca) ),
file('KRS001+0.ax',wca) ).
fof(csa,axiom,
! [Ax,C] :
( ? [I1] :
( model(I1,not(C))
& model(I1,Ax) )
<=> status(Ax,C,csa) ),
file('KRS001+0.ax',csa) ).
fof(uns,axiom,
! [Ax,C] :
( ( ! [I2] : model(I2,not(C))
& ! [I1] : model(I1,Ax) )
<=> status(Ax,C,uns) ),
file('KRS001+0.ax',uns) ).
fof(noc,axiom,
! [Ax,C] :
( ( ? [I2] :
( model(I2,not(C))
& model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) )
<=> status(Ax,C,noc) ),
file('KRS001+0.ax',noc) ).
fof(mighta,axiom,
! [S1,S2] :
( ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) )
<=> mighta(S1,S2) ),
file('KRS001+1.ax',mighta) ).
fof(isa,axiom,
! [S1,S2] :
( ! [Ax,C] :
( status(Ax,C,S1)
=> status(Ax,C,S2) )
<=> isa(S1,S2) ),
file('KRS001+1.ax',isa) ).
fof(nota,axiom,
! [S1,S2] :
( ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) )
<=> nota(S1,S2) ),
file('KRS001+1.ax',nota) ).
fof(nevera,axiom,
! [S1,S2] :
( ! [Ax,C] :
( status(Ax,C,S1)
=> ~ status(Ax,C,S2) )
<=> nevera(S1,S2) ),
file('KRS001+1.ax',nevera) ).
fof(xora,axiom,
! [S1,S2] :
( ! [Ax,C] :
( ( status(Ax,C,S2)
& ~ status(Ax,C,S1) )
| ( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) )
<=> xora(S1,S2) ),
file('KRS001+1.ax',xora) ).
fof(completeness,axiom,
! [I,F] :
( ( model(I,not(F))
& ~ model(I,F) )
| ( ~ model(I,not(F))
& model(I,F) ) ),
file('KRS001+1.ax',completeness) ).
fof(not,axiom,
! [I,F] :
( model(I,F)
<=> ~ model(I,not(F)) ),
file('KRS001+1.ax',not) ).
fof(tautology,axiom,
? [F] :
! [I] : model(I,F),
file('KRS001+1.ax',tautology) ).
fof(satisfiable,axiom,
? [F] :
( ? [I2] : ~ model(I2,F)
& ? [I1] : model(I1,F) ),
file('KRS001+1.ax',satisfiable) ).
fof(contradiction,axiom,
? [F] :
! [I] : ~ model(I,F),
file('KRS001+1.ax',contradiction) ).
fof(sat_non_taut_pair,axiom,
? [Ax,C] :
( ? [I2] :
( ~ model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) ),
file('KRS001+1.ax',sat_non_taut_pair) ).
fof(mixed_pair,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('KRS001+1.ax',mixed_pair) ).
fof(non_thm_spt,axiom,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
file('KRS001+1.ax',non_thm_spt) ).
fof(isa_wec_thm,conjecture,
isa(wec,thm),
file('theBenchmark.p',isa_wec_thm) ).
fof(f_1_1,plain,
! [Ax,C] :
( ( ! [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax)
| ~ status(Ax,C,unp) )
& ( status(Ax,C,unp)
| ( ? [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[unp]) ).
fof(f_1_2,plain,
! [U_5,U_4] :
( ( ! [U_3] : ~ model(U_3,U_4)
| ? [U_2] : model(U_2,U_5)
| ~ status(U_5,U_4,unp) )
& ( status(U_5,U_4,unp)
| ( ? [U_1] : model(U_1,U_4)
& ! [U_0] : ~ model(U_0,U_5) ) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_9,U_7] :
( ! [U_3] : ~ model(U_3,U_7)
| ? [U_2] : model(U_2,U_9)
| ~ status(U_9,U_7,unp) )
& ! [U_8,U_6] :
( status(U_8,U_6,unp)
| ( ? [U_1] : model(U_1,U_6)
& ! [U_0] : ~ model(U_0,U_8) ) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_9,U_7] :
( ! [U_3] : ~ model(U_3,U_7)
| ? [U_2] : model(U_2,U_9)
| ~ status(U_9,U_7,unp) )
& ! [U_8,U_6] :
( status(U_8,U_6,unp)
| ( model(sK1(U_8,U_6),U_6)
& ! [U_0] : ~ model(U_0,U_8) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_1,sK1(U_8,U_6))],[f_1_3]) ).
fof(f_1_5,plain,
( ! [U_9,U_7] :
( ! [U_3] : ~ model(U_3,U_7)
| model(sK2(U_9,U_7),U_9)
| ~ status(U_9,U_7,unp) )
& ! [U_8,U_6] :
( status(U_8,U_6,unp)
| ( model(sK1(U_8,U_6),U_6)
& ! [U_0] : ~ model(U_0,U_8) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_2,sK2(U_9,U_7))],[f_1_4]) ).
fof(f_1_6,plain,
( ! [U_6,U_8,U_0] :
( model(sK1(U_8,U_6),U_6)
| ~ sP0(U_6,U_8,U_0) )
& ! [U_6,U_8,U_0] :
( ~ model(U_0,U_8)
| ~ sP0(U_6,U_8,U_0) )
& ! [U_7,U_9,U_3] :
( ~ model(U_3,U_7)
| model(sK2(U_9,U_7),U_9)
| ~ status(U_9,U_7,unp) )
& ! [U_6,U_8,U_0] :
( status(U_8,U_6,unp)
| sP0(U_6,U_8,U_0) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_1_5]) ).
cnf(f_1_7,plain,
( status(U_8,U_6,unp)
| sP0(U_6,U_8,U_0) ),
inference(clausify,[status(thm)],[f_1_6]) ).
cnf(f_1_8,plain,
( ~ model(U_3,U_7)
| model(sK2(U_9,U_7),U_9)
| ~ status(U_9,U_7,unp) ),
inference(clausify,[status(thm)],[f_1_6]) ).
cnf(f_1_9,plain,
( ~ model(U_0,U_8)
| ~ sP0(U_6,U_8,U_0) ),
inference(clausify,[status(thm)],[f_1_6]) ).
cnf(f_1_10,plain,
( model(sK1(U_8,U_6),U_6)
| ~ sP0(U_6,U_8,U_0) ),
inference(clausify,[status(thm)],[f_1_6]) ).
fof(f_2_1,plain,
! [Ax,C] :
( ( ? [I2] : model(I2,C)
| ! [I1] : ~ model(I1,Ax)
| ~ status(Ax,C,sap) )
& ( status(Ax,C,sap)
| ( ! [I2] : ~ model(I2,C)
& ? [I1] : model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[sap]) ).
fof(f_2_2,plain,
! [U_15,U_14] :
( ( ? [U_13] : model(U_13,U_14)
| ! [U_12] : ~ model(U_12,U_15)
| ~ status(U_15,U_14,sap) )
& ( status(U_15,U_14,sap)
| ( ! [U_11] : ~ model(U_11,U_14)
& ? [U_10] : model(U_10,U_15) ) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_19,U_17] :
( ? [U_13] : model(U_13,U_17)
| ! [U_12] : ~ model(U_12,U_19)
| ~ status(U_19,U_17,sap) )
& ! [U_18,U_16] :
( status(U_18,U_16,sap)
| ( ! [U_11] : ~ model(U_11,U_16)
& ? [U_10] : model(U_10,U_18) ) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
fof(f_2_4,plain,
( ! [U_19,U_17] :
( ? [U_13] : model(U_13,U_17)
| ! [U_12] : ~ model(U_12,U_19)
| ~ status(U_19,U_17,sap) )
& ! [U_18,U_16] :
( status(U_18,U_16,sap)
| ( ! [U_11] : ~ model(U_11,U_16)
& model(sK3(U_18,U_16),U_18) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_10,sK3(U_18,U_16))],[f_2_3]) ).
fof(f_2_5,plain,
( ! [U_19,U_17] :
( model(sK4(U_19,U_17),U_17)
| ! [U_12] : ~ model(U_12,U_19)
| ~ status(U_19,U_17,sap) )
& ! [U_18,U_16] :
( status(U_18,U_16,sap)
| ( ! [U_11] : ~ model(U_11,U_16)
& model(sK3(U_18,U_16),U_18) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_13,sK4(U_19,U_17))],[f_2_4]) ).
fof(f_2_6,plain,
( ! [U_11,U_18,U_16] :
( ~ model(U_11,U_16)
| ~ sP1(U_11,U_18,U_16) )
& ! [U_11,U_18,U_16] :
( model(sK3(U_18,U_16),U_18)
| ~ sP1(U_11,U_18,U_16) )
& ! [U_17,U_19,U_12] :
( model(sK4(U_19,U_17),U_17)
| ~ model(U_12,U_19)
| ~ status(U_19,U_17,sap) )
& ! [U_11,U_18,U_16] :
( status(U_18,U_16,sap)
| sP1(U_11,U_18,U_16) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1])],[f_2_5]) ).
cnf(f_2_7,plain,
( status(U_18,U_16,sap)
| sP1(U_11,U_18,U_16) ),
inference(clausify,[status(thm)],[f_2_6]) ).
cnf(f_2_8,plain,
( model(sK4(U_19,U_17),U_17)
| ~ model(U_12,U_19)
| ~ status(U_19,U_17,sap) ),
inference(clausify,[status(thm)],[f_2_6]) ).
cnf(f_2_9,plain,
( model(sK3(U_18,U_16),U_18)
| ~ sP1(U_11,U_18,U_16) ),
inference(clausify,[status(thm)],[f_2_6]) ).
cnf(f_2_10,plain,
( ~ model(U_11,U_16)
| ~ sP1(U_11,U_18,U_16) ),
inference(clausify,[status(thm)],[f_2_6]) ).
fof(f_3_1,plain,
! [Ax,C] :
( ( ( ( ? [I1] : model(I1,Ax)
| ! [I2] : ~ model(I2,C) )
& ( ? [I2] : model(I2,C)
| ! [I1] : ~ model(I1,Ax) ) )
| ~ status(Ax,C,esa) )
& ( status(Ax,C,esa)
| ( ! [I1] : ~ model(I1,Ax)
& ? [I2] : model(I2,C) )
| ( ! [I2] : ~ model(I2,C)
& ? [I1] : model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[esa]) ).
fof(f_3_2,plain,
! [U_29,U_28] :
( ( ( ( ? [U_27] : model(U_27,U_29)
| ! [U_26] : ~ model(U_26,U_28) )
& ( ? [U_25] : model(U_25,U_28)
| ! [U_24] : ~ model(U_24,U_29) ) )
| ~ status(U_29,U_28,esa) )
& ( status(U_29,U_28,esa)
| ( ! [U_23] : ~ model(U_23,U_29)
& ? [U_22] : model(U_22,U_28) )
| ( ! [U_21] : ~ model(U_21,U_28)
& ? [U_20] : model(U_20,U_29) ) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_33,U_31] :
( ( ( ? [U_27] : model(U_27,U_33)
| ! [U_26] : ~ model(U_26,U_31) )
& ( ? [U_25] : model(U_25,U_31)
| ! [U_24] : ~ model(U_24,U_33) ) )
| ~ status(U_33,U_31,esa) )
& ! [U_32,U_30] :
( status(U_32,U_30,esa)
| ( ! [U_23] : ~ model(U_23,U_32)
& ? [U_22] : model(U_22,U_30) )
| ( ! [U_21] : ~ model(U_21,U_30)
& ? [U_20] : model(U_20,U_32) ) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_33,U_31] :
( ( ( ? [U_27] : model(U_27,U_33)
| ! [U_26] : ~ model(U_26,U_31) )
& ( ? [U_25] : model(U_25,U_31)
| ! [U_24] : ~ model(U_24,U_33) ) )
| ~ status(U_33,U_31,esa) )
& ! [U_32,U_30] :
( status(U_32,U_30,esa)
| ( ! [U_23] : ~ model(U_23,U_32)
& ? [U_22] : model(U_22,U_30) )
| ( ! [U_21] : ~ model(U_21,U_30)
& model(sK5(U_32,U_30),U_32) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_20,sK5(U_32,U_30))],[f_3_3]) ).
fof(f_3_5,plain,
( ! [U_33,U_31] :
( ( ( ? [U_27] : model(U_27,U_33)
| ! [U_26] : ~ model(U_26,U_31) )
& ( ? [U_25] : model(U_25,U_31)
| ! [U_24] : ~ model(U_24,U_33) ) )
| ~ status(U_33,U_31,esa) )
& ! [U_32,U_30] :
( status(U_32,U_30,esa)
| ( ! [U_23] : ~ model(U_23,U_32)
& model(sK6(U_32,U_30),U_30) )
| ( ! [U_21] : ~ model(U_21,U_30)
& model(sK5(U_32,U_30),U_32) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_22,sK6(U_32,U_30))],[f_3_4]) ).
fof(f_3_6,plain,
( ! [U_33,U_31] :
( ( ( ? [U_27] : model(U_27,U_33)
| ! [U_26] : ~ model(U_26,U_31) )
& ( model(sK7(U_33,U_31),U_31)
| ! [U_24] : ~ model(U_24,U_33) ) )
| ~ status(U_33,U_31,esa) )
& ! [U_32,U_30] :
( status(U_32,U_30,esa)
| ( ! [U_23] : ~ model(U_23,U_32)
& model(sK6(U_32,U_30),U_30) )
| ( ! [U_21] : ~ model(U_21,U_30)
& model(sK5(U_32,U_30),U_32) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_25,sK7(U_33,U_31))],[f_3_5]) ).
fof(f_3_7,plain,
( ! [U_33,U_31] :
( ( ( model(sK8(U_33,U_31),U_33)
| ! [U_26] : ~ model(U_26,U_31) )
& ( model(sK7(U_33,U_31),U_31)
| ! [U_24] : ~ model(U_24,U_33) ) )
| ~ status(U_33,U_31,esa) )
& ! [U_32,U_30] :
( status(U_32,U_30,esa)
| ( ! [U_23] : ~ model(U_23,U_32)
& model(sK6(U_32,U_30),U_30) )
| ( ! [U_21] : ~ model(U_21,U_30)
& model(sK5(U_32,U_30),U_32) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_27,sK8(U_33,U_31))],[f_3_6]) ).
fof(f_3_8,plain,
( ! [U_24,U_26,U_33,U_31] :
( model(sK8(U_33,U_31),U_33)
| ~ model(U_26,U_31)
| ~ sP4(U_24,U_26,U_33,U_31) )
& ! [U_24,U_26,U_33,U_31] :
( model(sK7(U_33,U_31),U_31)
| ~ model(U_24,U_33)
| ~ sP4(U_24,U_26,U_33,U_31) )
& ! [U_32,U_30,U_23] :
( ~ model(U_23,U_32)
| ~ sP3(U_32,U_30,U_23) )
& ! [U_32,U_30,U_23] :
( model(sK6(U_32,U_30),U_30)
| ~ sP3(U_32,U_30,U_23) )
& ! [U_21,U_32,U_30] :
( ~ model(U_21,U_30)
| ~ sP2(U_21,U_32,U_30) )
& ! [U_21,U_32,U_30] :
( model(sK5(U_32,U_30),U_32)
| ~ sP2(U_21,U_32,U_30) )
& ! [U_24,U_26,U_33,U_31] :
( sP4(U_24,U_26,U_33,U_31)
| ~ status(U_33,U_31,esa) )
& ! [U_21,U_32,U_30,U_23] :
( status(U_32,U_30,esa)
| sP3(U_32,U_30,U_23)
| sP2(U_21,U_32,U_30) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP2,sP3,sP4])],[f_3_7]) ).
cnf(f_3_9,plain,
( status(U_32,U_30,esa)
| sP3(U_32,U_30,U_23)
| sP2(U_21,U_32,U_30) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_10,plain,
( sP4(U_24,U_26,U_33,U_31)
| ~ status(U_33,U_31,esa) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_11,plain,
( model(sK5(U_32,U_30),U_32)
| ~ sP2(U_21,U_32,U_30) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_12,plain,
( ~ model(U_21,U_30)
| ~ sP2(U_21,U_32,U_30) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_13,plain,
( model(sK6(U_32,U_30),U_30)
| ~ sP3(U_32,U_30,U_23) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_14,plain,
( ~ model(U_23,U_32)
| ~ sP3(U_32,U_30,U_23) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_15,plain,
( model(sK7(U_33,U_31),U_31)
| ~ model(U_24,U_33)
| ~ sP4(U_24,U_26,U_33,U_31) ),
inference(clausify,[status(thm)],[f_3_8]) ).
cnf(f_3_16,plain,
( model(sK8(U_33,U_31),U_33)
| ~ model(U_26,U_31)
| ~ sP4(U_24,U_26,U_33,U_31) ),
inference(clausify,[status(thm)],[f_3_8]) ).
fof(f_4_1,plain,
! [Ax,C] :
( ( ? [I1] :
( model(I1,C)
& model(I1,Ax) )
| ~ status(Ax,C,sat) )
& ( status(Ax,C,sat)
| ! [I1] :
( ~ model(I1,C)
| ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[sat]) ).
fof(f_4_2,plain,
! [U_37,U_36] :
( ( ? [U_35] :
( model(U_35,U_36)
& model(U_35,U_37) )
| ~ status(U_37,U_36,sat) )
& ( status(U_37,U_36,sat)
| ! [U_34] :
( ~ model(U_34,U_36)
| ~ model(U_34,U_37) ) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_41,U_39] :
( ? [U_35] :
( model(U_35,U_39)
& model(U_35,U_41) )
| ~ status(U_41,U_39,sat) )
& ! [U_40,U_38] :
( status(U_40,U_38,sat)
| ! [U_34] :
( ~ model(U_34,U_38)
| ~ model(U_34,U_40) ) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_41,U_39] :
( ( model(sK9(U_41,U_39),U_39)
& model(sK9(U_41,U_39),U_41) )
| ~ status(U_41,U_39,sat) )
& ! [U_40,U_38] :
( status(U_40,U_38,sat)
| ! [U_34] :
( ~ model(U_34,U_38)
| ~ model(U_34,U_40) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_35,sK9(U_41,U_39))],[f_4_3]) ).
fof(f_4_5,plain,
( ! [U_39,U_41] :
( model(sK9(U_41,U_39),U_39)
| ~ sP5(U_39,U_41) )
& ! [U_39,U_41] :
( model(sK9(U_41,U_39),U_41)
| ~ sP5(U_39,U_41) )
& ! [U_39,U_41] :
( sP5(U_39,U_41)
| ~ status(U_41,U_39,sat) )
& ! [U_40,U_34,U_38] :
( status(U_40,U_38,sat)
| ~ model(U_34,U_38)
| ~ model(U_34,U_40) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5])],[f_4_4]) ).
cnf(f_4_6,plain,
( status(U_40,U_38,sat)
| ~ model(U_34,U_38)
| ~ model(U_34,U_40) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_7,plain,
( sP5(U_39,U_41)
| ~ status(U_41,U_39,sat) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_8,plain,
( model(sK9(U_41,U_39),U_41)
| ~ sP5(U_39,U_41) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_9,plain,
( model(sK9(U_41,U_39),U_39)
| ~ sP5(U_39,U_41) ),
inference(clausify,[status(thm)],[f_4_5]) ).
fof(f_5_1,plain,
! [Ax,C] :
( ( ! [I1] :
( model(I1,C)
| ~ model(I1,Ax) )
| ~ status(Ax,C,thm) )
& ( status(Ax,C,thm)
| ? [I1] :
( ~ model(I1,C)
& model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[thm]) ).
fof(f_5_2,plain,
! [U_45,U_44] :
( ( ! [U_43] :
( model(U_43,U_44)
| ~ model(U_43,U_45) )
| ~ status(U_45,U_44,thm) )
& ( status(U_45,U_44,thm)
| ? [U_42] :
( ~ model(U_42,U_44)
& model(U_42,U_45) ) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_49,U_47] :
( ! [U_43] :
( model(U_43,U_47)
| ~ model(U_43,U_49) )
| ~ status(U_49,U_47,thm) )
& ! [U_48,U_46] :
( status(U_48,U_46,thm)
| ? [U_42] :
( ~ model(U_42,U_46)
& model(U_42,U_48) ) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_49,U_47] :
( ! [U_43] :
( model(U_43,U_47)
| ~ model(U_43,U_49) )
| ~ status(U_49,U_47,thm) )
& ! [U_48,U_46] :
( status(U_48,U_46,thm)
| ( ~ model(sK10(U_48,U_46),U_46)
& model(sK10(U_48,U_46),U_48) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_42,sK10(U_48,U_46))],[f_5_3]) ).
fof(f_5_5,plain,
( ! [U_48,U_46] :
( ~ model(sK10(U_48,U_46),U_46)
| ~ sP6(U_48,U_46) )
& ! [U_48,U_46] :
( model(sK10(U_48,U_46),U_48)
| ~ sP6(U_48,U_46) )
& ! [U_49,U_47,U_43] :
( model(U_43,U_47)
| ~ model(U_43,U_49)
| ~ status(U_49,U_47,thm) )
& ! [U_48,U_46] :
( status(U_48,U_46,thm)
| sP6(U_48,U_46) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP6])],[f_5_4]) ).
cnf(f_5_6,plain,
( status(U_48,U_46,thm)
| sP6(U_48,U_46) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_7,plain,
( model(U_43,U_47)
| ~ model(U_43,U_49)
| ~ status(U_49,U_47,thm) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_8,plain,
( model(sK10(U_48,U_46),U_48)
| ~ sP6(U_48,U_46) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_9,plain,
( ~ model(sK10(U_48,U_46),U_46)
| ~ sP6(U_48,U_46) ),
inference(clausify,[status(thm)],[f_5_5]) ).
fof(f_6_1,plain,
! [Ax,C] :
( ( ( ! [I2] :
( ( model(I2,Ax)
| ~ model(I2,C) )
& ( model(I2,C)
| ~ model(I2,Ax) ) )
& ? [I1] : model(I1,Ax) )
| ~ status(Ax,C,eqv) )
& ( status(Ax,C,eqv)
| ? [I2] :
( ( ~ model(I2,Ax)
& model(I2,C) )
| ( ~ model(I2,C)
& model(I2,Ax) ) )
| ! [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[eqv]) ).
fof(f_6_2,plain,
! [U_55,U_54] :
( ( ( ! [U_53] :
( ( model(U_53,U_55)
| ~ model(U_53,U_54) )
& ( model(U_53,U_54)
| ~ model(U_53,U_55) ) )
& ? [U_52] : model(U_52,U_55) )
| ~ status(U_55,U_54,eqv) )
& ( status(U_55,U_54,eqv)
| ? [U_51] :
( ( ~ model(U_51,U_55)
& model(U_51,U_54) )
| ( ~ model(U_51,U_54)
& model(U_51,U_55) ) )
| ! [U_50] : ~ model(U_50,U_55) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_63,U_61] :
( ( ! [U_59] :
( model(U_59,U_63)
| ~ model(U_59,U_61) )
& ! [U_58] :
( model(U_58,U_61)
| ~ model(U_58,U_63) )
& ? [U_52] : model(U_52,U_63) )
| ~ status(U_63,U_61,eqv) )
& ! [U_62,U_60] :
( status(U_62,U_60,eqv)
| ? [U_57] :
( ~ model(U_57,U_62)
& model(U_57,U_60) )
| ? [U_56] :
( ~ model(U_56,U_60)
& model(U_56,U_62) )
| ! [U_50] : ~ model(U_50,U_62) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_63,U_61] :
( ( ! [U_59] :
( model(U_59,U_63)
| ~ model(U_59,U_61) )
& ! [U_58] :
( model(U_58,U_61)
| ~ model(U_58,U_63) )
& ? [U_52] : model(U_52,U_63) )
| ~ status(U_63,U_61,eqv) )
& ! [U_62,U_60] :
( status(U_62,U_60,eqv)
| ? [U_57] :
( ~ model(U_57,U_62)
& model(U_57,U_60) )
| ( ~ model(sK11(U_62,U_60),U_60)
& model(sK11(U_62,U_60),U_62) )
| ! [U_50] : ~ model(U_50,U_62) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_56,sK11(U_62,U_60))],[f_6_3]) ).
fof(f_6_5,plain,
( ! [U_63,U_61] :
( ( ! [U_59] :
( model(U_59,U_63)
| ~ model(U_59,U_61) )
& ! [U_58] :
( model(U_58,U_61)
| ~ model(U_58,U_63) )
& ? [U_52] : model(U_52,U_63) )
| ~ status(U_63,U_61,eqv) )
& ! [U_62,U_60] :
( status(U_62,U_60,eqv)
| ( ~ model(sK12(U_62,U_60),U_62)
& model(sK12(U_62,U_60),U_60) )
| ( ~ model(sK11(U_62,U_60),U_60)
& model(sK11(U_62,U_60),U_62) )
| ! [U_50] : ~ model(U_50,U_62) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_57,sK12(U_62,U_60))],[f_6_4]) ).
fof(f_6_6,plain,
( ! [U_63,U_61] :
( ( ! [U_59] :
( model(U_59,U_63)
| ~ model(U_59,U_61) )
& ! [U_58] :
( model(U_58,U_61)
| ~ model(U_58,U_63) )
& model(sK13(U_63,U_61),U_63) )
| ~ status(U_63,U_61,eqv) )
& ! [U_62,U_60] :
( status(U_62,U_60,eqv)
| ( ~ model(sK12(U_62,U_60),U_62)
& model(sK12(U_62,U_60),U_60) )
| ( ~ model(sK11(U_62,U_60),U_60)
& model(sK11(U_62,U_60),U_62) )
| ! [U_50] : ~ model(U_50,U_62) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_52,sK13(U_63,U_61))],[f_6_5]) ).
fof(f_6_7,plain,
( ! [U_58,U_61,U_63,U_59] :
( model(U_59,U_63)
| ~ model(U_59,U_61)
| ~ sP9(U_58,U_61,U_63,U_59) )
& ! [U_58,U_61,U_63,U_59] :
( model(U_58,U_61)
| ~ model(U_58,U_63)
| ~ sP9(U_58,U_61,U_63,U_59) )
& ! [U_58,U_61,U_63,U_59] :
( model(sK13(U_63,U_61),U_63)
| ~ sP9(U_58,U_61,U_63,U_59) )
& ! [U_62,U_60] :
( ~ model(sK12(U_62,U_60),U_62)
| ~ sP8(U_62,U_60) )
& ! [U_62,U_60] :
( model(sK12(U_62,U_60),U_60)
| ~ sP8(U_62,U_60) )
& ! [U_62,U_60] :
( ~ model(sK11(U_62,U_60),U_60)
| ~ sP7(U_62,U_60) )
& ! [U_62,U_60] :
( model(sK11(U_62,U_60),U_62)
| ~ sP7(U_62,U_60) )
& ! [U_58,U_61,U_63,U_59] :
( sP9(U_58,U_61,U_63,U_59)
| ~ status(U_63,U_61,eqv) )
& ! [U_50,U_62,U_60] :
( status(U_62,U_60,eqv)
| sP8(U_62,U_60)
| sP7(U_62,U_60)
| ~ model(U_50,U_62) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP7,sP8,sP9])],[f_6_6]) ).
cnf(f_6_8,plain,
( status(U_62,U_60,eqv)
| sP8(U_62,U_60)
| sP7(U_62,U_60)
| ~ model(U_50,U_62) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_9,plain,
( sP9(U_58,U_61,U_63,U_59)
| ~ status(U_63,U_61,eqv) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_10,plain,
( model(sK11(U_62,U_60),U_62)
| ~ sP7(U_62,U_60) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_11,plain,
( ~ model(sK11(U_62,U_60),U_60)
| ~ sP7(U_62,U_60) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_12,plain,
( model(sK12(U_62,U_60),U_60)
| ~ sP8(U_62,U_60) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_13,plain,
( ~ model(sK12(U_62,U_60),U_62)
| ~ sP8(U_62,U_60) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_14,plain,
( model(sK13(U_63,U_61),U_63)
| ~ sP9(U_58,U_61,U_63,U_59) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_15,plain,
( model(U_58,U_61)
| ~ model(U_58,U_63)
| ~ sP9(U_58,U_61,U_63,U_59) ),
inference(clausify,[status(thm)],[f_6_7]) ).
cnf(f_6_16,plain,
( model(U_59,U_63)
| ~ model(U_59,U_61)
| ~ sP9(U_58,U_61,U_63,U_59) ),
inference(clausify,[status(thm)],[f_6_7]) ).
fof(f_7_1,plain,
! [Ax,C] :
( ( ( ! [I2] : model(I2,C)
& ? [I1] : model(I1,Ax) )
| ~ status(Ax,C,tac) )
& ( status(Ax,C,tac)
| ? [I2] : ~ model(I2,C)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[tac]) ).
fof(f_7_2,plain,
! [U_69,U_68] :
( ( ( ! [U_67] : model(U_67,U_68)
& ? [U_66] : model(U_66,U_69) )
| ~ status(U_69,U_68,tac) )
& ( status(U_69,U_68,tac)
| ? [U_65] : ~ model(U_65,U_68)
| ! [U_64] : ~ model(U_64,U_69) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_73,U_71] :
( ( ! [U_67] : model(U_67,U_71)
& ? [U_66] : model(U_66,U_73) )
| ~ status(U_73,U_71,tac) )
& ! [U_72,U_70] :
( status(U_72,U_70,tac)
| ? [U_65] : ~ model(U_65,U_70)
| ! [U_64] : ~ model(U_64,U_72) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_73,U_71] :
( ( ! [U_67] : model(U_67,U_71)
& ? [U_66] : model(U_66,U_73) )
| ~ status(U_73,U_71,tac) )
& ! [U_72,U_70] :
( status(U_72,U_70,tac)
| ~ model(sK14(U_72,U_70),U_70)
| ! [U_64] : ~ model(U_64,U_72) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_65,sK14(U_72,U_70))],[f_7_3]) ).
fof(f_7_5,plain,
( ! [U_73,U_71] :
( ( ! [U_67] : model(U_67,U_71)
& model(sK15(U_73,U_71),U_73) )
| ~ status(U_73,U_71,tac) )
& ! [U_72,U_70] :
( status(U_72,U_70,tac)
| ~ model(sK14(U_72,U_70),U_70)
| ! [U_64] : ~ model(U_64,U_72) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_66,sK15(U_73,U_71))],[f_7_4]) ).
fof(f_7_6,plain,
( ! [U_67,U_73,U_71] :
( model(U_67,U_71)
| ~ sP10(U_67,U_73,U_71) )
& ! [U_67,U_73,U_71] :
( model(sK15(U_73,U_71),U_73)
| ~ sP10(U_67,U_73,U_71) )
& ! [U_67,U_73,U_71] :
( sP10(U_67,U_73,U_71)
| ~ status(U_73,U_71,tac) )
& ! [U_64,U_72,U_70] :
( status(U_72,U_70,tac)
| ~ model(sK14(U_72,U_70),U_70)
| ~ model(U_64,U_72) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP10])],[f_7_5]) ).
cnf(f_7_7,plain,
( status(U_72,U_70,tac)
| ~ model(sK14(U_72,U_70),U_70)
| ~ model(U_64,U_72) ),
inference(clausify,[status(thm)],[f_7_6]) ).
cnf(f_7_8,plain,
( sP10(U_67,U_73,U_71)
| ~ status(U_73,U_71,tac) ),
inference(clausify,[status(thm)],[f_7_6]) ).
cnf(f_7_9,plain,
( model(sK15(U_73,U_71),U_73)
| ~ sP10(U_67,U_73,U_71) ),
inference(clausify,[status(thm)],[f_7_6]) ).
cnf(f_7_10,plain,
( model(U_67,U_71)
| ~ sP10(U_67,U_73,U_71) ),
inference(clausify,[status(thm)],[f_7_6]) ).
fof(f_8_1,plain,
! [Ax,C] :
( ( ( ? [I3] :
( ~ model(I3,Ax)
& model(I3,C) )
& ! [I2] :
( model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] : model(I1,Ax) )
| ~ status(Ax,C,wec) )
& ( status(Ax,C,wec)
| ! [I3] :
( model(I3,Ax)
| ~ model(I3,C) )
| ? [I2] :
( ~ model(I2,C)
& model(I2,Ax) )
| ! [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[wec]) ).
fof(f_8_2,plain,
! [U_81,U_80] :
( ( ( ? [U_79] :
( ~ model(U_79,U_81)
& model(U_79,U_80) )
& ! [U_78] :
( model(U_78,U_80)
| ~ model(U_78,U_81) )
& ? [U_77] : model(U_77,U_81) )
| ~ status(U_81,U_80,wec) )
& ( status(U_81,U_80,wec)
| ! [U_76] :
( model(U_76,U_81)
| ~ model(U_76,U_80) )
| ? [U_75] :
( ~ model(U_75,U_80)
& model(U_75,U_81) )
| ! [U_74] : ~ model(U_74,U_81) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_85,U_83] :
( ( ? [U_79] :
( ~ model(U_79,U_85)
& model(U_79,U_83) )
& ! [U_78] :
( model(U_78,U_83)
| ~ model(U_78,U_85) )
& ? [U_77] : model(U_77,U_85) )
| ~ status(U_85,U_83,wec) )
& ! [U_84,U_82] :
( status(U_84,U_82,wec)
| ! [U_76] :
( model(U_76,U_84)
| ~ model(U_76,U_82) )
| ? [U_75] :
( ~ model(U_75,U_82)
& model(U_75,U_84) )
| ! [U_74] : ~ model(U_74,U_84) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
( ! [U_85,U_83] :
( ( ? [U_79] :
( ~ model(U_79,U_85)
& model(U_79,U_83) )
& ! [U_78] :
( model(U_78,U_83)
| ~ model(U_78,U_85) )
& ? [U_77] : model(U_77,U_85) )
| ~ status(U_85,U_83,wec) )
& ! [U_84,U_82] :
( status(U_84,U_82,wec)
| ! [U_76] :
( model(U_76,U_84)
| ~ model(U_76,U_82) )
| ( ~ model(sK16(U_84,U_82),U_82)
& model(sK16(U_84,U_82),U_84) )
| ! [U_74] : ~ model(U_74,U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_75,sK16(U_84,U_82))],[f_8_3]) ).
fof(f_8_5,plain,
( ! [U_85,U_83] :
( ( ? [U_79] :
( ~ model(U_79,U_85)
& model(U_79,U_83) )
& ! [U_78] :
( model(U_78,U_83)
| ~ model(U_78,U_85) )
& model(sK17(U_85,U_83),U_85) )
| ~ status(U_85,U_83,wec) )
& ! [U_84,U_82] :
( status(U_84,U_82,wec)
| ! [U_76] :
( model(U_76,U_84)
| ~ model(U_76,U_82) )
| ( ~ model(sK16(U_84,U_82),U_82)
& model(sK16(U_84,U_82),U_84) )
| ! [U_74] : ~ model(U_74,U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_77,sK17(U_85,U_83))],[f_8_4]) ).
fof(f_8_6,plain,
( ! [U_85,U_83] :
( ( ~ model(sK18(U_85,U_83),U_85)
& model(sK18(U_85,U_83),U_83)
& ! [U_78] :
( model(U_78,U_83)
| ~ model(U_78,U_85) )
& model(sK17(U_85,U_83),U_85) )
| ~ status(U_85,U_83,wec) )
& ! [U_84,U_82] :
( status(U_84,U_82,wec)
| ! [U_76] :
( model(U_76,U_84)
| ~ model(U_76,U_82) )
| ( ~ model(sK16(U_84,U_82),U_82)
& model(sK16(U_84,U_82),U_84) )
| ! [U_74] : ~ model(U_74,U_84) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_79,sK18(U_85,U_83))],[f_8_5]) ).
fof(f_8_7,plain,
( ! [U_83,U_78,U_85] :
( ~ model(sK18(U_85,U_83),U_85)
| ~ sP12(U_83,U_78,U_85) )
& ! [U_83,U_78,U_85] :
( model(sK18(U_85,U_83),U_83)
| ~ sP12(U_83,U_78,U_85) )
& ! [U_83,U_78,U_85] :
( model(U_78,U_83)
| ~ model(U_78,U_85)
| ~ sP12(U_83,U_78,U_85) )
& ! [U_83,U_78,U_85] :
( model(sK17(U_85,U_83),U_85)
| ~ sP12(U_83,U_78,U_85) )
& ! [U_84,U_82] :
( ~ model(sK16(U_84,U_82),U_82)
| ~ sP11(U_84,U_82) )
& ! [U_84,U_82] :
( model(sK16(U_84,U_82),U_84)
| ~ sP11(U_84,U_82) )
& ! [U_83,U_78,U_85] :
( sP12(U_83,U_78,U_85)
| ~ status(U_85,U_83,wec) )
& ! [U_84,U_82,U_76,U_74] :
( status(U_84,U_82,wec)
| model(U_76,U_84)
| ~ model(U_76,U_82)
| sP11(U_84,U_82)
| ~ model(U_74,U_84) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP11,sP12])],[f_8_6]) ).
cnf(f_8_8,plain,
( status(U_84,U_82,wec)
| model(U_76,U_84)
| ~ model(U_76,U_82)
| sP11(U_84,U_82)
| ~ model(U_74,U_84) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_9,plain,
( sP12(U_83,U_78,U_85)
| ~ status(U_85,U_83,wec) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_10,plain,
( model(sK16(U_84,U_82),U_84)
| ~ sP11(U_84,U_82) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_11,plain,
( ~ model(sK16(U_84,U_82),U_82)
| ~ sP11(U_84,U_82) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_12,plain,
( model(sK17(U_85,U_83),U_85)
| ~ sP12(U_83,U_78,U_85) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_13,plain,
( model(U_78,U_83)
| ~ model(U_78,U_85)
| ~ sP12(U_83,U_78,U_85) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_14,plain,
( model(sK18(U_85,U_83),U_83)
| ~ sP12(U_83,U_78,U_85) ),
inference(clausify,[status(thm)],[f_8_7]) ).
cnf(f_8_15,plain,
( ~ model(sK18(U_85,U_83),U_85)
| ~ sP12(U_83,U_78,U_85) ),
inference(clausify,[status(thm)],[f_8_7]) ).
fof(f_9_1,plain,
! [Ax,C] :
( ( ( ! [I3] :
( ( model(I3,Ax)
| ~ model(I3,C) )
& ( model(I3,C)
| ~ model(I3,Ax) ) )
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
| ~ status(Ax,C,eth) )
& ( status(Ax,C,eth)
| ? [I3] :
( ( ~ model(I3,Ax)
& model(I3,C) )
| ( ~ model(I3,C)
& model(I3,Ax) ) )
| ! [I2] : model(I2,Ax)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[eth]) ).
fof(f_9_2,plain,
! [U_93,U_92] :
( ( ( ! [U_91] :
( ( model(U_91,U_93)
| ~ model(U_91,U_92) )
& ( model(U_91,U_92)
| ~ model(U_91,U_93) ) )
& ? [U_90] : ~ model(U_90,U_93)
& ? [U_89] : model(U_89,U_93) )
| ~ status(U_93,U_92,eth) )
& ( status(U_93,U_92,eth)
| ? [U_88] :
( ( ~ model(U_88,U_93)
& model(U_88,U_92) )
| ( ~ model(U_88,U_92)
& model(U_88,U_93) ) )
| ! [U_87] : model(U_87,U_93)
| ! [U_86] : ~ model(U_86,U_93) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_101,U_99] :
( ( ! [U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99) )
& ! [U_96] :
( model(U_96,U_99)
| ~ model(U_96,U_101) )
& ? [U_90] : ~ model(U_90,U_101)
& ? [U_89] : model(U_89,U_101) )
| ~ status(U_101,U_99,eth) )
& ! [U_100,U_98] :
( status(U_100,U_98,eth)
| ? [U_95] :
( ~ model(U_95,U_100)
& model(U_95,U_98) )
| ? [U_94] :
( ~ model(U_94,U_98)
& model(U_94,U_100) )
| ! [U_87] : model(U_87,U_100)
| ! [U_86] : ~ model(U_86,U_100) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
( ! [U_101,U_99] :
( ( ! [U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99) )
& ! [U_96] :
( model(U_96,U_99)
| ~ model(U_96,U_101) )
& ? [U_90] : ~ model(U_90,U_101)
& ? [U_89] : model(U_89,U_101) )
| ~ status(U_101,U_99,eth) )
& ! [U_100,U_98] :
( status(U_100,U_98,eth)
| ? [U_95] :
( ~ model(U_95,U_100)
& model(U_95,U_98) )
| ( ~ model(sK19(U_100,U_98),U_98)
& model(sK19(U_100,U_98),U_100) )
| ! [U_87] : model(U_87,U_100)
| ! [U_86] : ~ model(U_86,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_94,sK19(U_100,U_98))],[f_9_3]) ).
fof(f_9_5,plain,
( ! [U_101,U_99] :
( ( ! [U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99) )
& ! [U_96] :
( model(U_96,U_99)
| ~ model(U_96,U_101) )
& ? [U_90] : ~ model(U_90,U_101)
& ? [U_89] : model(U_89,U_101) )
| ~ status(U_101,U_99,eth) )
& ! [U_100,U_98] :
( status(U_100,U_98,eth)
| ( ~ model(sK20(U_100,U_98),U_100)
& model(sK20(U_100,U_98),U_98) )
| ( ~ model(sK19(U_100,U_98),U_98)
& model(sK19(U_100,U_98),U_100) )
| ! [U_87] : model(U_87,U_100)
| ! [U_86] : ~ model(U_86,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_95,sK20(U_100,U_98))],[f_9_4]) ).
fof(f_9_6,plain,
( ! [U_101,U_99] :
( ( ! [U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99) )
& ! [U_96] :
( model(U_96,U_99)
| ~ model(U_96,U_101) )
& ? [U_90] : ~ model(U_90,U_101)
& model(sK21(U_101,U_99),U_101) )
| ~ status(U_101,U_99,eth) )
& ! [U_100,U_98] :
( status(U_100,U_98,eth)
| ( ~ model(sK20(U_100,U_98),U_100)
& model(sK20(U_100,U_98),U_98) )
| ( ~ model(sK19(U_100,U_98),U_98)
& model(sK19(U_100,U_98),U_100) )
| ! [U_87] : model(U_87,U_100)
| ! [U_86] : ~ model(U_86,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_89,sK21(U_101,U_99))],[f_9_5]) ).
fof(f_9_7,plain,
( ! [U_101,U_99] :
( ( ! [U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99) )
& ! [U_96] :
( model(U_96,U_99)
| ~ model(U_96,U_101) )
& ~ model(sK22(U_101,U_99),U_101)
& model(sK21(U_101,U_99),U_101) )
| ~ status(U_101,U_99,eth) )
& ! [U_100,U_98] :
( status(U_100,U_98,eth)
| ( ~ model(sK20(U_100,U_98),U_100)
& model(sK20(U_100,U_98),U_98) )
| ( ~ model(sK19(U_100,U_98),U_98)
& model(sK19(U_100,U_98),U_100) )
| ! [U_87] : model(U_87,U_100)
| ! [U_86] : ~ model(U_86,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_90,sK22(U_101,U_99))],[f_9_6]) ).
fof(f_9_8,plain,
( ! [U_99,U_96,U_101,U_97] :
( model(U_97,U_101)
| ~ model(U_97,U_99)
| ~ sP15(U_99,U_96,U_101,U_97) )
& ! [U_99,U_96,U_101,U_97] :
( model(U_96,U_99)
| ~ model(U_96,U_101)
| ~ sP15(U_99,U_96,U_101,U_97) )
& ! [U_99,U_96,U_101,U_97] :
( ~ model(sK22(U_101,U_99),U_101)
| ~ sP15(U_99,U_96,U_101,U_97) )
& ! [U_99,U_96,U_101,U_97] :
( model(sK21(U_101,U_99),U_101)
| ~ sP15(U_99,U_96,U_101,U_97) )
& ! [U_100,U_98] :
( ~ model(sK20(U_100,U_98),U_100)
| ~ sP14(U_100,U_98) )
& ! [U_100,U_98] :
( model(sK20(U_100,U_98),U_98)
| ~ sP14(U_100,U_98) )
& ! [U_100,U_98] :
( ~ model(sK19(U_100,U_98),U_98)
| ~ sP13(U_100,U_98) )
& ! [U_100,U_98] :
( model(sK19(U_100,U_98),U_100)
| ~ sP13(U_100,U_98) )
& ! [U_99,U_96,U_101,U_97] :
( sP15(U_99,U_96,U_101,U_97)
| ~ status(U_101,U_99,eth) )
& ! [U_87,U_100,U_86,U_98] :
( status(U_100,U_98,eth)
| sP14(U_100,U_98)
| sP13(U_100,U_98)
| model(U_87,U_100)
| ~ model(U_86,U_100) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP13,sP14,sP15])],[f_9_7]) ).
cnf(f_9_9,plain,
( status(U_100,U_98,eth)
| sP14(U_100,U_98)
| sP13(U_100,U_98)
| model(U_87,U_100)
| ~ model(U_86,U_100) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_10,plain,
( sP15(U_99,U_96,U_101,U_97)
| ~ status(U_101,U_99,eth) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_11,plain,
( model(sK19(U_100,U_98),U_100)
| ~ sP13(U_100,U_98) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_12,plain,
( ~ model(sK19(U_100,U_98),U_98)
| ~ sP13(U_100,U_98) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_13,plain,
( model(sK20(U_100,U_98),U_98)
| ~ sP14(U_100,U_98) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_14,plain,
( ~ model(sK20(U_100,U_98),U_100)
| ~ sP14(U_100,U_98) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_15,plain,
( model(sK21(U_101,U_99),U_101)
| ~ sP15(U_99,U_96,U_101,U_97) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_16,plain,
( ~ model(sK22(U_101,U_99),U_101)
| ~ sP15(U_99,U_96,U_101,U_97) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_17,plain,
( model(U_96,U_99)
| ~ model(U_96,U_101)
| ~ sP15(U_99,U_96,U_101,U_97) ),
inference(clausify,[status(thm)],[f_9_8]) ).
cnf(f_9_18,plain,
( model(U_97,U_101)
| ~ model(U_97,U_99)
| ~ sP15(U_99,U_96,U_101,U_97) ),
inference(clausify,[status(thm)],[f_9_8]) ).
fof(f_10_1,plain,
! [Ax,C] :
( ( ! [I1] :
( model(I1,C)
& model(I1,Ax) )
| ~ status(Ax,C,tau) )
& ( status(Ax,C,tau)
| ? [I1] :
( ~ model(I1,C)
| ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[tau]) ).
fof(f_10_2,plain,
! [U_105,U_104] :
( ( ! [U_103] :
( model(U_103,U_104)
& model(U_103,U_105) )
| ~ status(U_105,U_104,tau) )
& ( status(U_105,U_104,tau)
| ? [U_102] :
( ~ model(U_102,U_104)
| ~ model(U_102,U_105) ) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_113,U_111] :
( ( ! [U_109] : model(U_109,U_111)
& ! [U_108] : model(U_108,U_113) )
| ~ status(U_113,U_111,tau) )
& ! [U_112,U_110] :
( status(U_112,U_110,tau)
| ? [U_107] : ~ model(U_107,U_110)
| ? [U_106] : ~ model(U_106,U_112) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
( ! [U_113,U_111] :
( ( ! [U_109] : model(U_109,U_111)
& ! [U_108] : model(U_108,U_113) )
| ~ status(U_113,U_111,tau) )
& ! [U_112,U_110] :
( status(U_112,U_110,tau)
| ? [U_107] : ~ model(U_107,U_110)
| ~ model(sK23(U_112,U_110),U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_106,sK23(U_112,U_110))],[f_10_3]) ).
fof(f_10_5,plain,
( ! [U_113,U_111] :
( ( ! [U_109] : model(U_109,U_111)
& ! [U_108] : model(U_108,U_113) )
| ~ status(U_113,U_111,tau) )
& ! [U_112,U_110] :
( status(U_112,U_110,tau)
| ~ model(sK24(U_112,U_110),U_110)
| ~ model(sK23(U_112,U_110),U_112) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_107,sK24(U_112,U_110))],[f_10_4]) ).
fof(f_10_6,plain,
( ! [U_108,U_109,U_113,U_111] :
( model(U_109,U_111)
| ~ sP16(U_108,U_109,U_113,U_111) )
& ! [U_108,U_109,U_113,U_111] :
( model(U_108,U_113)
| ~ sP16(U_108,U_109,U_113,U_111) )
& ! [U_108,U_109,U_113,U_111] :
( sP16(U_108,U_109,U_113,U_111)
| ~ status(U_113,U_111,tau) )
& ! [U_110,U_112] :
( status(U_112,U_110,tau)
| ~ model(sK24(U_112,U_110),U_110)
| ~ model(sK23(U_112,U_110),U_112) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP16])],[f_10_5]) ).
cnf(f_10_7,plain,
( status(U_112,U_110,tau)
| ~ model(sK24(U_112,U_110),U_110)
| ~ model(sK23(U_112,U_110),U_112) ),
inference(clausify,[status(thm)],[f_10_6]) ).
cnf(f_10_8,plain,
( sP16(U_108,U_109,U_113,U_111)
| ~ status(U_113,U_111,tau) ),
inference(clausify,[status(thm)],[f_10_6]) ).
cnf(f_10_9,plain,
( model(U_108,U_113)
| ~ sP16(U_108,U_109,U_113,U_111) ),
inference(clausify,[status(thm)],[f_10_6]) ).
cnf(f_10_10,plain,
( model(U_109,U_111)
| ~ sP16(U_108,U_109,U_113,U_111) ),
inference(clausify,[status(thm)],[f_10_6]) ).
fof(f_11_1,plain,
! [Ax,C] :
( ( ( ! [I3] : model(I3,C)
& ? [I2] : ~ model(I2,Ax)
& ? [I1] : model(I1,Ax) )
| ~ status(Ax,C,wtc) )
& ( status(Ax,C,wtc)
| ? [I3] : ~ model(I3,C)
| ! [I2] : model(I2,Ax)
| ! [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[wtc]) ).
fof(f_11_2,plain,
! [U_121,U_120] :
( ( ( ! [U_119] : model(U_119,U_120)
& ? [U_118] : ~ model(U_118,U_121)
& ? [U_117] : model(U_117,U_121) )
| ~ status(U_121,U_120,wtc) )
& ( status(U_121,U_120,wtc)
| ? [U_116] : ~ model(U_116,U_120)
| ! [U_115] : model(U_115,U_121)
| ! [U_114] : ~ model(U_114,U_121) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_125,U_123] :
( ( ! [U_119] : model(U_119,U_123)
& ? [U_118] : ~ model(U_118,U_125)
& ? [U_117] : model(U_117,U_125) )
| ~ status(U_125,U_123,wtc) )
& ! [U_124,U_122] :
( status(U_124,U_122,wtc)
| ? [U_116] : ~ model(U_116,U_122)
| ! [U_115] : model(U_115,U_124)
| ! [U_114] : ~ model(U_114,U_124) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_125,U_123] :
( ( ! [U_119] : model(U_119,U_123)
& ? [U_118] : ~ model(U_118,U_125)
& ? [U_117] : model(U_117,U_125) )
| ~ status(U_125,U_123,wtc) )
& ! [U_124,U_122] :
( status(U_124,U_122,wtc)
| ~ model(sK25(U_124,U_122),U_122)
| ! [U_115] : model(U_115,U_124)
| ! [U_114] : ~ model(U_114,U_124) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_116,sK25(U_124,U_122))],[f_11_3]) ).
fof(f_11_5,plain,
( ! [U_125,U_123] :
( ( ! [U_119] : model(U_119,U_123)
& ? [U_118] : ~ model(U_118,U_125)
& model(sK26(U_125,U_123),U_125) )
| ~ status(U_125,U_123,wtc) )
& ! [U_124,U_122] :
( status(U_124,U_122,wtc)
| ~ model(sK25(U_124,U_122),U_122)
| ! [U_115] : model(U_115,U_124)
| ! [U_114] : ~ model(U_114,U_124) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26]),skolemize(U_117,sK26(U_125,U_123))],[f_11_4]) ).
fof(f_11_6,plain,
( ! [U_125,U_123] :
( ( ! [U_119] : model(U_119,U_123)
& ~ model(sK27(U_125,U_123),U_125)
& model(sK26(U_125,U_123),U_125) )
| ~ status(U_125,U_123,wtc) )
& ! [U_124,U_122] :
( status(U_124,U_122,wtc)
| ~ model(sK25(U_124,U_122),U_122)
| ! [U_115] : model(U_115,U_124)
| ! [U_114] : ~ model(U_114,U_124) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27]),skolemize(U_118,sK27(U_125,U_123))],[f_11_5]) ).
fof(f_11_7,plain,
( ! [U_119,U_123,U_125] :
( model(U_119,U_123)
| ~ sP17(U_119,U_123,U_125) )
& ! [U_119,U_123,U_125] :
( ~ model(sK27(U_125,U_123),U_125)
| ~ sP17(U_119,U_123,U_125) )
& ! [U_119,U_123,U_125] :
( model(sK26(U_125,U_123),U_125)
| ~ sP17(U_119,U_123,U_125) )
& ! [U_119,U_123,U_125] :
( sP17(U_119,U_123,U_125)
| ~ status(U_125,U_123,wtc) )
& ! [U_122,U_115,U_114,U_124] :
( status(U_124,U_122,wtc)
| ~ model(sK25(U_124,U_122),U_122)
| model(U_115,U_124)
| ~ model(U_114,U_124) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP17])],[f_11_6]) ).
cnf(f_11_8,plain,
( status(U_124,U_122,wtc)
| ~ model(sK25(U_124,U_122),U_122)
| model(U_115,U_124)
| ~ model(U_114,U_124) ),
inference(clausify,[status(thm)],[f_11_7]) ).
cnf(f_11_9,plain,
( sP17(U_119,U_123,U_125)
| ~ status(U_125,U_123,wtc) ),
inference(clausify,[status(thm)],[f_11_7]) ).
cnf(f_11_10,plain,
( model(sK26(U_125,U_123),U_125)
| ~ sP17(U_119,U_123,U_125) ),
inference(clausify,[status(thm)],[f_11_7]) ).
cnf(f_11_11,plain,
( ~ model(sK27(U_125,U_123),U_125)
| ~ sP17(U_119,U_123,U_125) ),
inference(clausify,[status(thm)],[f_11_7]) ).
cnf(f_11_12,plain,
( model(U_119,U_123)
| ~ sP17(U_119,U_123,U_125) ),
inference(clausify,[status(thm)],[f_11_7]) ).
fof(f_12_1,plain,
! [Ax,C] :
( ( ( ? [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) )
& ( 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(fof_nnf,[status(thm)],[wth]) ).
fof(f_12_2,plain,
! [U_135,U_134] :
( ( ( ? [U_133] : ~ model(U_133,U_134)
& ? [U_132] :
( ~ model(U_132,U_135)
& model(U_132,U_134) )
& ! [U_131] :
( model(U_131,U_134)
| ~ model(U_131,U_135) )
& ? [U_130] : model(U_130,U_135) )
| ~ status(U_135,U_134,wth) )
& ( status(U_135,U_134,wth)
| ! [U_129] : model(U_129,U_134)
| ! [U_128] :
( model(U_128,U_135)
| ~ model(U_128,U_134) )
| ? [U_127] :
( ~ model(U_127,U_134)
& model(U_127,U_135) )
| ! [U_126] : ~ model(U_126,U_135) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_139,U_137] :
( ( ? [U_133] : ~ model(U_133,U_137)
& ? [U_132] :
( ~ model(U_132,U_139)
& model(U_132,U_137) )
& ! [U_131] :
( model(U_131,U_137)
| ~ model(U_131,U_139) )
& ? [U_130] : model(U_130,U_139) )
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_136] :
( status(U_138,U_136,wth)
| ! [U_129] : model(U_129,U_136)
| ! [U_128] :
( model(U_128,U_138)
| ~ model(U_128,U_136) )
| ? [U_127] :
( ~ model(U_127,U_136)
& model(U_127,U_138) )
| ! [U_126] : ~ model(U_126,U_138) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
( ! [U_139,U_137] :
( ( ? [U_133] : ~ model(U_133,U_137)
& ? [U_132] :
( ~ model(U_132,U_139)
& model(U_132,U_137) )
& ! [U_131] :
( model(U_131,U_137)
| ~ model(U_131,U_139) )
& ? [U_130] : model(U_130,U_139) )
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_136] :
( status(U_138,U_136,wth)
| ! [U_129] : model(U_129,U_136)
| ! [U_128] :
( model(U_128,U_138)
| ~ model(U_128,U_136) )
| ( ~ model(sK28(U_138,U_136),U_136)
& model(sK28(U_138,U_136),U_138) )
| ! [U_126] : ~ model(U_126,U_138) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(U_127,sK28(U_138,U_136))],[f_12_3]) ).
fof(f_12_5,plain,
( ! [U_139,U_137] :
( ( ? [U_133] : ~ model(U_133,U_137)
& ? [U_132] :
( ~ model(U_132,U_139)
& model(U_132,U_137) )
& ! [U_131] :
( model(U_131,U_137)
| ~ model(U_131,U_139) )
& model(sK29(U_139,U_137),U_139) )
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_136] :
( status(U_138,U_136,wth)
| ! [U_129] : model(U_129,U_136)
| ! [U_128] :
( model(U_128,U_138)
| ~ model(U_128,U_136) )
| ( ~ model(sK28(U_138,U_136),U_136)
& model(sK28(U_138,U_136),U_138) )
| ! [U_126] : ~ model(U_126,U_138) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29]),skolemize(U_130,sK29(U_139,U_137))],[f_12_4]) ).
fof(f_12_6,plain,
( ! [U_139,U_137] :
( ( ? [U_133] : ~ model(U_133,U_137)
& ~ model(sK30(U_139,U_137),U_139)
& model(sK30(U_139,U_137),U_137)
& ! [U_131] :
( model(U_131,U_137)
| ~ model(U_131,U_139) )
& model(sK29(U_139,U_137),U_139) )
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_136] :
( status(U_138,U_136,wth)
| ! [U_129] : model(U_129,U_136)
| ! [U_128] :
( model(U_128,U_138)
| ~ model(U_128,U_136) )
| ( ~ model(sK28(U_138,U_136),U_136)
& model(sK28(U_138,U_136),U_138) )
| ! [U_126] : ~ model(U_126,U_138) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30]),skolemize(U_132,sK30(U_139,U_137))],[f_12_5]) ).
fof(f_12_7,plain,
( ! [U_139,U_137] :
( ( ~ model(sK31(U_139,U_137),U_137)
& ~ model(sK30(U_139,U_137),U_139)
& model(sK30(U_139,U_137),U_137)
& ! [U_131] :
( model(U_131,U_137)
| ~ model(U_131,U_139) )
& model(sK29(U_139,U_137),U_139) )
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_136] :
( status(U_138,U_136,wth)
| ! [U_129] : model(U_129,U_136)
| ! [U_128] :
( model(U_128,U_138)
| ~ model(U_128,U_136) )
| ( ~ model(sK28(U_138,U_136),U_136)
& model(sK28(U_138,U_136),U_138) )
| ! [U_126] : ~ model(U_126,U_138) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31]),skolemize(U_133,sK31(U_139,U_137))],[f_12_6]) ).
fof(f_12_8,plain,
( ! [U_137,U_131,U_139] :
( ~ model(sK31(U_139,U_137),U_137)
| ~ sP19(U_137,U_131,U_139) )
& ! [U_137,U_131,U_139] :
( ~ model(sK30(U_139,U_137),U_139)
| ~ sP19(U_137,U_131,U_139) )
& ! [U_137,U_131,U_139] :
( model(sK30(U_139,U_137),U_137)
| ~ sP19(U_137,U_131,U_139) )
& ! [U_137,U_131,U_139] :
( model(U_131,U_137)
| ~ model(U_131,U_139)
| ~ sP19(U_137,U_131,U_139) )
& ! [U_137,U_131,U_139] :
( model(sK29(U_139,U_137),U_139)
| ~ sP19(U_137,U_131,U_139) )
& ! [U_138,U_136] :
( ~ model(sK28(U_138,U_136),U_136)
| ~ sP18(U_138,U_136) )
& ! [U_138,U_136] :
( model(sK28(U_138,U_136),U_138)
| ~ sP18(U_138,U_136) )
& ! [U_137,U_131,U_139] :
( sP19(U_137,U_131,U_139)
| ~ status(U_139,U_137,wth) )
& ! [U_138,U_128,U_136,U_126,U_129] :
( status(U_138,U_136,wth)
| model(U_129,U_136)
| model(U_128,U_138)
| ~ model(U_128,U_136)
| sP18(U_138,U_136)
| ~ model(U_126,U_138) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP18,sP19])],[f_12_7]) ).
cnf(f_12_9,plain,
( status(U_138,U_136,wth)
| model(U_129,U_136)
| model(U_128,U_138)
| ~ model(U_128,U_136)
| sP18(U_138,U_136)
| ~ model(U_126,U_138) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_10,plain,
( sP19(U_137,U_131,U_139)
| ~ status(U_139,U_137,wth) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_11,plain,
( model(sK28(U_138,U_136),U_138)
| ~ sP18(U_138,U_136) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_12,plain,
( ~ model(sK28(U_138,U_136),U_136)
| ~ sP18(U_138,U_136) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_13,plain,
( model(sK29(U_139,U_137),U_139)
| ~ sP19(U_137,U_131,U_139) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_14,plain,
( model(U_131,U_137)
| ~ model(U_131,U_139)
| ~ sP19(U_137,U_131,U_139) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_15,plain,
( model(sK30(U_139,U_137),U_137)
| ~ sP19(U_137,U_131,U_139) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_16,plain,
( ~ model(sK30(U_139,U_137),U_139)
| ~ sP19(U_137,U_131,U_139) ),
inference(clausify,[status(thm)],[f_12_8]) ).
cnf(f_12_17,plain,
( ~ model(sK31(U_139,U_137),U_137)
| ~ sP19(U_137,U_131,U_139) ),
inference(clausify,[status(thm)],[f_12_8]) ).
fof(f_13_1,plain,
! [Ax,C] :
( ( ! [I1] : ~ model(I1,Ax)
| ~ status(Ax,C,cax) )
& ( status(Ax,C,cax)
| ? [I1] : model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[cax]) ).
fof(f_13_2,plain,
! [U_143,U_142] :
( ( ! [U_141] : ~ model(U_141,U_143)
| ~ status(U_143,U_142,cax) )
& ( status(U_143,U_142,cax)
| ? [U_140] : model(U_140,U_143) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_147] :
( ! [U_145] : ~ status(U_147,U_145,cax)
| ! [U_141] : ~ model(U_141,U_147) )
& ! [U_146] :
( ! [U_144] : status(U_146,U_144,cax)
| ? [U_140] : model(U_140,U_146) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_147] :
( ! [U_145] : ~ status(U_147,U_145,cax)
| ! [U_141] : ~ model(U_141,U_147) )
& ! [U_146] :
( ! [U_144] : status(U_146,U_144,cax)
| model(sK32(U_146),U_146) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32]),skolemize(U_140,sK32(U_146))],[f_13_3]) ).
fof(f_13_5,plain,
( ! [U_147,U_141,U_145] :
( ~ status(U_147,U_145,cax)
| ~ model(U_141,U_147) )
& ! [U_144,U_146] :
( status(U_146,U_144,cax)
| model(sK32(U_146),U_146) ) ),
inference(definitional_conversion,[status(esa)],[f_13_4]) ).
cnf(f_13_6,plain,
( status(U_146,U_144,cax)
| model(sK32(U_146),U_146) ),
inference(clausify,[status(thm)],[f_13_5]) ).
cnf(f_13_7,plain,
( ~ status(U_147,U_145,cax)
| ~ model(U_141,U_147) ),
inference(clausify,[status(thm)],[f_13_5]) ).
fof(f_14_1,plain,
! [Ax,C] :
( ( ( ? [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) )
| ~ status(Ax,C,sca) )
& ( status(Ax,C,sca)
| ! [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[sca]) ).
fof(f_14_2,plain,
! [U_153,U_152] :
( ( ( ? [U_151] : model(U_151,U_152)
& ! [U_150] : ~ model(U_150,U_153) )
| ~ status(U_153,U_152,sca) )
& ( status(U_153,U_152,sca)
| ! [U_149] : ~ model(U_149,U_152)
| ? [U_148] : model(U_148,U_153) ) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
( ! [U_157,U_155] :
( ( ? [U_151] : model(U_151,U_155)
& ! [U_150] : ~ model(U_150,U_157) )
| ~ status(U_157,U_155,sca) )
& ! [U_156,U_154] :
( status(U_156,U_154,sca)
| ! [U_149] : ~ model(U_149,U_154)
| ? [U_148] : model(U_148,U_156) ) ),
inference(miniscope,[status(thm)],[f_14_2]) ).
fof(f_14_4,plain,
( ! [U_157,U_155] :
( ( ? [U_151] : model(U_151,U_155)
& ! [U_150] : ~ model(U_150,U_157) )
| ~ status(U_157,U_155,sca) )
& ! [U_156,U_154] :
( status(U_156,U_154,sca)
| ! [U_149] : ~ model(U_149,U_154)
| model(sK33(U_156,U_154),U_156) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(U_148,sK33(U_156,U_154))],[f_14_3]) ).
fof(f_14_5,plain,
( ! [U_157,U_155] :
( ( model(sK34(U_157,U_155),U_155)
& ! [U_150] : ~ model(U_150,U_157) )
| ~ status(U_157,U_155,sca) )
& ! [U_156,U_154] :
( status(U_156,U_154,sca)
| ! [U_149] : ~ model(U_149,U_154)
| model(sK33(U_156,U_154),U_156) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34]),skolemize(U_151,sK34(U_157,U_155))],[f_14_4]) ).
fof(f_14_6,plain,
( ! [U_157,U_150,U_155] :
( model(sK34(U_157,U_155),U_155)
| ~ sP20(U_157,U_150,U_155) )
& ! [U_157,U_150,U_155] :
( ~ model(U_150,U_157)
| ~ sP20(U_157,U_150,U_155) )
& ! [U_157,U_150,U_155] :
( sP20(U_157,U_150,U_155)
| ~ status(U_157,U_155,sca) )
& ! [U_149,U_156,U_154] :
( status(U_156,U_154,sca)
| ~ model(U_149,U_154)
| model(sK33(U_156,U_154),U_156) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP20])],[f_14_5]) ).
cnf(f_14_7,plain,
( status(U_156,U_154,sca)
| ~ model(U_149,U_154)
| model(sK33(U_156,U_154),U_156) ),
inference(clausify,[status(thm)],[f_14_6]) ).
cnf(f_14_8,plain,
( sP20(U_157,U_150,U_155)
| ~ status(U_157,U_155,sca) ),
inference(clausify,[status(thm)],[f_14_6]) ).
cnf(f_14_9,plain,
( ~ model(U_150,U_157)
| ~ sP20(U_157,U_150,U_155) ),
inference(clausify,[status(thm)],[f_14_6]) ).
cnf(f_14_10,plain,
( model(sK34(U_157,U_155),U_155)
| ~ sP20(U_157,U_150,U_155) ),
inference(clausify,[status(thm)],[f_14_6]) ).
fof(f_15_1,plain,
! [Ax,C] :
( ( ( ! [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) )
| ~ status(Ax,C,tca) )
& ( status(Ax,C,tca)
| ? [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[tca]) ).
fof(f_15_2,plain,
! [U_163,U_162] :
( ( ( ! [U_161] : model(U_161,U_162)
& ! [U_160] : ~ model(U_160,U_163) )
| ~ status(U_163,U_162,tca) )
& ( status(U_163,U_162,tca)
| ? [U_159] : ~ model(U_159,U_162)
| ? [U_158] : model(U_158,U_163) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_167,U_165] :
( ( ! [U_161] : model(U_161,U_165)
& ! [U_160] : ~ model(U_160,U_167) )
| ~ status(U_167,U_165,tca) )
& ! [U_166,U_164] :
( status(U_166,U_164,tca)
| ? [U_159] : ~ model(U_159,U_164)
| ? [U_158] : model(U_158,U_166) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_167,U_165] :
( ( ! [U_161] : model(U_161,U_165)
& ! [U_160] : ~ model(U_160,U_167) )
| ~ status(U_167,U_165,tca) )
& ! [U_166,U_164] :
( status(U_166,U_164,tca)
| ? [U_159] : ~ model(U_159,U_164)
| model(sK35(U_166,U_164),U_166) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35]),skolemize(U_158,sK35(U_166,U_164))],[f_15_3]) ).
fof(f_15_5,plain,
( ! [U_167,U_165] :
( ( ! [U_161] : model(U_161,U_165)
& ! [U_160] : ~ model(U_160,U_167) )
| ~ status(U_167,U_165,tca) )
& ! [U_166,U_164] :
( status(U_166,U_164,tca)
| ~ model(sK36(U_166,U_164),U_164)
| model(sK35(U_166,U_164),U_166) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36]),skolemize(U_159,sK36(U_166,U_164))],[f_15_4]) ).
fof(f_15_6,plain,
( ! [U_161,U_160,U_165,U_167] :
( model(U_161,U_165)
| ~ sP21(U_161,U_160,U_165,U_167) )
& ! [U_161,U_160,U_165,U_167] :
( ~ model(U_160,U_167)
| ~ sP21(U_161,U_160,U_165,U_167) )
& ! [U_161,U_160,U_165,U_167] :
( sP21(U_161,U_160,U_165,U_167)
| ~ status(U_167,U_165,tca) )
& ! [U_166,U_164] :
( status(U_166,U_164,tca)
| ~ model(sK36(U_166,U_164),U_164)
| model(sK35(U_166,U_164),U_166) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP21])],[f_15_5]) ).
cnf(f_15_7,plain,
( status(U_166,U_164,tca)
| ~ model(sK36(U_166,U_164),U_164)
| model(sK35(U_166,U_164),U_166) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_8,plain,
( sP21(U_161,U_160,U_165,U_167)
| ~ status(U_167,U_165,tca) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_9,plain,
( ~ model(U_160,U_167)
| ~ sP21(U_161,U_160,U_165,U_167) ),
inference(clausify,[status(thm)],[f_15_6]) ).
cnf(f_15_10,plain,
( model(U_161,U_165)
| ~ sP21(U_161,U_160,U_165,U_167) ),
inference(clausify,[status(thm)],[f_15_6]) ).
fof(f_16_1,plain,
! [Ax,C] :
( ( ( ? [I3] : ~ model(I3,C)
& ? [I2] : model(I2,C)
& ! [I1] : ~ model(I1,Ax) )
| ~ status(Ax,C,wca) )
& ( status(Ax,C,wca)
| ! [I3] : model(I3,C)
| ! [I2] : ~ model(I2,C)
| ? [I1] : model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[wca]) ).
fof(f_16_2,plain,
! [U_175,U_174] :
( ( ( ? [U_173] : ~ model(U_173,U_174)
& ? [U_172] : model(U_172,U_174)
& ! [U_171] : ~ model(U_171,U_175) )
| ~ status(U_175,U_174,wca) )
& ( status(U_175,U_174,wca)
| ! [U_170] : model(U_170,U_174)
| ! [U_169] : ~ model(U_169,U_174)
| ? [U_168] : model(U_168,U_175) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_179,U_177] :
( ( ? [U_173] : ~ model(U_173,U_177)
& ? [U_172] : model(U_172,U_177)
& ! [U_171] : ~ model(U_171,U_179) )
| ~ status(U_179,U_177,wca) )
& ! [U_178,U_176] :
( status(U_178,U_176,wca)
| ! [U_170] : model(U_170,U_176)
| ! [U_169] : ~ model(U_169,U_176)
| ? [U_168] : model(U_168,U_178) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_179,U_177] :
( ( ? [U_173] : ~ model(U_173,U_177)
& ? [U_172] : model(U_172,U_177)
& ! [U_171] : ~ model(U_171,U_179) )
| ~ status(U_179,U_177,wca) )
& ! [U_178,U_176] :
( status(U_178,U_176,wca)
| ! [U_170] : model(U_170,U_176)
| ! [U_169] : ~ model(U_169,U_176)
| model(sK37(U_178,U_176),U_178) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(U_168,sK37(U_178,U_176))],[f_16_3]) ).
fof(f_16_5,plain,
( ! [U_179,U_177] :
( ( ? [U_173] : ~ model(U_173,U_177)
& model(sK38(U_179,U_177),U_177)
& ! [U_171] : ~ model(U_171,U_179) )
| ~ status(U_179,U_177,wca) )
& ! [U_178,U_176] :
( status(U_178,U_176,wca)
| ! [U_170] : model(U_170,U_176)
| ! [U_169] : ~ model(U_169,U_176)
| model(sK37(U_178,U_176),U_178) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38]),skolemize(U_172,sK38(U_179,U_177))],[f_16_4]) ).
fof(f_16_6,plain,
( ! [U_179,U_177] :
( ( ~ model(sK39(U_179,U_177),U_177)
& model(sK38(U_179,U_177),U_177)
& ! [U_171] : ~ model(U_171,U_179) )
| ~ status(U_179,U_177,wca) )
& ! [U_178,U_176] :
( status(U_178,U_176,wca)
| ! [U_170] : model(U_170,U_176)
| ! [U_169] : ~ model(U_169,U_176)
| model(sK37(U_178,U_176),U_178) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39]),skolemize(U_173,sK39(U_179,U_177))],[f_16_5]) ).
fof(f_16_7,plain,
( ! [U_179,U_171,U_177] :
( ~ model(sK39(U_179,U_177),U_177)
| ~ sP22(U_179,U_171,U_177) )
& ! [U_179,U_171,U_177] :
( model(sK38(U_179,U_177),U_177)
| ~ sP22(U_179,U_171,U_177) )
& ! [U_179,U_171,U_177] :
( ~ model(U_171,U_179)
| ~ sP22(U_179,U_171,U_177) )
& ! [U_179,U_171,U_177] :
( sP22(U_179,U_171,U_177)
| ~ status(U_179,U_177,wca) )
& ! [U_169,U_170,U_176,U_178] :
( status(U_178,U_176,wca)
| model(U_170,U_176)
| ~ model(U_169,U_176)
| model(sK37(U_178,U_176),U_178) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP22])],[f_16_6]) ).
cnf(f_16_8,plain,
( status(U_178,U_176,wca)
| model(U_170,U_176)
| ~ model(U_169,U_176)
| model(sK37(U_178,U_176),U_178) ),
inference(clausify,[status(thm)],[f_16_7]) ).
cnf(f_16_9,plain,
( sP22(U_179,U_171,U_177)
| ~ status(U_179,U_177,wca) ),
inference(clausify,[status(thm)],[f_16_7]) ).
cnf(f_16_10,plain,
( ~ model(U_171,U_179)
| ~ sP22(U_179,U_171,U_177) ),
inference(clausify,[status(thm)],[f_16_7]) ).
cnf(f_16_11,plain,
( model(sK38(U_179,U_177),U_177)
| ~ sP22(U_179,U_171,U_177) ),
inference(clausify,[status(thm)],[f_16_7]) ).
cnf(f_16_12,plain,
( ~ model(sK39(U_179,U_177),U_177)
| ~ sP22(U_179,U_171,U_177) ),
inference(clausify,[status(thm)],[f_16_7]) ).
fof(f_17_1,plain,
! [Ax,C] :
( ( ? [I1] :
( model(I1,not(C))
& model(I1,Ax) )
| ~ status(Ax,C,csa) )
& ( status(Ax,C,csa)
| ! [I1] :
( ~ model(I1,not(C))
| ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[csa]) ).
fof(f_17_2,plain,
! [U_183,U_182] :
( ( ? [U_181] :
( model(U_181,not(U_182))
& model(U_181,U_183) )
| ~ status(U_183,U_182,csa) )
& ( status(U_183,U_182,csa)
| ! [U_180] :
( ~ model(U_180,not(U_182))
| ~ model(U_180,U_183) ) ) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
( ! [U_187,U_185] :
( ? [U_181] :
( model(U_181,not(U_185))
& model(U_181,U_187) )
| ~ status(U_187,U_185,csa) )
& ! [U_186,U_184] :
( status(U_186,U_184,csa)
| ! [U_180] :
( ~ model(U_180,not(U_184))
| ~ model(U_180,U_186) ) ) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
fof(f_17_4,plain,
( ! [U_187,U_185] :
( ( model(sK40(U_187,U_185),not(U_185))
& model(sK40(U_187,U_185),U_187) )
| ~ status(U_187,U_185,csa) )
& ! [U_186,U_184] :
( status(U_186,U_184,csa)
| ! [U_180] :
( ~ model(U_180,not(U_184))
| ~ model(U_180,U_186) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK40]),skolemize(U_181,sK40(U_187,U_185))],[f_17_3]) ).
fof(f_17_5,plain,
( ! [U_187,U_185] :
( model(sK40(U_187,U_185),not(U_185))
| ~ sP23(U_187,U_185) )
& ! [U_187,U_185] :
( model(sK40(U_187,U_185),U_187)
| ~ sP23(U_187,U_185) )
& ! [U_187,U_185] :
( sP23(U_187,U_185)
| ~ status(U_187,U_185,csa) )
& ! [U_186,U_180,U_184] :
( status(U_186,U_184,csa)
| ~ model(U_180,not(U_184))
| ~ model(U_180,U_186) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP23])],[f_17_4]) ).
cnf(f_17_6,plain,
( status(U_186,U_184,csa)
| ~ model(U_180,not(U_184))
| ~ model(U_180,U_186) ),
inference(clausify,[status(thm)],[f_17_5]) ).
cnf(f_17_7,plain,
( sP23(U_187,U_185)
| ~ status(U_187,U_185,csa) ),
inference(clausify,[status(thm)],[f_17_5]) ).
cnf(f_17_8,plain,
( model(sK40(U_187,U_185),U_187)
| ~ sP23(U_187,U_185) ),
inference(clausify,[status(thm)],[f_17_5]) ).
cnf(f_17_9,plain,
( model(sK40(U_187,U_185),not(U_185))
| ~ sP23(U_187,U_185) ),
inference(clausify,[status(thm)],[f_17_5]) ).
fof(f_18_1,plain,
! [Ax,C] :
( ( ( ! [I2] : model(I2,not(C))
& ! [I1] : model(I1,Ax) )
| ~ status(Ax,C,uns) )
& ( status(Ax,C,uns)
| ? [I2] : ~ model(I2,not(C))
| ? [I1] : ~ model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[uns]) ).
fof(f_18_2,plain,
! [U_193,U_192] :
( ( ( ! [U_191] : model(U_191,not(U_192))
& ! [U_190] : model(U_190,U_193) )
| ~ status(U_193,U_192,uns) )
& ( status(U_193,U_192,uns)
| ? [U_189] : ~ model(U_189,not(U_192))
| ? [U_188] : ~ model(U_188,U_193) ) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_197,U_195] :
( ( ! [U_191] : model(U_191,not(U_195))
& ! [U_190] : model(U_190,U_197) )
| ~ status(U_197,U_195,uns) )
& ! [U_196,U_194] :
( status(U_196,U_194,uns)
| ? [U_189] : ~ model(U_189,not(U_194))
| ? [U_188] : ~ model(U_188,U_196) ) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_197,U_195] :
( ( ! [U_191] : model(U_191,not(U_195))
& ! [U_190] : model(U_190,U_197) )
| ~ status(U_197,U_195,uns) )
& ! [U_196,U_194] :
( status(U_196,U_194,uns)
| ? [U_189] : ~ model(U_189,not(U_194))
| ~ model(sK41(U_196,U_194),U_196) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(U_188,sK41(U_196,U_194))],[f_18_3]) ).
fof(f_18_5,plain,
( ! [U_197,U_195] :
( ( ! [U_191] : model(U_191,not(U_195))
& ! [U_190] : model(U_190,U_197) )
| ~ status(U_197,U_195,uns) )
& ! [U_196,U_194] :
( status(U_196,U_194,uns)
| ~ model(sK42(U_196,U_194),not(U_194))
| ~ model(sK41(U_196,U_194),U_196) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(U_189,sK42(U_196,U_194))],[f_18_4]) ).
fof(f_18_6,plain,
( ! [U_195,U_191,U_190,U_197] :
( model(U_191,not(U_195))
| ~ sP24(U_195,U_191,U_190,U_197) )
& ! [U_195,U_191,U_190,U_197] :
( model(U_190,U_197)
| ~ sP24(U_195,U_191,U_190,U_197) )
& ! [U_195,U_191,U_190,U_197] :
( sP24(U_195,U_191,U_190,U_197)
| ~ status(U_197,U_195,uns) )
& ! [U_194,U_196] :
( status(U_196,U_194,uns)
| ~ model(sK42(U_196,U_194),not(U_194))
| ~ model(sK41(U_196,U_194),U_196) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP24])],[f_18_5]) ).
cnf(f_18_7,plain,
( status(U_196,U_194,uns)
| ~ model(sK42(U_196,U_194),not(U_194))
| ~ model(sK41(U_196,U_194),U_196) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_8,plain,
( sP24(U_195,U_191,U_190,U_197)
| ~ status(U_197,U_195,uns) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_9,plain,
( model(U_190,U_197)
| ~ sP24(U_195,U_191,U_190,U_197) ),
inference(clausify,[status(thm)],[f_18_6]) ).
cnf(f_18_10,plain,
( model(U_191,not(U_195))
| ~ sP24(U_195,U_191,U_190,U_197) ),
inference(clausify,[status(thm)],[f_18_6]) ).
fof(f_19_1,plain,
! [Ax,C] :
( ( ( ? [I2] :
( model(I2,not(C))
& model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) )
| ~ status(Ax,C,noc) )
& ( status(Ax,C,noc)
| ! [I2] :
( ~ model(I2,not(C))
| ~ model(I2,Ax) )
| ! [I1] :
( ~ model(I1,C)
| ~ model(I1,Ax) ) ) ),
inference(fof_nnf,[status(thm)],[noc]) ).
fof(f_19_2,plain,
! [U_203,U_202] :
( ( ( ? [U_201] :
( model(U_201,not(U_202))
& model(U_201,U_203) )
& ? [U_200] :
( model(U_200,U_202)
& model(U_200,U_203) ) )
| ~ status(U_203,U_202,noc) )
& ( status(U_203,U_202,noc)
| ! [U_199] :
( ~ model(U_199,not(U_202))
| ~ model(U_199,U_203) )
| ! [U_198] :
( ~ model(U_198,U_202)
| ~ model(U_198,U_203) ) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_207,U_205] :
( ( ? [U_201] :
( model(U_201,not(U_205))
& model(U_201,U_207) )
& ? [U_200] :
( model(U_200,U_205)
& model(U_200,U_207) ) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
fof(f_19_4,plain,
( ! [U_207,U_205] :
( ( ? [U_201] :
( model(U_201,not(U_205))
& model(U_201,U_207) )
& model(sK43(U_207,U_205),U_205)
& model(sK43(U_207,U_205),U_207) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(U_200,sK43(U_207,U_205))],[f_19_3]) ).
fof(f_19_5,plain,
( ! [U_207,U_205] :
( ( model(sK44(U_207,U_205),not(U_205))
& model(sK44(U_207,U_205),U_207)
& model(sK43(U_207,U_205),U_205)
& model(sK43(U_207,U_205),U_207) )
| ~ status(U_207,U_205,noc) )
& ! [U_206,U_204] :
( status(U_206,U_204,noc)
| ! [U_199] :
( ~ model(U_199,not(U_204))
| ~ model(U_199,U_206) )
| ! [U_198] :
( ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(U_201,sK44(U_207,U_205))],[f_19_4]) ).
fof(f_19_6,plain,
( ! [U_205,U_207] :
( model(sK44(U_207,U_205),not(U_205))
| ~ sP25(U_205,U_207) )
& ! [U_205,U_207] :
( model(sK44(U_207,U_205),U_207)
| ~ sP25(U_205,U_207) )
& ! [U_205,U_207] :
( model(sK43(U_207,U_205),U_205)
| ~ sP25(U_205,U_207) )
& ! [U_205,U_207] :
( model(sK43(U_207,U_205),U_207)
| ~ sP25(U_205,U_207) )
& ! [U_205,U_207] :
( sP25(U_205,U_207)
| ~ status(U_207,U_205,noc) )
& ! [U_204,U_198,U_206,U_199] :
( status(U_206,U_204,noc)
| ~ model(U_199,not(U_204))
| ~ model(U_199,U_206)
| ~ model(U_198,U_204)
| ~ model(U_198,U_206) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP25])],[f_19_5]) ).
cnf(f_19_7,plain,
( status(U_206,U_204,noc)
| ~ model(U_199,not(U_204))
| ~ model(U_199,U_206)
| ~ model(U_198,U_204)
| ~ model(U_198,U_206) ),
inference(clausify,[status(thm)],[f_19_6]) ).
cnf(f_19_8,plain,
( sP25(U_205,U_207)
| ~ status(U_207,U_205,noc) ),
inference(clausify,[status(thm)],[f_19_6]) ).
cnf(f_19_9,plain,
( model(sK43(U_207,U_205),U_207)
| ~ sP25(U_205,U_207) ),
inference(clausify,[status(thm)],[f_19_6]) ).
cnf(f_19_10,plain,
( model(sK43(U_207,U_205),U_205)
| ~ sP25(U_205,U_207) ),
inference(clausify,[status(thm)],[f_19_6]) ).
cnf(f_19_11,plain,
( model(sK44(U_207,U_205),U_207)
| ~ sP25(U_205,U_207) ),
inference(clausify,[status(thm)],[f_19_6]) ).
cnf(f_19_12,plain,
( model(sK44(U_207,U_205),not(U_205))
| ~ sP25(U_205,U_207) ),
inference(clausify,[status(thm)],[f_19_6]) ).
fof(f_20_1,plain,
! [S1,S2] :
( ( ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) )
| ~ mighta(S1,S2) )
& ( mighta(S1,S2)
| ! [Ax,C] :
( ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ),
inference(fof_nnf,[status(thm)],[mighta]) ).
fof(f_20_2,plain,
! [U_213,U_212] :
( ( ? [U_211,U_210] :
( status(U_211,U_210,U_212)
& status(U_211,U_210,U_213) )
| ~ mighta(U_213,U_212) )
& ( mighta(U_213,U_212)
| ! [U_209,U_208] :
( ~ status(U_209,U_208,U_212)
| ~ status(U_209,U_208,U_213) ) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_217,U_215] :
( ? [U_211,U_210] :
( status(U_211,U_210,U_215)
& status(U_211,U_210,U_217) )
| ~ mighta(U_217,U_215) )
& ! [U_216,U_214] :
( mighta(U_216,U_214)
| ! [U_209,U_208] :
( ~ status(U_209,U_208,U_214)
| ~ status(U_209,U_208,U_216) ) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
fof(f_20_4,plain,
( ! [U_217,U_215] :
( ? [U_210] :
( status(sK45(U_217,U_215),U_210,U_215)
& status(sK45(U_217,U_215),U_210,U_217) )
| ~ mighta(U_217,U_215) )
& ! [U_216,U_214] :
( mighta(U_216,U_214)
| ! [U_209,U_208] :
( ~ status(U_209,U_208,U_214)
| ~ status(U_209,U_208,U_216) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(U_211,sK45(U_217,U_215))],[f_20_3]) ).
fof(f_20_5,plain,
( ! [U_217,U_215] :
( ( status(sK45(U_217,U_215),sK46(U_217,U_215),U_215)
& status(sK45(U_217,U_215),sK46(U_217,U_215),U_217) )
| ~ mighta(U_217,U_215) )
& ! [U_216,U_214] :
( mighta(U_216,U_214)
| ! [U_209,U_208] :
( ~ status(U_209,U_208,U_214)
| ~ status(U_209,U_208,U_216) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(U_210,sK46(U_217,U_215))],[f_20_4]) ).
fof(f_20_6,plain,
( ! [U_215,U_217] :
( status(sK45(U_217,U_215),sK46(U_217,U_215),U_215)
| ~ sP26(U_215,U_217) )
& ! [U_215,U_217] :
( status(sK45(U_217,U_215),sK46(U_217,U_215),U_217)
| ~ sP26(U_215,U_217) )
& ! [U_215,U_217] :
( sP26(U_215,U_217)
| ~ mighta(U_217,U_215) )
& ! [U_216,U_208,U_214,U_209] :
( mighta(U_216,U_214)
| ~ status(U_209,U_208,U_214)
| ~ status(U_209,U_208,U_216) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP26])],[f_20_5]) ).
cnf(f_20_7,plain,
( mighta(U_216,U_214)
| ~ status(U_209,U_208,U_214)
| ~ status(U_209,U_208,U_216) ),
inference(clausify,[status(thm)],[f_20_6]) ).
cnf(f_20_8,plain,
( sP26(U_215,U_217)
| ~ mighta(U_217,U_215) ),
inference(clausify,[status(thm)],[f_20_6]) ).
cnf(f_20_9,plain,
( status(sK45(U_217,U_215),sK46(U_217,U_215),U_217)
| ~ sP26(U_215,U_217) ),
inference(clausify,[status(thm)],[f_20_6]) ).
cnf(f_20_10,plain,
( status(sK45(U_217,U_215),sK46(U_217,U_215),U_215)
| ~ sP26(U_215,U_217) ),
inference(clausify,[status(thm)],[f_20_6]) ).
fof(f_21_1,plain,
! [S1,S2] :
( ( ! [Ax,C] :
( status(Ax,C,S2)
| ~ status(Ax,C,S1) )
| ~ isa(S1,S2) )
& ( isa(S1,S2)
| ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) ) ),
inference(fof_nnf,[status(thm)],[isa]) ).
fof(f_21_2,plain,
! [U_223,U_222] :
( ( ! [U_221,U_220] :
( status(U_221,U_220,U_222)
| ~ status(U_221,U_220,U_223) )
| ~ isa(U_223,U_222) )
& ( isa(U_223,U_222)
| ? [U_219,U_218] :
( ~ status(U_219,U_218,U_222)
& status(U_219,U_218,U_223) ) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_227,U_225] :
( ! [U_221,U_220] :
( status(U_221,U_220,U_225)
| ~ status(U_221,U_220,U_227) )
| ~ isa(U_227,U_225) )
& ! [U_226,U_224] :
( isa(U_226,U_224)
| ? [U_219,U_218] :
( ~ status(U_219,U_218,U_224)
& status(U_219,U_218,U_226) ) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
fof(f_21_4,plain,
( ! [U_227,U_225] :
( ! [U_221,U_220] :
( status(U_221,U_220,U_225)
| ~ status(U_221,U_220,U_227) )
| ~ isa(U_227,U_225) )
& ! [U_226,U_224] :
( isa(U_226,U_224)
| ? [U_218] :
( ~ status(sK47(U_226,U_224),U_218,U_224)
& status(sK47(U_226,U_224),U_218,U_226) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(U_219,sK47(U_226,U_224))],[f_21_3]) ).
fof(f_21_5,plain,
( ! [U_227,U_225] :
( ! [U_221,U_220] :
( status(U_221,U_220,U_225)
| ~ status(U_221,U_220,U_227) )
| ~ isa(U_227,U_225) )
& ! [U_226,U_224] :
( isa(U_226,U_224)
| ( ~ status(sK47(U_226,U_224),sK48(U_226,U_224),U_224)
& status(sK47(U_226,U_224),sK48(U_226,U_224),U_226) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(U_218,sK48(U_226,U_224))],[f_21_4]) ).
fof(f_21_6,plain,
( ! [U_224,U_226] :
( ~ status(sK47(U_226,U_224),sK48(U_226,U_224),U_224)
| ~ sP27(U_224,U_226) )
& ! [U_224,U_226] :
( status(sK47(U_226,U_224),sK48(U_226,U_224),U_226)
| ~ sP27(U_224,U_226) )
& ! [U_221,U_220,U_225,U_227] :
( status(U_221,U_220,U_225)
| ~ status(U_221,U_220,U_227)
| ~ isa(U_227,U_225) )
& ! [U_224,U_226] :
( isa(U_226,U_224)
| sP27(U_224,U_226) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP27])],[f_21_5]) ).
cnf(f_21_7,plain,
( isa(U_226,U_224)
| sP27(U_224,U_226) ),
inference(clausify,[status(thm)],[f_21_6]) ).
cnf(f_21_8,plain,
( status(U_221,U_220,U_225)
| ~ status(U_221,U_220,U_227)
| ~ isa(U_227,U_225) ),
inference(clausify,[status(thm)],[f_21_6]) ).
cnf(f_21_9,plain,
( status(sK47(U_226,U_224),sK48(U_226,U_224),U_226)
| ~ sP27(U_224,U_226) ),
inference(clausify,[status(thm)],[f_21_6]) ).
cnf(f_21_10,plain,
( ~ status(sK47(U_226,U_224),sK48(U_226,U_224),U_224)
| ~ sP27(U_224,U_226) ),
inference(clausify,[status(thm)],[f_21_6]) ).
fof(f_22_1,plain,
! [S1,S2] :
( ( ? [Ax,C] :
( ~ status(Ax,C,S2)
& status(Ax,C,S1) )
| ~ nota(S1,S2) )
& ( nota(S1,S2)
| ! [Ax,C] :
( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ),
inference(fof_nnf,[status(thm)],[nota]) ).
fof(f_22_2,plain,
! [U_233,U_232] :
( ( ? [U_231,U_230] :
( ~ status(U_231,U_230,U_232)
& status(U_231,U_230,U_233) )
| ~ nota(U_233,U_232) )
& ( nota(U_233,U_232)
| ! [U_229,U_228] :
( status(U_229,U_228,U_232)
| ~ status(U_229,U_228,U_233) ) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_237,U_235] :
( ? [U_231,U_230] :
( ~ status(U_231,U_230,U_235)
& status(U_231,U_230,U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
( ! [U_237,U_235] :
( ? [U_230] :
( ~ status(sK49(U_237,U_235),U_230,U_235)
& status(sK49(U_237,U_235),U_230,U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(U_231,sK49(U_237,U_235))],[f_22_3]) ).
fof(f_22_5,plain,
( ! [U_237,U_235] :
( ( ~ status(sK49(U_237,U_235),sK50(U_237,U_235),U_235)
& status(sK49(U_237,U_235),sK50(U_237,U_235),U_237) )
| ~ nota(U_237,U_235) )
& ! [U_236,U_234] :
( nota(U_236,U_234)
| ! [U_229,U_228] :
( status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(U_230,sK50(U_237,U_235))],[f_22_4]) ).
fof(f_22_6,plain,
( ! [U_235,U_237] :
( ~ status(sK49(U_237,U_235),sK50(U_237,U_235),U_235)
| ~ sP28(U_235,U_237) )
& ! [U_235,U_237] :
( status(sK49(U_237,U_235),sK50(U_237,U_235),U_237)
| ~ sP28(U_235,U_237) )
& ! [U_235,U_237] :
( sP28(U_235,U_237)
| ~ nota(U_237,U_235) )
& ! [U_234,U_236,U_229,U_228] :
( nota(U_236,U_234)
| status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP28])],[f_22_5]) ).
cnf(f_22_7,plain,
( nota(U_236,U_234)
| status(U_229,U_228,U_234)
| ~ status(U_229,U_228,U_236) ),
inference(clausify,[status(thm)],[f_22_6]) ).
cnf(f_22_8,plain,
( sP28(U_235,U_237)
| ~ nota(U_237,U_235) ),
inference(clausify,[status(thm)],[f_22_6]) ).
cnf(f_22_9,plain,
( status(sK49(U_237,U_235),sK50(U_237,U_235),U_237)
| ~ sP28(U_235,U_237) ),
inference(clausify,[status(thm)],[f_22_6]) ).
cnf(f_22_10,plain,
( ~ status(sK49(U_237,U_235),sK50(U_237,U_235),U_235)
| ~ sP28(U_235,U_237) ),
inference(clausify,[status(thm)],[f_22_6]) ).
fof(f_23_1,plain,
! [S1,S2] :
( ( ! [Ax,C] :
( ~ status(Ax,C,S2)
| ~ status(Ax,C,S1) )
| ~ nevera(S1,S2) )
& ( nevera(S1,S2)
| ? [Ax,C] :
( status(Ax,C,S2)
& status(Ax,C,S1) ) ) ),
inference(fof_nnf,[status(thm)],[nevera]) ).
fof(f_23_2,plain,
! [U_243,U_242] :
( ( ! [U_241,U_240] :
( ~ status(U_241,U_240,U_242)
| ~ status(U_241,U_240,U_243) )
| ~ nevera(U_243,U_242) )
& ( nevera(U_243,U_242)
| ? [U_239,U_238] :
( status(U_239,U_238,U_242)
& status(U_239,U_238,U_243) ) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_247,U_245] :
( ! [U_241,U_240] :
( ~ status(U_241,U_240,U_245)
| ~ status(U_241,U_240,U_247) )
| ~ nevera(U_247,U_245) )
& ! [U_246,U_244] :
( nevera(U_246,U_244)
| ? [U_239,U_238] :
( status(U_239,U_238,U_244)
& status(U_239,U_238,U_246) ) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_247,U_245] :
( ! [U_241,U_240] :
( ~ status(U_241,U_240,U_245)
| ~ status(U_241,U_240,U_247) )
| ~ nevera(U_247,U_245) )
& ! [U_246,U_244] :
( nevera(U_246,U_244)
| ? [U_238] :
( status(sK51(U_246,U_244),U_238,U_244)
& status(sK51(U_246,U_244),U_238,U_246) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(U_239,sK51(U_246,U_244))],[f_23_3]) ).
fof(f_23_5,plain,
( ! [U_247,U_245] :
( ! [U_241,U_240] :
( ~ status(U_241,U_240,U_245)
| ~ status(U_241,U_240,U_247) )
| ~ nevera(U_247,U_245) )
& ! [U_246,U_244] :
( nevera(U_246,U_244)
| ( status(sK51(U_246,U_244),sK52(U_246,U_244),U_244)
& status(sK51(U_246,U_244),sK52(U_246,U_244),U_246) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(U_238,sK52(U_246,U_244))],[f_23_4]) ).
fof(f_23_6,plain,
( ! [U_246,U_244] :
( status(sK51(U_246,U_244),sK52(U_246,U_244),U_244)
| ~ sP29(U_246,U_244) )
& ! [U_246,U_244] :
( status(sK51(U_246,U_244),sK52(U_246,U_244),U_246)
| ~ sP29(U_246,U_244) )
& ! [U_240,U_241,U_245,U_247] :
( ~ status(U_241,U_240,U_245)
| ~ status(U_241,U_240,U_247)
| ~ nevera(U_247,U_245) )
& ! [U_246,U_244] :
( nevera(U_246,U_244)
| sP29(U_246,U_244) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP29])],[f_23_5]) ).
cnf(f_23_7,plain,
( nevera(U_246,U_244)
| sP29(U_246,U_244) ),
inference(clausify,[status(thm)],[f_23_6]) ).
cnf(f_23_8,plain,
( ~ status(U_241,U_240,U_245)
| ~ status(U_241,U_240,U_247)
| ~ nevera(U_247,U_245) ),
inference(clausify,[status(thm)],[f_23_6]) ).
cnf(f_23_9,plain,
( status(sK51(U_246,U_244),sK52(U_246,U_244),U_246)
| ~ sP29(U_246,U_244) ),
inference(clausify,[status(thm)],[f_23_6]) ).
cnf(f_23_10,plain,
( status(sK51(U_246,U_244),sK52(U_246,U_244),U_244)
| ~ sP29(U_246,U_244) ),
inference(clausify,[status(thm)],[f_23_6]) ).
fof(f_24_1,plain,
! [S1,S2] :
( ( ! [Ax,C] :
( ( status(Ax,C,S2)
& ~ status(Ax,C,S1) )
| ( ~ status(Ax,C,S2)
& status(Ax,C,S1) ) )
| ~ xora(S1,S2) )
& ( xora(S1,S2)
| ? [Ax,C] :
( ( ~ status(Ax,C,S2)
| status(Ax,C,S1) )
& ( status(Ax,C,S2)
| ~ status(Ax,C,S1) ) ) ) ),
inference(fof_nnf,[status(thm)],[xora]) ).
fof(f_24_2,plain,
! [U_253,U_252] :
( ( ! [U_251,U_250] :
( ( status(U_251,U_250,U_252)
& ~ status(U_251,U_250,U_253) )
| ( ~ status(U_251,U_250,U_252)
& status(U_251,U_250,U_253) ) )
| ~ xora(U_253,U_252) )
& ( xora(U_253,U_252)
| ? [U_249,U_248] :
( ( ~ status(U_249,U_248,U_252)
| status(U_249,U_248,U_253) )
& ( status(U_249,U_248,U_252)
| ~ status(U_249,U_248,U_253) ) ) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_257,U_255] :
( ! [U_251,U_250] :
( ( status(U_251,U_250,U_255)
& ~ status(U_251,U_250,U_257) )
| ( ~ status(U_251,U_250,U_255)
& status(U_251,U_250,U_257) ) )
| ~ xora(U_257,U_255) )
& ! [U_256,U_254] :
( xora(U_256,U_254)
| ? [U_249,U_248] :
( ( ~ status(U_249,U_248,U_254)
| status(U_249,U_248,U_256) )
& ( status(U_249,U_248,U_254)
| ~ status(U_249,U_248,U_256) ) ) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( ! [U_257,U_255] :
( ! [U_251,U_250] :
( ( status(U_251,U_250,U_255)
& ~ status(U_251,U_250,U_257) )
| ( ~ status(U_251,U_250,U_255)
& status(U_251,U_250,U_257) ) )
| ~ xora(U_257,U_255) )
& ! [U_256,U_254] :
( xora(U_256,U_254)
| ? [U_248] :
( ( ~ status(sK53(U_256,U_254),U_248,U_254)
| status(sK53(U_256,U_254),U_248,U_256) )
& ( status(sK53(U_256,U_254),U_248,U_254)
| ~ status(sK53(U_256,U_254),U_248,U_256) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(U_249,sK53(U_256,U_254))],[f_24_3]) ).
fof(f_24_5,plain,
( ! [U_257,U_255] :
( ! [U_251,U_250] :
( ( status(U_251,U_250,U_255)
& ~ status(U_251,U_250,U_257) )
| ( ~ status(U_251,U_250,U_255)
& status(U_251,U_250,U_257) ) )
| ~ xora(U_257,U_255) )
& ! [U_256,U_254] :
( xora(U_256,U_254)
| ( ( ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| status(sK53(U_256,U_254),sK54(U_256,U_254),U_256) )
& ( status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_256) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(U_248,sK54(U_256,U_254))],[f_24_4]) ).
fof(f_24_6,plain,
( ! [U_251,U_250,U_255,U_257] :
( status(U_251,U_250,U_255)
| ~ sP32(U_251,U_250,U_255,U_257) )
& ! [U_251,U_250,U_255,U_257] :
( ~ status(U_251,U_250,U_257)
| ~ sP32(U_251,U_250,U_255,U_257) )
& ! [U_251,U_250,U_255,U_257] :
( ~ status(U_251,U_250,U_255)
| ~ sP31(U_251,U_250,U_255,U_257) )
& ! [U_251,U_250,U_255,U_257] :
( status(U_251,U_250,U_257)
| ~ sP31(U_251,U_250,U_255,U_257) )
& ! [U_254,U_256] :
( ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| status(sK53(U_256,U_254),sK54(U_256,U_254),U_256)
| ~ sP30(U_254,U_256) )
& ! [U_254,U_256] :
( status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_256)
| ~ sP30(U_254,U_256) )
& ! [U_251,U_250,U_255,U_257] :
( sP32(U_251,U_250,U_255,U_257)
| sP31(U_251,U_250,U_255,U_257)
| ~ xora(U_257,U_255) )
& ! [U_254,U_256] :
( xora(U_256,U_254)
| sP30(U_254,U_256) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP30,sP31,sP32])],[f_24_5]) ).
cnf(f_24_7,plain,
( xora(U_256,U_254)
| sP30(U_254,U_256) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_8,plain,
( sP32(U_251,U_250,U_255,U_257)
| sP31(U_251,U_250,U_255,U_257)
| ~ xora(U_257,U_255) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_9,plain,
( status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_256)
| ~ sP30(U_254,U_256) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_10,plain,
( ~ status(sK53(U_256,U_254),sK54(U_256,U_254),U_254)
| status(sK53(U_256,U_254),sK54(U_256,U_254),U_256)
| ~ sP30(U_254,U_256) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_11,plain,
( status(U_251,U_250,U_257)
| ~ sP31(U_251,U_250,U_255,U_257) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_12,plain,
( ~ status(U_251,U_250,U_255)
| ~ sP31(U_251,U_250,U_255,U_257) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_13,plain,
( ~ status(U_251,U_250,U_257)
| ~ sP32(U_251,U_250,U_255,U_257) ),
inference(clausify,[status(thm)],[f_24_6]) ).
cnf(f_24_14,plain,
( status(U_251,U_250,U_255)
| ~ sP32(U_251,U_250,U_255,U_257) ),
inference(clausify,[status(thm)],[f_24_6]) ).
fof(f_25_1,plain,
! [I,F] :
( ( model(I,not(F))
& ~ model(I,F) )
| ( ~ model(I,not(F))
& model(I,F) ) ),
inference(fof_nnf,[status(thm)],[completeness]) ).
fof(f_25_2,plain,
! [U_259,U_258] :
( ( model(U_259,not(U_258))
& ~ model(U_259,U_258) )
| ( ~ model(U_259,not(U_258))
& model(U_259,U_258) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_259,U_258] :
( model(U_259,not(U_258))
| ~ sP34(U_259,U_258) )
& ! [U_259,U_258] :
( ~ model(U_259,U_258)
| ~ sP34(U_259,U_258) )
& ! [U_259,U_258] :
( ~ model(U_259,not(U_258))
| ~ sP33(U_259,U_258) )
& ! [U_259,U_258] :
( model(U_259,U_258)
| ~ sP33(U_259,U_258) )
& ! [U_259,U_258] :
( sP34(U_259,U_258)
| sP33(U_259,U_258) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP33,sP34])],[f_25_2]) ).
cnf(f_25_4,plain,
( sP34(U_259,U_258)
| sP33(U_259,U_258) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( model(U_259,U_258)
| ~ sP33(U_259,U_258) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( ~ model(U_259,not(U_258))
| ~ sP33(U_259,U_258) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_7,plain,
( ~ model(U_259,U_258)
| ~ sP34(U_259,U_258) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_8,plain,
( model(U_259,not(U_258))
| ~ sP34(U_259,U_258) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [I,F] :
( ( model(I,F)
| model(I,not(F)) )
& ( ~ model(I,not(F))
| ~ model(I,F) ) ),
inference(fof_nnf,[status(thm)],[not]) ).
fof(f_26_2,plain,
! [U_261,U_260] :
( ( model(U_261,U_260)
| model(U_261,not(U_260)) )
& ( ~ model(U_261,not(U_260))
| ~ model(U_261,U_260) ) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
( ! [U_265,U_263] :
( model(U_265,U_263)
| model(U_265,not(U_263)) )
& ! [U_264,U_262] :
( ~ model(U_264,not(U_262))
| ~ model(U_264,U_262) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
fof(f_26_4,plain,
( ! [U_263,U_265] :
( model(U_265,U_263)
| model(U_265,not(U_263)) )
& ! [U_262,U_264] :
( ~ model(U_264,not(U_262))
| ~ model(U_264,U_262) ) ),
inference(definitional_conversion,[status(esa)],[f_26_3]) ).
cnf(f_26_5,plain,
( ~ model(U_264,not(U_262))
| ~ model(U_264,U_262) ),
inference(clausify,[status(thm)],[f_26_4]) ).
cnf(f_26_6,plain,
( model(U_265,U_263)
| model(U_265,not(U_263)) ),
inference(clausify,[status(thm)],[f_26_4]) ).
fof(f_27_1,plain,
? [F] :
! [I] : model(I,F),
inference(fof_nnf,[status(thm)],[tautology]) ).
fof(f_27_2,plain,
? [U_267] :
! [U_266] : model(U_266,U_267),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
! [U_266] : model(U_266,sK55),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(U_267,sK55)],[f_27_2]) ).
fof(f_27_4,plain,
! [U_266] : model(U_266,sK55),
inference(definitional_conversion,[status(esa)],[f_27_3]) ).
cnf(f_27_5,plain,
model(U_266,sK55),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,plain,
? [F] :
( ? [I2] : ~ model(I2,F)
& ? [I1] : model(I1,F) ),
inference(fof_nnf,[status(thm)],[satisfiable]) ).
fof(f_28_2,plain,
? [U_270] :
( ? [U_269] : ~ model(U_269,U_270)
& ? [U_268] : model(U_268,U_270) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ? [U_269] : ~ model(U_269,sK56)
& ? [U_268] : model(U_268,sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(U_270,sK56)],[f_28_2]) ).
fof(f_28_4,plain,
( ? [U_269] : ~ model(U_269,sK56)
& model(sK57,sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(U_268,sK57)],[f_28_3]) ).
fof(f_28_5,plain,
( ~ model(sK58,sK56)
& model(sK57,sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(U_269,sK58)],[f_28_4]) ).
fof(f_28_6,plain,
( ~ model(sK58,sK56)
& model(sK57,sK56) ),
inference(definitional_conversion,[status(esa)],[f_28_5]) ).
cnf(f_28_7,plain,
model(sK57,sK56),
inference(clausify,[status(thm)],[f_28_6]) ).
cnf(f_28_8,plain,
~ model(sK58,sK56),
inference(clausify,[status(thm)],[f_28_6]) ).
fof(f_29_1,plain,
? [F] :
! [I] : ~ model(I,F),
inference(fof_nnf,[status(thm)],[contradiction]) ).
fof(f_29_2,plain,
? [U_272] :
! [U_271] : ~ model(U_271,U_272),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
! [U_271] : ~ model(U_271,sK59),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(U_272,sK59)],[f_29_2]) ).
fof(f_29_4,plain,
! [U_271] : ~ model(U_271,sK59),
inference(definitional_conversion,[status(esa)],[f_29_3]) ).
cnf(f_29_5,plain,
~ model(U_271,sK59),
inference(clausify,[status(thm)],[f_29_4]) ).
fof(f_30_1,plain,
? [Ax,C] :
( ? [I2] :
( ~ model(I2,C)
| ~ model(I2,Ax) )
& ? [I1] :
( model(I1,C)
& model(I1,Ax) ) ),
inference(fof_nnf,[status(thm)],[sat_non_taut_pair]) ).
fof(f_30_2,plain,
? [U_276,U_275] :
( ? [U_274] :
( ~ model(U_274,U_275)
| ~ model(U_274,U_276) )
& ? [U_273] :
( model(U_273,U_275)
& model(U_273,U_276) ) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
? [U_276,U_275] :
( ( ? [U_278] : ~ model(U_278,U_275)
| ? [U_277] : ~ model(U_277,U_276) )
& ? [U_273] :
( model(U_273,U_275)
& model(U_273,U_276) ) ),
inference(miniscope,[status(thm)],[f_30_2]) ).
fof(f_30_4,plain,
? [U_275] :
( ( ? [U_278] : ~ model(U_278,U_275)
| ? [U_277] : ~ model(U_277,sK60) )
& ? [U_273] :
( model(U_273,U_275)
& model(U_273,sK60) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(U_276,sK60)],[f_30_3]) ).
fof(f_30_5,plain,
( ( ? [U_278] : ~ model(U_278,sK61)
| ? [U_277] : ~ model(U_277,sK60) )
& ? [U_273] :
( model(U_273,sK61)
& model(U_273,sK60) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(U_275,sK61)],[f_30_4]) ).
fof(f_30_6,plain,
( ( ? [U_278] : ~ model(U_278,sK61)
| ? [U_277] : ~ model(U_277,sK60) )
& model(sK62,sK61)
& model(sK62,sK60) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(U_273,sK62)],[f_30_5]) ).
fof(f_30_7,plain,
( ( ? [U_278] : ~ model(U_278,sK61)
| ~ model(sK63,sK60) )
& model(sK62,sK61)
& model(sK62,sK60) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(U_277,sK63)],[f_30_6]) ).
fof(f_30_8,plain,
( ( ~ model(sK64,sK61)
| ~ model(sK63,sK60) )
& model(sK62,sK61)
& model(sK62,sK60) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(U_278,sK64)],[f_30_7]) ).
fof(f_30_9,plain,
( ( ~ model(sK64,sK61)
| ~ model(sK63,sK60) )
& model(sK62,sK61)
& model(sK62,sK60) ),
inference(definitional_conversion,[status(esa)],[f_30_8]) ).
cnf(f_30_10,plain,
model(sK62,sK60),
inference(clausify,[status(thm)],[f_30_9]) ).
cnf(f_30_11,plain,
model(sK62,sK61),
inference(clausify,[status(thm)],[f_30_9]) ).
cnf(f_30_12,plain,
( ~ model(sK64,sK61)
| ~ model(sK63,sK60) ),
inference(clausify,[status(thm)],[f_30_9]) ).
fof(f_31_1,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(fof_nnf,[status(thm)],[mixed_pair]) ).
fof(f_31_2,plain,
? [U_284,U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,U_284) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,U_284) )
& ? [U_279] : model(U_279,U_284) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
? [U_284] :
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,U_284) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,U_284) ) )
& ? [U_279] : model(U_279,U_284) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
fof(f_31_4,plain,
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,sK65) ) )
& ? [U_279] : model(U_279,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(U_284,sK65)],[f_31_3]) ).
fof(f_31_5,plain,
( ? [U_283] :
( ? [U_282] : ~ model(U_282,U_283)
& ? [U_281] :
( model(U_281,U_283)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,U_283)
| ~ model(U_280,sK65) ) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(U_279,sK66)],[f_31_4]) ).
fof(f_31_6,plain,
( ? [U_282] : ~ model(U_282,sK67)
& ? [U_281] :
( model(U_281,sK67)
& ~ model(U_281,sK65) )
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(U_283,sK67)],[f_31_5]) ).
fof(f_31_7,plain,
( ? [U_282] : ~ model(U_282,sK67)
& model(sK68,sK67)
& ~ model(sK68,sK65)
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(U_281,sK68)],[f_31_6]) ).
fof(f_31_8,plain,
( ~ model(sK69,sK67)
& model(sK68,sK67)
& ~ model(sK68,sK65)
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(U_282,sK69)],[f_31_7]) ).
fof(f_31_9,plain,
( ~ model(sK69,sK67)
& model(sK68,sK67)
& ~ model(sK68,sK65)
& ! [U_280] :
( model(U_280,sK67)
| ~ model(U_280,sK65) )
& model(sK66,sK65) ),
inference(definitional_conversion,[status(esa)],[f_31_8]) ).
cnf(f_31_10,plain,
model(sK66,sK65),
inference(clausify,[status(thm)],[f_31_9]) ).
cnf(f_31_11,plain,
( model(U_280,sK67)
| ~ model(U_280,sK65) ),
inference(clausify,[status(thm)],[f_31_9]) ).
cnf(f_31_12,plain,
~ model(sK68,sK65),
inference(clausify,[status(thm)],[f_31_9]) ).
cnf(f_31_13,plain,
model(sK68,sK67),
inference(clausify,[status(thm)],[f_31_9]) ).
cnf(f_31_14,plain,
~ model(sK69,sK67),
inference(clausify,[status(thm)],[f_31_9]) ).
fof(f_32_1,plain,
? [I1,Ax,C] :
( ? [I2] : model(I2,C)
& ~ model(I1,C)
& model(I1,Ax) ),
inference(fof_nnf,[status(thm)],[non_thm_spt]) ).
fof(f_32_2,plain,
? [U_288,U_287,U_286] :
( ? [U_285] : model(U_285,U_286)
& ~ model(U_288,U_286)
& model(U_288,U_287) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
? [U_288] :
( ? [U_287] : model(U_288,U_287)
& ? [U_286] :
( ? [U_285] : model(U_285,U_286)
& ~ model(U_288,U_286) ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
fof(f_32_4,plain,
( ? [U_287] : model(sK70,U_287)
& ? [U_286] :
( ? [U_285] : model(U_285,U_286)
& ~ model(sK70,U_286) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(U_288,sK70)],[f_32_3]) ).
fof(f_32_5,plain,
( ? [U_287] : model(sK70,U_287)
& ? [U_285] : model(U_285,sK71)
& ~ model(sK70,sK71) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71]),skolemize(U_286,sK71)],[f_32_4]) ).
fof(f_32_6,plain,
( ? [U_287] : model(sK70,U_287)
& model(sK72,sK71)
& ~ model(sK70,sK71) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72]),skolemize(U_285,sK72)],[f_32_5]) ).
fof(f_32_7,plain,
( model(sK70,sK73)
& model(sK72,sK71)
& ~ model(sK70,sK71) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73]),skolemize(U_287,sK73)],[f_32_6]) ).
fof(f_32_8,plain,
( model(sK70,sK73)
& model(sK72,sK71)
& ~ model(sK70,sK71) ),
inference(definitional_conversion,[status(esa)],[f_32_7]) ).
cnf(f_32_9,plain,
~ model(sK70,sK71),
inference(clausify,[status(thm)],[f_32_8]) ).
cnf(f_32_10,plain,
model(sK72,sK71),
inference(clausify,[status(thm)],[f_32_8]) ).
cnf(f_32_11,plain,
model(sK70,sK73),
inference(clausify,[status(thm)],[f_32_8]) ).
fof(f_33_1,negated_conjecture,
~ isa(wec,thm),
inference(negate,[status(cth)],[isa_wec_thm]) ).
fof(f_33_2,negated_conjecture,
~ isa(wec,thm),
inference(definitional_conversion,[status(esa)],[f_33_1]) ).
cnf(f_33_3,negated_conjecture,
~ isa(wec,thm),
inference(clausify,[status(thm)],[f_33_2]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS188+1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 19 12:18:40 UTC 2026
% 0.08/0.35 % CPUTime :
% 36.35/36.67 % SZS status Theorem for theBenchmark
% 36.35/36.67 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------