%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP092-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:08:49 PM UTC 2026
% Result : Satisfiable 6.68s 1.54s
% Output : Saturation 6.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u231,negated_conjecture,
event(X0,skf11(X0,X5,X6,X7)) ).
cnf(u535,negated_conjecture,
present(X0,skf11(X0,X5,X6,X7)) ).
cnf(u576,negated_conjecture,
shot(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u581,negated_conjecture,
event(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u600,negated_conjecture,
fire(X0,skf11(X0,X5,X6,X7)) ).
cnf(u661,negated_conjecture,
nonreflexive(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u674,negated_conjecture,
~ patient(skc4,skf11(skc4,X0,skc6,skc7),skc7) ).
cnf(u726,negated_conjecture,
~ patient(skc4,skf11(skc4,X0,X1,skc7),skc7) ).
cnf(u735,negated_conjecture,
from_loc(X0,skf11(X0,X1,X3,X5),X3) ).
cnf(u742,negated_conjecture,
~ agent(skc4,skf11(skc4,skf13(X0,X1,X2,skc4),X0,X3),X1) ).
cnf(u793,axiom,
member(X0,skf23(X1,X0),X1) ).
cnf(u807,axiom,
member(X0,skf21(X1,X0),X1) ).
cnf(u821,axiom,
member(X0,skf19(X1,X0),X1) ).
cnf(u835,axiom,
member(X0,skf17(X1,X0),X1) ).
cnf(u849,axiom,
member(X0,skf15(X1,X0),X1) ).
cnf(u1702,negated_conjecture,
present(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u1735,negated_conjecture,
fire(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u1756,negated_conjecture,
~ agent(skc4,skf11(skc4,skf13(skc6,X0,X1,skc4),skc6,X2),X0) ).
cnf(u2380,negated_conjecture,
from_loc(X1,skf11(X1,skf25(X0,X1),X2,X4),X2) ).
cnf(u2699,negated_conjecture,
patient(X1,skf11(X1,skf25(X0,X1),X4,X5),skf25(X0,X1)) ).
cnf(u2711,negated_conjecture,
patient(X1,skf11(X1,skf21(X0,X1),X4,X5),skf21(X0,X1)) ).
cnf(u2717,negated_conjecture,
patient(X1,skf11(X1,skf19(X0,X1),X4,X5),skf19(X0,X1)) ).
cnf(u2723,negated_conjecture,
patient(X1,skf11(X1,skf17(X0,X1),X4,X5),skf17(X0,X1)) ).
cnf(u2729,negated_conjecture,
patient(X1,skf11(X1,skf15(X0,X1),X4,X5),skf15(X0,X1)) ).
cnf(u2777,negated_conjecture,
~ agent(X1,X2,skf25(X0,X1)) ).
cnf(u3070,negated_conjecture,
~ agent(X1,X2,skf23(X0,X1)) ).
cnf(u3189,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X1 ).
cnf(u5395,negated_conjecture,
skf21(X0,X1) = skf13(X2,skf19(X0,X1),X0,X1) ).
cnf(u5434,negated_conjecture,
~ agent(X1,X2,skf19(X0,X1)) ).
cnf(u5721,negated_conjecture,
~ agent(X1,X2,skf17(X0,X1)) ).
cnf(u6011,negated_conjecture,
~ agent(X1,X2,skf15(X0,X1)) ).
cnf(u7940,negated_conjecture,
~ agent(skc4,X1,skf21(X0,skc4)) ).
cnf(u8173,negated_conjecture,
from_loc(X1,skf11(X1,skf23(X0,X1),X2,X4),X2) ).
cnf(u8176,negated_conjecture,
from_loc(X1,skf11(X1,skf21(X0,X1),X2,X4),X2) ).
cnf(u8179,negated_conjecture,
from_loc(X1,skf11(X1,skf19(X0,X1),X2,X4),X2) ).
cnf(u8182,negated_conjecture,
from_loc(X1,skf11(X1,skf17(X0,X1),X2,X4),X2) ).
cnf(u8185,negated_conjecture,
from_loc(X1,skf11(X1,skf15(X0,X1),X2,X4),X2) ).
cnf(u8483,negated_conjecture,
from_loc(X1,skf11(X1,skf13(X4,X5,X0,X1),X2,X6),X2) ).
cnf(u8526,negated_conjecture,
patient(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X7),skf13(X4,X5,X0,X1)) ).
cnf(u8554,negated_conjecture,
~ agent(X0,skf11(X0,skf13(X1,X2,X3,X0),X4,X5),X2) ).
cnf(u8599,negated_conjecture,
from_loc(skc4,skf11(skc4,X0,X1,X2),X1) ).
cnf(u8763,negated_conjecture,
skf21(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0) ).
cnf(u8902,negated_conjecture,
~ agent(X1,X2,skf13(X4,X5,X0,X1)) ).
cnf(u10045,negated_conjecture,
( skf23(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4) ) ).
cnf(u10049,negated_conjecture,
skf23(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u10572,negated_conjecture,
member(skc4,skf25(skc5,skc4),skc5) ).
cnf(u10602,negated_conjecture,
skf21(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4) ).
cnf(u11063,negated_conjecture,
skf21(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4) ).
cnf(u11872,negated_conjecture,
( skf17(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4) ) ).
cnf(u11876,negated_conjecture,
skf25(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u12771,negated_conjecture,
( skf19(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4) ) ).
cnf(u12836,negated_conjecture,
( skf17(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4) ) ).
cnf(u13079,negated_conjecture,
skf21(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u13112,negated_conjecture,
( skf17(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4) ) ).
cnf(u13296,negated_conjecture,
skf25(skc5,skc4) != skf21(skc5,skc4) ).
cnf(u13468,negated_conjecture,
skf23(skc5,skc4) != skf21(skc5,skc4) ).
cnf(u13502,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X0 ).
cnf(u13602,negated_conjecture,
skf23(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u13753,negated_conjecture,
skf25(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u13830,negated_conjecture,
skf21(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4) ).
cnf(u14273,negated_conjecture,
skf23(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4) ).
cnf(u14707,negated_conjecture,
( skf23(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4) ) ).
cnf(u14837,negated_conjecture,
( skf19(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4) ) ).
cnf(u14940,negated_conjecture,
skf21(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4) ).
cnf(u15349,negated_conjecture,
skf21(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1) ).
cnf(u15745,negated_conjecture,
skf21(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1) ).
cnf(u16325,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf19(skc5,skc4),X0,skc4) ).
cnf(u16387,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X5 ).
cnf(u16390,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X4 ).
cnf(u16393,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X3 ).
cnf(u16396,axiom,
skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X2 ).
cnf(u16460,negated_conjecture,
~ patient(X1,skf11(X1,skf26(X4,X5,X6,X7,X8,X9,X0,X1),X2,X3),X3) ).
cnf(u778,negated_conjecture,
nonexistent(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u13827,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4) ) ).
cnf(clause21,axiom,
( ~ weapon(X0,X1)
| weaponry(X0,X1) ) ).
cnf(u8502,negated_conjecture,
( ~ patient(X1,skf11(X1,skf21(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause32,axiom,
( ~ man(X0,X1)
| human_person(X0,X1) ) ).
cnf(u803,negated_conjecture,
singleton(skc4,skf23(skc5,skc4)) ).
cnf(u1422,negated_conjecture,
( ~ member(X1,X4,X0)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| agent(X1,skf11(X1,X4,X2,X3),X3) ) ).
cnf(u3096,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf23(X3,X1),X0,X1) ) ).
cnf(u8583,negated_conjecture,
ssSkP0(X0,skc7,skc5,skc4) ).
cnf(clause38,axiom,
( ~ human_person(X0,X1)
| animate(X0,X1) ) ).
cnf(u12072,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4) ) ).
cnf(u61,axiom,
( skf19(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u824,negated_conjecture,
action(skc4,skf19(skc5,skc4)) ).
cnf(u8513,negated_conjecture,
( ~ six(X1,X0)
| skf23(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1) ) ).
cnf(u2472,negated_conjecture,
( patient(X1,skf11(X1,skf19(X0,X1),X4,X5),skf19(X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u1424,negated_conjecture,
( ~ member(X1,X4,X0)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| nonreflexive(X1,skf11(X1,X5,X6,X7)) ) ).
cnf(clause51,axiom,
( skf25(X0,X1) != skf15(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2361,negated_conjecture,
( from_loc(X1,skf11(X1,skf23(X0,X1),X2,X4),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u444,negated_conjecture,
~ nonexistent(skc4,skc6) ).
cnf(u2478,negated_conjecture,
( patient(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X7),skf13(X4,X5,X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1) ) ).
cnf(u828,negated_conjecture,
unisex(skc4,skf19(skc5,skc4)) ).
cnf(u8621,negated_conjecture,
( agent(X1,skf11(X1,skf15(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8506,negated_conjecture,
( ~ patient(X1,skf11(X1,skf19(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u2489,negated_conjecture,
( agent(X1,skf11(X1,skf21(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u78,axiom,
( ~ member(X0,X1,X2)
| ~ six(X0,X2)
| skf15(X2,X0) = X1
| skf17(X2,X0) = X1
| skf19(X2,X0) = X1
| skf21(X2,X0) = X1
| skf23(X2,X0) = X1
| skf25(X2,X0) = X1 ) ).
cnf(u8645,negated_conjecture,
( ~ patient(X1,skf11(X1,skf21(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause66,axiom,
( ~ agent(X0,X1,X2)
| ~ patient(X0,X1,X2)
| ~ nonreflexive(X0,X1) ) ).
cnf(clause80,negated_conjecture,
group(skc4,skc5) ).
cnf(clause78,negated_conjecture,
cannon(skc4,skc6) ).
cnf(clause84,negated_conjecture,
( member(X3,skf13(X0,X1,X2,X3),X2)
| ssSkP0(X0,X1,X2,X3) ) ).
cnf(u217,negated_conjecture,
( shot(skc4,skf13(X0,X1,skc5,skc4))
| ssSkP0(X0,X1,skc5,skc4) ) ).
cnf(u8521,negated_conjecture,
( ~ patient(X1,skf11(X1,skf25(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u489,negated_conjecture,
thing(skc4,skc7) ).
cnf(clause5,axiom,
( ~ eventuality(X0,X1)
| thing(X0,X1) ) ).
cnf(u768,negated_conjecture,
event(skc4,skf25(skc5,skc4)) ).
cnf(u789,negated_conjecture,
singleton(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause16,axiom,
( ~ group(X0,X1)
| set(X0,X1) ) ).
cnf(u14904,negated_conjecture,
( skf19(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4) ) ).
cnf(u303,negated_conjecture,
set(skc4,skc5) ).
cnf(clause22,axiom,
( ~ weaponry(X0,X1)
| instrumentality(X0,X1) ) ).
cnf(u8743,negated_conjecture,
( ssSkP0(X3,X4,X1,X0)
| skf15(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0)
| skf17(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0)
| skf19(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0)
| skf21(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0)
| skf23(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0)
| ~ six(X0,X1)
| skf25(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0) ) ).
cnf(u802,negated_conjecture,
thing(skc4,skf23(skc5,skc4)) ).
cnf(clause45,axiom,
( member(X0,skf25(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u1699,negated_conjecture,
( ~ member(X0,X1,X2)
| present(X0,skf11(X0,X3,X4,X5))
| skf15(X2,X0) = skf13(X6,X7,X2,X0)
| skf17(X2,X0) = skf13(X6,X7,X2,X0)
| skf19(X2,X0) = skf13(X6,X7,X2,X0)
| skf21(X2,X0) = skf13(X6,X7,X2,X0)
| skf23(X2,X0) = skf13(X6,X7,X2,X0)
| skf25(X2,X0) = skf13(X6,X7,X2,X0)
| ~ six(X0,X2) ) ).
cnf(u8588,negated_conjecture,
( agent(skc4,skf11(skc4,X0,X1,skc7),skc7)
| ~ member(skc4,X0,skc5) ) ).
cnf(u73,axiom,
( skf17(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u812,negated_conjecture,
event(skc4,skf21(skc5,skc4)) ).
cnf(u8629,negated_conjecture,
( agent(X1,skf11(X1,skf25(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u817,negated_conjecture,
singleton(skc4,skf21(skc5,skc4)) ).
cnf(u557,negated_conjecture,
shot(skc4,skf25(skc5,skc4)) ).
cnf(u14737,negated_conjecture,
skf21(skc5,skc4) = skf13(X0,skf23(skc5,skc4),skc5,skc4) ).
cnf(u831,negated_conjecture,
singleton(skc4,skf19(skc5,skc4)) ).
cnf(clause50,axiom,
( member(X0,skf15(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u2369,negated_conjecture,
( from_loc(X1,skf11(X1,skf15(X0,X1),X2,X4),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u75,axiom,
( skf15(X0,X1) != skf17(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2497,negated_conjecture,
( agent(X1,skf11(X1,skf13(X4,X5,X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1) ) ).
cnf(u852,negated_conjecture,
action(skc4,skf15(skc5,skc4)) ).
cnf(u8669,negated_conjecture,
( ~ patient(X1,skf11(X1,skf15(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u458,negated_conjecture,
unisex(skc4,skc6) ).
cnf(u857,negated_conjecture,
nonexistent(skc4,skf15(skc5,skc4)) ).
cnf(clause89,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| agent(X0,skf11(X0,X1,X3,X4),X4) ) ).
cnf(u587,negated_conjecture,
nonexistent(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(clause68,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X1
| ~ member(X8,X0,X9)
| ~ member(X8,X1,X9)
| ~ member(X8,X10,X9)
| ~ member(X8,X11,X9)
| ~ member(X8,X12,X9)
| ~ member(X8,X13,X9)
| six(X8,X9)
| X0 = X13
| X0 = X12
| X0 = X11
| X0 = X10
| X0 = X1
| X1 = X13
| X1 = X12
| X1 = X11
| X1 = X10
| X10 = X13
| X10 = X12
| X10 = X11
| X11 = X13
| X11 = X12
| X12 = X13 ) ).
cnf(clause79,negated_conjecture,
six(skc4,skc5) ).
cnf(u606,negated_conjecture,
( agent(skc4,skf11(skc4,X0,skc6,skc7),skc7)
| ~ member(skc4,X0,skc5) ) ).
cnf(u345,negated_conjecture,
multiple(skc4,skc5) ).
cnf(clause77,negated_conjecture,
man(skc4,skc7) ).
cnf(u859,negated_conjecture,
singleton(skc4,skf15(skc5,skc4)) ).
cnf(u757,negated_conjecture,
action(skc4,skf25(skc5,skc4)) ).
cnf(u8575,negated_conjecture,
~ member(skc4,skf13(X0,skc7,X1,skc4),skc5) ).
cnf(u617,negated_conjecture,
( patient(skc4,skf11(skc4,X0,X1,X2),X0)
| ~ member(skc4,X0,skc5) ) ).
cnf(u773,negated_conjecture,
singleton(skc4,skf25(skc5,skc4)) ).
cnf(u771,negated_conjecture,
nonexistent(skc4,skf25(skc5,skc4)) ).
cnf(u385,negated_conjecture,
instrumentality(skc4,skc6) ).
cnf(clause6,axiom,
( ~ thing(X0,X1)
| singleton(X0,X1) ) ).
cnf(clause46,axiom,
( member(X0,skf23(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u1423,negated_conjecture,
( ~ member(X1,X4,X0)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| fire(X1,skf11(X1,X5,X6,X7)) ) ).
cnf(u786,negated_conjecture,
unisex(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause29,axiom,
( ~ object(X0,X1)
| nonliving(X0,X1) ) ).
cnf(clause19,axiom,
( ~ fire(X0,X1)
| event(X0,X1) ) ).
cnf(u8615,negated_conjecture,
( agent(X1,skf11(X1,skf21(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8204,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4) ) ).
cnf(u6037,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf15(X3,X1),X0,X1) ) ).
cnf(u671,negated_conjecture,
( ~ patient(skc4,skf11(skc4,X0,skc6,skc7),skc7)
| ~ member(skc4,X0,skc5) ) ).
cnf(clause17,axiom,
( ~ set(X0,X1)
| multiple(X0,X1) ) ).
cnf(u796,negated_conjecture,
action(skc4,skf23(skc5,skc4)) ).
cnf(u8498,negated_conjecture,
( ~ patient(X1,skf11(X1,skf23(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u801,negated_conjecture,
nonexistent(skc4,skf23(skc5,skc4)) ).
cnf(clause44,axiom,
( ~ animate(X0,X1)
| ~ nonliving(X0,X1) ) ).
cnf(u815,negated_conjecture,
nonexistent(skc4,skf21(skc5,skc4)) ).
cnf(u9224,negated_conjecture,
skf21(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1) ).
cnf(u59,axiom,
( skf17(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2470,negated_conjecture,
( patient(X1,skf11(X1,skf21(X0,X1),X4,X5),skf21(X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u788,negated_conjecture,
thing(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause34,axiom,
( ~ organism(X0,X1)
| entity(X0,X1) ) ).
cnf(u830,negated_conjecture,
thing(skc4,skf19(skc5,skc4)) ).
cnf(u57,axiom,
( skf15(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u63,axiom,
( skf21(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u8653,negated_conjecture,
( ~ patient(X1,skf11(X1,skf19(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8619,negated_conjecture,
( agent(X1,skf11(X1,skf17(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u841,negated_conjecture,
eventuality(skc4,skf17(skc5,skc4)) ).
cnf(clause73,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X3
| ~ member(X8,X0,X9)
| ~ member(X8,X1,X9)
| ~ member(X8,X2,X9)
| ~ member(X8,X3,X9)
| ~ member(X8,X10,X9)
| ~ member(X8,X11,X9)
| six(X8,X9)
| X0 = X11
| X0 = X10
| X0 = X3
| X0 = X2
| X0 = X1
| X1 = X11
| X1 = X10
| X1 = X3
| X1 = X2
| X2 = X11
| X2 = X10
| X2 = X3
| X3 = X11
| X3 = X10
| X10 = X11 ) ).
cnf(u855,negated_conjecture,
eventuality(skc4,skf15(skc5,skc4)) ).
cnf(u2503,negated_conjecture,
( agent(X1,skf11(X1,skf25(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8518,negated_conjecture,
( ~ six(X1,X0)
| skf23(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf15(X0,X1),X0,X1) ) ).
cnf(u845,negated_conjecture,
singleton(skc4,skf17(skc5,skc4)) ).
cnf(u787,negated_conjecture,
nonexistent(X0,skf11(X0,X1,X2,X3)) ).
cnf(u843,negated_conjecture,
nonexistent(skc4,skf17(skc5,skc4)) ).
cnf(clause92,negated_conjecture,
( ~ patient(X0,X1,skf13(X2,X3,X4,X0))
| ~ fire(X0,X1)
| ~ nonreflexive(X0,X1)
| ~ present(X0,X1)
| ~ from_loc(X0,X1,X2)
| ~ agent(X0,X1,X3)
| ~ event(X0,X1) ) ).
cnf(u457,negated_conjecture,
nonliving(skc4,skc6) ).
cnf(u8709,negated_conjecture,
( from_loc(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X7),X6)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1) ) ).
cnf(u858,negated_conjecture,
thing(skc4,skf15(skc5,skc4)) ).
cnf(clause90,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| patient(X0,skf11(X0,X1,X5,X6),X1) ) ).
cnf(u758,negated_conjecture,
action(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u497,negated_conjecture,
~ nonliving(skc4,skc7) ).
cnf(clause43,axiom,
( ~ existent(X0,X1)
| ~ nonexistent(X0,X1) ) ).
cnf(u770,negated_conjecture,
unisex(skc4,skf25(skc5,skc4)) ).
cnf(clause13,axiom,
( ~ action(X0,X1)
| act(X0,X1) ) ).
cnf(u776,negated_conjecture,
eventuality(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u8661,negated_conjecture,
( ~ patient(X1,skf11(X1,skf17(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u774,negated_conjecture,
act(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause1,axiom,
~ member(X0,X1,X1) ).
cnf(u780,negated_conjecture,
singleton(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u8511,negated_conjecture,
( ~ patient(X1,skf11(X1,skf17(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8623,negated_conjecture,
( agent(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1) ) ).
cnf(u785,negated_conjecture,
eventuality(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause28,axiom,
( ~ entity(X0,X1)
| existent(X0,X1) ) ).
cnf(u799,negated_conjecture,
eventuality(skc4,skf23(skc5,skc4)) ).
cnf(clause18,axiom,
( ~ six(X0,X1)
| group(X0,X1) ) ).
cnf(u814,negated_conjecture,
unisex(skc4,skf21(skc5,skc4)) ).
cnf(clause41,axiom,
( ~ multiple(X0,X1)
| ~ singleton(X0,X1) ) ).
cnf(u8613,negated_conjecture,
( agent(X1,skf11(X1,skf23(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u426,negated_conjecture,
entity(skc4,skc6) ).
cnf(u825,negated_conjecture,
act(skc4,skf19(skc5,skc4)) ).
cnf(u16159,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4) ).
cnf(u2468,negated_conjecture,
( patient(X1,skf11(X1,skf23(X0,X1),X4,X5),skf23(X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause47,axiom,
( member(X0,skf21(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u2487,negated_conjecture,
( agent(X1,skf11(X1,skf23(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u839,negated_conjecture,
act(skc4,skf17(skc5,skc4)) ).
cnf(clause91,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| from_loc(X0,skf11(X0,X1,X3,X5),X3) ) ).
cnf(u443,negated_conjecture,
existent(skc4,skc6) ).
cnf(u827,negated_conjecture,
eventuality(skc4,skf19(skc5,skc4)) ).
cnf(clause76,negated_conjecture,
male(skc4,skc7) ).
cnf(u842,negated_conjecture,
unisex(skc4,skf17(skc5,skc4)) ).
cnf(clause74,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X2
| ~ member(X8,X0,X9)
| ~ member(X8,X1,X9)
| ~ member(X8,X2,X9)
| ~ member(X8,X10,X9)
| ~ member(X8,X11,X9)
| ~ member(X8,X12,X9)
| six(X8,X9)
| X0 = X12
| X0 = X11
| X0 = X10
| X0 = X2
| X0 = X1
| X1 = X12
| X1 = X11
| X1 = X10
| X1 = X2
| X2 = X12
| X2 = X11
| X2 = X10
| X10 = X12
| X10 = X11
| X11 = X12 ) ).
cnf(clause85,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| event(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u1758,negated_conjecture,
~ member(skc4,skf13(skc6,skc7,X0,skc4),skc5) ).
cnf(u16462,negated_conjecture,
~ member(skc4,skf26(X0,X1,X2,X3,X4,X5,X6,skc4),skc5) ).
cnf(u485,negated_conjecture,
entity(skc4,skc7) ).
cnf(u736,negated_conjecture,
( from_loc(skc4,skf11(skc4,X0,skc6,X1),skc6)
| ~ member(skc4,X0,skc5) ) ).
cnf(clause14,axiom,
( ~ act(X0,X1)
| event(X0,X1) ) ).
cnf(u9241,negated_conjecture,
~ agent(X1,X2,skf21(X0,X1)) ).
cnf(u769,negated_conjecture,
eventuality(skc4,skf25(skc5,skc4)) ).
cnf(u2321,negated_conjecture,
( ~ six(X1,X0)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| nonreflexive(X1,skf11(X1,X4,X5,X6)) ) ).
cnf(u496,negated_conjecture,
living(skc4,skc7) ).
cnf(u798,negated_conjecture,
event(skc4,skf23(skc5,skc4)) ).
cnf(clause25,axiom,
( ~ object(X0,X1)
| entity(X0,X1) ) ).
cnf(u809,negated_conjecture,
shot(skc4,skf21(skc5,skc4)) ).
cnf(clause52,axiom,
( skf25(X0,X1) != skf17(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u823,negated_conjecture,
shot(skc4,skf19(skc5,skc4)) ).
cnf(clause31,axiom,
( ~ object(X0,X1)
| unisex(X0,X1) ) ).
cnf(u8611,negated_conjecture,
( ~ member(X1,X4,X0)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| from_loc(X1,skf11(X1,X4,X5,X6),X5) ) ).
cnf(clause42,axiom,
( ~ living(X0,X1)
| ~ nonliving(X0,X1) ) ).
cnf(u2367,negated_conjecture,
( from_loc(X1,skf11(X1,skf17(X0,X1),X2,X4),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u159,negated_conjecture,
~ unisex(skc4,skc7) ).
cnf(u2476,negated_conjecture,
( patient(X1,skf11(X1,skf15(X0,X1),X4,X5),skf15(X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u414,negated_conjecture,
object(skc4,skc6) ).
cnf(u813,negated_conjecture,
eventuality(skc4,skf21(skc5,skc4)) ).
cnf(clause40,axiom,
( ~ male(X0,X1)
| ~ unisex(X0,X1) ) ).
cnf(u811,negated_conjecture,
act(skc4,skf21(skc5,skc4)) ).
cnf(u2365,negated_conjecture,
( from_loc(X1,skf11(X1,skf19(X0,X1),X2,X4),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u2495,negated_conjecture,
( agent(X1,skf11(X1,skf15(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8523,negated_conjecture,
( ~ six(X1,X0)
| skf23(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf25(X0,X1),X0,X1) ) ).
cnf(u826,negated_conjecture,
event(skc4,skf19(skc5,skc4)) ).
cnf(u2493,negated_conjecture,
( agent(X1,skf11(X1,skf17(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u71,axiom,
( skf15(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u10078,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4) ) ).
cnf(clause86,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| present(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u69,axiom,
( skf19(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2371,negated_conjecture,
( from_loc(X1,skf11(X1,skf13(X4,X5,X0,X1),X2,X6),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1) ) ).
cnf(u853,negated_conjecture,
act(skc4,skf15(skc5,skc4)) ).
cnf(clause69,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X0
| ~ member(X8,X0,X9)
| ~ member(X8,X10,X9)
| ~ member(X8,X11,X9)
| ~ member(X8,X12,X9)
| ~ member(X8,X13,X9)
| ~ member(X8,X14,X9)
| six(X8,X9)
| X0 = X14
| X0 = X13
| X0 = X12
| X0 = X11
| X0 = X10
| X10 = X14
| X10 = X13
| X10 = X12
| X10 = X11
| X11 = X14
| X11 = X13
| X11 = X12
| X12 = X14
| X12 = X13
| X13 = X14 ) ).
cnf(u583,negated_conjecture,
eventuality(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u851,negated_conjecture,
shot(skc4,skf15(skc5,skc4)) ).
cnf(u465,negated_conjecture,
human_person(skc4,skc7) ).
cnf(u586,negated_conjecture,
unisex(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u1748,negated_conjecture,
( ~ from_loc(skc4,skf11(skc4,skf13(X0,X1,X2,skc4),X3,X4),X0)
| ~ member(skc4,skf13(X0,X1,X2,skc4),skc5)
| ~ agent(skc4,skf11(skc4,skf13(X0,X1,X2,skc4),X3,X4),X1) ) ).
cnf(u592,negated_conjecture,
singleton(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(clause88,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| fire(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u10593,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf15(skc5,skc4),skc5,skc4) ) ).
cnf(clause9,axiom,
( ~ eventuality(X0,X1)
| unisex(X0,X1) ) ).
cnf(u1420,negated_conjecture,
( ~ member(X1,X4,X0)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| from_loc(X1,skf11(X1,X4,X2,X5),X2) ) ).
cnf(u8576,negated_conjecture,
( ssSkP0(X4,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause36,axiom,
( ~ organism(X0,X1)
| living(X0,X1) ) ).
cnf(clause15,axiom,
( ~ shot(X0,X1)
| action(X0,X1) ) ).
cnf(clause26,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(u14732,negated_conjecture,
patient(skc4,skf11(skc4,skf23(skc5,skc4),X2,X3),skf23(skc5,skc4)) ).
cnf(clause49,axiom,
( member(X0,skf17(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u797,negated_conjecture,
act(skc4,skf23(skc5,skc4)) ).
cnf(clause24,axiom,
( ~ artifact(X0,X1)
| object(X0,X1) ) ).
cnf(u795,negated_conjecture,
shot(skc4,skf23(skc5,skc4)) ).
cnf(clause55,axiom,
( skf25(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u676,negated_conjecture,
~ member(skc4,skc7,skc5) ).
cnf(u810,negated_conjecture,
action(skc4,skf21(skc5,skc4)) ).
cnf(clause53,axiom,
( skf25(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u816,negated_conjecture,
thing(skc4,skf21(skc5,skc4)) ).
cnf(u829,negated_conjecture,
nonexistent(skc4,skf19(skc5,skc4)) ).
cnf(u8609,negated_conjecture,
( ~ member(X1,X4,X0)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| agent(X1,skf11(X1,X4,X5,X3),X3) ) ).
cnf(u11060,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf25(X1,skc4),skc5,skc4) ) ).
cnf(u14937,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf15(X1,skc4),skc5,skc4) ) ).
cnf(u588,negated_conjecture,
thing(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u837,negated_conjecture,
shot(skc4,skf17(skc5,skc4)) ).
cnf(clause82,negated_conjecture,
ssSkP0(skc6,skc7,skc5,skc4) ).
cnf(u856,negated_conjecture,
unisex(skc4,skf15(skc5,skc4)) ).
cnf(u325,negated_conjecture,
weapon(skc4,skc6) ).
cnf(u348,negated_conjecture,
~ singleton(skc4,skc5) ).
cnf(clause72,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X4
| ~ member(X8,X0,X9)
| ~ member(X8,X1,X9)
| ~ member(X8,X2,X9)
| ~ member(X8,X3,X9)
| ~ member(X8,X4,X9)
| ~ member(X8,X10,X9)
| six(X8,X9)
| X0 = X10
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| X1 = X10
| X1 = X4
| X1 = X3
| X1 = X2
| X2 = X10
| X2 = X4
| X2 = X3
| X3 = X10
| X3 = X4
| X4 = X10 ) ).
cnf(u854,negated_conjecture,
event(skc4,skf15(skc5,skc4)) ).
cnf(clause70,axiom,
( member(X0,skf26(X1,X3,X4,X5,X6,X7,X2,X0),X2)
| ~ member(X0,X3,X2)
| ~ member(X0,X4,X2)
| ~ member(X0,X5,X2)
| ~ member(X0,X6,X2)
| ~ member(X0,X7,X2)
| six(X0,X2)
| ~ member(X0,X1,X2)
| X1 = X7
| X1 = X6
| X1 = X5
| X1 = X4
| X1 = X3
| X3 = X7
| X3 = X6
| X3 = X5
| X3 = X4
| X4 = X7
| X4 = X6
| X4 = X5
| X5 = X7
| X5 = X6
| X6 = X7 ) ).
cnf(clause87,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| nonreflexive(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u772,negated_conjecture,
thing(skc4,skf25(skc5,skc4)) ).
cnf(u777,negated_conjecture,
unisex(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause20,axiom,
( ~ cannon(X0,X1)
| weapon(X0,X1) ) ).
cnf(u5747,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1) ) ).
cnf(u8966,negated_conjecture,
( ~ six(X1,X0)
| skf25(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf13(X3,X4,X5,X1),X0,X1) ) ).
cnf(u434,negated_conjecture,
thing(skc4,skc6) ).
cnf(u2807,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf25(X3,X1),X0,X1) ) ).
cnf(u8733,negated_conjecture,
( ~ patient(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| ssSkP0(X4,X5,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u9255,negated_conjecture,
( ~ six(X1,X0)
| skf25(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1) ) ).
cnf(u765,negated_conjecture,
act(skc4,skf25(skc5,skc4)) ).
cnf(u1421,negated_conjecture,
( ~ member(X1,X4,X0)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| patient(X1,skf11(X1,X4,X5,X6),X4) ) ).
cnf(clause33,axiom,
( ~ human_person(X0,X1)
| organism(X0,X1) ) ).
cnf(clause8,axiom,
( ~ eventuality(X0,X1)
| nonexistent(X0,X1) ) ).
cnf(u779,negated_conjecture,
thing(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause39,axiom,
( ~ man(X0,X1)
| male(X0,X1) ) ).
cnf(u7987,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf21(X2,skc4),X0,skc4) ) ).
cnf(u800,negated_conjecture,
unisex(skc4,skf23(skc5,skc4)) ).
cnf(u8617,negated_conjecture,
( agent(X1,skf11(X1,skf19(X0,X1),X4,X3),X3)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause48,axiom,
( member(X0,skf19(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(clause83,negated_conjecture,
( ~ member(skc4,X0,skc5)
| shot(skc4,X0) ) ).
cnf(u2474,negated_conjecture,
( patient(X1,skf11(X1,skf17(X0,X1),X4,X5),skf17(X0,X1))
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(clause54,axiom,
( skf25(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2363,negated_conjecture,
( from_loc(X1,skf11(X1,skf21(X0,X1),X2,X4),X2)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u8516,negated_conjecture,
( ~ patient(X1,skf11(X1,skf15(X0,X1),X2,X3),X3)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u2491,negated_conjecture,
( agent(X1,skf11(X1,skf19(X0,X1),X2,X3),X3)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u840,negated_conjecture,
event(skc4,skf17(skc5,skc4)) ).
cnf(u437,negated_conjecture,
singleton(skc4,skc6) ).
cnf(u14267,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4) ) ).
cnf(u591,negated_conjecture,
~ nonexistent(skc4,skc7) ).
cnf(u67,axiom,
( skf17(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u8637,negated_conjecture,
( ~ patient(X1,skf11(X1,skf23(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u5460,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1) ) ).
cnf(u1750,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf13(skc6,X0,X1,skc4),skc6,X2),X0)
| ~ member(skc4,skf13(skc6,X0,X1,skc4),skc5) ) ).
cnf(u838,negated_conjecture,
action(skc4,skf17(skc5,skc4)) ).
cnf(u65,axiom,
( skf15(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u844,negated_conjecture,
thing(skc4,skf17(skc5,skc4)) ).
cnf(u401,negated_conjecture,
artifact(skc4,skc6) ).
cnf(u477,negated_conjecture,
organism(skc4,skc7) ).
cnf(clause71,axiom,
( skf26(X0,X1,X2,X3,X4,X5,X6,X7) != X5
| ~ member(X8,X0,X9)
| ~ member(X8,X1,X9)
| ~ member(X8,X2,X9)
| ~ member(X8,X3,X9)
| ~ member(X8,X4,X9)
| ~ member(X8,X5,X9)
| six(X8,X9)
| X0 = X5
| X0 = X4
| X0 = X3
| X0 = X2
| X0 = X1
| X1 = X5
| X1 = X4
| X1 = X3
| X1 = X2
| X2 = X5
| X2 = X4
| X2 = X3
| X3 = X5
| X3 = X4
| X4 = X5 ) ).
cnf(u8677,negated_conjecture,
( ~ patient(X1,skf11(X1,skf25(X0,X1),X4,X3),X3)
| ~ six(X1,X0)
| skf15(X0,X1) = skf13(X2,X3,X0,X1)
| skf17(X0,X1) = skf13(X2,X3,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1)
| skf23(X0,X1) = skf13(X2,X3,X0,X1)
| skf25(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u360,negated_conjecture,
weaponry(skc4,skc6) ).
cnf(u490,negated_conjecture,
singleton(skc4,skc7) ).
cnf(clause4,axiom,
( ~ event(X0,X1)
| eventuality(X0,X1) ) ).
cnf(u775,negated_conjecture,
event(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u488,negated_conjecture,
existent(skc4,skc7) ).
cnf(u507,negated_conjecture,
animate(skc4,skc7) ).
cnf(u891,negated_conjecture,
( ssSkP0(X2,X3,X1,X0)
| skf15(X1,X0) = skf13(X2,X3,X1,X0)
| skf17(X1,X0) = skf13(X2,X3,X1,X0)
| skf19(X1,X0) = skf13(X2,X3,X1,X0)
| skf21(X1,X0) = skf13(X2,X3,X1,X0)
| skf23(X1,X0) = skf13(X2,X3,X1,X0)
| skf25(X1,X0) = skf13(X2,X3,X1,X0)
| ~ six(X0,X1) ) ).
cnf(clause23,axiom,
( ~ instrumentality(X0,X1)
| artifact(X0,X1) ) ).
cnf(u8590,negated_conjecture,
( from_loc(skc4,skf11(skc4,X0,X1,X2),X1)
| ~ member(skc4,X0,skc5) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP092-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n017.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 17:59:05 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.68/1.54 % (2850868)Will run a generic schedule for satisfiability detection.
% 6.68/1.54 % (2850876)dis+10_1_sil=32000:sp=arity:random_seed=1090252726:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.68/1.54 % (2850874)% WARNING: option uhcvi not known.
% 6.68/1.54 % (2850873)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=467935408_2999 on theBenchmark for (2999ds/0Mi)
% 6.68/1.54 % (2850874)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1354933850:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.68/1.54 % (2850875)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=894127711:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.68/1.54 % (2850877)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2957040639:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.68/1.54 % TRYING [1]
% 6.68/1.54 % TRYING [2]
% 6.68/1.54 % (2850878)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3400592716:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.68/1.54 % (2850879)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1922277497:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.68/1.54 % TRYING [3]
% 6.68/1.54 % (2850876)Instruction limit reached!
% 6.68/1.54 % (2850876)------------------------------
% 6.68/1.54 % (2850876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850876)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850876)Termination reason: Instruction limit
% 6.68/1.54 % (2850876)Termination phase: Saturation
% 6.68/1.54 % (2850876)Time elapsed: 0.030 s
% 6.68/1.54 % (2850876)Peak memory usage: 12 MB
% 6.68/1.54 % (2850876)Instructions burned: 104 (million)
% 6.68/1.54 % (2850887)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3336401266:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.68/1.54 % TRYING [1]
% 6.68/1.54 % TRYING [2]
% 6.68/1.54 % TRYING [3]
% 6.68/1.54 % (2850877)Instruction limit reached!
% 6.68/1.54 % (2850877)------------------------------
% 6.68/1.54 % (2850877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850877)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850877)Termination reason: Instruction limit
% 6.68/1.54 % (2850877)Termination phase: Saturation
% 6.68/1.54 % (2850877)Time elapsed: 0.054 s
% 6.68/1.54 % (2850877)Peak memory usage: 12 MB
% 6.68/1.54 % (2850877)Instructions burned: 117 (million)
% 6.68/1.54 % (2850878)Instruction limit reached!
% 6.68/1.54 % (2850878)------------------------------
% 6.68/1.54 % (2850878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850878)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850878)Termination reason: Instruction limit
% 6.68/1.54 % (2850878)Termination phase: Saturation
% 6.68/1.54 % (2850878)Time elapsed: 0.054 s
% 6.68/1.54 % (2850878)Peak memory usage: 12 MB
% 6.68/1.54 % (2850878)Instructions burned: 131 (million)
% 6.68/1.54 % (2850889)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1855506634:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.68/1.54 % TRYING [4]
% 6.68/1.54 % (2850890)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3937452065:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.68/1.54 % (2850879)Instruction limit reached!
% 6.68/1.54 % (2850879)------------------------------
% 6.68/1.54 % (2850879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850879)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850879)Termination reason: Instruction limit
% 6.68/1.54 % (2850879)Termination phase: Saturation
% 6.68/1.54 % (2850879)Time elapsed: 0.094 s
% 6.68/1.54 % (2850879)Peak memory usage: 13 MB
% 6.68/1.54 % (2850879)Instructions burned: 160 (million)
% 6.68/1.54 % TRYING [4]
% 6.68/1.54 % (2850894)ott-21_1_sil=16000:fs=off:random_seed=369828193:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.68/1.54 % (2850889)Instruction limit reached!
% 6.68/1.54 % (2850889)------------------------------
% 6.68/1.54 % (2850889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850889)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850889)Termination reason: Instruction limit
% 6.68/1.54 % (2850889)Termination phase: Saturation
% 6.68/1.54 % (2850889)Time elapsed: 0.079 s
% 6.68/1.54 % (2850889)Peak memory usage: 13 MB
% 6.68/1.54 % (2850889)Instructions burned: 131 (million)
% 6.68/1.54 % (2850903)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1410661452:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.68/1.54 % (2850887)Instruction limit reached!
% 6.68/1.54 % (2850887)------------------------------
% 6.68/1.54 % (2850887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850887)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850887)Termination reason: Instruction limit
% 6.68/1.54 % (2850887)Termination phase: Finite model building constraint generation
% 6.68/1.54 % (2850887)Time elapsed: 0.178 s
% 6.68/1.54 % (2850887)Peak memory usage: 32 MB
% 6.68/1.54 % (2850887)Instructions burned: 715 (million)
% 6.68/1.54 % (2850905)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1099137521:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.68/1.54 % TRYING [1]
% 6.68/1.54 % TRYING [2]
% 6.68/1.54 % (2850894)Instruction limit reached!
% 6.68/1.54 % (2850894)------------------------------
% 6.68/1.54 % (2850894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850894)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850894)Termination reason: Instruction limit
% 6.68/1.54 % (2850894)Termination phase: Saturation
% 6.68/1.54 % (2850894)Time elapsed: 0.137 s
% 6.68/1.54 % (2850894)Peak memory usage: 11 MB
% 6.68/1.54 % (2850894)Instructions burned: 180 (million)
% 6.68/1.54 % TRYING [3]
% 6.68/1.54 % (2850908)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2095746936:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 6.68/1.54 % TRYING [4]
% 6.68/1.54 % (2850890)Instruction limit reached!
% 6.68/1.54 % (2850890)------------------------------
% 6.68/1.54 % (2850890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850890)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850890)Termination reason: Instruction limit
% 6.68/1.54 % (2850890)Termination phase: Saturation
% 6.68/1.54 % (2850890)Time elapsed: 0.516 s
% 6.68/1.54 % (2850890)Peak memory usage: 15 MB
% 6.68/1.54 % (2850890)Instructions burned: 685 (million)
% 6.68/1.54 % (2850903)Instruction limit reached!
% 6.68/1.54 % (2850903)------------------------------
% 6.68/1.54 % (2850903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850903)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850903)Termination reason: Instruction limit
% 6.68/1.54 % (2850903)Termination phase: Saturation
% 6.68/1.54 % (2850903)Time elapsed: 0.434 s
% 6.68/1.54 % (2850903)Peak memory usage: 13 MB
% 6.68/1.54 % (2850903)Instructions burned: 477 (million)
% 6.68/1.54 % (2850905)Instruction limit reached!
% 6.68/1.54 % (2850905)------------------------------
% 6.68/1.54 % (2850905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850905)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850905)Termination reason: Instruction limit
% 6.68/1.54 % (2850905)Termination phase: Finite model building constraint generation
% 6.68/1.54 % (2850905)Time elapsed: 0.383 s
% 6.68/1.54 % (2850905)Peak memory usage: 66 MB
% 6.68/1.54 % (2850905)Instructions burned: 868 (million)
% 6.68/1.54 % (2850917)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1185365519:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 6.68/1.54 % (2850917)Cannot represent all propositional literals internally
% 6.68/1.54 % (2850917)Refutation not found, incomplete strategy
% 6.68/1.54 % (2850917)------------------------------
% 6.68/1.54 % (2850917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850917)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850917)Termination reason: Refutation not found, incomplete strategy
% 6.68/1.54 % (2850917)Time elapsed: 0.008 s
% 6.68/1.54 % (2850917)Peak memory usage: 10 MB
% 6.68/1.54 % (2850917)Instructions burned: 9 (million)
% 6.68/1.54 % (2850917)------------------------------
% 6.68/1.54 % (2850917)------------------------------
% 6.68/1.54 % (2850918)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1116898371:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 6.68/1.54 % (2850919)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1198921430:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 6.68/1.54 % (2850921)fmb+10_1_sil=64000:random_seed=684287629:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 6.68/1.54 % TRYING [1]
% 6.68/1.54 % TRYING [2]
% 6.68/1.54 % TRYING [3]
% 6.68/1.54 % TRYING [5]
% 6.68/1.54 % (2850918)Instruction limit reached!
% 6.68/1.54 % (2850918)------------------------------
% 6.68/1.54 % (2850918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850918)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850918)Termination reason: Instruction limit
% 6.68/1.54 % (2850918)Termination phase: Saturation
% 6.68/1.54 % (2850918)Time elapsed: 0.342 s
% 6.68/1.54 % (2850918)Peak memory usage: 14 MB
% 6.68/1.54 % (2850918)Instructions burned: 694 (million)
% 6.68/1.54 % (2850930)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2576273530:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 6.68/1.54 % (2850875) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2850868-2850875"...
% 6.68/1.54 % (2850930)Cannot represent all propositional literals internally
% 6.68/1.54 % (2850930)Refutation not found, incomplete strategy
% 6.68/1.54 % (2850930)------------------------------
% 6.68/1.54 % (2850930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.54 % (2850930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.54 % (2850930)CaDiCaL version: 2.1.3
% 6.68/1.54 % (2850930)Termination reason: Refutation not found, incomplete strategy
% 6.68/1.54 % (2850930)Time elapsed: 0.007 s
% 6.68/1.54 % (2850930)Peak memory usage: 10 MB
% 6.68/1.54 % (2850930)Instructions burned: 9 (million)
% 6.68/1.54 % (2850930)------------------------------
% 6.68/1.54 % (2850930)------------------------------
% 6.68/1.54 % (2850875)...printing done.
% 6.68/1.54 % TRYING [4]
% 6.68/1.54 % SZS status Satisfiable for theBenchmark
% 6.68/1.54 % SZS output start Saturation.
% See solution above
% 6.68/1.55 % SZS output start Definitions and Model Updates.
% 6.68/1.55 for all inputs,
% 6.68/1.55 define sound(X0,X1) := $false
% 6.68/1.55 for all inputs,
% 6.68/1.55 define scream(X0,X1) := $false
% 6.68/1.55 for all inputs,
% 6.68/1.55 define specific(X0,X1) := $true
% 6.68/1.55 for all inputs,
% 6.68/1.55 define cry(X0,X1) := $false
% 6.68/1.55 for all inputs,
% 6.68/1.55 define of(X0,X1,X2) := $true
% 6.68/1.55 for all inputs,
% 6.68/1.55 define actual_world(X0) := $true
% 6.68/1.55 for all inputs,
% 6.68/1.55 define revenge(X0,X1) := $false
% 6.68/1.55 for all inputs,
% 6.68/1.55 define impartial(X0,X1) := $true
% 6.68/1.55 for all inputs,
% 6.68/1.55 define human(X0,X1) := $true
% 6.68/1.55 % SZS output end Definitions and Model Updates.
% 6.68/1.55 % (2850875)------------------------------
% 6.68/1.55 % (2850875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.68/1.55 % (2850875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.68/1.55 % (2850875)CaDiCaL version: 2.1.3
% 6.68/1.55 % (2850875)Termination reason: Satisfiable
% 6.68/1.55 % (2850875)Time elapsed: 1.035 s
% 6.68/1.55 % (2850875)Peak memory usage: 24 MB
% 6.68/1.55 % (2850875)Instructions burned: 1249 (million)
% 6.68/1.55 % (2850868)Success in time 1.103 s
% 6.68/1.55 % Vampire exiting
%------------------------------------------------------------------------------