%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET803+4 : TPTP v9.3.1. Released v3.2.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 : n001.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:57:28 AM UTC 2026
% Result : Theorem 24.56s 24.80s
% Output : Proof 24.66s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(order,axiom,
! [R,E] :
( order(R,E)
<=> ( ! [X,Y,Z] :
( ( member(Z,E)
& member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,Z)
& apply(R,X,Y) )
=> apply(R,X,Z) ) )
& ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ( ( apply(R,Y,X)
& apply(R,X,Y) )
=> X = Y ) )
& ! [X] :
( member(X,E)
=> apply(R,X,X) ) ) ),
file('SET006+3.ax',order) ).
fof(total_order,axiom,
! [R,E] :
( total_order(R,E)
<=> ( ! [X,Y] :
( ( member(Y,E)
& member(X,E) )
=> ( apply(R,Y,X)
| apply(R,X,Y) ) )
& order(R,E) ) ),
file('SET006+3.ax',total_order) ).
fof(upper_bound,axiom,
! [R,E,M] :
( upper_bound(M,R,E)
<=> ! [X] :
( member(X,E)
=> apply(R,X,M) ) ),
file('SET006+3.ax',upper_bound) ).
fof(lower_bound,axiom,
! [R,E,M] :
( lower_bound(M,R,E)
<=> ! [X] :
( member(X,E)
=> apply(R,M,X) ) ),
file('SET006+3.ax',lower_bound) ).
fof(greatest,axiom,
! [R,E,M] :
( greatest(M,R,E)
<=> ( ! [X] :
( member(X,E)
=> apply(R,X,M) )
& member(M,E) ) ),
file('SET006+3.ax',greatest) ).
fof(least,axiom,
! [R,E,M] :
( least(M,R,E)
<=> ( ! [X] :
( member(X,E)
=> apply(R,M,X) )
& member(M,E) ) ),
file('SET006+3.ax',least) ).
fof(max,axiom,
! [R,E,M] :
( max(M,R,E)
<=> ( ! [X] :
( ( apply(R,M,X)
& member(X,E) )
=> M = X )
& member(M,E) ) ),
file('SET006+3.ax',max) ).
fof(min,axiom,
! [R,E,M] :
( min(M,R,E)
<=> ( ! [X] :
( ( apply(R,X,M)
& member(X,E) )
=> M = X )
& member(M,E) ) ),
file('SET006+3.ax',min) ).
fof(least_upper_bound,axiom,
! [A,X,R,E] :
( least_upper_bound(A,X,R,E)
<=> ( ! [M] :
( ( upper_bound(M,R,X)
& member(M,E) )
=> apply(R,A,M) )
& upper_bound(A,R,X)
& member(A,X) ) ),
file('SET006+3.ax',least_upper_bound) ).
fof(greatest_lower_bound,axiom,
! [A,X,R,E] :
( greatest_lower_bound(A,X,R,E)
<=> ( ! [M] :
( ( lower_bound(M,R,X)
& member(M,E) )
=> apply(R,M,A) )
& lower_bound(A,R,X)
& member(A,X) ) ),
file('SET006+3.ax',greatest_lower_bound) ).
fof(thIV15,conjecture,
! [R,E] :
( order(R,E)
=> ! [M1,M2] :
( ( M1 != M2
& max(M2,R,E)
& max(M1,R,E) )
=> ~ ? [M] : greatest(M,R,E) ) ),
file('theBenchmark.p',thIV15) ).
fof(f_1_1,plain,
! [R,E] :
( ( order(R,E)
| ? [X,Y,Z] :
( ~ apply(R,X,Z)
& apply(R,Y,Z)
& apply(R,X,Y)
& member(Z,E)
& member(Y,E)
& member(X,E) )
| ? [X,Y] :
( X != Y
& apply(R,Y,X)
& apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ? [X] :
( ~ apply(R,X,X)
& member(X,E) ) )
& ( ( ! [X,Y,Z] :
( apply(R,X,Z)
| ~ apply(R,Y,Z)
| ~ apply(R,X,Y)
| ~ member(Z,E)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X,Y] :
( X = Y
| ~ apply(R,Y,X)
| ~ apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& ! [X] :
( apply(R,X,X)
| ~ member(X,E) ) )
| ~ order(R,E) ) ),
inference(fof_nnf,[status(thm)],[order]) ).
fof(f_1_2,plain,
! [U_13,U_12] :
( ( order(U_13,U_12)
| ? [U_11,U_10,U_9] :
( ~ apply(U_13,U_11,U_9)
& apply(U_13,U_10,U_9)
& apply(U_13,U_11,U_10)
& member(U_9,U_12)
& member(U_10,U_12)
& member(U_11,U_12) )
| ? [U_8,U_7] :
( U_8 != U_7
& apply(U_13,U_7,U_8)
& apply(U_13,U_8,U_7)
& member(U_7,U_12)
& member(U_8,U_12) )
| ? [U_6] :
( ~ apply(U_13,U_6,U_6)
& member(U_6,U_12) ) )
& ( ( ! [U_5,U_4,U_3] :
( apply(U_13,U_5,U_3)
| ~ apply(U_13,U_4,U_3)
| ~ apply(U_13,U_5,U_4)
| ~ member(U_3,U_12)
| ~ member(U_4,U_12)
| ~ member(U_5,U_12) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_13,U_1,U_2)
| ~ apply(U_13,U_2,U_1)
| ~ member(U_1,U_12)
| ~ member(U_2,U_12) )
& ! [U_0] :
( apply(U_13,U_0,U_0)
| ~ member(U_0,U_12) ) )
| ~ order(U_13,U_12) ) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_11,U_10,U_9] :
( ~ apply(U_17,U_11,U_9)
& apply(U_17,U_10,U_9)
& apply(U_17,U_11,U_10)
& member(U_9,U_15)
& member(U_10,U_15)
& member(U_11,U_15) )
| ? [U_8,U_7] :
( U_8 != U_7
& apply(U_17,U_7,U_8)
& apply(U_17,U_8,U_7)
& member(U_7,U_15)
& member(U_8,U_15) )
| ? [U_6] :
( ~ apply(U_17,U_6,U_6)
& member(U_6,U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
fof(f_1_4,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_11,U_10,U_9] :
( ~ apply(U_17,U_11,U_9)
& apply(U_17,U_10,U_9)
& apply(U_17,U_11,U_10)
& member(U_9,U_15)
& member(U_10,U_15)
& member(U_11,U_15) )
| ? [U_8,U_7] :
( U_8 != U_7
& apply(U_17,U_7,U_8)
& apply(U_17,U_8,U_7)
& member(U_7,U_15)
& member(U_8,U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_6,sK1(U_17,U_15))],[f_1_3]) ).
fof(f_1_5,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_11,U_10,U_9] :
( ~ apply(U_17,U_11,U_9)
& apply(U_17,U_10,U_9)
& apply(U_17,U_11,U_10)
& member(U_9,U_15)
& member(U_10,U_15)
& member(U_11,U_15) )
| ? [U_7] :
( sK2(U_17,U_15) != U_7
& apply(U_17,U_7,sK2(U_17,U_15))
& apply(U_17,sK2(U_17,U_15),U_7)
& member(U_7,U_15)
& member(sK2(U_17,U_15),U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_8,sK2(U_17,U_15))],[f_1_4]) ).
fof(f_1_6,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_11,U_10,U_9] :
( ~ apply(U_17,U_11,U_9)
& apply(U_17,U_10,U_9)
& apply(U_17,U_11,U_10)
& member(U_9,U_15)
& member(U_10,U_15)
& member(U_11,U_15) )
| ( sK2(U_17,U_15) != sK3(U_17,U_15)
& apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
& apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
& member(sK3(U_17,U_15),U_15)
& member(sK2(U_17,U_15),U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_7,sK3(U_17,U_15))],[f_1_5]) ).
fof(f_1_7,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_10,U_9] :
( ~ apply(U_17,sK4(U_17,U_15),U_9)
& apply(U_17,U_10,U_9)
& apply(U_17,sK4(U_17,U_15),U_10)
& member(U_9,U_15)
& member(U_10,U_15)
& member(sK4(U_17,U_15),U_15) )
| ( sK2(U_17,U_15) != sK3(U_17,U_15)
& apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
& apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
& member(sK3(U_17,U_15),U_15)
& member(sK2(U_17,U_15),U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_11,sK4(U_17,U_15))],[f_1_6]) ).
fof(f_1_8,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ? [U_9] :
( ~ apply(U_17,sK4(U_17,U_15),U_9)
& apply(U_17,sK5(U_17,U_15),U_9)
& apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
& member(U_9,U_15)
& member(sK5(U_17,U_15),U_15)
& member(sK4(U_17,U_15),U_15) )
| ( sK2(U_17,U_15) != sK3(U_17,U_15)
& apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
& apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
& member(sK3(U_17,U_15),U_15)
& member(sK2(U_17,U_15),U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_10,sK5(U_17,U_15))],[f_1_7]) ).
fof(f_1_9,plain,
( ! [U_17,U_15] :
( order(U_17,U_15)
| ( ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
& apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
& apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
& member(sK6(U_17,U_15),U_15)
& member(sK5(U_17,U_15),U_15)
& member(sK4(U_17,U_15),U_15) )
| ( sK2(U_17,U_15) != sK3(U_17,U_15)
& apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
& apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
& member(sK3(U_17,U_15),U_15)
& member(sK2(U_17,U_15),U_15) )
| ( ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
& member(sK1(U_17,U_15),U_15) ) )
& ! [U_16,U_14] :
( ( ! [U_5,U_4,U_3] :
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14) )
& ! [U_2,U_1] :
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14) )
& ! [U_0] :
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14) ) )
| ~ order(U_16,U_14) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_9,sK6(U_17,U_15))],[f_1_8]) ).
cnf(f_1_10,plain,
( apply(U_16,U_0,U_0)
| ~ member(U_0,U_14)
| ~ order(U_16,U_14) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_11,plain,
( U_2 = U_1
| ~ apply(U_16,U_1,U_2)
| ~ apply(U_16,U_2,U_1)
| ~ member(U_1,U_14)
| ~ member(U_2,U_14)
| ~ order(U_16,U_14) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_12,plain,
( apply(U_16,U_5,U_3)
| ~ apply(U_16,U_4,U_3)
| ~ apply(U_16,U_5,U_4)
| ~ member(U_3,U_14)
| ~ member(U_4,U_14)
| ~ member(U_5,U_14)
| ~ order(U_16,U_14) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_13,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_14,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_15,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_16,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_17,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_18,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_19,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_20,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_21,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_22,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_23,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_24,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_25,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_26,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_27,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_28,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_29,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_30,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_31,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_32,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK4(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_33,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_34,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_35,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_36,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_37,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK5(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_38,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_39,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_40,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_41,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_42,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| member(sK6(U_17,U_15),U_15)
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_43,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_44,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_45,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_46,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_47,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_48,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_49,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_50,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_51,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_52,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_53,plain,
( member(sK2(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_54,plain,
( member(sK3(U_17,U_15),U_15)
| member(sK1(U_17,U_15),U_15)
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_55,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_56,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| member(sK1(U_17,U_15),U_15)
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_57,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| member(sK1(U_17,U_15),U_15)
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_58,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_59,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_60,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_61,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_62,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK4(U_17,U_15),sK5(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_63,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_64,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_65,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_66,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_67,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| apply(U_17,sK5(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_68,plain,
( member(sK2(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_69,plain,
( member(sK3(U_17,U_15),U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_70,plain,
( apply(U_17,sK2(U_17,U_15),sK3(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_71,plain,
( apply(U_17,sK3(U_17,U_15),sK2(U_17,U_15))
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
cnf(f_1_72,plain,
( sK2(U_17,U_15) != sK3(U_17,U_15)
| ~ apply(U_17,sK1(U_17,U_15),sK1(U_17,U_15))
| ~ apply(U_17,sK4(U_17,U_15),sK6(U_17,U_15))
| order(U_17,U_15) ),
inference(clausify,[status(thm)],[f_1_9]) ).
fof(f_2_1,plain,
! [R,E] :
( ( total_order(R,E)
| ? [X,Y] :
( ~ apply(R,Y,X)
& ~ apply(R,X,Y)
& member(Y,E)
& member(X,E) )
| ~ order(R,E) )
& ( ( ! [X,Y] :
( apply(R,Y,X)
| apply(R,X,Y)
| ~ member(Y,E)
| ~ member(X,E) )
& order(R,E) )
| ~ total_order(R,E) ) ),
inference(fof_nnf,[status(thm)],[total_order]) ).
fof(f_2_2,plain,
! [U_23,U_22] :
( ( total_order(U_23,U_22)
| ? [U_21,U_20] :
( ~ apply(U_23,U_20,U_21)
& ~ apply(U_23,U_21,U_20)
& member(U_20,U_22)
& member(U_21,U_22) )
| ~ order(U_23,U_22) )
& ( ( ! [U_19,U_18] :
( apply(U_23,U_18,U_19)
| apply(U_23,U_19,U_18)
| ~ member(U_18,U_22)
| ~ member(U_19,U_22) )
& order(U_23,U_22) )
| ~ total_order(U_23,U_22) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_27,U_25] :
( total_order(U_27,U_25)
| ? [U_21,U_20] :
( ~ apply(U_27,U_20,U_21)
& ~ apply(U_27,U_21,U_20)
& member(U_20,U_25)
& member(U_21,U_25) )
| ~ order(U_27,U_25) )
& ! [U_26,U_24] :
( ( ! [U_19,U_18] :
( apply(U_26,U_18,U_19)
| apply(U_26,U_19,U_18)
| ~ member(U_18,U_24)
| ~ member(U_19,U_24) )
& order(U_26,U_24) )
| ~ total_order(U_26,U_24) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
fof(f_2_4,plain,
( ! [U_27,U_25] :
( total_order(U_27,U_25)
| ? [U_20] :
( ~ apply(U_27,U_20,sK7(U_27,U_25))
& ~ apply(U_27,sK7(U_27,U_25),U_20)
& member(U_20,U_25)
& member(sK7(U_27,U_25),U_25) )
| ~ order(U_27,U_25) )
& ! [U_26,U_24] :
( ( ! [U_19,U_18] :
( apply(U_26,U_18,U_19)
| apply(U_26,U_19,U_18)
| ~ member(U_18,U_24)
| ~ member(U_19,U_24) )
& order(U_26,U_24) )
| ~ total_order(U_26,U_24) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_21,sK7(U_27,U_25))],[f_2_3]) ).
fof(f_2_5,plain,
( ! [U_27,U_25] :
( total_order(U_27,U_25)
| ( ~ apply(U_27,sK8(U_27,U_25),sK7(U_27,U_25))
& ~ apply(U_27,sK7(U_27,U_25),sK8(U_27,U_25))
& member(sK8(U_27,U_25),U_25)
& member(sK7(U_27,U_25),U_25) )
| ~ order(U_27,U_25) )
& ! [U_26,U_24] :
( ( ! [U_19,U_18] :
( apply(U_26,U_18,U_19)
| apply(U_26,U_19,U_18)
| ~ member(U_18,U_24)
| ~ member(U_19,U_24) )
& order(U_26,U_24) )
| ~ total_order(U_26,U_24) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_20,sK8(U_27,U_25))],[f_2_4]) ).
cnf(f_2_6,plain,
( order(U_26,U_24)
| ~ total_order(U_26,U_24) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_7,plain,
( apply(U_26,U_18,U_19)
| apply(U_26,U_19,U_18)
| ~ member(U_18,U_24)
| ~ member(U_19,U_24)
| ~ total_order(U_26,U_24) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_8,plain,
( member(sK7(U_27,U_25),U_25)
| ~ order(U_27,U_25)
| total_order(U_27,U_25) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_9,plain,
( member(sK8(U_27,U_25),U_25)
| ~ order(U_27,U_25)
| total_order(U_27,U_25) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_10,plain,
( ~ apply(U_27,sK7(U_27,U_25),sK8(U_27,U_25))
| ~ order(U_27,U_25)
| total_order(U_27,U_25) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_11,plain,
( ~ apply(U_27,sK8(U_27,U_25),sK7(U_27,U_25))
| ~ order(U_27,U_25)
| total_order(U_27,U_25) ),
inference(clausify,[status(thm)],[f_2_5]) ).
fof(f_3_1,plain,
! [R,E,M] :
( ( upper_bound(M,R,E)
| ? [X] :
( ~ apply(R,X,M)
& member(X,E) ) )
& ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
| ~ upper_bound(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[upper_bound]) ).
fof(f_3_2,plain,
! [U_32,U_31,U_30] :
( ( upper_bound(U_30,U_32,U_31)
| ? [U_29] :
( ~ apply(U_32,U_29,U_30)
& member(U_29,U_31) ) )
& ( ! [U_28] :
( apply(U_32,U_28,U_30)
| ~ member(U_28,U_31) )
| ~ upper_bound(U_30,U_32,U_31) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_38,U_36,U_34] :
( upper_bound(U_34,U_38,U_36)
| ? [U_29] :
( ~ apply(U_38,U_29,U_34)
& member(U_29,U_36) ) )
& ! [U_37,U_35,U_33] :
( ! [U_28] :
( apply(U_37,U_28,U_33)
| ~ member(U_28,U_35) )
| ~ upper_bound(U_33,U_37,U_35) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_38,U_36,U_34] :
( upper_bound(U_34,U_38,U_36)
| ( ~ apply(U_38,sK9(U_38,U_36,U_34),U_34)
& member(sK9(U_38,U_36,U_34),U_36) ) )
& ! [U_37,U_35,U_33] :
( ! [U_28] :
( apply(U_37,U_28,U_33)
| ~ member(U_28,U_35) )
| ~ upper_bound(U_33,U_37,U_35) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_29,sK9(U_38,U_36,U_34))],[f_3_3]) ).
cnf(f_3_5,plain,
( apply(U_37,U_28,U_33)
| ~ member(U_28,U_35)
| ~ upper_bound(U_33,U_37,U_35) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_6,plain,
( member(sK9(U_38,U_36,U_34),U_36)
| upper_bound(U_34,U_38,U_36) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_7,plain,
( ~ apply(U_38,sK9(U_38,U_36,U_34),U_34)
| upper_bound(U_34,U_38,U_36) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_4_1,plain,
! [R,E,M] :
( ( lower_bound(M,R,E)
| ? [X] :
( ~ apply(R,M,X)
& member(X,E) ) )
& ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
| ~ lower_bound(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[lower_bound]) ).
fof(f_4_2,plain,
! [U_43,U_42,U_41] :
( ( lower_bound(U_41,U_43,U_42)
| ? [U_40] :
( ~ apply(U_43,U_41,U_40)
& member(U_40,U_42) ) )
& ( ! [U_39] :
( apply(U_43,U_41,U_39)
| ~ member(U_39,U_42) )
| ~ lower_bound(U_41,U_43,U_42) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_49,U_47,U_45] :
( lower_bound(U_45,U_49,U_47)
| ? [U_40] :
( ~ apply(U_49,U_45,U_40)
& member(U_40,U_47) ) )
& ! [U_48,U_46,U_44] :
( ! [U_39] :
( apply(U_48,U_44,U_39)
| ~ member(U_39,U_46) )
| ~ lower_bound(U_44,U_48,U_46) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
( ! [U_49,U_47,U_45] :
( lower_bound(U_45,U_49,U_47)
| ( ~ apply(U_49,U_45,sK10(U_49,U_47,U_45))
& member(sK10(U_49,U_47,U_45),U_47) ) )
& ! [U_48,U_46,U_44] :
( ! [U_39] :
( apply(U_48,U_44,U_39)
| ~ member(U_39,U_46) )
| ~ lower_bound(U_44,U_48,U_46) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_40,sK10(U_49,U_47,U_45))],[f_4_3]) ).
cnf(f_4_5,plain,
( apply(U_48,U_44,U_39)
| ~ member(U_39,U_46)
| ~ lower_bound(U_44,U_48,U_46) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_6,plain,
( member(sK10(U_49,U_47,U_45),U_47)
| lower_bound(U_45,U_49,U_47) ),
inference(clausify,[status(thm)],[f_4_4]) ).
cnf(f_4_7,plain,
( ~ apply(U_49,U_45,sK10(U_49,U_47,U_45))
| lower_bound(U_45,U_49,U_47) ),
inference(clausify,[status(thm)],[f_4_4]) ).
fof(f_5_1,plain,
! [R,E,M] :
( ( greatest(M,R,E)
| ? [X] :
( ~ apply(R,X,M)
& member(X,E) )
| ~ member(M,E) )
& ( ( ! [X] :
( apply(R,X,M)
| ~ member(X,E) )
& member(M,E) )
| ~ greatest(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[greatest]) ).
fof(f_5_2,plain,
! [U_54,U_53,U_52] :
( ( greatest(U_52,U_54,U_53)
| ? [U_51] :
( ~ apply(U_54,U_51,U_52)
& member(U_51,U_53) )
| ~ member(U_52,U_53) )
& ( ( ! [U_50] :
( apply(U_54,U_50,U_52)
| ~ member(U_50,U_53) )
& member(U_52,U_53) )
| ~ greatest(U_52,U_54,U_53) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_60,U_58,U_56] :
( greatest(U_56,U_60,U_58)
| ? [U_51] :
( ~ apply(U_60,U_51,U_56)
& member(U_51,U_58) )
| ~ member(U_56,U_58) )
& ! [U_59,U_57,U_55] :
( ( ! [U_50] :
( apply(U_59,U_50,U_55)
| ~ member(U_50,U_57) )
& member(U_55,U_57) )
| ~ greatest(U_55,U_59,U_57) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_60,U_58,U_56] :
( greatest(U_56,U_60,U_58)
| ( ~ apply(U_60,sK11(U_60,U_58,U_56),U_56)
& member(sK11(U_60,U_58,U_56),U_58) )
| ~ member(U_56,U_58) )
& ! [U_59,U_57,U_55] :
( ( ! [U_50] :
( apply(U_59,U_50,U_55)
| ~ member(U_50,U_57) )
& member(U_55,U_57) )
| ~ greatest(U_55,U_59,U_57) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_51,sK11(U_60,U_58,U_56))],[f_5_3]) ).
cnf(f_5_5,plain,
( member(U_55,U_57)
| ~ greatest(U_55,U_59,U_57) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( apply(U_59,U_50,U_55)
| ~ member(U_50,U_57)
| ~ greatest(U_55,U_59,U_57) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( member(sK11(U_60,U_58,U_56),U_58)
| ~ member(U_56,U_58)
| greatest(U_56,U_60,U_58) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_8,plain,
( ~ apply(U_60,sK11(U_60,U_58,U_56),U_56)
| ~ member(U_56,U_58)
| greatest(U_56,U_60,U_58) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [R,E,M] :
( ( least(M,R,E)
| ? [X] :
( ~ apply(R,M,X)
& member(X,E) )
| ~ member(M,E) )
& ( ( ! [X] :
( apply(R,M,X)
| ~ member(X,E) )
& member(M,E) )
| ~ least(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[least]) ).
fof(f_6_2,plain,
! [U_65,U_64,U_63] :
( ( least(U_63,U_65,U_64)
| ? [U_62] :
( ~ apply(U_65,U_63,U_62)
& member(U_62,U_64) )
| ~ member(U_63,U_64) )
& ( ( ! [U_61] :
( apply(U_65,U_63,U_61)
| ~ member(U_61,U_64) )
& member(U_63,U_64) )
| ~ least(U_63,U_65,U_64) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_71,U_69,U_67] :
( least(U_67,U_71,U_69)
| ? [U_62] :
( ~ apply(U_71,U_67,U_62)
& member(U_62,U_69) )
| ~ member(U_67,U_69) )
& ! [U_70,U_68,U_66] :
( ( ! [U_61] :
( apply(U_70,U_66,U_61)
| ~ member(U_61,U_68) )
& member(U_66,U_68) )
| ~ least(U_66,U_70,U_68) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_71,U_69,U_67] :
( least(U_67,U_71,U_69)
| ( ~ apply(U_71,U_67,sK12(U_71,U_69,U_67))
& member(sK12(U_71,U_69,U_67),U_69) )
| ~ member(U_67,U_69) )
& ! [U_70,U_68,U_66] :
( ( ! [U_61] :
( apply(U_70,U_66,U_61)
| ~ member(U_61,U_68) )
& member(U_66,U_68) )
| ~ least(U_66,U_70,U_68) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_62,sK12(U_71,U_69,U_67))],[f_6_3]) ).
cnf(f_6_5,plain,
( member(U_66,U_68)
| ~ least(U_66,U_70,U_68) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_6,plain,
( apply(U_70,U_66,U_61)
| ~ member(U_61,U_68)
| ~ least(U_66,U_70,U_68) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_7,plain,
( member(sK12(U_71,U_69,U_67),U_69)
| ~ member(U_67,U_69)
| least(U_67,U_71,U_69) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_8,plain,
( ~ apply(U_71,U_67,sK12(U_71,U_69,U_67))
| ~ member(U_67,U_69)
| least(U_67,U_71,U_69) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [R,E,M] :
( ( max(M,R,E)
| ? [X] :
( M != X
& apply(R,M,X)
& member(X,E) )
| ~ member(M,E) )
& ( ( ! [X] :
( M = X
| ~ apply(R,M,X)
| ~ member(X,E) )
& member(M,E) )
| ~ max(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[max]) ).
fof(f_7_2,plain,
! [U_76,U_75,U_74] :
( ( max(U_74,U_76,U_75)
| ? [U_73] :
( U_74 != U_73
& apply(U_76,U_74,U_73)
& member(U_73,U_75) )
| ~ member(U_74,U_75) )
& ( ( ! [U_72] :
( U_74 = U_72
| ~ apply(U_76,U_74,U_72)
| ~ member(U_72,U_75) )
& member(U_74,U_75) )
| ~ max(U_74,U_76,U_75) ) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
( ! [U_82,U_80,U_78] :
( max(U_78,U_82,U_80)
| ? [U_73] :
( U_78 != U_73
& apply(U_82,U_78,U_73)
& member(U_73,U_80) )
| ~ member(U_78,U_80) )
& ! [U_81,U_79,U_77] :
( ( ! [U_72] :
( U_77 = U_72
| ~ apply(U_81,U_77,U_72)
| ~ member(U_72,U_79) )
& member(U_77,U_79) )
| ~ max(U_77,U_81,U_79) ) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_82,U_80,U_78] :
( max(U_78,U_82,U_80)
| ( U_78 != sK13(U_82,U_80,U_78)
& apply(U_82,U_78,sK13(U_82,U_80,U_78))
& member(sK13(U_82,U_80,U_78),U_80) )
| ~ member(U_78,U_80) )
& ! [U_81,U_79,U_77] :
( ( ! [U_72] :
( U_77 = U_72
| ~ apply(U_81,U_77,U_72)
| ~ member(U_72,U_79) )
& member(U_77,U_79) )
| ~ max(U_77,U_81,U_79) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_73,sK13(U_82,U_80,U_78))],[f_7_3]) ).
cnf(f_7_5,plain,
( member(U_77,U_79)
| ~ max(U_77,U_81,U_79) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_6,plain,
( U_77 = U_72
| ~ apply(U_81,U_77,U_72)
| ~ member(U_72,U_79)
| ~ max(U_77,U_81,U_79) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_7,plain,
( member(sK13(U_82,U_80,U_78),U_80)
| ~ member(U_78,U_80)
| max(U_78,U_82,U_80) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_8,plain,
( apply(U_82,U_78,sK13(U_82,U_80,U_78))
| ~ member(U_78,U_80)
| max(U_78,U_82,U_80) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_9,plain,
( U_78 != sK13(U_82,U_80,U_78)
| ~ member(U_78,U_80)
| max(U_78,U_82,U_80) ),
inference(clausify,[status(thm)],[f_7_4]) ).
fof(f_8_1,plain,
! [R,E,M] :
( ( min(M,R,E)
| ? [X] :
( M != X
& apply(R,X,M)
& member(X,E) )
| ~ member(M,E) )
& ( ( ! [X] :
( M = X
| ~ apply(R,X,M)
| ~ member(X,E) )
& member(M,E) )
| ~ min(M,R,E) ) ),
inference(fof_nnf,[status(thm)],[min]) ).
fof(f_8_2,plain,
! [U_87,U_86,U_85] :
( ( min(U_85,U_87,U_86)
| ? [U_84] :
( U_85 != U_84
& apply(U_87,U_84,U_85)
& member(U_84,U_86) )
| ~ member(U_85,U_86) )
& ( ( ! [U_83] :
( U_85 = U_83
| ~ apply(U_87,U_83,U_85)
| ~ member(U_83,U_86) )
& member(U_85,U_86) )
| ~ min(U_85,U_87,U_86) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_93,U_91,U_89] :
( min(U_89,U_93,U_91)
| ? [U_84] :
( U_89 != U_84
& apply(U_93,U_84,U_89)
& member(U_84,U_91) )
| ~ member(U_89,U_91) )
& ! [U_92,U_90,U_88] :
( ( ! [U_83] :
( U_88 = U_83
| ~ apply(U_92,U_83,U_88)
| ~ member(U_83,U_90) )
& member(U_88,U_90) )
| ~ min(U_88,U_92,U_90) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
( ! [U_93,U_91,U_89] :
( min(U_89,U_93,U_91)
| ( U_89 != sK14(U_93,U_91,U_89)
& apply(U_93,sK14(U_93,U_91,U_89),U_89)
& member(sK14(U_93,U_91,U_89),U_91) )
| ~ member(U_89,U_91) )
& ! [U_92,U_90,U_88] :
( ( ! [U_83] :
( U_88 = U_83
| ~ apply(U_92,U_83,U_88)
| ~ member(U_83,U_90) )
& member(U_88,U_90) )
| ~ min(U_88,U_92,U_90) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_84,sK14(U_93,U_91,U_89))],[f_8_3]) ).
cnf(f_8_5,plain,
( member(U_88,U_90)
| ~ min(U_88,U_92,U_90) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_6,plain,
( U_88 = U_83
| ~ apply(U_92,U_83,U_88)
| ~ member(U_83,U_90)
| ~ min(U_88,U_92,U_90) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_7,plain,
( member(sK14(U_93,U_91,U_89),U_91)
| ~ member(U_89,U_91)
| min(U_89,U_93,U_91) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_8,plain,
( apply(U_93,sK14(U_93,U_91,U_89),U_89)
| ~ member(U_89,U_91)
| min(U_89,U_93,U_91) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_9,plain,
( U_89 != sK14(U_93,U_91,U_89)
| ~ member(U_89,U_91)
| min(U_89,U_93,U_91) ),
inference(clausify,[status(thm)],[f_8_4]) ).
fof(f_9_1,plain,
! [A,X,R,E] :
( ( least_upper_bound(A,X,R,E)
| ? [M] :
( ~ apply(R,A,M)
& upper_bound(M,R,X)
& member(M,E) )
| ~ upper_bound(A,R,X)
| ~ member(A,X) )
& ( ( ! [M] :
( apply(R,A,M)
| ~ upper_bound(M,R,X)
| ~ member(M,E) )
& upper_bound(A,R,X)
& member(A,X) )
| ~ least_upper_bound(A,X,R,E) ) ),
inference(fof_nnf,[status(thm)],[least_upper_bound]) ).
fof(f_9_2,plain,
! [U_99,U_98,U_97,U_96] :
( ( least_upper_bound(U_99,U_98,U_97,U_96)
| ? [U_95] :
( ~ apply(U_97,U_99,U_95)
& upper_bound(U_95,U_97,U_98)
& member(U_95,U_96) )
| ~ upper_bound(U_99,U_97,U_98)
| ~ member(U_99,U_98) )
& ( ( ! [U_94] :
( apply(U_97,U_99,U_94)
| ~ upper_bound(U_94,U_97,U_98)
| ~ member(U_94,U_96) )
& upper_bound(U_99,U_97,U_98)
& member(U_99,U_98) )
| ~ least_upper_bound(U_99,U_98,U_97,U_96) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_107,U_105,U_103,U_101] :
( least_upper_bound(U_107,U_105,U_103,U_101)
| ? [U_95] :
( ~ apply(U_103,U_107,U_95)
& upper_bound(U_95,U_103,U_105)
& member(U_95,U_101) )
| ~ upper_bound(U_107,U_103,U_105)
| ~ member(U_107,U_105) )
& ! [U_106,U_104,U_102,U_100] :
( ( ! [U_94] :
( apply(U_102,U_106,U_94)
| ~ upper_bound(U_94,U_102,U_104)
| ~ member(U_94,U_100) )
& upper_bound(U_106,U_102,U_104)
& member(U_106,U_104) )
| ~ least_upper_bound(U_106,U_104,U_102,U_100) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
( ! [U_107,U_105,U_103,U_101] :
( least_upper_bound(U_107,U_105,U_103,U_101)
| ( ~ apply(U_103,U_107,sK15(U_107,U_105,U_103,U_101))
& upper_bound(sK15(U_107,U_105,U_103,U_101),U_103,U_105)
& member(sK15(U_107,U_105,U_103,U_101),U_101) )
| ~ upper_bound(U_107,U_103,U_105)
| ~ member(U_107,U_105) )
& ! [U_106,U_104,U_102,U_100] :
( ( ! [U_94] :
( apply(U_102,U_106,U_94)
| ~ upper_bound(U_94,U_102,U_104)
| ~ member(U_94,U_100) )
& upper_bound(U_106,U_102,U_104)
& member(U_106,U_104) )
| ~ least_upper_bound(U_106,U_104,U_102,U_100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_95,sK15(U_107,U_105,U_103,U_101))],[f_9_3]) ).
cnf(f_9_5,plain,
( member(U_106,U_104)
| ~ least_upper_bound(U_106,U_104,U_102,U_100) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_6,plain,
( upper_bound(U_106,U_102,U_104)
| ~ least_upper_bound(U_106,U_104,U_102,U_100) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_7,plain,
( apply(U_102,U_106,U_94)
| ~ upper_bound(U_94,U_102,U_104)
| ~ member(U_94,U_100)
| ~ least_upper_bound(U_106,U_104,U_102,U_100) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_8,plain,
( member(sK15(U_107,U_105,U_103,U_101),U_101)
| ~ upper_bound(U_107,U_103,U_105)
| ~ member(U_107,U_105)
| least_upper_bound(U_107,U_105,U_103,U_101) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_9,plain,
( upper_bound(sK15(U_107,U_105,U_103,U_101),U_103,U_105)
| ~ upper_bound(U_107,U_103,U_105)
| ~ member(U_107,U_105)
| least_upper_bound(U_107,U_105,U_103,U_101) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_10,plain,
( ~ apply(U_103,U_107,sK15(U_107,U_105,U_103,U_101))
| ~ upper_bound(U_107,U_103,U_105)
| ~ member(U_107,U_105)
| least_upper_bound(U_107,U_105,U_103,U_101) ),
inference(clausify,[status(thm)],[f_9_4]) ).
fof(f_10_1,plain,
! [A,X,R,E] :
( ( greatest_lower_bound(A,X,R,E)
| ? [M] :
( ~ apply(R,M,A)
& lower_bound(M,R,X)
& member(M,E) )
| ~ lower_bound(A,R,X)
| ~ member(A,X) )
& ( ( ! [M] :
( apply(R,M,A)
| ~ lower_bound(M,R,X)
| ~ member(M,E) )
& lower_bound(A,R,X)
& member(A,X) )
| ~ greatest_lower_bound(A,X,R,E) ) ),
inference(fof_nnf,[status(thm)],[greatest_lower_bound]) ).
fof(f_10_2,plain,
! [U_113,U_112,U_111,U_110] :
( ( greatest_lower_bound(U_113,U_112,U_111,U_110)
| ? [U_109] :
( ~ apply(U_111,U_109,U_113)
& lower_bound(U_109,U_111,U_112)
& member(U_109,U_110) )
| ~ lower_bound(U_113,U_111,U_112)
| ~ member(U_113,U_112) )
& ( ( ! [U_108] :
( apply(U_111,U_108,U_113)
| ~ lower_bound(U_108,U_111,U_112)
| ~ member(U_108,U_110) )
& lower_bound(U_113,U_111,U_112)
& member(U_113,U_112) )
| ~ greatest_lower_bound(U_113,U_112,U_111,U_110) ) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
( ! [U_121,U_119,U_117,U_115] :
( greatest_lower_bound(U_121,U_119,U_117,U_115)
| ? [U_109] :
( ~ apply(U_117,U_109,U_121)
& lower_bound(U_109,U_117,U_119)
& member(U_109,U_115) )
| ~ lower_bound(U_121,U_117,U_119)
| ~ member(U_121,U_119) )
& ! [U_120,U_118,U_116,U_114] :
( ( ! [U_108] :
( apply(U_116,U_108,U_120)
| ~ lower_bound(U_108,U_116,U_118)
| ~ member(U_108,U_114) )
& lower_bound(U_120,U_116,U_118)
& member(U_120,U_118) )
| ~ greatest_lower_bound(U_120,U_118,U_116,U_114) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
( ! [U_121,U_119,U_117,U_115] :
( greatest_lower_bound(U_121,U_119,U_117,U_115)
| ( ~ apply(U_117,sK16(U_121,U_119,U_117,U_115),U_121)
& lower_bound(sK16(U_121,U_119,U_117,U_115),U_117,U_119)
& member(sK16(U_121,U_119,U_117,U_115),U_115) )
| ~ lower_bound(U_121,U_117,U_119)
| ~ member(U_121,U_119) )
& ! [U_120,U_118,U_116,U_114] :
( ( ! [U_108] :
( apply(U_116,U_108,U_120)
| ~ lower_bound(U_108,U_116,U_118)
| ~ member(U_108,U_114) )
& lower_bound(U_120,U_116,U_118)
& member(U_120,U_118) )
| ~ greatest_lower_bound(U_120,U_118,U_116,U_114) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_109,sK16(U_121,U_119,U_117,U_115))],[f_10_3]) ).
cnf(f_10_5,plain,
( member(U_120,U_118)
| ~ greatest_lower_bound(U_120,U_118,U_116,U_114) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_6,plain,
( lower_bound(U_120,U_116,U_118)
| ~ greatest_lower_bound(U_120,U_118,U_116,U_114) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_7,plain,
( apply(U_116,U_108,U_120)
| ~ lower_bound(U_108,U_116,U_118)
| ~ member(U_108,U_114)
| ~ greatest_lower_bound(U_120,U_118,U_116,U_114) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_8,plain,
( member(sK16(U_121,U_119,U_117,U_115),U_115)
| ~ lower_bound(U_121,U_117,U_119)
| ~ member(U_121,U_119)
| greatest_lower_bound(U_121,U_119,U_117,U_115) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_9,plain,
( lower_bound(sK16(U_121,U_119,U_117,U_115),U_117,U_119)
| ~ lower_bound(U_121,U_117,U_119)
| ~ member(U_121,U_119)
| greatest_lower_bound(U_121,U_119,U_117,U_115) ),
inference(clausify,[status(thm)],[f_10_4]) ).
cnf(f_10_10,plain,
( ~ apply(U_117,sK16(U_121,U_119,U_117,U_115),U_121)
| ~ lower_bound(U_121,U_117,U_119)
| ~ member(U_121,U_119)
| greatest_lower_bound(U_121,U_119,U_117,U_115) ),
inference(clausify,[status(thm)],[f_10_4]) ).
fof(f_11_1,negated_conjecture,
~ ! [R,E] :
( order(R,E)
=> ! [M1,M2] :
( ( M1 != M2
& max(M2,R,E)
& max(M1,R,E) )
=> ~ ? [M] : greatest(M,R,E) ) ),
inference(negate,[status(cth)],[thIV15]) ).
fof(f_11_2,negated_conjecture,
? [R,E] :
( ? [M1,M2] :
( ? [M] : greatest(M,R,E)
& M1 != M2
& max(M2,R,E)
& max(M1,R,E) )
& order(R,E) ),
inference(fof_nnf,[status(thm)],[f_11_1]) ).
fof(f_11_3,negated_conjecture,
? [U_126,U_125] :
( ? [U_124,U_123] :
( ? [U_122] : greatest(U_122,U_126,U_125)
& U_124 != U_123
& max(U_123,U_126,U_125)
& max(U_124,U_126,U_125) )
& order(U_126,U_125) ),
inference(variable_rename,[status(thm)],[f_11_2]) ).
fof(f_11_4,negated_conjecture,
? [U_126,U_125] :
( ? [U_124] :
( ? [U_123] :
( U_124 != U_123
& max(U_123,U_126,U_125) )
& max(U_124,U_126,U_125) )
& ? [U_122] : greatest(U_122,U_126,U_125)
& order(U_126,U_125) ),
inference(miniscope,[status(thm)],[f_11_3]) ).
fof(f_11_5,negated_conjecture,
? [U_125] :
( ? [U_124] :
( ? [U_123] :
( U_124 != U_123
& max(U_123,sK17,U_125) )
& max(U_124,sK17,U_125) )
& ? [U_122] : greatest(U_122,sK17,U_125)
& order(sK17,U_125) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_126,sK17)],[f_11_4]) ).
fof(f_11_6,negated_conjecture,
( ? [U_124] :
( ? [U_123] :
( U_124 != U_123
& max(U_123,sK17,sK18) )
& max(U_124,sK17,sK18) )
& ? [U_122] : greatest(U_122,sK17,sK18)
& order(sK17,sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_125,sK18)],[f_11_5]) ).
fof(f_11_7,negated_conjecture,
( ? [U_124] :
( ? [U_123] :
( U_124 != U_123
& max(U_123,sK17,sK18) )
& max(U_124,sK17,sK18) )
& greatest(sK19,sK17,sK18)
& order(sK17,sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_122,sK19)],[f_11_6]) ).
fof(f_11_8,negated_conjecture,
( ? [U_123] :
( sK20 != U_123
& max(U_123,sK17,sK18) )
& max(sK20,sK17,sK18)
& greatest(sK19,sK17,sK18)
& order(sK17,sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_124,sK20)],[f_11_7]) ).
fof(f_11_9,negated_conjecture,
( sK20 != sK21
& max(sK21,sK17,sK18)
& max(sK20,sK17,sK18)
& greatest(sK19,sK17,sK18)
& order(sK17,sK18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_123,sK21)],[f_11_8]) ).
fof(f_11_10,negated_conjecture,
( sK20 != sK21
& max(sK21,sK17,sK18)
& max(sK20,sK17,sK18)
& greatest(sK19,sK17,sK18)
& order(sK17,sK18) ),
inference(definitional_conversion,[status(esa)],[f_11_9]) ).
cnf(f_11_11,negated_conjecture,
order(sK17,sK18),
inference(clausify,[status(thm)],[f_11_10]) ).
cnf(f_11_12,negated_conjecture,
greatest(sK19,sK17,sK18),
inference(clausify,[status(thm)],[f_11_10]) ).
cnf(f_11_13,negated_conjecture,
max(sK20,sK17,sK18),
inference(clausify,[status(thm)],[f_11_10]) ).
cnf(f_11_14,negated_conjecture,
max(sK21,sK17,sK18),
inference(clausify,[status(thm)],[f_11_10]) ).
cnf(f_11_15,negated_conjecture,
sK20 != sK21,
inference(clausify,[status(thm)],[f_11_10]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( sK1(Eq_x_0,Eq_x_1) = sK1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK3(Eq_x_0,Eq_x_1) = sK3(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK4(Eq_x_0,Eq_x_1) = sK4(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK5(Eq_x_0,Eq_x_1) = sK5(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK6(Eq_x_0,Eq_x_1) = sK6(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK7(Eq_x_0,Eq_x_1) = sK7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK9(Eq_x_0,Eq_x_1,Eq_x_2) = sK9(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK10(Eq_x_0,Eq_x_1,Eq_x_2) = sK10(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK11(Eq_x_0,Eq_x_1,Eq_x_2) = sK11(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK12(Eq_x_0,Eq_x_1,Eq_x_2) = sK12(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK13(Eq_x_0,Eq_x_1,Eq_x_2) = sK13(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK14(Eq_x_0,Eq_x_1,Eq_x_2) = sK14(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK15(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK15(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK16(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK16(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( order(Eq_y_0,Eq_y_1)
| ~ order(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( member(Eq_y_0,Eq_y_1)
| ~ member(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( apply(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ apply(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( total_order(Eq_y_0,Eq_y_1)
| ~ total_order(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( upper_bound(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ upper_bound(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( lower_bound(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ lower_bound(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( greatest(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ greatest(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( least(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ least(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( max(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ max(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( min(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ min(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( least_upper_bound(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ least_upper_bound(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( greatest_lower_bound(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ greatest_lower_bound(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET803+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ 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.34 % Computer : n001.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 19 23:06:11 UTC 2026
% 0.08/0.35 % CPUTime :
% 24.56/24.80 % SZS status Theorem for theBenchmark
% 24.56/24.80 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------