Vampire---5.0.1.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : NLP096+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n003.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 : Tue Sep 29 12:07:21 PM UTC 2026

% Result   : CounterSatisfiable 3.23s 1.32s
% Output   : Saturation 3.95s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u64,negated_conjecture,
    ( ~ in(sK16,X8,X9)
    | sP0(sK16,X8)
    | ~ restaurant(sK16,X9)
    | ~ customer(sK16,X8) ) ).

cnf(u89,negated_conjecture,
    ~ sP2 ).

cnf(u71,negated_conjecture,
    actual_world(sK16) ).

cnf(u75,negated_conjecture,
    ( in(X0,sK14(X0,X1),sK15(X0,X1))
    | ~ actual_world(X0)
    | ~ coffee(X0,X1) ) ).

cnf(u79,negated_conjecture,
    ( restaurant(X0,sK15(X0,X1))
    | ~ actual_world(X0)
    | ~ coffee(X0,X1) ) ).

cnf(u83,negated_conjecture,
    ( customer(X0,sK14(X0,X1))
    | ~ actual_world(X0)
    | ~ coffee(X0,X1) ) ).

cnf(u87,negated_conjecture,
    ( ~ see(X0,X6)
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,X6)
    | ~ past(X0,X6)
    | ~ patient(X0,X6,X4)
    | ~ agent(X0,X6,sK14(X0,X1))
    | ~ event(X0,X6)
    | ~ drink(X0,X5)
    | ~ nonreflexive(X0,X5)
    | ~ past(X0,X5)
    | ~ patient(X0,X5,X1)
    | ~ agent(X0,X5,X4)
    | ~ event(X0,X5)
    | ~ human_person(X0,X4)
    | ~ coffee(X0,X1) ) ).

cnf(u92,axiom,
    ( ~ in(sK5,X9,X10)
    | sP1(sK5,sK6,X9)
    | ~ restaurant(sK5,X10)
    | ~ customer(sK5,X9) ) ).

cnf(u96,axiom,
    coffee(sK5,sK6) ).

cnf(u119,axiom,
    ~ actual_world(sK5) ).

cnf(u104,axiom,
    ( in(X0,sK3(X0),sK4(X0))
    | ~ actual_world(X0) ) ).

cnf(u108,axiom,
    ( restaurant(X0,sK4(X0))
    | ~ actual_world(X0) ) ).

cnf(u116,axiom,
    ( ~ see(X0,X6)
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,X6)
    | ~ past(X0,X6)
    | ~ patient(X0,X6,X3)
    | ~ agent(X0,X6,sK3(X0))
    | ~ event(X0,X6)
    | ~ drink(X0,X5)
    | ~ nonreflexive(X0,X5)
    | ~ past(X0,X5)
    | ~ patient(X0,X5,X4)
    | ~ agent(X0,X5,X3)
    | ~ event(X0,X5)
    | ~ coffee(X0,X4)
    | ~ human_person(X0,X3) ) ).

cnf(u498,axiom,
    ~ sP1(sK5,sK6,sK3(sK5)) ).

cnf(u141,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X0))
    | ~ nonreflexive(sK5,sK12(sK5,X2))
    | ~ sP0(sK5,X2)
    | ~ sP0(sK5,X1)
    | ~ event(sK5,sK12(sK5,X2))
    | ~ sP0(sK5,X0)
    | ~ agent(sK5,sK12(sK5,X2),sK10(sK5,X1))
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ past(sK5,sK12(sK5,X2))
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X1))
    | ~ past(sK5,sK13(sK5,X0)) ) ).

cnf(u178,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X0,X1))
    | ~ nonreflexive(sK5,sK12(sK5,X3))
    | ~ sP0(sK5,X3)
    | ~ past(sK5,sK9(sK5,X0,X1))
    | ~ event(sK5,sK12(sK5,X3))
    | ~ sP0(sK5,X2)
    | ~ agent(sK5,sK12(sK5,X3),sK10(sK5,X2))
    | ~ patient(sK5,sK12(sK5,X3),sK6)
    | ~ past(sK5,sK12(sK5,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X2)) ) ).

cnf(u218,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X0))
    | ~ nonreflexive(sK5,sK8(sK5,X2,X3))
    | ~ sP0(sK5,X0)
    | ~ sP1(sK5,X2,X3)
    | ~ past(sK5,sK13(sK5,X0))
    | ~ event(sK5,sK8(sK5,X2,X3))
    | ~ sP0(sK5,X1)
    | ~ agent(sK5,sK8(sK5,X2,X3),sK10(sK5,X1))
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ past(sK5,sK8(sK5,X2,X3))
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X1)) ) ).

cnf(u224,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X0,X1))
    | ~ nonreflexive(sK5,sK8(sK5,X3,X4))
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK8(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ agent(sK5,sK8(sK5,X3,X4),sK10(sK5,X2))
    | ~ patient(sK5,sK8(sK5,X3,X4),sK6)
    | ~ past(sK5,sK8(sK5,X3,X4))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X2))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u290,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X0))
    | ~ nonreflexive(sK5,sK12(sK5,X3))
    | ~ sP0(sK5,X3)
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK12(sK5,X3))
    | ~ agent(sK5,sK12(sK5,X3),sK7(sK5,X1,X2))
    | ~ sP0(sK5,X0)
    | ~ patient(sK5,sK12(sK5,X3),sK6)
    | ~ past(sK5,sK12(sK5,X3))
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK7(sK5,X1,X2))
    | ~ past(sK5,sK13(sK5,X0)) ) ).

cnf(u296,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X0))
    | ~ nonreflexive(sK5,sK8(sK5,X3,X4))
    | ~ sP1(sK5,X3,X4)
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK8(sK5,X3,X4))
    | ~ agent(sK5,sK8(sK5,X3,X4),sK7(sK5,X1,X2))
    | ~ sP0(sK5,X0)
    | ~ patient(sK5,sK8(sK5,X3,X4),sK6)
    | ~ past(sK5,sK8(sK5,X3,X4))
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK7(sK5,X1,X2))
    | ~ past(sK5,sK13(sK5,X0)) ) ).

cnf(u306,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X0,X1))
    | ~ nonreflexive(sK5,sK12(sK5,X4))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK12(sK5,X4))
    | ~ agent(sK5,sK12(sK5,X4),sK7(sK5,X2,X3))
    | ~ sP0(sK5,X4)
    | ~ patient(sK5,sK12(sK5,X4),sK6)
    | ~ past(sK5,sK12(sK5,X4))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X2,X3))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u314,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X0,X1))
    | ~ nonreflexive(sK5,sK8(sK5,X4,X5))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK8(sK5,X4,X5))
    | ~ agent(sK5,sK8(sK5,X4,X5),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X4,X5)
    | ~ patient(sK5,sK8(sK5,X4,X5),sK6)
    | ~ past(sK5,sK8(sK5,X4,X5))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X2,X3))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u514,negated_conjecture,
    ~ customer(sK16,sK3(sK16)) ).

cnf(u526,negated_conjecture,
    ( ~ restaurant(sK16,sK15(sK16,X0))
    | ~ customer(sK16,sK14(sK16,X0))
    | ~ coffee(sK16,X0)
    | sP0(sK16,sK14(sK16,X0)) ) ).

cnf(u544,negated_conjecture,
    ( ~ customer(sK16,sK14(sK16,X0))
    | sP0(sK16,sK14(sK16,X0))
    | ~ coffee(sK16,X0) ) ).

cnf(u550,negated_conjecture,
    ( ~ coffee(sK16,X0)
    | sP0(sK16,sK14(sK16,X0)) ) ).

cnf(u228,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X2))
    | ~ sP0(sK5,X2)
    | ~ sP1(sK5,X0,X1)
    | ~ past(sK5,sK13(sK5,X2))
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK8(sK5,X0,X1),sK10(sK5,X3))
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ past(sK5,sK8(sK5,X0,X1))
    | ~ event(sK5,sK13(sK5,X2))
    | ~ agent(sK5,sK13(sK5,X2),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X2),sK10(sK5,X3)) ) ).

cnf(u404,axiom,
    ( ~ agent(X0,sK8(X0,sK11(X0,X2),X3),sK10(X0,X1))
    | ~ sP1(X0,sK11(X0,X2),X3)
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ event(X0,sK8(X0,sK11(X0,X2),X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ sP0(X0,X2) ) ).

cnf(u580,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u367,axiom,
    ( ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5) ) ).

cnf(u191,axiom,
    ( ~ past(sK5,sK9(sK5,X0,X1))
    | ~ past(sK5,sK12(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK12(sK5,X2))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK12(sK5,X2),sK10(sK5,X3))
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X3)) ) ).

cnf(u534,negated_conjecture,
    ( ~ drink(X0,X4)
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),X2)
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,X4)
    | ~ past(X0,X4)
    | ~ patient(X0,X4,X3)
    | ~ agent(X0,X4,X2)
    | ~ event(X0,X4)
    | ~ human_person(X0,X2)
    | ~ coffee(X0,X3)
    | ~ sP0(X0,X1) ) ).

cnf(u135,axiom,
    ( ~ human_person(X0,X3)
    | ~ nonreflexive(X0,sK13(X0,X2))
    | ~ past(X0,sK13(X0,X2))
    | ~ patient(X0,sK13(X0,X2),X3)
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X1))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),X4)
    | ~ agent(X0,sK12(X0,X1),X3)
    | ~ event(X0,sK12(X0,X1))
    | ~ coffee(X0,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2) ) ).

cnf(u578,negated_conjecture,
    ( ~ past(X0,sK12(X0,X3))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X4) ) ).

cnf(u707,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X2,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK9(X0,X2,X3),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5) ) ).

cnf(u652,negated_conjecture,
    ( ~ past(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),sK10(X0,X4))
    | ~ event(X0,sK13(X0,X3))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X4))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u138,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X1))
    | ~ nonreflexive(X0,sK12(X0,X3))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u442,axiom,
    ( ~ past(X0,sK9(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X7) ) ).

cnf(u37,axiom,
    ( past(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u49,axiom,
    ( nonreflexive(X0,sK12(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u596,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X6,X7))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ past(X0,sK8(X0,X6,X7))
    | ~ patient(X0,sK8(X0,X6,X7),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X6,X7),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X6,X7))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X6,X7)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u617,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X2,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X4,X5))
    | ~ past(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X2,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X2,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u724,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X7))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X7)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X7) ) ).

cnf(u40,axiom,
    ( event(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u213,axiom,
    ( ~ coffee(X0,X6)
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),X6)
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ actual_world(X0)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3) ) ).

cnf(u276,axiom,
    ( ~ past(X0,sK9(X0,X3,X4))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ patient(X0,sK9(X0,X3,X4),sK10(X0,X5))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u172,axiom,
    ( ~ human_person(X0,X3)
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),X3)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),X5)
    | ~ agent(X0,sK12(X0,X4),X3)
    | ~ event(X0,sK12(X0,X4))
    | ~ coffee(X0,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X4) ) ).

cnf(u283,axiom,
    ( ~ coffee(X0,X6)
    | ~ nonreflexive(X0,sK13(X0,X3))
    | ~ past(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),X6)
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X1,X2))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3) ) ).

cnf(u588,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X4) ) ).

cnf(u684,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5) ) ).

cnf(u343,axiom,
    ( ~ past(sK5,sK8(sK5,X0,X1))
    | ~ past(sK5,sK13(sK5,X4))
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X2,X3))
    | ~ sP0(sK5,X4)
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK13(sK5,X4))
    | ~ agent(sK5,sK13(sK5,X4),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X4),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3) ) ).

cnf(u387,axiom,
    ( ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ sP1(X0,X2,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u638,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X5) ) ).

cnf(u704,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X6))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X6) ) ).

cnf(u239,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X3))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X3))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK13(X0,X3),sK10(X0,X5))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u251,axiom,
    ( ~ past(sK5,sK8(sK5,X2,X3))
    | ~ sP0(sK5,X4)
    | ~ agent(sK5,sK8(sK5,X2,X3),sK10(sK5,X4))
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ sP1(sK5,X2,X3)
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X4))
    | ~ event(sK5,sK8(sK5,X2,X3)) ) ).

cnf(u698,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK13(X0,X3))
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X1) ) ).

cnf(u418,axiom,
    ( ~ past(sK5,sK8(sK5,X2,X3))
    | ~ agent(sK5,sK8(sK5,X2,X3),sK7(sK5,X4,X5))
    | ~ sP1(sK5,X2,X3)
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ sP1(sK5,X4,X5)
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X4,X5))
    | ~ event(sK5,sK8(sK5,X2,X3)) ) ).

cnf(u625,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u490,axiom,
    ( ~ agent(sK5,sK9(sK5,sK6,X0),sK3(sK5))
    | ~ event(sK5,sK9(sK5,sK6,X0))
    | ~ sP1(sK5,sK6,X0)
    | ~ event(sK5,sK8(sK5,sK6,X0)) ) ).

cnf(u632,negated_conjecture,
    ( ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X5,X6))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK14(X0,sK11(X0,X7)))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u157,axiom,
    ( ~ past(sK5,sK12(sK5,X1))
    | ~ event(sK5,sK12(sK5,X1))
    | ~ sP0(sK5,X0)
    | ~ agent(sK5,sK12(sK5,X1),sK10(sK5,X2))
    | ~ patient(sK5,sK12(sK5,X1),sK6)
    | ~ sP0(sK5,X1)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X2))
    | ~ sP0(sK5,X2) ) ).

cnf(u44,axiom,
    ( past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u201,axiom,
    ( ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X3))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK12(sK5,X2),sK10(sK5,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ event(sK5,sK12(sK5,X2)) ) ).

cnf(u568,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X5))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X5))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u160,axiom,
    ( ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u336,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X2,X3))
    | ~ sP1(sK5,X4,X5)
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X4,X5))
    | ~ sP1(sK5,X0,X1)
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ past(sK5,sK8(sK5,X0,X1))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK9(sK5,X2,X3))
    | ~ agent(sK5,sK9(sK5,X2,X3),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X2,X3),sK7(sK5,X4,X5))
    | ~ past(sK5,sK9(sK5,X2,X3)) ) ).

cnf(u51,axiom,
    ( patient(X0,sK12(X0,X1),sK11(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u670,negated_conjecture,
    ( ~ past(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u554,negated_conjecture,
    ( ~ human_person(X0,X2)
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),X2)
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),X3)
    | ~ agent(X0,sK8(X0,X4,X5),X2)
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ coffee(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5) ) ).

cnf(u744,axiom,
    ( ~ event(X0,sK9(X0,sK11(X0,X1),sK3(X0)))
    | ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),sK3(X0))
    | ~ event(X0,sK8(X0,sK11(X0,X1),sK3(X0)))
    | ~ sP0(X0,X1) ) ).

cnf(u183,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X2,X3))
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ past(X0,sK9(X0,X2,X3))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ patient(X0,sK9(X0,X2,X3),sK10(X0,X5))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u635,negated_conjecture,
    ( ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X3,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u686,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X2,X3),sK10(X0,X4))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK9(X0,X2,X3),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u693,negated_conjecture,
    ( ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X4,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u293,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X1))
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ sP1(X0,X2,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u422,axiom,
    ( ~ past(X0,sK13(X0,X3))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u29,axiom,
    ( see(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u745,negated_conjecture,
    ( ~ sP1(sK16,sK11(sK16,X0),sK14(sK16,sK11(sK16,X0)))
    | ~ sP0(sK16,X0) ) ).

cnf(u644,negated_conjecture,
    ( ~ past(X0,sK12(X0,X4))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5) ) ).

cnf(u32,axiom,
    ( patient(X0,sK9(X0,X1,X2),sK7(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u205,axiom,
    ( ~ past(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u136,axiom,
    ( ~ coffee(X0,X4)
    | ~ nonreflexive(X0,sK13(X0,X2))
    | ~ past(X0,sK13(X0,X2))
    | ~ patient(X0,sK13(X0,X2),sK10(X0,X1))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X3))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),X4)
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X1))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X2) ) ).

cnf(u263,axiom,
    ( ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ patient(sK5,sK9(sK5,X3,X4),sK10(sK5,X2))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK10(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK9(sK5,X3,X4))
    | ~ agent(sK5,sK9(sK5,X3,X4),sK3(sK5))
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK8(sK5,X0,X1)) ) ).

cnf(u55,axiom,
    ( human_person(X0,sK10(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u561,negated_conjecture,
    ( ~ coffee(X0,X3)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),X3)
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X2) ) ).

cnf(u676,negated_conjecture,
    ( ~ past(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X7)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X7) ) ).

cnf(u558,negated_conjecture,
    ( ~ coffee(X0,X4)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X5))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),X4)
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X5))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP1(X0,X2,X3) ) ).

cnf(u720,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u171,axiom,
    ( ~ drink(X0,X4)
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),X3)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ nonreflexive(X0,X4)
    | ~ past(X0,X4)
    | ~ patient(X0,X4,X5)
    | ~ agent(X0,X4,X3)
    | ~ event(X0,X4)
    | ~ coffee(X0,X5)
    | ~ human_person(X0,X3) ) ).

cnf(u747,axiom,
    ( ~ event(X0,sK8(X0,sK11(X0,X1),sK3(X0)))
    | ~ sP1(X0,sK11(X0,X1),sK3(X0))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1) ) ).

cnf(u573,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X2))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X3))
    | ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u277,axiom,
    ( ~ past(X0,sK8(X0,X3,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ actual_world(X0)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u162,axiom,
    ( ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ patient(sK5,sK13(sK5,X1),sK10(sK5,X2))
    | ~ agent(sK5,sK12(sK5,X0),sK10(sK5,X2))
    | ~ event(sK5,sK12(sK5,X0))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK13(sK5,X1))
    | ~ agent(sK5,sK13(sK5,X1),sK3(sK5))
    | ~ sP0(sK5,X1)
    | ~ sP0(sK5,X2) ) ).

cnf(u190,axiom,
    ( ~ nonreflexive(sK5,sK12(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ sP0(sK5,X2)
    | ~ past(sK5,sK9(sK5,X0,X1))
    | ~ event(sK5,sK12(sK5,X2))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK12(sK5,X2),sK10(sK5,X3))
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ past(sK5,sK12(sK5,X2))
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X3)) ) ).

cnf(u309,axiom,
    ( ~ past(sK5,sK12(sK5,X0))
    | ~ past(sK5,sK13(sK5,X3))
    | ~ event(sK5,sK12(sK5,X0))
    | ~ agent(sK5,sK12(sK5,X0),sK7(sK5,X1,X2))
    | ~ sP0(sK5,X3)
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK13(sK5,X3))
    | ~ agent(sK5,sK13(sK5,X3),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X3),sK7(sK5,X1,X2))
    | ~ sP1(sK5,X1,X2) ) ).

cnf(u341,axiom,
    ( ~ nonreflexive(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X2,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u175,axiom,
    ( ~ nonreflexive(X0,sK12(X0,X4))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ actual_world(X0)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5) ) ).

cnf(u457,axiom,
    ( ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ actual_world(X0)
    | ~ event(X0,sK12(X0,X1)) ) ).

cnf(u607,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X2,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X4))
    | ~ past(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X4))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u459,axiom,
    ( ~ event(X0,sK13(X0,sK3(X0)))
    | ~ sP0(X0,sK3(X0))
    | ~ actual_world(X0)
    | ~ event(X0,sK12(X0,sK3(X0))) ) ).

cnf(u36,axiom,
    ( nonreflexive(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u608,negated_conjecture,
    ( ~ nonreflexive(X0,sK13(X0,X3))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X3),sK10(X0,X4))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X4))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK13(X0,X3))
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u711,negated_conjecture,
    ( ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X5,X6))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X7)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u560,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X4))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X3))
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X4))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X3)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u31,axiom,
    ( past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u43,axiom,
    ( nonreflexive(X0,sK13(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u488,axiom,
    ( ~ agent(sK5,sK8(sK5,sK6,X2),sK7(sK5,X0,X1))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ sP1(sK5,sK6,X2)
    | ~ event(sK5,sK8(sK5,sK6,X2)) ) ).

cnf(u439,axiom,
    ( ~ patient(X0,sK13(X0,X2),sK7(X0,X3,X4))
    | ~ sP0(X0,X1)
    | ~ event(X0,sK13(X0,X2))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X2) ) ).

cnf(u555,negated_conjecture,
    ( ~ human_person(X0,X3)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),X3)
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X5))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),X4)
    | ~ agent(X0,sK12(X0,X5),X3)
    | ~ event(X0,sK12(X0,X5))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ coffee(X0,X4)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u483,axiom,
    ( ~ agent(X0,sK12(X0,X3),sK7(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ sP1(X0,X1,X2)
    | ~ event(X0,sK12(X0,X3))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3) ) ).

cnf(u34,axiom,
    ( event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u207,axiom,
    ( ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u270,axiom,
    ( ~ past(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK13(X0,X3),sK10(X0,X5))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u282,axiom,
    ( ~ coffee(X0,X7)
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),X7)
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X1,X2))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6) ) ).

cnf(u722,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X3,X4),sK10(X0,X5))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X1) ) ).

cnf(u621,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X4,X5))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u285,axiom,
    ( ~ coffee(X0,X5)
    | ~ nonreflexive(X0,sK13(X0,X3))
    | ~ past(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),X5)
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X1,X2))
    | ~ event(X0,sK12(X0,X4))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X3) ) ).

cnf(u210,axiom,
    ( ~ human_person(X0,X5)
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X3,X4),X5)
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ nonreflexive(X0,sK8(X0,X1,X2))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),X6)
    | ~ agent(X0,sK8(X0,X1,X2),X5)
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ coffee(X0,X6)
    | ~ sP1(X0,X1,X2) ) ).

cnf(u238,axiom,
    ( ~ nonreflexive(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X5))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u329,axiom,
    ( ~ nonreflexive(sK5,sK12(sK5,X2))
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK12(sK5,X2))
    | ~ agent(sK5,sK12(sK5,X2),sK7(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ past(sK5,sK12(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X3,X4))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u389,axiom,
    ( ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X5))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u181,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X1,X2))
    | ~ sP0(sK5,X0)
    | ~ past(sK5,sK9(sK5,X1,X2))
    | ~ event(sK5,sK12(sK5,X0))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK12(sK5,X0),sK10(sK5,X3))
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ past(sK5,sK12(sK5,X0))
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK9(sK5,X1,X2))
    | ~ agent(sK5,sK9(sK5,X1,X2),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X1,X2),sK10(sK5,X3)) ) ).

cnf(u253,axiom,
    ( ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X2,X3))
    | ~ actual_world(X0)
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X5))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u535,negated_conjecture,
    ( ~ drink(X0,X5)
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),X3)
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,X5)
    | ~ past(X0,X5)
    | ~ patient(X0,X5,X4)
    | ~ agent(X0,X5,X3)
    | ~ event(X0,X5)
    | ~ human_person(X0,X3)
    | ~ coffee(X0,X4)
    | ~ sP1(X0,X1,X2) ) ).

cnf(u716,negated_conjecture,
    ( ~ agent(X0,sK12(X0,X1),sK7(X0,X2,sK14(X0,sK11(X0,X1))))
    | ~ event(X0,sK12(X0,X1))
    | ~ event(X0,sK9(X0,X2,sK14(X0,sK11(X0,X1))))
    | ~ actual_world(X0)
    | ~ sP1(X0,X2,sK14(X0,sK11(X0,X1)))
    | ~ sP0(X0,X1) ) ).

cnf(u311,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u244,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X3,X4),sK10(X0,X5))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u355,axiom,
    ( ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X7) ) ).

cnf(u383,axiom,
    ( ~ past(sK5,sK8(sK5,X2,X3))
    | ~ past(sK5,sK9(sK5,X4,X5))
    | ~ agent(sK5,sK8(sK5,X2,X3),sK7(sK5,X0,X1))
    | ~ sP1(sK5,X2,X3)
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ sP1(sK5,X4,X5)
    | ~ event(sK5,sK9(sK5,X4,X5))
    | ~ agent(sK5,sK9(sK5,X4,X5),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X4,X5),sK7(sK5,X0,X1))
    | ~ event(sK5,sK8(sK5,X2,X3)) ) ).

cnf(u640,negated_conjecture,
    ( ~ past(X0,sK8(X0,X3,X4))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u487,axiom,
    ( ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ agent(sK5,sK8(sK5,X2,X3),sK7(sK5,X0,X1))
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK8(sK5,X2,X3)) ) ).

cnf(u594,negated_conjecture,
    ( ~ patient(X0,sK12(X0,X2),sK11(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X1))
    | ~ event(X0,sK12(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X3)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u38,axiom,
    ( patient(X0,sK8(X0,X1,X2),X1)
    | ~ sP1(X0,X1,X2) ) ).

cnf(u654,negated_conjecture,
    ( ~ past(X0,sK8(X0,X4,X5))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u565,negated_conjecture,
    ( ~ coffee(X0,X4)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),X4)
    | ~ agent(X0,sK8(X0,X5,X6),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X3) ) ).

cnf(u261,axiom,
    ( ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ patient(sK5,sK13(sK5,X2),sK10(sK5,X3))
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK8(sK5,X0,X1),sK10(sK5,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK13(sK5,X2))
    | ~ agent(sK5,sK13(sK5,X2),sK3(sK5))
    | ~ sP0(sK5,X2) ) ).

cnf(u53,axiom,
    ( event(X0,sK12(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u333,axiom,
    ( ~ nonreflexive(X0,sK12(X0,X2))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X3,X4))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X2))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5) ) ).

cnf(u449,axiom,
    ( ~ patient(sK5,sK9(sK5,X1,X2),sK7(sK5,X3,X4))
    | ~ agent(sK5,sK8(sK5,sK6,X0),sK7(sK5,X3,X4))
    | ~ sP1(sK5,X3,X4)
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK9(sK5,X1,X2))
    | ~ agent(sK5,sK9(sK5,X1,X2),sK3(sK5))
    | ~ sP1(sK5,sK6,X0)
    | ~ event(sK5,sK8(sK5,sK6,X0)) ) ).

cnf(u730,negated_conjecture,
    ( ~ agent(X0,sK8(X0,sK11(X0,X3),X4),sK7(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ event(X0,sK8(X0,sK11(X0,X3),X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X3)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,sK11(X0,X3),X4)
    | ~ sP0(X0,X3) ) ).

cnf(u188,axiom,
    ( ~ nonreflexive(X0,sK12(X0,X3))
    | ~ sP1(X0,X1,X2)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u364,axiom,
    ( ~ past(sK5,sK12(sK5,X2))
    | ~ agent(sK5,sK12(sK5,X2),sK7(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ sP1(sK5,X3,X4)
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X3,X4))
    | ~ event(sK5,sK12(sK5,X2)) ) ).

cnf(u679,negated_conjecture,
    ( ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X4))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u232,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X2,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ sP0(sK5,X4)
    | ~ agent(sK5,sK8(sK5,X0,X1),sK10(sK5,X4))
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ past(sK5,sK8(sK5,X0,X1))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK9(sK5,X2,X3))
    | ~ agent(sK5,sK9(sK5,X2,X3),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X2,X3),sK10(sK5,X4))
    | ~ past(sK5,sK9(sK5,X2,X3)) ) ).

cnf(u359,axiom,
    ( ~ past(sK5,sK12(sK5,X2))
    | ~ past(sK5,sK9(sK5,X3,X4))
    | ~ agent(sK5,sK12(sK5,X2),sK7(sK5,X0,X1))
    | ~ sP0(sK5,X2)
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK9(sK5,X3,X4))
    | ~ agent(sK5,sK9(sK5,X3,X4),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X3,X4),sK7(sK5,X0,X1))
    | ~ event(sK5,sK12(sK5,X2)) ) ).

cnf(u631,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X5,X6))
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X7)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u403,axiom,
    ( ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X4))
    | ~ sP0(X0,X1)
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X1))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u431,axiom,
    ( ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5) ) ).

cnf(u463,axiom,
    ( ~ event(X0,sK12(X0,sK3(X0)))
    | ~ actual_world(X0)
    | ~ sP0(X0,sK3(X0)) ) ).

cnf(u666,negated_conjecture,
    ( ~ agent(X0,sK8(X0,sK11(X0,X2),X3),sK10(X0,X1))
    | ~ event(X0,sK13(X0,X1))
    | ~ event(X0,sK8(X0,sK11(X0,X2),X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X2)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,sK11(X0,X2),X3)
    | ~ sP0(X0,X2) ) ).

cnf(u598,negated_conjecture,
    ( ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X2)))
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X1))
    | ~ event(X0,sK12(X0,X2))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2) ) ).

cnf(u318,axiom,
    ( ~ past(sK5,sK12(sK5,X1))
    | ~ event(sK5,sK12(sK5,X1))
    | ~ agent(sK5,sK12(sK5,X1),sK7(sK5,X2,X3))
    | ~ sP0(sK5,X0)
    | ~ patient(sK5,sK12(sK5,X1),sK6)
    | ~ sP0(sK5,X1)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3) ) ).

cnf(u642,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK13(X0,X2))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK13(X0,X2),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X3,X4) ) ).

cnf(u553,negated_conjecture,
    ( ~ human_person(X0,X2)
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),X2)
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),X3)
    | ~ agent(X0,sK12(X0,X4),X2)
    | ~ event(X0,sK12(X0,X4))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ coffee(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u130,axiom,
    ( ~ drink(X0,X3)
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),X2)
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,X3)
    | ~ past(X0,X3)
    | ~ patient(X0,X3,X4)
    | ~ agent(X0,X3,X2)
    | ~ event(X0,X3)
    | ~ coffee(X0,X4)
    | ~ human_person(X0,X2)
    | ~ sP0(X0,X1) ) ).

cnf(u377,axiom,
    ( ~ patient(sK5,sK13(sK5,X1),sK10(sK5,X2))
    | ~ sP1(sK5,sK6,X0)
    | ~ event(sK5,sK8(sK5,sK6,X0))
    | ~ sP0(sK5,X2)
    | ~ agent(sK5,sK8(sK5,sK6,X0),sK10(sK5,X2))
    | ~ event(sK5,sK13(sK5,X1))
    | ~ agent(sK5,sK13(sK5,X1),sK3(sK5))
    | ~ sP0(sK5,X1) ) ).

cnf(u41,axiom,
    ( human_person(X0,sK7(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u30,axiom,
    ( nonreflexive(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u437,axiom,
    ( ~ patient(X0,sK9(X0,X2,X3),sK10(X0,X4))
    | ~ sP0(X0,X1)
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X2,X3)
    | ~ actual_world(X0)
    | ~ sP0(X0,X4) ) ).

cnf(u509,negated_conjecture,
    ~ sP0(sK16,sK3(sK16)) ).

cnf(u145,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X1))
    | ~ sP0(sK5,X0)
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK12(sK5,X0))
    | ~ sP0(sK5,X1)
    | ~ agent(sK5,sK12(sK5,X0),sK10(sK5,X2))
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ past(sK5,sK12(sK5,X0))
    | ~ event(sK5,sK13(sK5,X1))
    | ~ agent(sK5,sK13(sK5,X1),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X1),sK10(sK5,X2))
    | ~ past(sK5,sK13(sK5,X1)) ) ).

cnf(u173,axiom,
    ( ~ coffee(X0,X5)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),X5)
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X3) ) ).

cnf(u601,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X2))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X3,X4))
    | ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u340,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X3))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u303,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ nonreflexive(X0,sK12(X0,X5))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X5))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u412,axiom,
    ( ~ past(X0,sK13(X0,X2))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u347,axiom,
    ( ~ nonreflexive(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP1(X0,X4,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u570,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X3))
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X3)))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u708,negated_conjecture,
    ( ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X1,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X4)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u407,axiom,
    ( ~ agent(sK5,sK8(sK5,sK6,X1),sK10(sK5,X0))
    | ~ sP1(sK5,sK6,X1)
    | ~ event(sK5,sK8(sK5,sK6,X1))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5)) ) ).

cnf(u451,axiom,
    ( ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ sP1(X0,X2,X3)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u583,negated_conjecture,
    ( ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u378,axiom,
    ( ~ patient(sK5,sK9(sK5,X1,X2),sK10(sK5,X3))
    | ~ sP1(sK5,sK6,X0)
    | ~ agent(sK5,sK8(sK5,sK6,X0),sK10(sK5,X3))
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK9(sK5,X1,X2))
    | ~ agent(sK5,sK9(sK5,X1,X2),sK3(sK5))
    | ~ sP0(sK5,X3)
    | ~ event(sK5,sK8(sK5,sK6,X0)) ) ).

cnf(u52,axiom,
    ( agent(X0,sK12(X0,X1),sK10(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u438,axiom,
    ( ~ agent(X0,sK12(X0,X1),sK10(X0,X2))
    | ~ sP0(X0,X2)
    | ~ event(X0,sK13(X0,X2))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ event(X0,sK12(X0,X1)) ) ).

cnf(u45,axiom,
    ( patient(X0,sK13(X0,X1),sK10(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u661,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X3),sK10(X0,X4))
    | ~ event(X0,sK13(X0,X3))
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK10(X0,X4))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X1) ) ).

cnf(u287,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X1))
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5) ) ).

cnf(u149,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X2))
    | ~ patient(X0,sK13(X0,X2),sK10(X0,X3))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X2))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X4) ) ).

cnf(u48,axiom,
    ( drink(X0,sK12(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u221,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ nonreflexive(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ actual_world(X0)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u284,axiom,
    ( ~ coffee(X0,X6)
    | ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ nonreflexive(X0,sK12(X0,X5))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),X6)
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X1,X2))
    | ~ event(X0,sK12(X0,X5))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ sP0(X0,X5) ) ).

cnf(u152,axiom,
    ( ~ past(sK5,sK12(sK5,X0))
    | ~ past(sK5,sK13(sK5,X2))
    | ~ event(sK5,sK12(sK5,X0))
    | ~ sP0(sK5,X2)
    | ~ agent(sK5,sK12(sK5,X0),sK10(sK5,X1))
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK13(sK5,X2))
    | ~ agent(sK5,sK13(sK5,X2),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X2),sK10(sK5,X1))
    | ~ sP0(sK5,X1) ) ).

cnf(u328,axiom,
    ( ~ nonreflexive(sK5,sK9(sK5,X1,X2))
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK12(sK5,X0))
    | ~ agent(sK5,sK12(sK5,X0),sK7(sK5,X3,X4))
    | ~ sP0(sK5,X0)
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ past(sK5,sK12(sK5,X0))
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK9(sK5,X1,X2))
    | ~ agent(sK5,sK9(sK5,X1,X2),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X1,X2),sK7(sK5,X3,X4))
    | ~ past(sK5,sK9(sK5,X1,X2)) ) ).

cnf(u279,axiom,
    ( ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ sP1(X0,X1,X2)
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ actual_world(X0)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u212,axiom,
    ( ~ coffee(X0,X5)
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),X5)
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2) ) ).

cnf(u351,axiom,
    ( ~ past(sK5,sK13(sK5,X2))
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK13(sK5,X2))
    | ~ agent(sK5,sK13(sK5,X2),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X2),sK7(sK5,X3,X4))
    | ~ sP1(sK5,X3,X4) ) ).

cnf(u736,negated_conjecture,
    ( ~ event(X0,sK9(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1))))
    | ~ event(X0,sK8(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1))))
    | ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1)))
    | ~ sP0(X0,X1) ) ).

cnf(u395,axiom,
    ( ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u618,negated_conjecture,
    ( ~ nonreflexive(X0,sK13(X0,X3))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK13(X0,X3))
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u455,axiom,
    ( ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X6))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ sP1(X0,X1,X2)
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X5))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u247,axiom,
    ( ~ past(sK5,sK8(sK5,X0,X1))
    | ~ past(sK5,sK9(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ agent(sK5,sK8(sK5,X0,X1),sK10(sK5,X2))
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK9(sK5,X3,X4))
    | ~ agent(sK5,sK9(sK5,X3,X4),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X3,X4),sK10(sK5,X2))
    | ~ event(sK5,sK8(sK5,X0,X1)) ) ).

cnf(u690,negated_conjecture,
    ( ~ past(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK13(X0,X3))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK13(X0,X3),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u750,negated_conjecture,
    ( ~ sP1(sK16,sK11(sK16,X0),sK3(sK16))
    | ~ sP0(sK16,X0) ) ).

cnf(u354,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X1,X2),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X7) ) ).

cnf(u357,axiom,
    ( ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ patient(sK5,sK13(sK5,X4),sK7(sK5,X2,X3))
    | ~ sP0(sK5,X4)
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK13(sK5,X4))
    | ~ agent(sK5,sK13(sK5,X4),sK3(sK5))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3) ) ).

cnf(u369,axiom,
    ( ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ patient(sK5,sK9(sK5,X3,X4),sK7(sK5,X1,X2))
    | ~ agent(sK5,sK12(sK5,X0),sK7(sK5,X1,X2))
    | ~ sP1(sK5,X1,X2)
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK9(sK5,X3,X4))
    | ~ agent(sK5,sK9(sK5,X3,X4),sK3(sK5))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK12(sK5,X0)) ) ).

cnf(u33,axiom,
    ( agent(X0,sK9(X0,X1,X2),X2)
    | ~ sP1(X0,X1,X2) ) ).

cnf(u486,axiom,
    ( ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ sP1(sK5,X0,X1)
    | ~ agent(sK5,sK12(sK5,X2),sK7(sK5,X0,X1))
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK12(sK5,X2)) ) ).

cnf(u429,axiom,
    ( ~ past(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP1(X0,X4,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u197,axiom,
    ( ~ past(sK5,sK12(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK12(sK5,X2))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK12(sK5,X2),sK10(sK5,X3))
    | ~ patient(sK5,sK12(sK5,X2),sK6)
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X3)) ) ).

cnf(u564,negated_conjecture,
    ( ~ coffee(X0,X5)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X6))
    | ~ past(X0,sK12(X0,X6))
    | ~ patient(X0,sK12(X0,X6),X5)
    | ~ agent(X0,sK12(X0,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X6))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X6)
    | ~ sP1(X0,X3,X4) ) ).

cnf(u332,axiom,
    ( ~ nonreflexive(X0,sK13(X0,X2))
    | ~ patient(X0,sK13(X0,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X2))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u47,axiom,
    ( event(X0,sK13(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u562,negated_conjecture,
    ( ~ coffee(X0,X4)
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),X4)
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X2,X3) ) ).

cnf(u740,negated_conjecture,
    ( ~ event(X0,sK8(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1))))
    | ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1)))
    | ~ sP0(X0,X1) ) ).

cnf(u622,negated_conjecture,
    ( ~ nonreflexive(X0,sK9(X0,X2,X3))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X2,X3),sK7(X0,X4,X5))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK9(X0,X2,X3),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u50,axiom,
    ( past(X0,sK12(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u586,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X6))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ past(X0,sK12(X0,X6))
    | ~ patient(X0,sK12(X0,X6),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X6)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u235,axiom,
    ( ~ past(sK5,sK13(sK5,X0))
    | ~ past(sK5,sK8(sK5,X1,X2))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK8(sK5,X1,X2))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK8(sK5,X1,X2),sK10(sK5,X3))
    | ~ patient(sK5,sK8(sK5,X1,X2),sK6)
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X3)) ) ).

cnf(u738,axiom,
    ( ~ agent(X0,sK9(X0,sK11(X0,X1),X2),sK3(X0))
    | ~ actual_world(X0)
    | ~ event(X0,sK9(X0,sK11(X0,X1),X2))
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ sP0(X0,X1) ) ).

cnf(u402,axiom,
    ( ~ patient(X0,sK12(X0,X2),sK11(X0,X3))
    | ~ sP0(X0,X1)
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X1))
    | ~ event(X0,sK12(X0,X2))
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u405,axiom,
    ( ~ patient(sK5,sK12(sK5,X1),sK6)
    | ~ sP0(sK5,X0)
    | ~ agent(sK5,sK12(sK5,X1),sK10(sK5,X0))
    | ~ event(sK5,sK12(sK5,X1))
    | ~ sP0(sK5,X1)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5)) ) ).

cnf(u241,axiom,
    ( ~ past(sK5,sK8(sK5,X1,X2))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK8(sK5,X1,X2))
    | ~ sP0(sK5,X3)
    | ~ agent(sK5,sK8(sK5,X1,X2),sK10(sK5,X3))
    | ~ patient(sK5,sK8(sK5,X1,X2),sK6)
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X3)) ) ).

cnf(u376,axiom,
    ( ~ patient(X0,sK9(X0,X3,X4),sK10(X0,X5))
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ sP1(X0,X3,X4)
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ actual_world(X0)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X1) ) ).

cnf(u552,negated_conjecture,
    ( sP0(sK16,sK14(sK16,sK11(sK16,X0)))
    | ~ sP0(sK16,X0) ) ).

cnf(u436,axiom,
    ( ~ patient(X0,sK13(X0,X2),sK10(X0,X3))
    | ~ sP0(X0,X1)
    | ~ event(X0,sK13(X0,X2))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X2) ) ).

cnf(u612,negated_conjecture,
    ( ~ nonreflexive(X0,sK9(X0,X2,X3))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X2,X3),sK10(X0,X4))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X4))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK9(X0,X2,X3),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u35,axiom,
    ( drink(X0,sK8(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u204,axiom,
    ( ~ past(X0,sK9(X0,X2,X3))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ patient(X0,sK9(X0,X2,X3),sK10(X0,X5))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u656,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X5))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u443,axiom,
    ( ~ past(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X7))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X7) ) ).

cnf(u485,axiom,
    ( ~ agent(X0,sK8(X0,sK11(X0,X3),X4),sK7(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ event(X0,sK8(X0,sK11(X0,X3),X4))
    | ~ sP1(X0,sK11(X0,X3),X4)
    | ~ sP0(X0,X3) ) ).

cnf(u566,negated_conjecture,
    ( ~ coffee(X0,X5)
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X6,X7))
    | ~ past(X0,sK8(X0,X6,X7))
    | ~ patient(X0,sK8(X0,X6,X7),X5)
    | ~ agent(X0,sK8(X0,X6,X7),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X6,X7))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X6,X7)
    | ~ sP1(X0,X3,X4) ) ).

cnf(u728,negated_conjecture,
    ( ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X1,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u167,axiom,
    ( ~ past(X0,sK13(X0,X2))
    | ~ event(X0,sK13(X0,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK13(X0,X2),sK10(X0,X3))
    | ~ agent(X0,sK13(X0,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X4) ) ).

cnf(u54,axiom,
    ( coffee(X0,sK11(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u211,axiom,
    ( ~ human_person(X0,X4)
    | ~ nonreflexive(X0,sK13(X0,X3))
    | ~ past(X0,sK13(X0,X3))
    | ~ patient(X0,sK13(X0,X3),X4)
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X1,X2))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),X5)
    | ~ agent(X0,sK8(X0,X1,X2),X4)
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ coffee(X0,X5)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u576,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X5))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X5),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X4)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u714,negated_conjecture,
    ( ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X3)))
    | ~ agent(X0,sK12(X0,X3),sK7(X0,X1,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3) ) ).

cnf(u742,negated_conjecture,
    ( ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),sK14(X0,sK11(X0,X1)))
    | ~ sP0(X0,X1) ) ).

cnf(u170,axiom,
    ( ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X3))
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u346,axiom,
    ( ~ nonreflexive(X0,sK9(X0,X2,X3))
    | ~ patient(X0,sK9(X0,X2,X3),sK7(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ past(X0,sK9(X0,X2,X3))
    | ~ past(X0,sK12(X0,X1))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X4,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u749,axiom,
    ( ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),sK3(X0))
    | ~ sP0(X0,X1) ) ).

cnf(u474,axiom,
    ( ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X5,X6))
    | ~ sP1(X0,X3,X4)
    | ~ actual_world(X0)
    | ~ agent(X0,sK9(X0,X3,X4),sK3(X0))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ sP1(X0,X5,X6)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP0(X0,X1) ) ).

cnf(u406,axiom,
    ( ~ patient(sK5,sK8(sK5,X1,X2),sK6)
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK8(sK5,X1,X2))
    | ~ agent(sK5,sK8(sK5,X1,X2),sK10(sK5,X0))
    | ~ sP1(sK5,X1,X2)
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5)) ) ).

cnf(u273,axiom,
    ( ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X4))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X5))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u701,negated_conjecture,
    ( ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u734,negated_conjecture,
    ( ~ agent(X0,sK9(X0,sK11(X0,X1),X2),sK14(X0,sK11(X0,X1)))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ event(X0,sK9(X0,sK11(X0,X1),X2))
    | ~ actual_world(X0)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP0(X0,X1) ) ).

cnf(u379,axiom,
    ( ~ patient(sK5,sK13(sK5,X1),sK7(sK5,X2,X3))
    | ~ sP1(sK5,sK6,X0)
    | ~ sP0(sK5,X1)
    | ~ event(sK5,sK8(sK5,sK6,X0))
    | ~ event(sK5,sK13(sK5,X1))
    | ~ agent(sK5,sK13(sK5,X1),sK3(sK5))
    | ~ agent(sK5,sK8(sK5,sK6,X0),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3) ) ).

cnf(u453,axiom,
    ( ~ patient(X0,sK13(X0,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK13(X0,X3))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ actual_world(X0)
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK7(X0,X4,X5))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X1) ) ).

cnf(u465,axiom,
    ( ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X7))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK8(X0,X5,X6),sK7(X0,X3,X4))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X7) ) ).

cnf(u556,negated_conjecture,
    ( ~ human_person(X0,X3)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),X3)
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),X4)
    | ~ agent(X0,sK8(X0,X5,X6),X3)
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ coffee(X0,X4)
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6) ) ).

cnf(u375,axiom,
    ( ~ patient(X0,sK13(X0,X3),sK10(X0,X4))
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ event(X0,sK13(X0,X3))
    | ~ actual_world(X0)
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK10(X0,X4))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ agent(X0,sK13(X0,X3),sK3(X0))
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X1) ) ).

cnf(u39,axiom,
    ( agent(X0,sK8(X0,X1,X2),sK7(X0,X1,X2))
    | ~ sP1(X0,X1,X2) ) ).

cnf(u484,axiom,
    ( ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X5))
    | ~ sP1(X0,X1,X2)
    | ~ actual_world(X0)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ agent(X0,sK8(X0,X3,X4),sK7(X0,X1,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u447,axiom,
    ( ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ patient(sK5,sK9(sK5,X4,X5),sK7(sK5,X2,X3))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3)
    | ~ sP1(sK5,X4,X5)
    | ~ event(sK5,sK9(sK5,X4,X5))
    | ~ agent(sK5,sK9(sK5,X4,X5),sK3(sK5))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK8(sK5,X0,X1)) ) ).

cnf(u563,negated_conjecture,
    ( ~ coffee(X0,X4)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X5))
    | ~ past(X0,sK12(X0,X5))
    | ~ patient(X0,sK12(X0,X5),X4)
    | ~ agent(X0,sK12(X0,X5),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X5))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X3) ) ).

cnf(u245,axiom,
    ( ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ actual_world(X0)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u42,axiom,
    ( see(X0,sK13(X0,X1))
    | ~ sP0(X0,X1) ) ).

cnf(u215,axiom,
    ( ~ nonreflexive(X0,sK8(X0,X3,X4))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK8(X0,X3,X4),sK11(X0,X5))
    | ~ agent(X0,sK8(X0,X3,X4),sK10(X0,X2))
    | ~ event(X0,sK8(X0,X3,X4))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X5) ) ).

cnf(u658,negated_conjecture,
    ( ~ past(X0,sK12(X0,X5))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK9(X0,X1,X2),sK7(X0,X3,X4))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ patient(X0,sK12(X0,X5),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X5),sK7(X0,X3,X4))
    | ~ event(X0,sK12(X0,X5))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP1(X0,X3,X4)
    | ~ sP0(X0,X6) ) ).

cnf(u593,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X2),sK10(X0,X3))
    | ~ event(X0,sK13(X0,X2))
    | ~ agent(X0,sK12(X0,X1),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X1))
    | ~ agent(X0,sK13(X0,X2),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X3) ) ).

cnf(u557,negated_conjecture,
    ( ~ coffee(X0,X3)
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X2))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ nonreflexive(X0,sK12(X0,X4))
    | ~ past(X0,sK12(X0,X4))
    | ~ patient(X0,sK12(X0,X4),X3)
    | ~ agent(X0,sK12(X0,X4),sK10(X0,X2))
    | ~ event(X0,sK12(X0,X4))
    | ~ nonreflexive(X0,sK13(X0,X1))
    | ~ past(X0,sK13(X0,X1))
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X2) ) ).

cnf(u727,negated_conjecture,
    ( ~ patient(X0,sK9(X0,X3,X4),sK7(X0,X5,X6))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ agent(X0,sK8(X0,sK11(X0,X1),X2),sK7(X0,X5,X6))
    | ~ event(X0,sK8(X0,sK11(X0,X1),X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK14(X0,sK11(X0,X1)))
    | ~ actual_world(X0)
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,sK11(X0,X1),X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X1) ) ).

cnf(u146,axiom,
    ( ~ nonreflexive(sK5,sK12(sK5,X1))
    | ~ sP0(sK5,X1)
    | ~ sP0(sK5,X2)
    | ~ event(sK5,sK12(sK5,X1))
    | ~ sP0(sK5,X0)
    | ~ agent(sK5,sK12(sK5,X1),sK10(sK5,X2))
    | ~ patient(sK5,sK12(sK5,X1),sK6)
    | ~ past(sK5,sK12(sK5,X1))
    | ~ event(sK5,sK13(sK5,X0))
    | ~ agent(sK5,sK13(sK5,X0),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X0),sK10(sK5,X2))
    | ~ past(sK5,sK13(sK5,X0)) ) ).

cnf(u322,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X2))
    | ~ sP1(sK5,X0,X1)
    | ~ sP1(sK5,X3,X4)
    | ~ event(sK5,sK8(sK5,X0,X1))
    | ~ agent(sK5,sK8(sK5,X0,X1),sK7(sK5,X3,X4))
    | ~ sP0(sK5,X2)
    | ~ patient(sK5,sK8(sK5,X0,X1),sK6)
    | ~ past(sK5,sK8(sK5,X0,X1))
    | ~ event(sK5,sK13(sK5,X2))
    | ~ agent(sK5,sK13(sK5,X2),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X2),sK7(sK5,X3,X4))
    | ~ past(sK5,sK13(sK5,X2)) ) ).

cnf(u265,axiom,
    ( ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK8(X0,X4,X5))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X4,X5),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ actual_world(X0)
    | ~ sP1(X0,X4,X5)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u325,axiom,
    ( ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ patient(sK5,sK13(sK5,X3),sK7(sK5,X1,X2))
    | ~ sP0(sK5,X3)
    | ~ event(sK5,sK12(sK5,X0))
    | ~ sP0(sK5,X0)
    | ~ event(sK5,sK13(sK5,X3))
    | ~ agent(sK5,sK13(sK5,X3),sK3(sK5))
    | ~ agent(sK5,sK12(sK5,X0),sK7(sK5,X1,X2))
    | ~ sP1(sK5,X1,X2) ) ).

cnf(u337,axiom,
    ( ~ nonreflexive(sK5,sK8(sK5,X2,X3))
    | ~ sP1(sK5,X4,X5)
    | ~ event(sK5,sK8(sK5,X2,X3))
    | ~ agent(sK5,sK8(sK5,X2,X3),sK7(sK5,X4,X5))
    | ~ sP1(sK5,X2,X3)
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ past(sK5,sK8(sK5,X2,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK7(sK5,X4,X5))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u189,axiom,
    ( ~ past(X0,sK9(X0,X1,X2))
    | ~ past(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ agent(X0,sK9(X0,X1,X2),sK3(X0))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X5))
    | ~ event(X0,sK12(X0,X3))
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X5))
    | ~ actual_world(X0)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X4) ) ).

cnf(u233,axiom,
    ( ~ nonreflexive(sK5,sK8(sK5,X2,X3))
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK8(sK5,X2,X3))
    | ~ sP0(sK5,X4)
    | ~ agent(sK5,sK8(sK5,X2,X3),sK10(sK5,X4))
    | ~ patient(sK5,sK8(sK5,X2,X3),sK6)
    | ~ past(sK5,sK8(sK5,X2,X3))
    | ~ sP1(sK5,X0,X1)
    | ~ event(sK5,sK9(sK5,X0,X1))
    | ~ agent(sK5,sK9(sK5,X0,X1),sK3(sK5))
    | ~ patient(sK5,sK9(sK5,X0,X1),sK10(sK5,X4))
    | ~ past(sK5,sK9(sK5,X0,X1)) ) ).

cnf(u628,negated_conjecture,
    ( ~ past(X0,sK12(X0,X4))
    | ~ past(X0,sK13(X0,X1))
    | ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ event(X0,sK13(X0,X1))
    | ~ patient(X0,sK12(X0,X4),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X4),sK7(X0,X2,X3))
    | ~ event(X0,sK12(X0,X4))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X5)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X5) ) ).

cnf(u428,axiom,
    ( ~ past(X0,sK9(X0,X2,X3))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ sP1(X0,X2,X3)
    | ~ patient(X0,sK9(X0,X2,X3),sK7(X0,X4,X5))
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ patient(X0,sK12(X0,X1),sK11(X0,X6))
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X4,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X6) ) ).

cnf(u604,negated_conjecture,
    ( ~ agent(X0,sK12(X0,X1),sK10(X0,sK14(X0,sK11(X0,X1))))
    | ~ event(X0,sK12(X0,X1))
    | ~ event(X0,sK13(X0,sK14(X0,sK11(X0,X1))))
    | ~ actual_world(X0)
    | ~ sP0(X0,sK14(X0,sK11(X0,X1)))
    | ~ sP0(X0,X1) ) ).

cnf(u472,axiom,
    ( ~ patient(X0,sK9(X0,X2,X3),sK7(X0,X4,X5))
    | ~ event(X0,sK9(X0,X2,X3))
    | ~ agent(X0,sK9(X0,X2,X3),sK3(X0))
    | ~ sP1(X0,X2,X3)
    | ~ agent(X0,sK12(X0,X1),sK7(X0,X4,X5))
    | ~ event(X0,sK12(X0,X1))
    | ~ sP1(X0,X4,X5)
    | ~ actual_world(X0)
    | ~ sP0(X0,X1) ) ).

cnf(u467,axiom,
    ( ~ actual_world(X0)
    | ~ sP0(X0,sK3(X0)) ) ).

cnf(u626,negated_conjecture,
    ( ~ nonreflexive(X0,sK9(X0,X3,X4))
    | ~ event(X0,sK9(X0,X3,X4))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X3,X4),sK10(X0,X5))
    | ~ past(X0,sK8(X0,X1,X2))
    | ~ patient(X0,sK8(X0,X1,X2),sK11(X0,X6))
    | ~ agent(X0,sK8(X0,X1,X2),sK10(X0,X5))
    | ~ event(X0,sK8(X0,X1,X2))
    | ~ agent(X0,sK9(X0,X3,X4),sK14(X0,sK11(X0,X6)))
    | ~ past(X0,sK9(X0,X3,X4))
    | ~ sP1(X0,X3,X4)
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X5)
    | ~ sP0(X0,X6) ) ).

cnf(u590,negated_conjecture,
    ( ~ nonreflexive(X0,sK8(X0,X5,X6))
    | ~ nonreflexive(X0,sK9(X0,X1,X2))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X3))
    | ~ past(X0,sK8(X0,X5,X6))
    | ~ patient(X0,sK8(X0,X5,X6),sK11(X0,X4))
    | ~ agent(X0,sK8(X0,X5,X6),sK10(X0,X3))
    | ~ event(X0,sK8(X0,X5,X6))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X4)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP1(X0,X5,X6)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u611,negated_conjecture,
    ( ~ nonreflexive(X0,sK12(X0,X3))
    | ~ event(X0,sK9(X0,X1,X2))
    | ~ actual_world(X0)
    | ~ patient(X0,sK9(X0,X1,X2),sK10(X0,X4))
    | ~ past(X0,sK12(X0,X3))
    | ~ patient(X0,sK12(X0,X3),sK11(X0,X5))
    | ~ agent(X0,sK12(X0,X3),sK10(X0,X4))
    | ~ event(X0,sK12(X0,X3))
    | ~ agent(X0,sK9(X0,X1,X2),sK14(X0,sK11(X0,X5)))
    | ~ past(X0,sK9(X0,X1,X2))
    | ~ sP1(X0,X1,X2)
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X4)
    | ~ sP0(X0,X5) ) ).

cnf(u46,axiom,
    ( agent(X0,sK13(X0,X1),X1)
    | ~ sP0(X0,X1) ) ).

cnf(u662,negated_conjecture,
    ( ~ patient(X0,sK8(X0,X2,X3),sK11(X0,X4))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK8(X0,X2,X3),sK10(X0,X1))
    | ~ event(X0,sK8(X0,X2,X3))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X4)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X4) ) ).

cnf(u150,axiom,
    ( ~ nonreflexive(X0,sK12(X0,X2))
    | ~ patient(X0,sK13(X0,X1),sK10(X0,X3))
    | ~ agent(X0,sK13(X0,X1),sK3(X0))
    | ~ event(X0,sK13(X0,X1))
    | ~ actual_world(X0)
    | ~ past(X0,sK13(X0,X1))
    | ~ past(X0,sK12(X0,X2))
    | ~ patient(X0,sK12(X0,X2),sK11(X0,X4))
    | ~ agent(X0,sK12(X0,X2),sK10(X0,X3))
    | ~ event(X0,sK12(X0,X2))
    | ~ sP0(X0,X3)
    | ~ sP0(X0,X2)
    | ~ sP0(X0,X1)
    | ~ sP0(X0,X4) ) ).

cnf(u696,negated_conjecture,
    ( ~ patient(X0,sK13(X0,X1),sK7(X0,X2,X3))
    | ~ patient(X0,sK8(X0,X4,X5),sK11(X0,X6))
    | ~ event(X0,sK13(X0,X1))
    | ~ agent(X0,sK8(X0,X4,X5),sK7(X0,X2,X3))
    | ~ event(X0,sK8(X0,X4,X5))
    | ~ agent(X0,sK13(X0,X1),sK14(X0,sK11(X0,X6)))
    | ~ actual_world(X0)
    | ~ sP0(X0,X1)
    | ~ sP1(X0,X4,X5)
    | ~ sP1(X0,X2,X3)
    | ~ sP0(X0,X6) ) ).

cnf(u300,axiom,
    ( ~ nonreflexive(sK5,sK13(sK5,X1))
    | ~ sP0(sK5,X0)
    | ~ sP1(sK5,X2,X3)
    | ~ event(sK5,sK12(sK5,X0))
    | ~ agent(sK5,sK12(sK5,X0),sK7(sK5,X2,X3))
    | ~ sP0(sK5,X1)
    | ~ patient(sK5,sK12(sK5,X0),sK6)
    | ~ past(sK5,sK12(sK5,X0))
    | ~ event(sK5,sK13(sK5,X1))
    | ~ agent(sK5,sK13(sK5,X1),sK3(sK5))
    | ~ patient(sK5,sK13(sK5,X1),sK7(sK5,X2,X3))
    | ~ past(sK5,sK13(sK5,X1)) ) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP096+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37  % Computer : n003.cluster.edu
% 0.10/0.37  % Model    : x86_64 x86_64
% 0.10/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37  % Memory   : 8046.5625MB
% 0.10/0.37  % OS       : Linux 6.8.0-71-generic
% 0.10/0.37  % CPULimit : 300
% 0.10/0.37  % WCLimit  : 300
% 0.10/0.37  % DateTime : Sun Sep 27 18:05:11 UTC 2026
% 0.10/0.38  % CPUTime  : 
% 0.10/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.41  Running first-order theorem proving
% 0.10/0.41  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.23/1.32  % (829025)Detected formulas, will run a generic FOF schedule.
% 3.23/1.32  % (829034)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3446188723:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.23/1.32  % (829034)Refutation not found, incomplete strategy
% 3.23/1.32  % (829034)------------------------------
% 3.23/1.32  % (829034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.32  % (829034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.32  % (829034)CaDiCaL version: 2.1.3
% 3.23/1.32  % (829034)Termination reason: Refutation not found, incomplete strategy
% 3.23/1.32  % (829034)Time elapsed: 0.003 s
% 3.23/1.32  % (829034)Peak memory usage: 88 MB
% 3.23/1.32  % (829034)Instructions burned: 7 (million)
% 3.23/1.32  % (829030)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2459833734:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.23/1.32  % (829036)dis-21_1_sil=8000:lcm=predicate:random_seed=1782957355:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.23/1.32  % (829033)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1096521436:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.23/1.32  % (829031)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2716940245:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.23/1.32  % (829032)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=320255968:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.23/1.32  % (829033)Refutation not found, incomplete strategy
% 3.23/1.32  % (829033)------------------------------
% 3.23/1.32  % (829033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.32  % (829033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.32  % (829033)CaDiCaL version: 2.1.3
% 3.23/1.32  % (829033)Termination reason: Refutation not found, incomplete strategy
% 3.23/1.32  % (829033)Time elapsed: 0.004 s
% 3.23/1.32  % (829033)Peak memory usage: 88 MB
% 3.23/1.32  % (829033)Instructions burned: 5 (million)
% 3.23/1.32  % (829035)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3842321229:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.23/1.32  % (829036)First to succeed.
% 3.23/1.32  % (829036)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-829025"
% 3.23/1.32  % (829035)Instruction limit reached! 
% 3.23/1.32  % (829035)------------------------------
% 3.23/1.32  % (829035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.32  % (829035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.32  % (829035)CaDiCaL version: 2.1.3
% 3.23/1.32  % (829035)Termination reason: Instruction limit
% 3.23/1.32  % (829035)Termination phase: Saturation
% 3.23/1.32  % (829035)Time elapsed: 0.062 s
% 3.23/1.32  % (829035)Peak memory usage: 89 MB
% 3.23/1.32  % (829035)Instructions burned: 142 (million)
% 3.23/1.32  % (829034)------------------------------
% 3.23/1.32  % (829034)------------------------------
% 3.23/1.32  % (829044)lrs+10_1_sil=8000:sp=occurrence:random_seed=2909314342:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 3.23/1.32  % (829044)Also succeeded, but the first one will report.
% 3.23/1.32  % (829045)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1183510326:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.23/1.32  % (829033)------------------------------
% 3.23/1.32  % (829033)------------------------------
% 3.23/1.32  % (829045)Refutation not found, incomplete strategy
% 3.23/1.32  % (829045)------------------------------
% 3.23/1.32  % (829045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.23/1.32  % (829045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/1.32  % (829045)CaDiCaL version: 2.1.3
% 3.23/1.32  % (829045)Termination reason: Refutation not found, incomplete strategy
% 3.23/1.32  % (829045)Time elapsed: 0.003 s
% 3.23/1.32  % (829045)Peak memory usage: 88 MB
% 3.23/1.32  % (829045)Instructions burned: 8 (million)
% 3.23/1.32  % SZS status CounterSatisfiable for theBenchmark
% 3.23/1.32  % SZS output start Saturation.
% See solution above
% 3.95/1.51  % SZS output start Definitions and Model Updates.
% 3.95/1.51  % SZS output end Definitions and Model Updates.
% 3.95/1.51  % (829036)------------------------------
% 3.95/1.51  % (829036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.95/1.51  % (829036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.95/1.51  % (829036)CaDiCaL version: 2.1.3
% 3.95/1.51  % (829036)Termination reason: Satisfiable
% 3.95/1.51  % (829036)Time elapsed: 0.040 s
% 3.95/1.51  % (829036)Peak memory usage: 89 MB
% 3.95/1.51  % (829036)Instructions burned: 74 (million)
% 3.95/1.51  % (829036)------------------------------
% 3.95/1.51  % (829036)------------------------------
% 3.95/1.51  % (829025)Success in time 0.469 s
% 3.95/1.51  % Vampire exiting
%------------------------------------------------------------------------------