%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NLP093-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 11.46s 2.48s
% Output : Saturation 11.46s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u231,negated_conjecture,
event(X0,skf11(X0,X5,X6,X7)) ).
cnf(u572,negated_conjecture,
shot(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u577,negated_conjecture,
event(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u591,negated_conjecture,
present(X0,skf11(X0,X5,X6,X7)) ).
cnf(u601,negated_conjecture,
fire(X0,skf11(X0,X5,X6,X7)) ).
cnf(u662,negated_conjecture,
nonreflexive(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u728,negated_conjecture,
~ patient(skc4,skf11(skc4,X0,X1,skc7),skc7) ).
cnf(u737,negated_conjecture,
from_loc(X0,skf11(X0,X1,X3,X5),X3) ).
cnf(u823,axiom,
member(X0,skf19(X1,X0),X1) ).
cnf(u1350,negated_conjecture,
present(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u1387,negated_conjecture,
fire(skc4,skf11(skc4,X1,X2,X3)) ).
cnf(u2594,negated_conjecture,
from_loc(X1,skf11(X1,skf25(X0,X1),X2,X4),X2) ).
cnf(u2629,negated_conjecture,
patient(X1,skf11(X1,skf21(X0,X1),X4,X5),skf21(X0,X1)) ).
cnf(u2641,negated_conjecture,
patient(X1,skf11(X1,skf17(X0,X1),X4,X5),skf17(X0,X1)) ).
cnf(u2647,negated_conjecture,
patient(X1,skf11(X1,skf15(X0,X1),X4,X5),skf15(X0,X1)) ).
cnf(u5328,negated_conjecture,
skf19(X0,X1) = skf13(X2,skf19(X0,X1),X0,X1) ).
cnf(u5376,negated_conjecture,
~ agent(X1,X2,skf19(X0,X1)) ).
cnf(u5639,negated_conjecture,
skf19(X0,X1) = skf13(X2,skf17(X0,X1),X0,X1) ).
cnf(u5663,negated_conjecture,
~ agent(X1,X2,skf17(X0,X1)) ).
cnf(u6777,negated_conjecture,
skf19(X0,X1) = skf13(X2,skf19(X3,X1),X0,X1) ).
cnf(u7062,negated_conjecture,
skf19(X0,X1) = skf13(X2,skf17(X3,X1),X0,X1) ).
cnf(u8339,negated_conjecture,
~ agent(X1,X2,skf21(X0,X1)) ).
cnf(u9856,negated_conjecture,
member(skc4,skf17(skc5,skc4),skc5) ).
cnf(u9889,negated_conjecture,
~ agent(skc4,X0,skf25(skc5,skc4)) ).
cnf(u9979,negated_conjecture,
from_loc(skc4,skf11(skc4,X0,X1,X2),X1) ).
cnf(u10002,negated_conjecture,
patient(skc4,skf11(skc4,skf17(skc5,skc4),X2,X3),skf17(skc5,skc4)) ).
cnf(u10274,negated_conjecture,
from_loc(X1,skf11(X1,skf15(X0,X1),X2,X4),X2) ).
cnf(u10277,negated_conjecture,
from_loc(X1,skf11(X1,skf17(X0,X1),X2,X4),X2) ).
cnf(u10280,negated_conjecture,
from_loc(X1,skf11(X1,skf19(X0,X1),X2,X4),X2) ).
cnf(u10283,negated_conjecture,
from_loc(X1,skf11(X1,skf21(X0,X1),X2,X4),X2) ).
cnf(u10286,negated_conjecture,
from_loc(X1,skf11(X1,skf23(X0,X1),X2,X4),X2) ).
cnf(u10636,negated_conjecture,
from_loc(X1,skf11(X1,skf13(X4,X5,X0,X1),X2,X6),X2) ).
cnf(u11037,negated_conjecture,
skf19(X1,X0) = skf13(X2,skf13(X3,X4,X1,X0),X1,X0) ).
cnf(u12720,negated_conjecture,
skf25(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u13234,negated_conjecture,
member(skc4,skf25(skc5,skc4),skc5) ).
cnf(u13356,negated_conjecture,
~ agent(skc4,X0,skf17(skc5,skc4)) ).
cnf(u13788,negated_conjecture,
member(skc4,skf23(skc5,skc4),skc5) ).
cnf(u13812,negated_conjecture,
( skf25(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4) ) ).
cnf(u13816,negated_conjecture,
skf21(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u13861,negated_conjecture,
skf19(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4) ).
cnf(u14404,negated_conjecture,
( skf25(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf19(X1,skc4),skc5,skc4) ) ).
cnf(u14408,negated_conjecture,
skf17(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u14952,negated_conjecture,
skf19(skc5,skc4) = skf13(X0,skf21(X1,skc4),skc5,skc4) ).
cnf(u15465,negated_conjecture,
member(skc4,skf15(skc5,skc4),skc5) ).
cnf(u15489,negated_conjecture,
skf19(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u15493,negated_conjecture,
skf23(skc5,skc4) != skf15(skc5,skc4) ).
cnf(u15821,negated_conjecture,
skf23(skc5,skc4) != skf17(skc5,skc4) ).
cnf(u15858,negated_conjecture,
( skf23(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf17(skc5,skc4),skc5,skc4) ) ).
cnf(u18647,negated_conjecture,
~ patient(X0,skf11(X0,skf19(X1,X0),X2,skf21(X3,X0)),skf23(X5,X0)) ).
cnf(u18734,negated_conjecture,
~ agent(skc4,skf11(skc4,skf23(X0,skc4),skc6,X2),skf21(X1,skc4)) ).
cnf(u18762,negated_conjecture,
~ agent(skc4,skf11(skc4,skf23(X0,skc4),X1,X3),skf21(X2,skc4)) ).
cnf(u18781,negated_conjecture,
~ patient(X0,skf11(X0,skf19(X1,X0),X2,skf21(X3,X0)),skf21(X3,X0)) ).
cnf(u19008,negated_conjecture,
skf25(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u19289,negated_conjecture,
~ agent(X0,skf11(X0,skf13(X1,X2,X3,X0),X1,X4),X2) ).
cnf(u19350,negated_conjecture,
member(skc4,skf19(skc5,skc4),skc5) ).
cnf(u19365,negated_conjecture,
~ agent(skc4,skf11(skc4,skf19(X0,skc4),X1,X4),skf13(X2,X3,X0,skc4)) ).
cnf(u19388,negated_conjecture,
~ agent(X1,skf11(X1,skf19(X0,X1),X2,X5),skf13(X3,X4,X0,X1)) ).
cnf(u19606,negated_conjecture,
skf23(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u19610,negated_conjecture,
skf21(skc5,skc4) != skf19(skc5,skc4) ).
cnf(u19712,negated_conjecture,
skf25(skc5,skc4) != skf21(skc5,skc4) ).
cnf(u20415,negated_conjecture,
( skf19(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)
| skf25(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4) ) ).
cnf(u20419,negated_conjecture,
skf25(skc5,skc4) != skf17(skc5,skc4) ).
cnf(u21281,negated_conjecture,
member(skc4,skf21(skc5,skc4),skc5) ).
cnf(u21341,negated_conjecture,
skf23(skc5,skc4) != skf21(skc5,skc4) ).
cnf(u21420,negated_conjecture,
( skf17(skc5,skc4) = skf13(X1,skf25(X2,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X1,skf25(X2,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X1,skf25(X2,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X1,skf25(X2,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X1,skf25(X2,skc4),skc5,skc4) ) ).
cnf(u21769,negated_conjecture,
patient(skc4,skf11(skc4,skf21(skc5,skc4),X2,X3),skf21(skc5,skc4)) ).
cnf(u21817,negated_conjecture,
skf19(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4) ).
cnf(u22393,negated_conjecture,
( skf25(skc5,skc4) = skf13(X0,skf17(X1,skc4),skc5,skc4)
| skf23(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) ) ).
cnf(u22397,negated_conjecture,
skf19(skc5,skc4) != skf17(skc5,skc4) ).
cnf(u22818,negated_conjecture,
~ patient(X0,skf11(X0,skf15(X1,X0),X2,skf13(X3,X4,X5,X0)),skf19(X5,X0)) ).
cnf(u22821,negated_conjecture,
skf19(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0) ).
cnf(u23560,negated_conjecture,
patient(skc4,skf11(skc4,skf19(skc5,skc4),X2,X3),skf19(skc5,skc4)) ).
cnf(u24067,negated_conjecture,
skf19(skc5,skc4) != skf13(skc6,skc7,skc5,skc4) ).
cnf(u24071,negated_conjecture,
skf21(skc5,skc4) != skf13(skc6,skc7,skc5,skc4) ).
cnf(u24075,negated_conjecture,
skf23(skc5,skc4) != skf13(skc6,skc7,skc5,skc4) ).
cnf(u24079,negated_conjecture,
skf25(skc5,skc4) != skf13(skc6,skc7,skc5,skc4) ).
cnf(u24083,negated_conjecture,
skf17(skc5,skc4) != skf13(skc6,skc7,skc5,skc4) ).
cnf(u24715,negated_conjecture,
~ agent(skc4,X0,skf21(skc5,skc4)) ).
cnf(u25634,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(u25766,negated_conjecture,
( skf23(skc5,skc4) = skf13(X2,skf21(X3,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X2,skf21(X3,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X2,skf21(X3,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X2,skf21(X3,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X2,skf21(X3,skc4),skc5,skc4) ) ).
cnf(u25769,negated_conjecture,
~ patient(skc4,skf11(skc4,skf15(X0,skc4),X1,skf15(skc5,skc4)),skf19(skc5,skc4)) ).
cnf(u26197,negated_conjecture,
skf21(skc5,skc4) != skf17(skc5,skc4) ).
cnf(u26348,negated_conjecture,
patient(X1,skf11(X1,skf26(X4,X5,X6,X7,X8,X9,X0,X1),X10,X11),skf26(X4,X5,X6,X7,X8,X9,X0,X1)) ).
cnf(u32959,negated_conjecture,
~ agent(skc4,X0,skf17(X2,skc4)) ).
cnf(u33045,negated_conjecture,
~ agent(skc4,X0,skf25(X8,skc4)) ).
cnf(u33115,negated_conjecture,
~ agent(skc4,X0,skf23(skc5,skc4)) ).
cnf(u33157,negated_conjecture,
~ agent(skc4,X0,skf15(X2,skc4)) ).
cnf(u33232,negated_conjecture,
~ agent(skc4,X0,skf26(X2,X3,X4,X5,X6,X7,X8,skc4)) ).
cnf(u33737,negated_conjecture,
~ agent(skc4,skf11(skc4,skf19(skc5,skc4),skc6,X1),skf23(X0,skc4)) ).
cnf(u33879,negated_conjecture,
~ agent(skc4,skf11(skc4,skf19(skc5,skc4),X0,X2),skf23(X1,skc4)) ).
cnf(u33929,negated_conjecture,
~ agent(skc4,skf11(skc4,skf19(skc5,skc4),skc6,X1),skf25(X0,skc4)) ).
cnf(u33985,negated_conjecture,
~ agent(skc4,skf11(skc4,skf25(skc5,skc4),X1,X2),skf25(X0,skc4)) ).
cnf(u34194,negated_conjecture,
~ agent(skc4,X0,skf23(X2,skc4)) ).
cnf(u34287,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4) ).
cnf(u35015,negated_conjecture,
member(skc4,skf21(X0,skc4),X0) ).
cnf(u35506,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4) ).
cnf(u36073,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4) ).
cnf(u36544,negated_conjecture,
skf21(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4) ).
cnf(u36962,negated_conjecture,
~ patient(X0,skf11(X0,skf17(X1,X0),X2,skf13(X3,X4,X5,X0)),skf19(X5,X0)) ).
cnf(u778,negated_conjecture,
eventuality(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause21,axiom,
( ~ weapon(X0,X1)
| weaponry(X0,X1) ) ).
cnf(u22906,negated_conjecture,
~ patient(X1,skf11(X1,skf15(X2,X1),X3,skf19(X0,X1)),skf19(X0,X1)) ).
cnf(u37059,negated_conjecture,
~ agent(X1,skf11(X1,skf19(X0,X1),X2,X6),skf13(X3,X4,X5,X1)) ).
cnf(u805,negated_conjecture,
singleton(skc4,skf23(skc5,skc4)) ).
cnf(clause32,axiom,
( ~ man(X0,X1)
| human_person(X0,X1) ) ).
cnf(u803,negated_conjecture,
nonexistent(skc4,skf23(skc5,skc4)) ).
cnf(u2589,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(u2587,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(clause38,axiom,
( ~ human_person(X0,X1)
| animate(X0,X1) ) ).
cnf(u818,negated_conjecture,
thing(skc4,skf21(skc5,skc4)) ).
cnf(u61,axiom,
( skf19(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u33271,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf26(X2,X3,X4,X5,X6,X7,X8,skc4),X0,skc4) ) ).
cnf(u8256,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(clause51,axiom,
( skf25(X0,X1) != skf15(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u672,negated_conjecture,
( ~ patient(skc4,skf11(skc4,X0,skc6,skc7),skc7)
| ~ member(skc4,X0,skc5) ) ).
cnf(u1081,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(u444,negated_conjecture,
~ nonexistent(skc4,skc6) ).
cnf(u774,negated_conjecture,
thing(skc4,skf25(skc5,skc4)) ).
cnf(u780,negated_conjecture,
nonexistent(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u9234,negated_conjecture,
( ~ six(X1,X0)
| skf23(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf23(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X3,X4,X0,X1)
| skf21(X0,X1) = skf13(X3,X4,X0,X1)
| skf23(X0,X1) = skf13(X3,X4,X0,X1)
| skf25(X0,X1) = skf13(X3,X4,X0,X1)
| skf15(X0,X1) = skf13(X3,X4,X0,X1)
| skf17(X0,X1) = skf13(X3,X4,X0,X1) ) ).
cnf(u828,negated_conjecture,
event(skc4,skf19(skc5,skc4)) ).
cnf(u2368,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(u10288,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(u434,negated_conjecture,
thing(skc4,skc6) ).
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(u2374,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(u584,negated_conjecture,
thing(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u833,negated_conjecture,
singleton(skc4,skf19(skc5,skc4)) ).
cnf(clause66,axiom,
( ~ agent(X0,X1,X2)
| ~ patient(X0,X1,X2)
| ~ nonreflexive(X0,X1) ) ).
cnf(u847,negated_conjecture,
singleton(skc4,skf17(skc5,skc4)) ).
cnf(clause80,negated_conjecture,
group(skc4,skc5) ).
cnf(u33695,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf19(skc5,skc4),skc6,X1),skf25(X0,skc4))
| skf25(skc5,skc4) = skf13(skc6,skf25(X0,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(skc6,skf25(X0,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(skc6,skf25(X0,skc4),skc5,skc4) ) ).
cnf(u772,negated_conjecture,
unisex(skc4,skf25(skc5,skc4)) ).
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(u34228,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf23(X2,skc4),X0,skc4) ) ).
cnf(u22812,negated_conjecture,
( ~ patient(X0,skf11(X0,skf15(X1,X0),X2,skf13(X3,X4,X5,X0)),skf19(X5,X0))
| ~ from_loc(X0,skf11(X0,skf15(X1,X0),X2,skf13(X3,X4,X5,X0)),X6)
| skf19(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf21(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf23(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf25(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| ~ six(X0,X1)
| skf15(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf17(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0) ) ).
cnf(u489,negated_conjecture,
thing(skc4,skc7) ).
cnf(u2568,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(clause5,axiom,
( ~ eventuality(X0,X1)
| thing(X0,X1) ) ).
cnf(u789,negated_conjecture,
nonexistent(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause16,axiom,
( ~ group(X0,X1)
| set(X0,X1) ) ).
cnf(u787,negated_conjecture,
eventuality(X0,skf11(X0,X1,X2,X3)) ).
cnf(u24589,negated_conjecture,
( skf15(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf23(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf17(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4)
| skf19(skc5,skc4) = skf13(X0,skf21(skc5,skc4),skc5,skc4) ) ).
cnf(u401,negated_conjecture,
artifact(skc4,skc6) ).
cnf(u2571,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(clause22,axiom,
( ~ weaponry(X0,X1)
| instrumentality(X0,X1) ) ).
cnf(u802,negated_conjecture,
unisex(skc4,skf23(skc5,skc4)) ).
cnf(clause45,axiom,
( member(X0,skf25(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u829,negated_conjecture,
eventuality(skc4,skf19(skc5,skc4)) ).
cnf(u33625,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf19(skc5,skc4),X0,X2),skf23(X1,skc4))
| skf23(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X0,skf23(X1,skc4),skc5,skc4) ) ).
cnf(u812,negated_conjecture,
action(skc4,skf21(skc5,skc4)) ).
cnf(u18565,negated_conjecture,
( ~ patient(X1,skf11(X1,skf13(X4,X5,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)
| ssSkP0(X4,X5,X0,X1)
| skf19(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u817,negated_conjecture,
nonexistent(skc4,skf21(skc5,skc4)) ).
cnf(u831,negated_conjecture,
nonexistent(skc4,skf19(skc5,skc4)) ).
cnf(u1082,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(clause50,axiom,
( member(X0,skf15(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u1080,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)
| present(X1,skf11(X1,X5,X6,X7)) ) ).
cnf(u2369,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(u75,axiom,
( skf15(X0,X1) != skf17(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2372,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(u846,negated_conjecture,
thing(skc4,skf17(skc5,skc4)) ).
cnf(u73,axiom,
( skf17(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u458,negated_conjecture,
unisex(skc4,skc6) ).
cnf(u857,negated_conjecture,
eventuality(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,skc7) ).
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(u37031,negated_conjecture,
skf19(X1,skc4) = skf13(X2,skf21(X0,skc4),X1,skc4) ).
cnf(clause79,negated_conjecture,
six(skc4,skc5) ).
cnf(u345,negated_conjecture,
multiple(skc4,skc5) ).
cnf(u861,negated_conjecture,
singleton(skc4,skf15(skc5,skc4)) ).
cnf(clause77,negated_conjecture,
man(skc4,skc7) ).
cnf(u859,negated_conjecture,
nonexistent(skc4,skf15(skc5,skc4)) ).
cnf(u24605,negated_conjecture,
( ~ six(X1,X0)
| skf23(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1)
| skf21(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1)
| skf15(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1)
| skf17(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1)
| skf19(X0,X1) = skf13(X2,skf21(X0,X1),X0,X1) ) ).
cnf(u773,negated_conjecture,
nonexistent(skc4,skf25(skc5,skc4)) ).
cnf(u22791,negated_conjecture,
( ~ agent(X1,skf11(X1,skf13(X4,X5,X0,X1),X4,X6),X5)
| 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)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| skf21(X0,X1) = skf13(X2,X3,X0,X1) ) ).
cnf(u771,negated_conjecture,
eventuality(skc4,skf25(skc5,skc4)) ).
cnf(u385,negated_conjecture,
instrumentality(skc4,skc6) ).
cnf(clause6,axiom,
( ~ thing(X0,X1)
| singleton(X0,X1) ) ).
cnf(u759,negated_conjecture,
action(skc4,skf25(skc5,skc4)) ).
cnf(clause29,axiom,
( ~ object(X0,X1)
| nonliving(X0,X1) ) ).
cnf(clause19,axiom,
( ~ fire(X0,X1)
| event(X0,X1) ) ).
cnf(u2590,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(u303,negated_conjecture,
set(skc4,skc5) ).
cnf(u2329,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(clause46,axiom,
( member(X0,skf23(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u790,negated_conjecture,
thing(X0,skf11(X0,X1,X2,X3)) ).
cnf(clause17,axiom,
( ~ set(X0,X1)
| multiple(X0,X1) ) ).
cnf(u801,negated_conjecture,
eventuality(skc4,skf23(skc5,skc4)) ).
cnf(clause44,axiom,
( ~ animate(X0,X1)
| ~ nonliving(X0,X1) ) ).
cnf(u1085,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(u9235,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(u815,negated_conjecture,
eventuality(skc4,skf21(skc5,skc4)) ).
cnf(u2569,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(u59,axiom,
( skf17(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(clause34,axiom,
( ~ organism(X0,X1)
| entity(X0,X1) ) ).
cnf(u830,negated_conjecture,
unisex(skc4,skf19(skc5,skc4)) ).
cnf(u57,axiom,
( skf15(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u1468,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)
| present(X1,skf11(X1,X4,X5,X6)) ) ).
cnf(u63,axiom,
( skf21(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u37081,negated_conjecture,
( ~ agent(X1,X2,skf13(X4,X5,X6,X1))
| ~ fire(X1,X2)
| ~ nonreflexive(X1,X2)
| ~ present(X1,X2)
| ~ from_loc(X1,X2,X3)
| ~ patient(X1,X2,skf19(X0,X1)) ) ).
cnf(u841,negated_conjecture,
act(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,
act(skc4,skf15(skc5,skc4)) ).
cnf(u2373,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(u845,negated_conjecture,
nonexistent(skc4,skf17(skc5,skc4)) ).
cnf(u843,negated_conjecture,
eventuality(skc4,skf17(skc5,skc4)) ).
cnf(u25045,negated_conjecture,
( ~ six(X1,X0)
| skf21(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf23(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf25(X0,X1) = skf13(X2,skf21(X3,X1),X0,X1)
| skf19(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) ) ).
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(u858,negated_conjecture,
unisex(skc4,skf15(skc5,skc4)) ).
cnf(u24602,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf13(X0,X1,X2,skc4),X0,X3),X1)
| ~ member(skc4,skf13(X0,X1,X2,skc4),skc5) ) ).
cnf(clause90,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| patient(X0,skf11(X0,X1,X5,X6),X1) ) ).
cnf(u9964,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(u497,negated_conjecture,
~ nonliving(skc4,skc7) ).
cnf(u33148,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf23(skc5,skc4),X0,skc4) ) ).
cnf(u33194,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf19(skc5,skc4),skc6,X1),skf23(X0,skc4))
| skf23(skc5,skc4) = skf13(skc6,skf23(X0,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(skc6,skf23(X0,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(skc6,skf23(X0,skc4),skc5,skc4) ) ).
cnf(u770,negated_conjecture,
event(skc4,skf25(skc5,skc4)) ).
cnf(u618,negated_conjecture,
( patient(skc4,skf11(skc4,X0,X1,X2),X0)
| ~ member(skc4,X0,skc5) ) ).
cnf(clause13,axiom,
( ~ action(X0,X1)
| act(X0,X1) ) ).
cnf(u776,negated_conjecture,
act(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u29080,negated_conjecture,
( ~ patient(X0,skf11(X0,skf17(X1,X0),X2,skf13(X3,X4,X5,X0)),skf19(X5,X0))
| ~ from_loc(X0,skf11(X0,skf17(X1,X0),X2,skf13(X3,X4,X5,X0)),X6)
| skf19(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf21(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf23(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf25(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| ~ six(X0,X1)
| skf15(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0)
| skf17(X1,X0) = skf13(X2,skf13(X3,X4,X5,X0),X1,X0) ) ).
cnf(u33195,negated_conjecture,
( ~ member(X0,X2,X1)
| member(X0,skf19(X1,X0),X1) ) ).
cnf(clause1,axiom,
~ member(X0,X1,X1) ).
cnf(u553,negated_conjecture,
shot(skc4,skf25(skc5,skc4)) ).
cnf(clause28,axiom,
( ~ entity(X0,X1)
| existent(X0,X1) ) ).
cnf(u799,negated_conjecture,
act(skc4,skf23(skc5,skc4)) ).
cnf(clause43,axiom,
( ~ existent(X0,X1)
| ~ nonexistent(X0,X1) ) ).
cnf(clause18,axiom,
( ~ six(X0,X1)
| group(X0,X1) ) ).
cnf(u2585,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(u814,negated_conjecture,
event(skc4,skf21(skc5,skc4)) ).
cnf(u2591,negated_conjecture,
( from_loc(X1,skf11(X1,skf25(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(clause41,axiom,
( ~ multiple(X0,X1)
| ~ singleton(X0,X1) ) ).
cnf(u426,negated_conjecture,
entity(skc4,skc6) ).
cnf(u825,negated_conjecture,
shot(skc4,skf19(skc5,skc4)) ).
cnf(u2586,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(clause47,axiom,
( member(X0,skf21(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u1084,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(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(u839,negated_conjecture,
shot(skc4,skf17(skc5,skc4)) ).
cnf(u443,negated_conjecture,
existent(skc4,skc6) ).
cnf(u827,negated_conjecture,
act(skc4,skf19(skc5,skc4)) ).
cnf(u33024,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(u2370,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(clause76,negated_conjecture,
male(skc4,skc7) ).
cnf(u32805,negated_conjecture,
( ~ agent(X1,X2,skf17(X0,X1))
| ~ fire(X1,X2)
| ~ nonreflexive(X1,X2)
| ~ present(X1,X2)
| ~ from_loc(X1,X2,X3)
| ~ patient(X1,X2,skf19(X0,X1)) ) ).
cnf(u842,negated_conjecture,
event(skc4,skf17(skc5,skc4)) ).
cnf(clause85,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| event(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(clause91,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| from_loc(X0,skf11(X0,X1,X3,X5),X3) ) ).
cnf(u32813,negated_conjecture,
( ~ agent(skc4,X0,skf23(X2,skc4))
| ~ fire(skc4,X0)
| ~ nonreflexive(skc4,X0)
| ~ present(skc4,X0)
| ~ from_loc(skc4,X0,X1)
| ~ patient(skc4,X0,skf19(skc5,skc4))
| skf23(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4)
| skf21(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4)
| skf25(skc5,skc4) = skf13(X1,skf23(X2,skc4),skc5,skc4) ) ).
cnf(u32806,negated_conjecture,
( ~ agent(skc4,X0,skf17(X2,skc4))
| ~ fire(skc4,X0)
| ~ nonreflexive(skc4,X0)
| ~ present(skc4,X0)
| ~ from_loc(skc4,X0,X1)
| ~ patient(skc4,X0,skf19(skc5,skc4)) ) ).
cnf(u22788,negated_conjecture,
( ~ from_loc(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X7),X4)
| 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)
| skf19(X0,X1) = skf13(X2,X3,X0,X1)
| ~ agent(X1,skf11(X1,skf13(X4,X5,X0,X1),X6,X7),X5) ) ).
cnf(u485,negated_conjecture,
entity(skc4,skc7) ).
cnf(clause14,axiom,
( ~ act(X0,X1)
| event(X0,X1) ) ).
cnf(u1400,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf13(skc6,X0,X1,skc4),skc6,X2),X0)
| ~ member(skc4,skf13(skc6,X0,X1,skc4),skc5) ) ).
cnf(u767,negated_conjecture,
act(skc4,skf25(skc5,skc4)) ).
cnf(u2588,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(u9230,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(u496,negated_conjecture,
living(skc4,skc7) ).
cnf(u798,negated_conjecture,
action(skc4,skf23(skc5,skc4)) ).
cnf(clause25,axiom,
( ~ object(X0,X1)
| entity(X0,X1) ) ).
cnf(u804,negated_conjecture,
thing(skc4,skf23(skc5,skc4)) ).
cnf(clause52,axiom,
( skf25(X0,X1) != skf17(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u2570,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(u34662,negated_conjecture,
~ patient(skc4,skf11(skc4,skf15(X1,skc4),X2,skf21(X0,skc4)),skf19(X0,skc4)) ).
cnf(clause31,axiom,
( ~ object(X0,X1)
| unisex(X0,X1) ) ).
cnf(clause42,axiom,
( ~ living(X0,X1)
| ~ nonliving(X0,X1) ) ).
cnf(u1083,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(u1453,negated_conjecture,
~ member(skc4,skf13(skc6,skc7,X0,skc4),skc5) ).
cnf(u159,negated_conjecture,
~ unisex(skc4,skc7) ).
cnf(u414,negated_conjecture,
object(skc4,skc6) ).
cnf(u813,negated_conjecture,
act(skc4,skf21(skc5,skc4)) ).
cnf(clause40,axiom,
( ~ male(X0,X1)
| ~ unisex(X0,X1) ) ).
cnf(u811,negated_conjecture,
shot(skc4,skf21(skc5,skc4)) ).
cnf(u11568,negated_conjecture,
( ssSkP0(X2,skf13(X3,X4,X0,X1),X0,X1)
| member(X1,skf19(X0,X1),X0) ) ).
cnf(u826,negated_conjecture,
action(skc4,skf19(skc5,skc4)) ).
cnf(u579,negated_conjecture,
eventuality(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u71,axiom,
( skf15(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u37009,negated_conjecture,
~ patient(X1,skf11(X1,skf17(X2,X1),X3,skf19(X0,X1)),skf19(X0,X1)) ).
cnf(u69,axiom,
( skf19(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u832,negated_conjecture,
thing(skc4,skf19(skc5,skc4)) ).
cnf(u2371,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(u853,negated_conjecture,
shot(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,
nonexistent(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u465,negated_conjecture,
human_person(skc4,skc7) ).
cnf(u8259,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(clause88,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| fire(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(clause86,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| present(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u2566,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(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(u1397,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(u2572,negated_conjecture,
( patient(X1,skf11(X1,skf25(X0,X1),X4,X5),skf25(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(u760,negated_conjecture,
action(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(u11779,negated_conjecture,
( ssSkP0(X2,skf19(X0,X1),X0,X1)
| member(X1,skf19(X0,X1),X0) ) ).
cnf(u782,negated_conjecture,
singleton(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause9,axiom,
( ~ eventuality(X0,X1)
| unisex(X0,X1) ) ).
cnf(u788,negated_conjecture,
unisex(X0,skf11(X0,X1,X2,X3)) ).
cnf(u11567,negated_conjecture,
( ~ agent(skc4,skf11(skc4,skf19(X0,skc4),skc6,X3),skf13(X1,X2,X0,skc4))
| ~ member(skc4,skf19(X0,skc4),skc5) ) ).
cnf(clause15,axiom,
( ~ shot(X0,X1)
| action(X0,X1) ) ).
cnf(clause36,axiom,
( ~ organism(X0,X1)
| living(X0,X1) ) ).
cnf(u34655,negated_conjecture,
skf19(X0,skc4) = skf13(X1,skf21(X0,skc4),X0,skc4) ).
cnf(clause24,axiom,
( ~ artifact(X0,X1)
| object(X0,X1) ) ).
cnf(clause26,axiom,
( ~ entity(X0,X1)
| thing(X0,X1) ) ).
cnf(clause49,axiom,
( member(X0,skf17(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u797,negated_conjecture,
shot(skc4,skf23(skc5,skc4)) ).
cnf(clause55,axiom,
( skf25(X0,X1) != skf23(X0,X1)
| ~ six(X1,X0) ) ).
cnf(clause53,axiom,
( skf25(X0,X1) != skf19(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u816,negated_conjecture,
unisex(skc4,skf21(skc5,skc4)) ).
cnf(u582,negated_conjecture,
unisex(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(u8253,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(u588,negated_conjecture,
singleton(skc4,skf11(skc4,X0,X1,X2)) ).
cnf(clause82,negated_conjecture,
ssSkP0(skc6,skc7,skc5,skc4) ).
cnf(u856,negated_conjecture,
event(skc4,skf15(skc5,skc4)) ).
cnf(u325,negated_conjecture,
weapon(skc4,skc6) ).
cnf(u348,negated_conjecture,
~ singleton(skc4,skc5) ).
cnf(u607,negated_conjecture,
( agent(skc4,skf11(skc4,X0,skc6,skc7),skc7)
| ~ member(skc4,X0,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(u33317,negated_conjecture,
( member(X0,skf19(X1,X0),X1)
| ssSkP0(X2,X3,X1,X0) ) ).
cnf(u34099,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf25(X2,skc4),X0,skc4) ) ).
cnf(u854,negated_conjecture,
action(skc4,skf15(skc5,skc4)) ).
cnf(u860,negated_conjecture,
thing(skc4,skf15(skc5,skc4)) ).
cnf(u24131,negated_conjecture,
( ~ agent(X1,X2,skf19(X4,X1))
| ~ fire(X1,X2)
| ~ nonreflexive(X1,X2)
| ~ present(X1,X2)
| ~ from_loc(X1,X2,X3)
| ~ patient(X1,X2,skf19(X0,X1)) ) ).
cnf(u738,negated_conjecture,
( from_loc(skc4,skf11(skc4,X0,skc6,X1),skc6)
| ~ member(skc4,X0,skc5) ) ).
cnf(u34091,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf25(skc5,skc4),X0,skc4) ) ).
cnf(clause87,negated_conjecture,
( ~ ssSkP0(X3,X4,X2,X0)
| ~ member(X0,X1,X2)
| nonreflexive(X0,skf11(X0,X5,X6,X7)) ) ).
cnf(u777,negated_conjecture,
event(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause20,axiom,
( ~ cannon(X0,X1)
| weapon(X0,X1) ) ).
cnf(u791,negated_conjecture,
singleton(X0,skf11(X0,X1,X2,X3)) ).
cnf(u25725,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(clause33,axiom,
( ~ human_person(X0,X1)
| organism(X0,X1) ) ).
cnf(u781,negated_conjecture,
thing(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause8,axiom,
( ~ eventuality(X0,X1)
| nonexistent(X0,X1) ) ).
cnf(u33217,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf15(X2,skc4),X0,skc4) ) ).
cnf(u779,negated_conjecture,
unisex(skc4,skf13(X0,X1,skc5,skc4)) ).
cnf(clause39,axiom,
( ~ man(X0,X1)
| male(X0,X1) ) ).
cnf(u677,negated_conjecture,
~ member(skc4,skc7,skc5) ).
cnf(u11445,negated_conjecture,
( skf15(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)
| skf21(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(u800,negated_conjecture,
event(skc4,skf23(skc5,skc4)) ).
cnf(u24749,negated_conjecture,
( ~ six(skc4,X0)
| skf21(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4)
| skf23(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4)
| skf25(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4)
| skf19(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4)
| skf15(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4)
| skf17(X0,skc4) = skf13(X1,skf21(skc5,skc4),X0,skc4) ) ).
cnf(clause48,axiom,
( member(X0,skf19(X1,X0),X1)
| ~ six(X0,X1) ) ).
cnf(u819,negated_conjecture,
singleton(skc4,skf21(skc5,skc4)) ).
cnf(u34649,negated_conjecture,
( member(skc4,skf21(X0,skc4),X0)
| ssSkP0(X1,skf25(X2,skc4),X0,skc4) ) ).
cnf(clause54,axiom,
( skf25(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u11821,negated_conjecture,
( ~ agent(X1,X2,skf13(X4,X5,X0,X1))
| ~ fire(X1,X2)
| ~ nonreflexive(X1,X2)
| ~ present(X1,X2)
| ~ from_loc(X1,X2,X3)
| ~ patient(X1,X2,skf19(X0,X1)) ) ).
cnf(u840,negated_conjecture,
action(skc4,skf17(skc5,skc4)) ).
cnf(u437,negated_conjecture,
singleton(skc4,skc6) ).
cnf(u67,axiom,
( skf17(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u37012,negated_conjecture,
~ patient(skc4,skf11(skc4,skf17(X1,skc4),X2,skf21(X0,skc4)),skf19(X0,skc4)) ).
cnf(clause83,negated_conjecture,
( ~ member(skc4,X0,skc5)
| shot(skc4,X0) ) ).
cnf(u65,axiom,
( skf15(X0,X1) != skf21(X0,X1)
| ~ six(X1,X0) ) ).
cnf(u844,negated_conjecture,
unisex(skc4,skf17(skc5,skc4)) ).
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(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,
singleton(skc4,skf25(skc5,skc4)) ).
cnf(u9239,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)
| skf19(X0,X1) = skf13(X3,X4,X0,X1)
| skf21(X0,X1) = skf13(X3,X4,X0,X1)
| skf23(X0,X1) = skf13(X3,X4,X0,X1)
| skf25(X0,X1) = skf13(X3,X4,X0,X1)
| skf15(X0,X1) = skf13(X3,X4,X0,X1)
| skf17(X0,X1) = skf13(X3,X4,X0,X1) ) ).
cnf(u488,negated_conjecture,
existent(skc4,skc7) ).
cnf(u507,negated_conjecture,
animate(skc4,skc7) ).
cnf(u893,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(u10618,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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP093-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n016.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 18:08:33 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.53/1.44 % (2901020)Will run a generic schedule for satisfiability detection.
% 6.53/1.44 % (2901030)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=319072713:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.53/1.44 % (2901026)% WARNING: option uhcvi not known.
% 6.53/1.44 % (2901025)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2289485194_2999 on theBenchmark for (2999ds/0Mi)
% 6.53/1.44 % (2901026)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2004293081:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.53/1.44 % (2901031)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=907356729:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.53/1.44 % (2901027)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4134777082:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.53/1.44 % (2901028)dis+10_1_sil=32000:sp=arity:random_seed=3140364362:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.53/1.44 % (2901029)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1117683570:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.53/1.44 % TRYING [1]
% 6.53/1.44 % TRYING [2]
% 6.53/1.44 % TRYING [3]
% 6.53/1.44 % (2901030)Instruction limit reached!
% 6.53/1.44 % (2901030)------------------------------
% 6.53/1.44 % (2901030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.44 % (2901030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.44 % (2901030)CaDiCaL version: 2.1.3
% 6.53/1.44 % (2901030)Termination reason: Instruction limit
% 6.53/1.44 % (2901030)Termination phase: Saturation
% 6.53/1.44 % (2901030)Time elapsed: 0.030 s
% 6.53/1.44 % (2901030)Peak memory usage: 12 MB
% 6.53/1.44 % (2901030)Instructions burned: 136 (million)
% 6.53/1.44 % (2901039)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3330651919:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.53/1.44 % TRYING [1]
% 6.53/1.44 % TRYING [2]
% 6.53/1.44 % TRYING [3]
% 6.53/1.44 % (2901029)Instruction limit reached!
% 6.53/1.44 % (2901029)------------------------------
% 6.53/1.44 % (2901029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.44 % (2901029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.44 % (2901029)CaDiCaL version: 2.1.3
% 6.53/1.44 % (2901029)Termination reason: Instruction limit
% 6.53/1.44 % (2901029)Termination phase: Saturation
% 6.53/1.44 % (2901029)Time elapsed: 0.054 s
% 6.53/1.44 % (2901029)Peak memory usage: 12 MB
% 6.53/1.44 % (2901029)Instructions burned: 116 (million)
% 6.53/1.44 % (2901028)Instruction limit reached!
% 6.53/1.44 % (2901028)------------------------------
% 6.53/1.44 % (2901028)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.44 % (2901028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.44 % (2901028)CaDiCaL version: 2.1.3
% 6.53/1.44 % (2901028)Termination reason: Instruction limit
% 6.53/1.44 % (2901028)Termination phase: Saturation
% 6.53/1.44 % (2901028)Time elapsed: 0.055 s
% 6.53/1.44 % (2901028)Peak memory usage: 12 MB
% 6.53/1.44 % (2901028)Instructions burned: 104 (million)
% 6.53/1.44 % (2901041)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1248648208:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.53/1.44 % (2901042)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=650522684:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 6.53/1.44 % TRYING [4]
% 6.53/1.44 % (2901031)Instruction limit reached!
% 6.53/1.44 % (2901031)------------------------------
% 6.53/1.44 % (2901031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.44 % (2901031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.53/1.44 % (2901031)CaDiCaL version: 2.1.3
% 6.53/1.44 % (2901031)Termination reason: Instruction limit
% 6.53/1.44 % (2901031)Termination phase: Saturation
% 6.53/1.44 % (2901031)Time elapsed: 0.094 s
% 6.53/1.44 % (2901031)Peak memory usage: 13 MB
% 6.53/1.44 % (2901031)Instructions burned: 160 (million)
% 6.53/1.44 % (2901045)ott-21_1_sil=16000:fs=off:random_seed=990396011:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.53/1.44 % TRYING [4]
% 6.53/1.44 % (2901041)Instruction limit reached!
% 6.53/1.44 % (2901041)------------------------------
% 6.53/1.44 % (2901041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.53/1.44 % (2901041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901041)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901041)Termination reason: Instruction limit
% 11.46/2.48 % (2901041)Termination phase: Saturation
% 11.46/2.48 % (2901041)Time elapsed: 0.065 s
% 11.46/2.48 % (2901041)Peak memory usage: 13 MB
% 11.46/2.48 % (2901041)Instructions burned: 133 (million)
% 11.46/2.48 % (2901047)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2437472569:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 11.46/2.48 % (2901039)Instruction limit reached!
% 11.46/2.48 % (2901039)------------------------------
% 11.46/2.48 % (2901039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901039)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901039)Termination reason: Instruction limit
% 11.46/2.48 % (2901039)Termination phase: Finite model building constraint generation
% 11.46/2.48 % (2901039)Time elapsed: 0.137 s
% 11.46/2.48 % (2901039)Peak memory usage: 32 MB
% 11.46/2.48 % (2901039)Instructions burned: 714 (million)
% 11.46/2.48 % (2901049)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=405044218:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 11.46/2.48 % TRYING [1]
% 11.46/2.48 % TRYING [2]
% 11.46/2.48 % TRYING [3]
% 11.46/2.48 % (2901045)Instruction limit reached!
% 11.46/2.48 % (2901045)------------------------------
% 11.46/2.48 % (2901045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901045)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901045)Termination reason: Instruction limit
% 11.46/2.48 % (2901045)Termination phase: Saturation
% 11.46/2.48 % (2901045)Time elapsed: 0.091 s
% 11.46/2.48 % (2901045)Peak memory usage: 12 MB
% 11.46/2.48 % (2901045)Instructions burned: 181 (million)
% 11.46/2.48 % (2901051)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=631268154:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 11.46/2.48 % TRYING [4]
% 11.46/2.48 % (2901049)Instruction limit reached!
% 11.46/2.48 % (2901049)------------------------------
% 11.46/2.48 % (2901049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901049)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901049)Termination reason: Instruction limit
% 11.46/2.48 % (2901049)Termination phase: Finite model building constraint generation
% 11.46/2.48 % (2901049)Time elapsed: 0.190 s
% 11.46/2.48 % (2901049)Peak memory usage: 61 MB
% 11.46/2.48 % (2901049)Instructions burned: 869 (million)
% 11.46/2.48 % (2901053)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1600012477:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 11.46/2.48 % (2901053)Cannot represent all propositional literals internally
% 11.46/2.48 % (2901053)Refutation not found, incomplete strategy
% 11.46/2.48 % (2901053)------------------------------
% 11.46/2.48 % (2901053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901053)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901053)Termination reason: Refutation not found, incomplete strategy
% 11.46/2.48 % (2901053)Time elapsed: 0.002 s
% 11.46/2.48 % (2901053)Peak memory usage: 10 MB
% 11.46/2.48 % (2901053)Instructions burned: 9 (million)
% 11.46/2.48 % (2901053)------------------------------
% 11.46/2.48 % (2901053)------------------------------
% 11.46/2.48 % (2901055)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=3996628226:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 11.46/2.48 % (2901042)Instruction limit reached!
% 11.46/2.48 % (2901042)------------------------------
% 11.46/2.48 % (2901042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901042)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901042)Termination reason: Instruction limit
% 11.46/2.48 % (2901042)Termination phase: Saturation
% 11.46/2.48 % (2901042)Time elapsed: 0.331 s
% 11.46/2.48 % (2901042)Peak memory usage: 15 MB
% 11.46/2.48 % (2901042)Instructions burned: 685 (million)
% 11.46/2.48 % (2901057)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1929076078:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 11.46/2.48 % (2901047)Instruction limit reached!
% 11.46/2.48 % (2901047)------------------------------
% 11.46/2.48 % (2901047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901047)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901047)Termination reason: Instruction limit
% 11.46/2.48 % (2901047)Termination phase: Saturation
% 11.46/2.48 % (2901047)Time elapsed: 0.275 s
% 11.46/2.48 % (2901047)Peak memory usage: 13 MB
% 11.46/2.48 % (2901047)Instructions burned: 478 (million)
% 11.46/2.48 % (2901059)fmb+10_1_sil=64000:random_seed=513529213:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 11.46/2.48 % TRYING [1]
% 11.46/2.48 % TRYING [2]
% 11.46/2.48 % TRYING [3]
% 11.46/2.48 % (2901055)Instruction limit reached!
% 11.46/2.48 % (2901055)------------------------------
% 11.46/2.48 % (2901055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901055)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901055)Termination reason: Instruction limit
% 11.46/2.48 % (2901055)Termination phase: Saturation
% 11.46/2.48 % (2901055)Time elapsed: 0.189 s
% 11.46/2.48 % (2901055)Peak memory usage: 15 MB
% 11.46/2.48 % (2901055)Instructions burned: 694 (million)
% 11.46/2.48 % TRYING [5]
% 11.46/2.48 % (2901061)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3326841618:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 11.46/2.48 % (2901061)Cannot represent all propositional literals internally
% 11.46/2.48 % (2901061)Refutation not found, incomplete strategy
% 11.46/2.48 % (2901061)------------------------------
% 11.46/2.48 % (2901061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901061)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901061)Termination reason: Refutation not found, incomplete strategy
% 11.46/2.48 % (2901061)Time elapsed: 0.005 s
% 11.46/2.48 % (2901061)Peak memory usage: 10 MB
% 11.46/2.48 % (2901061)Instructions burned: 9 (million)
% 11.46/2.48 % (2901061)------------------------------
% 11.46/2.48 % (2901061)------------------------------
% 11.46/2.48 % (2901063)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=496211320:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 11.46/2.48 % TRYING [8]
% 11.46/2.48 % TRYING [4]
% 11.46/2.48 % (2901051)Instruction limit reached!
% 11.46/2.48 % (2901051)------------------------------
% 11.46/2.48 % (2901051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901051)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901051)Termination reason: Instruction limit
% 11.46/2.48 % (2901051)Termination phase: Saturation
% 11.46/2.48 % (2901051)Time elapsed: 0.548 s
% 11.46/2.48 % (2901051)Peak memory usage: 16 MB
% 11.46/2.48 % (2901051)Instructions burned: 1179 (million)
% 11.46/2.48 % (2901065)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=890140128:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 11.46/2.48 % (2901063)Instruction limit reached!
% 11.46/2.48 % (2901063)------------------------------
% 11.46/2.48 % (2901063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901063)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901063)Termination reason: Instruction limit
% 11.46/2.48 % (2901063)Termination phase: Finite model building constraint generation
% 11.46/2.48 % (2901063)Time elapsed: 0.182 s
% 11.46/2.48 % (2901063)Peak memory usage: 59 MB
% 11.46/2.48 % (2901063)Instructions burned: 926 (million)
% 11.46/2.48 % (2901067)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3530286673:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 11.46/2.48 % (2901057)Instruction limit reached!
% 11.46/2.48 % (2901057)------------------------------
% 11.46/2.48 % (2901057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901057)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901057)Termination reason: Instruction limit
% 11.46/2.48 % (2901057)Termination phase: Saturation
% 11.46/2.48 % (2901057)Time elapsed: 0.529 s
% 11.46/2.48 % (2901057)Peak memory usage: 16 MB
% 11.46/2.48 % (2901057)Instructions burned: 879 (million)
% 11.46/2.48 % (2901069)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=919534176:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 11.46/2.48 % (2901069)Cannot represent all propositional literals internally
% 11.46/2.48 % (2901069)Refutation not found, incomplete strategy
% 11.46/2.48 % (2901069)------------------------------
% 11.46/2.48 % (2901069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901069)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901069)Termination reason: Refutation not found, incomplete strategy
% 11.46/2.48 % (2901069)Time elapsed: 0.008 s
% 11.46/2.48 % (2901069)Peak memory usage: 10 MB
% 11.46/2.48 % (2901069)Instructions burned: 17 (million)
% 11.46/2.48 % (2901069)------------------------------
% 11.46/2.48 % (2901069)------------------------------
% 11.46/2.48 % (2901071)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=281947304:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 11.46/2.48 % (2901071)Cannot represent all propositional literals internally
% 11.46/2.48 % (2901071)Refutation not found, incomplete strategy
% 11.46/2.48 % (2901071)------------------------------
% 11.46/2.48 % (2901071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901071)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901071)Termination reason: Refutation not found, incomplete strategy
% 11.46/2.48 % (2901071)Time elapsed: 0.065 s
% 11.46/2.48 % (2901071)Peak memory usage: 11 MB
% 11.46/2.48 % (2901071)Instructions burned: 143 (million)
% 11.46/2.48 % (2901071)------------------------------
% 11.46/2.48 % (2901071)------------------------------
% 11.46/2.48 % (2901073)ott-2_1_sil=16000:newcnf=on:random_seed=1637451004:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 11.46/2.48 % (2901067)Instruction limit reached!
% 11.46/2.48 % (2901067)------------------------------
% 11.46/2.48 % (2901067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901067)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901067)Termination reason: Instruction limit
% 11.46/2.48 % (2901067)Termination phase: Saturation
% 11.46/2.48 % (2901067)Time elapsed: 0.464 s
% 11.46/2.48 % (2901067)Peak memory usage: 27 MB
% 11.46/2.48 % (2901067)Instructions burned: 1475 (million)
% 11.46/2.48 % (2901075)ott+10_1_sil=32000:tgt=ground:random_seed=1858620818:i=5114:av=off_2986 on theBenchmark for (2986ds/5114Mi)
% 11.46/2.48 % (2901073)Instruction limit reached!
% 11.46/2.48 % (2901073)------------------------------
% 11.46/2.48 % (2901073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.48 % (2901073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.48 % (2901073)CaDiCaL version: 2.1.3
% 11.46/2.48 % (2901073)Termination reason: Instruction limit
% 11.46/2.48 % (2901073)Termination phase: Saturation
% 11.46/2.48 % (2901073)Time elapsed: 0.430 s
% 11.46/2.48 % (2901073)Peak memory usage: 16 MB
% 11.46/2.48 % (2901073)Instructions burned: 869 (million)
% 11.46/2.48 % (2901077)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1129475876:i=54282_2984 on theBenchmark for (2984ds/54282Mi)
% 11.46/2.48 % TRYING [1]
% 11.46/2.48 % TRYING [2]
% 11.46/2.48 % TRYING [3]
% 11.46/2.48 % TRYING [4]
% 11.46/2.48 % (2901027) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2901020-2901027"...
% 11.46/2.48 % (2901027)...printing done.
% 11.46/2.48 % SZS status Satisfiable for theBenchmark
% 11.46/2.48 % SZS output start Saturation.
% See solution above
% 11.46/2.49 % SZS output start Definitions and Model Updates.
% 11.46/2.49 for all inputs,
% 11.46/2.49 define sound(X0,X1) := $false
% 11.46/2.49 for all inputs,
% 11.46/2.49 define scream(X0,X1) := $false
% 11.46/2.49 for all inputs,
% 11.46/2.49 define specific(X0,X1) := $true
% 11.46/2.49 for all inputs,
% 11.46/2.49 define cry(X0,X1) := $false
% 11.46/2.49 for all inputs,
% 11.46/2.49 define of(X0,X1,X2) := $true
% 11.46/2.49 for all inputs,
% 11.46/2.49 define actual_world(X0) := $true
% 11.46/2.49 for all inputs,
% 11.46/2.49 define revenge(X0,X1) := $false
% 11.46/2.49 for all inputs,
% 11.46/2.49 define impartial(X0,X1) := $true
% 11.46/2.49 for all inputs,
% 11.46/2.49 define human(X0,X1) := $true
% 11.46/2.49 % SZS output end Definitions and Model Updates.
% 11.46/2.49 % (2901027)------------------------------
% 11.46/2.49 % (2901027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 11.46/2.49 % (2901027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.46/2.49 % (2901027)CaDiCaL version: 2.1.3
% 11.46/2.49 % (2901027)Termination reason: Satisfiable
% 11.46/2.49 % (2901027)Time elapsed: 1.914 s
% 11.46/2.49 % (2901027)Peak memory usage: 30 MB
% 11.46/2.49 % (2901027)Instructions burned: 3542 (million)
% 11.46/2.49 % (2901020)Success in time 2.046 s
% 11.46/2.49 % Vampire exiting
%------------------------------------------------------------------------------