%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP026+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 01:31:58 PM UTC 2026
% Result : CounterSatisfiable 0.10s 15.48s
% Output : Saturation 0.10s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ~ ( ( ? [X4] :
( ? [X5] :
( ! [X12] :
( member(X4,X12,X5)
=> hamburger(X4,X12) )
& group(X4,X5)
& ! [X6] :
( member(X4,X6,X5)
=> ? [X7] :
( ! [X11] :
( member(X4,X11,X7)
=> ( young(X4,X11)
& guy(X4,X11) ) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( member(X4,X8,X7)
=> ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) ) ) ) )
& actual_world(X4) )
=> ? [U] :
( ? [V,W] :
( ! [X3] :
( member(U,X3,W)
=> hamburger(U,X3) )
& group(U,W)
& ! [X] :
( member(U,X,W)
=> ? [Y] :
( ! [X2] :
( member(U,X2,Y)
=> ( young(U,X2)
& guy(U,X2) ) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( member(U,Z,Y)
=> ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) ) ) ) )
& table(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W] :
( ! [X3] :
( member(U,X3,W)
=> hamburger(U,X3) )
& group(U,W)
& ! [X] :
( member(U,X,W)
=> ? [Y] :
( ! [X2] :
( member(U,X2,Y)
=> ( young(U,X2)
& guy(U,X2) ) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( member(U,Z,Y)
=> ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) ) ) ) )
& table(U,V) )
& actual_world(U) )
=> ? [X4] :
( ? [X5] :
( ! [X12] :
( member(X4,X12,X5)
=> hamburger(X4,X12) )
& group(X4,X5)
& ! [X6] :
( member(X4,X6,X5)
=> ? [X7] :
( ! [X11] :
( member(X4,X11,X7)
=> ( young(X4,X11)
& guy(X4,X11) ) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( member(X4,X8,X7)
=> ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) ) ) ) )
& actual_world(X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ~ ( ( ? [X4] :
( ? [X5] :
( ! [X12] :
( member(X4,X12,X5)
=> hamburger(X4,X12) )
& group(X4,X5)
& ! [X6] :
( member(X4,X6,X5)
=> ? [X7] :
( ! [X11] :
( member(X4,X11,X7)
=> ( young(X4,X11)
& guy(X4,X11) ) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( member(X4,X8,X7)
=> ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) ) ) ) )
& actual_world(X4) )
=> ? [U] :
( ? [V,W] :
( ! [X3] :
( member(U,X3,W)
=> hamburger(U,X3) )
& group(U,W)
& ! [X] :
( member(U,X,W)
=> ? [Y] :
( ! [X2] :
( member(U,X2,Y)
=> ( young(U,X2)
& guy(U,X2) ) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( member(U,Z,Y)
=> ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) ) ) ) )
& table(U,V) )
& actual_world(U) ) )
& ( ? [U] :
( ? [V,W] :
( ! [X3] :
( member(U,X3,W)
=> hamburger(U,X3) )
& group(U,W)
& ! [X] :
( member(U,X,W)
=> ? [Y] :
( ! [X2] :
( member(U,X2,Y)
=> ( young(U,X2)
& guy(U,X2) ) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( member(U,Z,Y)
=> ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) ) ) ) )
& table(U,V) )
& actual_world(U) )
=> ? [X4] :
( ? [X5] :
( ! [X12] :
( member(X4,X12,X5)
=> hamburger(X4,X12) )
& group(X4,X5)
& ! [X6] :
( member(X4,X6,X5)
=> ? [X7] :
( ! [X11] :
( member(X4,X11,X7)
=> ( young(X4,X11)
& guy(X4,X11) ) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( member(X4,X8,X7)
=> ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) ) ) ) )
& actual_world(X4) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ! [U] :
( ! [V,W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ? [X] :
( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) ) )
& member(U,X,W) )
| ~ table(U,V) )
| ~ actual_world(U) )
& ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) )
| ~ member(X4,X8,X7) ) )
| ~ member(X4,X6,X5) ) )
& actual_world(X4) ) )
| ( ! [X4] :
( ! [X5] :
( ? [X12] :
( ~ hamburger(X4,X12)
& member(X4,X12,X5) )
| ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X9,X10] :
( ~ with(X4,X10,X6)
| ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) )
& member(X4,X8,X7) ) )
& member(X4,X6,X5) ) )
| ~ actual_world(X4) )
& ? [U] :
( ? [V,W] :
( ! [X3] :
( hamburger(U,X3)
| ~ member(U,X3,W) )
& group(U,W)
& ! [X] :
( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| ~ member(U,X,W) )
& table(U,V) )
& actual_world(U) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
( sP0_prd
<=> ( ! [X4] :
( ! [X5] :
( ? [X12] :
( ~ hamburger(X4,X12)
& member(X4,X12,X5) )
| ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X9,X10] :
( ~ with(X4,X10,X6)
| ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) )
& member(X4,X8,X7) ) )
& member(X4,X6,X5) ) )
| ~ actual_world(X4) )
& ? [U] :
( ? [V,W] :
( ! [X3] :
( hamburger(U,X3)
| ~ member(U,X3,W) )
& group(U,W)
& ! [X] :
( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| ~ member(U,X,W) )
& table(U,V) )
& actual_world(U) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,plain,
( ( ! [U] :
( ! [V,W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ? [X] :
( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) ) )
& member(U,X,W) )
| ~ table(U,V) )
| ~ actual_world(U) )
& ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) )
| ~ member(X4,X8,X7) ) )
| ~ member(X4,X6,X5) ) )
& actual_world(X4) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f3,f4]) ).
fof(f6,definition,
! [U,V,W,X] :
( sP1_prd(X,W,V,U)
<=> ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) ) )
& member(U,X,W) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f7,plain,
( ( ! [U] :
( ! [V,W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ? [X] : sP1_prd(X,W,V,U)
| ~ table(U,V) )
| ~ actual_world(U) )
& ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) )
| ~ member(X4,X8,X7) ) )
| ~ member(X4,X6,X5) ) )
& actual_world(X4) ) )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f5,f6]) ).
fof(f8,plain,
( ( ! [U] :
( ! [W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ! [V] :
( ? [X] : sP1_prd(X,W,V,U)
| ~ table(U,V) ) )
| ~ actual_world(U) )
& ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X10] :
( with(X4,X10,X6)
& ? [X9] :
( at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) )
| ~ member(X4,X8,X7) ) )
| ~ member(X4,X6,X5) ) )
& actual_world(X4) ) )
| sP0_prd ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f9,plain,
( ( ! [U] :
( ! [W] :
( ( ~ hamburger(U,sK6_skl(W,U))
& member(U,sK6_skl(W,U),W) )
| ~ group(U,W)
| ! [V] :
( sP1_prd(sK5_skl(V,W,U),W,V,U)
| ~ table(U,V) ) )
| ~ actual_world(U) )
& ! [X12] :
( hamburger(sK0_skl,X12)
| ~ member(sK0_skl,X12,sK1_skl) )
& group(sK0_skl,sK1_skl)
& ! [X6] :
( ( ! [X11] :
( ( young(sK0_skl,X11)
& guy(sK0_skl,X11) )
| ~ member(sK0_skl,X11,sK2_skl(X6)) )
& group(sK0_skl,sK2_skl(X6))
& three(sK0_skl,sK2_skl(X6))
& ! [X8] :
( ( with(sK0_skl,sK3_skl(X8,X6),X6)
& at(sK0_skl,sK3_skl(X8,X6),sK4_skl(X8,X6))
& sit(sK0_skl,sK3_skl(X8,X6))
& present(sK0_skl,sK3_skl(X8,X6))
& agent(sK0_skl,sK3_skl(X8,X6),X8)
& event(sK0_skl,sK3_skl(X8,X6))
& table(sK0_skl,sK4_skl(X8,X6)) )
| ~ member(sK0_skl,X8,sK2_skl(X6)) ) )
| ~ member(sK0_skl,X6,sK1_skl) )
& actual_world(sK0_skl) )
| sP0_prd ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(X4,sK0_skl),skolemize(X5,sK1_skl),skolemize(X7,sK2_skl(X6)),skolemize(X10,sK3_skl(X8,X6)),skolemize(X9,sK4_skl(X8,X6)),skolemize(X,sK5_skl(V,W,U)),skolemize(X3,sK6_skl(W,U))],[f8]) ).
fof(f10,plain,
( actual_world(sK0_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f11,plain,
! [X0,X1] :
( table(sK0_skl,sK4_skl(X1,X0))
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f12,plain,
! [X0,X1] :
( event(sK0_skl,sK3_skl(X1,X0))
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f13,plain,
! [X0,X1] :
( agent(sK0_skl,sK3_skl(X1,X0),X1)
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f14,plain,
! [X0,X1] :
( present(sK0_skl,sK3_skl(X1,X0))
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f15,plain,
! [X0,X1] :
( sit(sK0_skl,sK3_skl(X1,X0))
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f16,plain,
! [X0,X1] :
( at(sK0_skl,sK3_skl(X1,X0),sK4_skl(X1,X0))
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f17,plain,
! [X0,X1] :
( with(sK0_skl,sK3_skl(X1,X0),X0)
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f18,plain,
! [X0] :
( three(sK0_skl,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f19,plain,
! [X0] :
( group(sK0_skl,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f20,plain,
! [X0,X1] :
( guy(sK0_skl,X1)
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f21,plain,
! [X0,X1] :
( young(sK0_skl,X1)
| ~ member(sK0_skl,X1,sK2_skl(X0))
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f22,plain,
( group(sK0_skl,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f23,plain,
! [X0] :
( hamburger(sK0_skl,X0)
| ~ member(sK0_skl,X0,sK1_skl)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f24,plain,
! [X0,X1,X2] :
( member(X0,sK6_skl(X2,X0),X2)
| ~ group(X0,X2)
| sP1_prd(sK5_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f25,plain,
! [X0,X1,X2] :
( ~ hamburger(X0,sK6_skl(X2,X0))
| ~ group(X0,X2)
| sP1_prd(sK5_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f26,definition,
! [U,V,W,X] :
( sP2_prd(X,W,V,U)
<=> ( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| ~ member(U,X,W) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f27,definition,
! [X4,X5] :
( sP3_prd(X5,X4)
<=> ( ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X9,X10] :
( ~ with(X4,X10,X6)
| ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) )
& member(X4,X8,X7) ) )
& member(X4,X6,X5) ) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f28,plain,
( sP0_prd
<=> ( ! [X4] :
( ! [X5] :
( ? [X12] :
( ~ hamburger(X4,X12)
& member(X4,X12,X5) )
| sP3_prd(X5,X4) )
| ~ actual_world(X4) )
& ? [U] :
( ? [V,W] :
( ! [X3] :
( hamburger(U,X3)
| ~ member(U,X3,W) )
& group(U,W)
& ! [X] : sP2_prd(X,W,V,U)
& table(U,V) )
& actual_world(U) ) ) ),
inference(formula_renaming,[status(thm)],[f4,f27,f26]) ).
fof(f29,plain,
( ( ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& ~ sP3_prd(X5,X4) )
& actual_world(X4) )
| ! [U] :
( ! [V,W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ? [X] : ~ sP2_prd(X,W,V,U)
| ~ table(U,V) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X4] :
( ! [X5] :
( ? [X12] :
( ~ hamburger(X4,X12)
& member(X4,X12,X5) )
| sP3_prd(X5,X4) )
| ~ actual_world(X4) )
& ? [U] :
( ? [V,W] :
( ! [X3] :
( hamburger(U,X3)
| ~ member(U,X3,W) )
& group(U,W)
& ! [X] : sP2_prd(X,W,V,U)
& table(U,V) )
& actual_world(U) ) )
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
( ( ? [X4] :
( ? [X5] :
( ! [X12] :
( hamburger(X4,X12)
| ~ member(X4,X12,X5) )
& ~ sP3_prd(X5,X4) )
& actual_world(X4) )
| ! [U] :
( ! [W] :
( ? [X3] :
( ~ hamburger(U,X3)
& member(U,X3,W) )
| ~ group(U,W)
| ! [V] :
( ? [X] : ~ sP2_prd(X,W,V,U)
| ~ table(U,V) ) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X4] :
( ! [X5] :
( ? [X12] :
( ~ hamburger(X4,X12)
& member(X4,X12,X5) )
| sP3_prd(X5,X4) )
| ~ actual_world(X4) )
& ? [U] :
( ? [W] :
( ! [X3] :
( hamburger(U,X3)
| ~ member(U,X3,W) )
& group(U,W)
& ? [V] :
( ! [X] : sP2_prd(X,W,V,U)
& table(U,V) ) )
& actual_world(U) ) )
| ~ sP0_prd ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f31,plain,
( ( ( ! [X12] :
( hamburger(sK13_skl,X12)
| ~ member(sK13_skl,X12,sK14_skl) )
& ~ sP3_prd(sK14_skl,sK13_skl)
& actual_world(sK13_skl) )
| ! [U] :
( ! [W] :
( ( ~ hamburger(U,sK12_skl(W,U))
& member(U,sK12_skl(W,U),W) )
| ~ group(U,W)
| ! [V] :
( ~ sP2_prd(sK11_skl(V,W,U),W,V,U)
| ~ table(U,V) ) )
| ~ actual_world(U) )
| sP0_prd )
& ( ( ! [X4] :
( ! [X5] :
( ( ~ hamburger(X4,sK10_skl(X5,X4))
& member(X4,sK10_skl(X5,X4),X5) )
| sP3_prd(X5,X4) )
| ~ actual_world(X4) )
& ! [X3] :
( hamburger(sK7_skl,X3)
| ~ member(sK7_skl,X3,sK8_skl) )
& group(sK7_skl,sK8_skl)
& ! [X] : sP2_prd(X,sK8_skl,sK9_skl,sK7_skl)
& table(sK7_skl,sK9_skl)
& actual_world(sK7_skl) )
| ~ sP0_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(U,sK7_skl),skolemize(W,sK8_skl),skolemize(V,sK9_skl),skolemize(X12,sK10_skl(X5,X4)),skolemize(X,sK11_skl(V,W,U)),skolemize(X3,sK12_skl(W,U)),skolemize(X4,sK13_skl),skolemize(X5,sK14_skl)],[f30]) ).
fof(f32,plain,
( actual_world(sK7_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f33,plain,
( table(sK7_skl,sK9_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f34,plain,
! [X0] :
( sP2_prd(X0,sK8_skl,sK9_skl,sK7_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f35,plain,
( group(sK7_skl,sK8_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f36,plain,
! [X0] :
( hamburger(sK7_skl,X0)
| ~ member(sK7_skl,X0,sK8_skl)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f37,plain,
! [X0,X1] :
( member(X0,sK10_skl(X1,X0),X1)
| sP3_prd(X1,X0)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f38,plain,
! [X0,X1] :
( ~ hamburger(X0,sK10_skl(X1,X0))
| sP3_prd(X1,X0)
| ~ actual_world(X0)
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f39,plain,
! [X0,X1,X2] :
( actual_world(sK13_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f40,plain,
! [X0,X1,X2] :
( ~ sP3_prd(sK14_skl,sK13_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( hamburger(sK13_skl,X3)
| ~ member(sK13_skl,X3,sK14_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f42,plain,
! [X0,X1,X2] :
( actual_world(sK13_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ~ sP3_prd(sK14_skl,sK13_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f44,plain,
! [X0,X1,X2,X3] :
( hamburger(sK13_skl,X3)
| ~ member(sK13_skl,X3,sK14_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ sP2_prd(sK11_skl(X1,X2,X0),X2,X1,X0)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f45,definition,
! [U,V,X,Y] :
( sP4_prd(Y,X,V,U)
<=> ( ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) ) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f46,plain,
! [U,V,W,X] :
( sP1_prd(X,W,V,U)
<=> ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| sP4_prd(Y,X,V,U) )
& member(U,X,W) ) ),
inference(formula_renaming,[status(thm)],[f6,f45]) ).
fof(f47,plain,
! [U,V,W,X] :
( ( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& ~ sP4_prd(Y,X,V,U) )
| ~ member(U,X,W)
| sP1_prd(X,W,V,U) )
& ( ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| sP4_prd(Y,X,V,U) )
& member(U,X,W) )
| ~ sP1_prd(X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f48,plain,
( ! [U,V,W,X] :
( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& ~ sP4_prd(Y,X,V,U) )
| ~ member(U,X,W)
| sP1_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| sP4_prd(Y,X,V,U) )
& member(U,X,W) )
| ~ sP1_prd(X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f49,plain,
( ! [U,V,W,X] :
( ( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,sK16_skl(X,W,V,U)) )
& ~ sP4_prd(sK16_skl(X,W,V,U),X,V,U) )
| ~ member(U,X,W)
| sP1_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [Y] :
( ( ( ~ young(U,sK15_skl(Y,X,W,V,U))
| ~ guy(U,sK15_skl(Y,X,W,V,U)) )
& member(U,sK15_skl(Y,X,W,V,U),Y) )
| sP4_prd(Y,X,V,U) )
& member(U,X,W) )
| ~ sP1_prd(X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X2,sK15_skl(Y,X,W,V,U)),skolemize(Y,sK16_skl(X,W,V,U))],[f48]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( member(X3,X0,X1)
| ~ sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1,X2,X3,X4] :
( member(X3,sK15_skl(X4,X0,X1,X2,X3),X4)
| sP4_prd(X4,X0,X2,X3)
| ~ sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f52,plain,
! [X0,X1,X2,X3,X4] :
( ~ young(X3,sK15_skl(X4,X0,X1,X2,X3))
| ~ guy(X3,sK15_skl(X4,X0,X1,X2,X3))
| sP4_prd(X4,X0,X2,X3)
| ~ sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f53,plain,
! [X0,X1,X2,X3] :
( ~ sP4_prd(sK16_skl(X0,X1,X2,X3),X0,X2,X3)
| ~ member(X3,X0,X1)
| sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f54,plain,
! [X0,X1,X2,X3,X4] :
( guy(X3,X4)
| ~ member(X3,X4,sK16_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4] :
( young(X3,X4)
| ~ member(X3,X4,sK16_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| sP1_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f56,definition,
! [U,V,X,Y] :
( sP5_prd(Y,X,V,U)
<=> ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f57,plain,
! [U,V,W,X] :
( sP2_prd(X,W,V,U)
<=> ( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& sP5_prd(Y,X,V,U) )
| ~ member(U,X,W) ) ),
inference(formula_renaming,[status(thm)],[f26,f56]) ).
fof(f58,plain,
! [U,V,W,X] :
( ( ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| ~ sP5_prd(Y,X,V,U) )
& member(U,X,W) )
| sP2_prd(X,W,V,U) )
& ( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& sP5_prd(Y,X,V,U) )
| ~ member(U,X,W)
| ~ sP2_prd(X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f59,plain,
( ! [U,V,W,X] :
( ( ! [Y] :
( ? [X2] :
( ( ~ young(U,X2)
| ~ guy(U,X2) )
& member(U,X2,Y) )
| ~ sP5_prd(Y,X,V,U) )
& member(U,X,W) )
| sP2_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ? [Y] :
( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,Y) )
& sP5_prd(Y,X,V,U) )
| ~ member(U,X,W)
| ~ sP2_prd(X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f58]) ).
fof(f60,plain,
( ! [U,V,W,X] :
( ( ! [Y] :
( ( ( ~ young(U,sK18_skl(Y,X,W,V,U))
| ~ guy(U,sK18_skl(Y,X,W,V,U)) )
& member(U,sK18_skl(Y,X,W,V,U),Y) )
| ~ sP5_prd(Y,X,V,U) )
& member(U,X,W) )
| sP2_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [X2] :
( ( young(U,X2)
& guy(U,X2) )
| ~ member(U,X2,sK17_skl(X,W,V,U)) )
& sP5_prd(sK17_skl(X,W,V,U),X,V,U) )
| ~ member(U,X,W)
| ~ sP2_prd(X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(Y,sK17_skl(X,W,V,U)),skolemize(X2,sK18_skl(Y,X,W,V,U))],[f59]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( sP5_prd(sK17_skl(X0,X1,X2,X3),X0,X2,X3)
| ~ member(X3,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1,X2,X3,X4] :
( guy(X3,X4)
| ~ member(X3,X4,sK17_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
! [X0,X1,X2,X3,X4] :
( young(X3,X4)
| ~ member(X3,X4,sK17_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| ~ sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( member(X3,X0,X1)
| sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f65,plain,
! [X0,X1,X2,X3,X4] :
( member(X3,sK18_skl(X4,X0,X1,X2,X3),X4)
| ~ sP5_prd(X4,X0,X2,X3)
| sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f66,plain,
! [X0,X1,X2,X3,X4] :
( ~ young(X3,sK18_skl(X4,X0,X1,X2,X3))
| ~ guy(X3,sK18_skl(X4,X0,X1,X2,X3))
| ~ sP5_prd(X4,X0,X2,X3)
| sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f67,definition,
! [X4,X6,X7] :
( sP6_prd(X7,X6,X4)
<=> ( ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X9,X10] :
( ~ with(X4,X10,X6)
| ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) )
& member(X4,X8,X7) ) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f68,plain,
! [X4,X5] :
( sP3_prd(X5,X4)
<=> ( ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| sP6_prd(X7,X6,X4) )
& member(X4,X6,X5) ) ) ),
inference(formula_renaming,[status(thm)],[f27,f67]) ).
fof(f69,plain,
! [X4,X5] :
( ( ( group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& ~ sP6_prd(X7,X6,X4) )
| ~ member(X4,X6,X5) ) )
| sP3_prd(X5,X4) )
& ( ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| sP6_prd(X7,X6,X4) )
& member(X4,X6,X5) )
| ~ sP3_prd(X5,X4) ) ),
inference(NNF_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
( ! [X4,X5] :
( ( group(X4,X5)
& ! [X6] :
( ? [X7] :
( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,X7) )
& ~ sP6_prd(X7,X6,X4) )
| ~ member(X4,X6,X5) ) )
| sP3_prd(X5,X4) )
& ! [X4,X5] :
( ~ group(X4,X5)
| ? [X6] :
( ! [X7] :
( ? [X11] :
( ( ~ young(X4,X11)
| ~ guy(X4,X11) )
& member(X4,X11,X7) )
| sP6_prd(X7,X6,X4) )
& member(X4,X6,X5) )
| ~ sP3_prd(X5,X4) ) ),
inference(miniscoping,[status(thm)],[f69]) ).
fof(f71,plain,
( ! [X4,X5] :
( ( group(X4,X5)
& ! [X6] :
( ( ! [X11] :
( ( young(X4,X11)
& guy(X4,X11) )
| ~ member(X4,X11,sK21_skl(X6,X5,X4)) )
& ~ sP6_prd(sK21_skl(X6,X5,X4),X6,X4) )
| ~ member(X4,X6,X5) ) )
| sP3_prd(X5,X4) )
& ! [X4,X5] :
( ~ group(X4,X5)
| ( ! [X7] :
( ( ( ~ young(X4,sK20_skl(X7,X5,X4))
| ~ guy(X4,sK20_skl(X7,X5,X4)) )
& member(X4,sK20_skl(X7,X5,X4),X7) )
| sP6_prd(X7,sK19_skl(X5,X4),X4) )
& member(X4,sK19_skl(X5,X4),X5) )
| ~ sP3_prd(X5,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(X6,sK19_skl(X5,X4)),skolemize(X11,sK20_skl(X7,X5,X4)),skolemize(X7,sK21_skl(X6,X5,X4))],[f70]) ).
fof(f72,plain,
! [X0,X1] :
( ~ group(X1,X0)
| member(X1,sK19_skl(X0,X1),X0)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ group(X1,X0)
| member(X1,sK20_skl(X2,X0,X1),X2)
| sP6_prd(X2,sK19_skl(X0,X1),X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ~ group(X1,X0)
| ~ young(X1,sK20_skl(X2,X0,X1))
| ~ guy(X1,sK20_skl(X2,X0,X1))
| sP6_prd(X2,sK19_skl(X0,X1),X1)
| ~ sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ sP6_prd(sK21_skl(X2,X0,X1),X2,X1)
| ~ member(X1,X2,X0)
| sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f76,plain,
! [X0,X1,X2,X3] :
( guy(X1,X3)
| ~ member(X1,X3,sK21_skl(X2,X0,X1))
| ~ member(X1,X2,X0)
| sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f77,plain,
! [X0,X1,X2,X3] :
( young(X1,X3)
| ~ member(X1,X3,sK21_skl(X2,X0,X1))
| ~ member(X1,X2,X0)
| sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f78,plain,
! [X0,X1] :
( group(X1,X0)
| sP3_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f79,plain,
! [U,V,X,Y] :
( ( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| sP4_prd(Y,X,V,U) )
& ( ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) )
| ~ sP4_prd(Y,X,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f80,plain,
( ! [U,V,X,Y] :
( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| sP4_prd(Y,X,V,U) )
& ! [U,V,X,Y] :
( ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) )
| ~ sP4_prd(Y,X,V,U) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
( ! [U,V,X,Y] :
( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ( with(U,sK23_skl(Z,Y,X,V,U),X)
& at(U,sK23_skl(Z,Y,X,V,U),V)
& sit(U,sK23_skl(Z,Y,X,V,U))
& present(U,sK23_skl(Z,Y,X,V,U))
& agent(U,sK23_skl(Z,Y,X,V,U),Z)
& event(U,sK23_skl(Z,Y,X,V,U)) )
| ~ member(U,Z,Y) ) )
| sP4_prd(Y,X,V,U) )
& ! [U,V,X,Y] :
( ~ group(U,Y)
| ~ three(U,Y)
| ( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,sK22_skl(Y,X,V,U))
| ~ event(U,X1) )
& member(U,sK22_skl(Y,X,V,U),Y) )
| ~ sP4_prd(Y,X,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl,sK23_skl]),skolemize(Z,sK22_skl(Y,X,V,U)),skolemize(X1,sK23_skl(Z,Y,X,V,U))],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ group(X3,X0)
| ~ three(X3,X0)
| member(X3,sK22_skl(X0,X1,X2,X3),X0)
| ~ sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
! [X0,X1,X2,X3,X4] :
( ~ group(X3,X0)
| ~ three(X3,X0)
| ~ with(X3,X4,X1)
| ~ at(X3,X4,X2)
| ~ sit(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK22_skl(X0,X1,X2,X3))
| ~ event(X3,X4)
| ~ sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f84,plain,
! [X0,X1,X2,X3,X4] :
( event(X3,sK23_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f85,plain,
! [X0,X1,X2,X3,X4] :
( agent(X3,sK23_skl(X4,X0,X1,X2,X3),X4)
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f86,plain,
! [X0,X1,X2,X3,X4] :
( present(X3,sK23_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
! [X0,X1,X2,X3,X4] :
( sit(X3,sK23_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f88,plain,
! [X0,X1,X2,X3,X4] :
( at(X3,sK23_skl(X4,X0,X1,X2,X3),X2)
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f89,plain,
! [X0,X1,X2,X3,X4] :
( with(X3,sK23_skl(X4,X0,X1,X2,X3),X1)
| ~ member(X3,X4,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( three(X3,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( group(X3,X0)
| sP4_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f92,plain,
! [U,V,X,Y] :
( ( ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) )
| sP5_prd(Y,X,V,U) )
& ( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| ~ sP5_prd(Y,X,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f93,plain,
( ! [U,V,X,Y] :
( ~ group(U,Y)
| ~ three(U,Y)
| ? [Z] :
( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,Z)
| ~ event(U,X1) )
& member(U,Z,Y) )
| sP5_prd(Y,X,V,U) )
& ! [U,V,X,Y] :
( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ? [X1] :
( with(U,X1,X)
& at(U,X1,V)
& sit(U,X1)
& present(U,X1)
& agent(U,X1,Z)
& event(U,X1) )
| ~ member(U,Z,Y) ) )
| ~ sP5_prd(Y,X,V,U) ) ),
inference(miniscoping,[status(thm)],[f92]) ).
fof(f94,plain,
( ! [U,V,X,Y] :
( ~ group(U,Y)
| ~ three(U,Y)
| ( ! [X1] :
( ~ with(U,X1,X)
| ~ at(U,X1,V)
| ~ sit(U,X1)
| ~ present(U,X1)
| ~ agent(U,X1,sK25_skl(Y,X,V,U))
| ~ event(U,X1) )
& member(U,sK25_skl(Y,X,V,U),Y) )
| sP5_prd(Y,X,V,U) )
& ! [U,V,X,Y] :
( ( group(U,Y)
& three(U,Y)
& ! [Z] :
( ( with(U,sK24_skl(Z,Y,X,V,U),X)
& at(U,sK24_skl(Z,Y,X,V,U),V)
& sit(U,sK24_skl(Z,Y,X,V,U))
& present(U,sK24_skl(Z,Y,X,V,U))
& agent(U,sK24_skl(Z,Y,X,V,U),Z)
& event(U,sK24_skl(Z,Y,X,V,U)) )
| ~ member(U,Z,Y) ) )
| ~ sP5_prd(Y,X,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl,sK25_skl]),skolemize(X1,sK24_skl(Z,Y,X,V,U)),skolemize(Z,sK25_skl(Y,X,V,U))],[f93]) ).
fof(f95,plain,
! [X0,X1,X2,X3,X4] :
( event(X3,sK24_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
! [X0,X1,X2,X3,X4] :
( agent(X3,sK24_skl(X4,X0,X1,X2,X3),X4)
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f97,plain,
! [X0,X1,X2,X3,X4] :
( present(X3,sK24_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f98,plain,
! [X0,X1,X2,X3,X4] :
( sit(X3,sK24_skl(X4,X0,X1,X2,X3))
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f99,plain,
! [X0,X1,X2,X3,X4] :
( at(X3,sK24_skl(X4,X0,X1,X2,X3),X2)
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f100,plain,
! [X0,X1,X2,X3,X4] :
( with(X3,sK24_skl(X4,X0,X1,X2,X3),X1)
| ~ member(X3,X4,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( three(X3,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( group(X3,X0)
| ~ sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( ~ group(X3,X0)
| ~ three(X3,X0)
| member(X3,sK25_skl(X0,X1,X2,X3),X0)
| sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] :
( ~ group(X3,X0)
| ~ three(X3,X0)
| ~ with(X3,X4,X1)
| ~ at(X3,X4,X2)
| ~ sit(X3,X4)
| ~ present(X3,X4)
| ~ agent(X3,X4,sK25_skl(X0,X1,X2,X3))
| ~ event(X3,X4)
| sP5_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f105,plain,
! [X4,X6,X7] :
( ( ( group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X9,X10] :
( with(X4,X10,X6)
& at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) )
| ~ member(X4,X8,X7) ) )
| sP6_prd(X7,X6,X4) )
& ( ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X9,X10] :
( ~ with(X4,X10,X6)
| ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) )
& member(X4,X8,X7) )
| ~ sP6_prd(X7,X6,X4) ) ),
inference(NNF_transformation,[status(thm)],[f67]) ).
fof(f106,plain,
( ! [X4,X6,X7] :
( ( group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ? [X10] :
( with(X4,X10,X6)
& ? [X9] :
( at(X4,X10,X9)
& sit(X4,X10)
& present(X4,X10)
& agent(X4,X10,X8)
& event(X4,X10)
& table(X4,X9) ) )
| ~ member(X4,X8,X7) ) )
| sP6_prd(X7,X6,X4) )
& ! [X4,X6,X7] :
( ~ group(X4,X7)
| ~ three(X4,X7)
| ? [X8] :
( ! [X10] :
( ~ with(X4,X10,X6)
| ! [X9] :
( ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,X8)
| ~ event(X4,X10)
| ~ table(X4,X9) ) )
& member(X4,X8,X7) )
| ~ sP6_prd(X7,X6,X4) ) ),
inference(miniscoping,[status(thm)],[f105]) ).
fof(f107,plain,
( ! [X4,X6,X7] :
( ( group(X4,X7)
& three(X4,X7)
& ! [X8] :
( ( with(X4,sK27_skl(X8,X7,X6,X4),X6)
& at(X4,sK27_skl(X8,X7,X6,X4),sK28_skl(X8,X7,X6,X4))
& sit(X4,sK27_skl(X8,X7,X6,X4))
& present(X4,sK27_skl(X8,X7,X6,X4))
& agent(X4,sK27_skl(X8,X7,X6,X4),X8)
& event(X4,sK27_skl(X8,X7,X6,X4))
& table(X4,sK28_skl(X8,X7,X6,X4)) )
| ~ member(X4,X8,X7) ) )
| sP6_prd(X7,X6,X4) )
& ! [X4,X6,X7] :
( ~ group(X4,X7)
| ~ three(X4,X7)
| ( ! [X10] :
( ~ with(X4,X10,X6)
| ! [X9] :
( ~ at(X4,X10,X9)
| ~ sit(X4,X10)
| ~ present(X4,X10)
| ~ agent(X4,X10,sK26_skl(X7,X6,X4))
| ~ event(X4,X10)
| ~ table(X4,X9) ) )
& member(X4,sK26_skl(X7,X6,X4),X7) )
| ~ sP6_prd(X7,X6,X4) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl,sK27_skl,sK28_skl]),skolemize(X8,sK26_skl(X7,X6,X4)),skolemize(X10,sK27_skl(X8,X7,X6,X4)),skolemize(X9,sK28_skl(X8,X7,X6,X4))],[f106]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ~ group(X2,X0)
| ~ three(X2,X0)
| member(X2,sK26_skl(X0,X1,X2),X0)
| ~ sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f109,plain,
! [X0,X1,X2,X3,X4] :
( ~ group(X2,X0)
| ~ three(X2,X0)
| ~ with(X2,X4,X1)
| ~ at(X2,X4,X3)
| ~ sit(X2,X4)
| ~ present(X2,X4)
| ~ agent(X2,X4,sK26_skl(X0,X1,X2))
| ~ event(X2,X4)
| ~ table(X2,X3)
| ~ sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f110,plain,
! [X0,X1,X2,X3] :
( table(X2,sK28_skl(X3,X0,X1,X2))
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f111,plain,
! [X0,X1,X2,X3] :
( event(X2,sK27_skl(X3,X0,X1,X2))
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f112,plain,
! [X0,X1,X2,X3] :
( agent(X2,sK27_skl(X3,X0,X1,X2),X3)
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( present(X2,sK27_skl(X3,X0,X1,X2))
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( sit(X2,sK27_skl(X3,X0,X1,X2))
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( at(X2,sK27_skl(X3,X0,X1,X2),sK28_skl(X3,X0,X1,X2))
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( with(X2,sK27_skl(X3,X0,X1,X2),X1)
| ~ member(X2,X3,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f117,plain,
! [X0,X1,X2] :
( three(X2,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f118,plain,
! [X0,X1,X2] :
( group(X2,X0)
| sP6_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| hamburger(sK13_skl,X3)
| ~ member(sK13_skl,X3,sK14_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f44,f64]) ).
fof(f127,plain,
! [X0,X1,X2,X3] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| hamburger(sK13_skl,X3)
| ~ member(sK13_skl,X3,sK14_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f41,f64]) ).
fof(f128,plain,
! [X0,X1,X2] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| actual_world(sK13_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f39,f64]) ).
fof(f129,plain,
! [X0,X1,X2] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| ~ sP3_prd(sK14_skl,sK13_skl)
| member(X0,sK12_skl(X2,X0),X2)
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f40,f64]) ).
fof(f130,plain,
! [X0,X1,X2] :
( group(X1,sK21_skl(X2,X0,X1))
| ~ member(X1,X2,X0)
| sP3_prd(X0,X1) ),
inference(resolution,[status(thm)],[f75,f118]) ).
fof(f131,plain,
! [X0,X1,X2] :
( three(X1,sK21_skl(X2,X0,X1))
| ~ member(X1,X2,X0)
| sP3_prd(X0,X1) ),
inference(resolution,[status(thm)],[f75,f117]) ).
fof(f132,plain,
! [X0,X1,X2] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| actual_world(sK13_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f42,f64]) ).
fof(f133,plain,
! [X0,X1,X2] :
( member(X0,sK11_skl(X1,X2,X0),X2)
| ~ sP3_prd(sK14_skl,sK13_skl)
| ~ hamburger(X0,sK12_skl(X2,X0))
| ~ group(X0,X2)
| ~ table(X0,X1)
| ~ actual_world(X0)
| sP0_prd ),
inference(resolution,[status(thm)],[f43,f64]) ).
fof(f134,plain,
! [X0,X1,X2,X3] :
( group(X3,sK16_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| sP1_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f53,f91]) ).
fof(f135,plain,
! [X0,X1,X2,X3] :
( three(X3,sK16_skl(X0,X1,X2,X3))
| ~ member(X3,X0,X1)
| sP1_prd(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f53,f90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP026+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.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.10/15.42 % CPULimit : 300
% 0.10/15.43 % WCLimit : 300
% 0.10/15.43 % DateTime : Mon Sep 21 01:36:47 UTC 2026
% 0.10/15.43 % CPUTime :
% 0.10/15.44 % Drodi V4.1.1
% 0.10/15.48 % SZS status CounterSatisfiable for theBenchmark: Theorem is counter-satisfiable, conjecture is false
% 0.10/15.48 % SZS output start Saturation for theBenchmark
% See solution above
% 0.34/15.50 % Elapsed time: 0.059441 seconds
% 0.34/15.50 % CPU time: 0.279262 seconds
% 0.34/15.50 % Total memory used: 24.895 MB
% 0.34/15.50 % Net memory used: 24.717 MB
%------------------------------------------------------------------------------