%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP081-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 05:26:35 EDT 2022
% Result : Unsatisfiable 0.20s 0.51s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 40
% Syntax : Number of clauses : 112 ( 44 unt; 18 nHn; 112 RR)
% Number of literals : 514 ( 0 equ; 402 neg)
% Maximal clause size : 19 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 2 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 22 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
actual_world(skc39),
file('NLP081-1.p',unknown),
[] ).
cnf(2,axiom,
actual_world(skc14),
file('NLP081-1.p',unknown),
[] ).
cnf(3,axiom,
( ssskC0
| revenge(skc39,skc45) ),
file('NLP081-1.p',unknown),
[] ).
cnf(4,axiom,
( ssskC0
| event(skc39,skc40) ),
file('NLP081-1.p',unknown),
[] ).
cnf(5,axiom,
( ssskC0
| present(skc39,skc40) ),
file('NLP081-1.p',unknown),
[] ).
cnf(6,axiom,
( ssskC0
| nonreflexive(skc39,skc40) ),
file('NLP081-1.p',unknown),
[] ).
cnf(7,axiom,
( ssskC0
| scream(skc39,skc40) ),
file('NLP081-1.p',unknown),
[] ).
cnf(8,axiom,
( ssskC0
| group(skc39,skc42) ),
file('NLP081-1.p',unknown),
[] ).
cnf(9,axiom,
( ssskC0
| six(skc39,skc42) ),
file('NLP081-1.p',unknown),
[] ).
cnf(10,axiom,
( ssskC0
| cannon(skc39,skc43) ),
file('NLP081-1.p',unknown),
[] ).
cnf(11,axiom,
( ssskC0
| man(skc39,skc44) ),
file('NLP081-1.p',unknown),
[] ).
cnf(12,axiom,
( ssskC0
| male(skc39,skc44) ),
file('NLP081-1.p',unknown),
[] ).
cnf(13,axiom,
( ssskC0
| cry(skc39,skc41) ),
file('NLP081-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ ssskC0
| cry(skc14,skc20) ),
file('NLP081-1.p',unknown),
[] ).
cnf(15,axiom,
( ~ ssskC0
| event(skc14,skc15) ),
file('NLP081-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ ssskC0
| present(skc14,skc15) ),
file('NLP081-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ ssskC0
| nonreflexive(skc14,skc15) ),
file('NLP081-1.p',unknown),
[] ).
cnf(18,axiom,
( ~ ssskC0
| scream(skc14,skc15) ),
file('NLP081-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ ssskC0
| group(skc14,skc17) ),
file('NLP081-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ ssskC0
| six(skc14,skc17) ),
file('NLP081-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ ssskC0
| cannon(skc14,skc18) ),
file('NLP081-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ ssskC0
| man(skc14,skc19) ),
file('NLP081-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ ssskC0
| male(skc14,skc19) ),
file('NLP081-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ ssskC0
| revenge(skc14,skc16) ),
file('NLP081-1.p',unknown),
[] ).
cnf(25,axiom,
( ssskC0
| of(skc39,skc40,skc45) ),
file('NLP081-1.p',unknown),
[] ).
cnf(26,axiom,
( ssskC0
| agent(skc39,skc40,skc44) ),
file('NLP081-1.p',unknown),
[] ).
cnf(27,axiom,
( ssskC0
| of(skc39,skc43,skc44) ),
file('NLP081-1.p',unknown),
[] ).
cnf(28,axiom,
( ssskC0
| patient(skc39,skc40,skc41) ),
file('NLP081-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ ssskC0
| patient(skc14,skc15,skc20) ),
file('NLP081-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ ssskC0
| agent(skc14,skc15,skc19) ),
file('NLP081-1.p',unknown),
[] ).
cnf(31,axiom,
( ~ ssskC0
| of(skc14,skc18,skc19) ),
file('NLP081-1.p',unknown),
[] ).
cnf(32,axiom,
( ~ ssskC0
| of(skc14,skc15,skc16) ),
file('NLP081-1.p',unknown),
[] ).
cnf(33,axiom,
( ssskC0
| ssskP0(skc43,skc44,skc42,skc39) ),
file('NLP081-1.p',unknown),
[] ).
cnf(34,axiom,
( ~ ssskC0
| ssskP0(skc18,skc19,skc17,skc14) ),
file('NLP081-1.p',unknown),
[] ).
cnf(35,axiom,
( ~ member(skc39,u,skc42)
| ssskC0
| shot(skc39,u) ),
file('NLP081-1.p',unknown),
[] ).
cnf(36,axiom,
( ~ ssskC0
| ~ member(skc14,u,skc17)
| shot(skc14,u) ),
file('NLP081-1.p',unknown),
[] ).
cnf(46,axiom,
( ~ actual_world(u)
| ~ cry(u,v)
| ~ revenge(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ of(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ patient(u,x1,v)
| ~ ssskP0(y,x,z,u)
| ssskC0
| member(u,skf12(u,z),z) ),
file('NLP081-1.p',unknown),
[] ).
cnf(47,axiom,
( ~ actual_world(u)
| ~ cry(u,v)
| ~ revenge(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ shot(u,skf12(u,x2))
| ~ of(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ patient(u,x1,v)
| ~ ssskP0(y,x,z,u)
| ssskC0 ),
file('NLP081-1.p',unknown),
[] ).
cnf(48,axiom,
( ~ actual_world(u)
| ~ ssskC0
| ~ revenge(u,v)
| ~ cry(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ patient(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ of(u,x1,v)
| ~ ssskP0(y,x,z,u)
| member(u,skf6(u,z),z) ),
file('NLP081-1.p',unknown),
[] ).
cnf(49,axiom,
( ~ actual_world(u)
| ~ ssskC0
| ~ revenge(u,v)
| ~ cry(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ shot(u,skf6(u,x2))
| ~ patient(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ of(u,x1,v)
| ~ ssskP0(y,x,z,u) ),
file('NLP081-1.p',unknown),
[] ).
cnf(52,plain,
ssskC0,
inference(spt,[spt(split,[position(s1)])],[13]),
[iquote('1:Spt:13.0')] ).
cnf(53,plain,
revenge(skc14,skc16),
inference(mrr,[status(thm)],[24,52]),
[iquote('1:MRR:24.0,52.0')] ).
cnf(54,plain,
male(skc14,skc19),
inference(mrr,[status(thm)],[23,52]),
[iquote('1:MRR:23.0,52.0')] ).
cnf(55,plain,
man(skc14,skc19),
inference(mrr,[status(thm)],[22,52]),
[iquote('1:MRR:22.0,52.0')] ).
cnf(56,plain,
cannon(skc14,skc18),
inference(mrr,[status(thm)],[21,52]),
[iquote('1:MRR:21.0,52.0')] ).
cnf(57,plain,
six(skc14,skc17),
inference(mrr,[status(thm)],[20,52]),
[iquote('1:MRR:20.0,52.0')] ).
cnf(58,plain,
group(skc14,skc17),
inference(mrr,[status(thm)],[19,52]),
[iquote('1:MRR:19.0,52.0')] ).
cnf(59,plain,
scream(skc14,skc15),
inference(mrr,[status(thm)],[18,52]),
[iquote('1:MRR:18.0,52.0')] ).
cnf(60,plain,
nonreflexive(skc14,skc15),
inference(mrr,[status(thm)],[17,52]),
[iquote('1:MRR:17.0,52.0')] ).
cnf(61,plain,
present(skc14,skc15),
inference(mrr,[status(thm)],[16,52]),
[iquote('1:MRR:16.0,52.0')] ).
cnf(62,plain,
event(skc14,skc15),
inference(mrr,[status(thm)],[15,52]),
[iquote('1:MRR:15.0,52.0')] ).
cnf(63,plain,
cry(skc14,skc20),
inference(mrr,[status(thm)],[14,52]),
[iquote('1:MRR:14.0,52.0')] ).
cnf(64,plain,
of(skc14,skc15,skc16),
inference(mrr,[status(thm)],[32,52]),
[iquote('1:MRR:32.0,52.0')] ).
cnf(65,plain,
of(skc14,skc18,skc19),
inference(mrr,[status(thm)],[31,52]),
[iquote('1:MRR:31.0,52.0')] ).
cnf(66,plain,
agent(skc14,skc15,skc19),
inference(mrr,[status(thm)],[30,52]),
[iquote('1:MRR:30.0,52.0')] ).
cnf(67,plain,
patient(skc14,skc15,skc20),
inference(mrr,[status(thm)],[29,52]),
[iquote('1:MRR:29.0,52.0')] ).
cnf(68,plain,
ssskP0(skc18,skc19,skc17,skc14),
inference(mrr,[status(thm)],[34,52]),
[iquote('1:MRR:34.0,52.0')] ).
cnf(69,plain,
( ~ member(skc14,u,skc17)
| shot(skc14,u) ),
inference(mrr,[status(thm)],[36,52]),
[iquote('1:MRR:36.0,52.0')] ).
cnf(70,plain,
( ~ actual_world(u)
| ~ revenge(u,v)
| ~ cry(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ shot(u,skf6(u,x2))
| ~ patient(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ of(u,x1,v)
| ~ ssskP0(y,x,z,u) ),
inference(mrr,[status(thm)],[49,52]),
[iquote('1:MRR:49.1,52.0')] ).
cnf(71,plain,
( ~ actual_world(u)
| ~ revenge(u,v)
| ~ cry(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ patient(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ of(u,x1,v)
| ~ ssskP0(y,x,z,u)
| member(u,skf6(u,z),z) ),
inference(mrr,[status(thm)],[48,52]),
[iquote('1:MRR:48.1,52.0')] ).
cnf(203,plain,
( ~ actual_world(skc14)
| ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ male(skc14,skc19)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,w)
| ~ nonreflexive(skc14,w)
| ~ present(skc14,w)
| ~ event(skc14,w)
| ~ patient(skc14,w,v)
| ~ of(skc14,skc18,skc19)
| ~ agent(skc14,w,skc19)
| ~ of(skc14,w,u)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(res,[status(thm),theory(equality)],[68,71]),
[iquote('1:Res:68.0,71.16')] ).
cnf(211,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ male(skc14,skc19)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,w)
| ~ nonreflexive(skc14,w)
| ~ present(skc14,w)
| ~ event(skc14,w)
| ~ patient(skc14,w,v)
| ~ of(skc14,skc18,skc19)
| ~ agent(skc14,w,skc19)
| ~ of(skc14,w,u)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(ssi,[status(thm)],[203,2]),
[iquote('1:SSi:203.0,2.0')] ).
cnf(212,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ scream(skc14,w)
| ~ nonreflexive(skc14,w)
| ~ present(skc14,w)
| ~ event(skc14,w)
| ~ patient(skc14,w,v)
| ~ agent(skc14,w,skc19)
| ~ of(skc14,w,u)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(mrr,[status(thm)],[211,54,55,56,57,58,65]),
[iquote('1:MRR:211.2,211.3,211.4,211.5,211.6,211.12,54.0,55.0,56.0,57.0,58.0,65.0')] ).
cnf(238,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,skc20)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,u)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(res,[status(thm),theory(equality)],[67,212]),
[iquote('1:Res:67.0,212.6')] ).
cnf(240,plain,
( ~ revenge(skc14,u)
| ~ of(skc14,skc15,u)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(mrr,[status(thm)],[238,63,59,60,61,62,66]),
[iquote('1:MRR:238.1,238.2,238.3,238.4,238.5,238.6,63.0,59.0,60.0,61.0,62.0,66.0')] ).
cnf(242,plain,
( ~ revenge(skc14,skc16)
| member(skc14,skf6(skc14,skc17),skc17) ),
inference(res,[status(thm),theory(equality)],[64,240]),
[iquote('1:Res:64.0,240.1')] ).
cnf(243,plain,
member(skc14,skf6(skc14,skc17),skc17),
inference(mrr,[status(thm)],[242,53]),
[iquote('1:MRR:242.0,53.0')] ).
cnf(244,plain,
shot(skc14,skf6(skc14,skc17)),
inference(res,[status(thm),theory(equality)],[243,69]),
[iquote('1:Res:243.0,69.0')] ).
cnf(252,plain,
( ~ actual_world(skc14)
| ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ male(skc14,w)
| ~ man(skc14,w)
| ~ cannon(skc14,x)
| ~ six(skc14,y)
| ~ group(skc14,y)
| ~ scream(skc14,z)
| ~ nonreflexive(skc14,z)
| ~ present(skc14,z)
| ~ event(skc14,z)
| ~ patient(skc14,z,v)
| ~ of(skc14,x,w)
| ~ agent(skc14,z,w)
| ~ of(skc14,z,u)
| ~ ssskP0(x,w,y,skc14) ),
inference(res,[status(thm),theory(equality)],[244,70]),
[iquote('1:Res:244.0,70.12')] ).
cnf(253,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ male(skc14,w)
| ~ man(skc14,w)
| ~ cannon(skc14,x)
| ~ six(skc14,y)
| ~ group(skc14,y)
| ~ scream(skc14,z)
| ~ nonreflexive(skc14,z)
| ~ present(skc14,z)
| ~ event(skc14,z)
| ~ patient(skc14,z,v)
| ~ of(skc14,x,w)
| ~ agent(skc14,z,w)
| ~ of(skc14,z,u)
| ~ ssskP0(x,w,y,skc14) ),
inference(ssi,[status(thm)],[252,2]),
[iquote('1:SSi:252.0,2.0')] ).
cnf(322,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ male(skc14,skc19)
| ~ man(skc14,skc19)
| ~ cannon(skc14,skc18)
| ~ six(skc14,skc17)
| ~ group(skc14,skc17)
| ~ scream(skc14,w)
| ~ nonreflexive(skc14,w)
| ~ present(skc14,w)
| ~ event(skc14,w)
| ~ patient(skc14,w,v)
| ~ of(skc14,skc18,skc19)
| ~ agent(skc14,w,skc19)
| ~ of(skc14,w,u) ),
inference(res,[status(thm),theory(equality)],[68,253]),
[iquote('1:Res:68.0,253.15')] ).
cnf(323,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,v)
| ~ scream(skc14,w)
| ~ nonreflexive(skc14,w)
| ~ present(skc14,w)
| ~ event(skc14,w)
| ~ patient(skc14,w,v)
| ~ agent(skc14,w,skc19)
| ~ of(skc14,w,u) ),
inference(mrr,[status(thm)],[322,54,55,56,57,58,65]),
[iquote('1:MRR:322.2,322.3,322.4,322.5,322.6,322.12,54.0,55.0,56.0,57.0,58.0,65.0')] ).
cnf(324,plain,
( ~ revenge(skc14,u)
| ~ cry(skc14,skc20)
| ~ scream(skc14,skc15)
| ~ nonreflexive(skc14,skc15)
| ~ present(skc14,skc15)
| ~ event(skc14,skc15)
| ~ agent(skc14,skc15,skc19)
| ~ of(skc14,skc15,u) ),
inference(res,[status(thm),theory(equality)],[67,323]),
[iquote('1:Res:67.0,323.6')] ).
cnf(326,plain,
( ~ revenge(skc14,u)
| ~ of(skc14,skc15,u) ),
inference(mrr,[status(thm)],[324,63,59,60,61,62,66]),
[iquote('1:MRR:324.1,324.2,324.3,324.4,324.5,324.6,63.0,59.0,60.0,61.0,62.0,66.0')] ).
cnf(328,plain,
~ revenge(skc14,skc16),
inference(res,[status(thm),theory(equality)],[64,326]),
[iquote('1:Res:64.0,326.1')] ).
cnf(329,plain,
$false,
inference(mrr,[status(thm)],[328,53]),
[iquote('1:MRR:328.0,53.0')] ).
cnf(330,plain,
~ ssskC0,
inference(spt,[spt(split,[position(sa)])],[329,52]),
[iquote('1:Spt:329.0,13.0,52.0')] ).
cnf(331,plain,
cry(skc39,skc41),
inference(spt,[spt(split,[position(s2)])],[13]),
[iquote('1:Spt:329.0,13.1')] ).
cnf(332,plain,
male(skc39,skc44),
inference(mrr,[status(thm)],[12,330]),
[iquote('1:MRR:12.0,330.0')] ).
cnf(333,plain,
man(skc39,skc44),
inference(mrr,[status(thm)],[11,330]),
[iquote('1:MRR:11.0,330.0')] ).
cnf(334,plain,
cannon(skc39,skc43),
inference(mrr,[status(thm)],[10,330]),
[iquote('1:MRR:10.0,330.0')] ).
cnf(335,plain,
six(skc39,skc42),
inference(mrr,[status(thm)],[9,330]),
[iquote('1:MRR:9.0,330.0')] ).
cnf(336,plain,
group(skc39,skc42),
inference(mrr,[status(thm)],[8,330]),
[iquote('1:MRR:8.0,330.0')] ).
cnf(337,plain,
scream(skc39,skc40),
inference(mrr,[status(thm)],[7,330]),
[iquote('1:MRR:7.0,330.0')] ).
cnf(338,plain,
nonreflexive(skc39,skc40),
inference(mrr,[status(thm)],[6,330]),
[iquote('1:MRR:6.0,330.0')] ).
cnf(339,plain,
present(skc39,skc40),
inference(mrr,[status(thm)],[5,330]),
[iquote('1:MRR:5.0,330.0')] ).
cnf(340,plain,
event(skc39,skc40),
inference(mrr,[status(thm)],[4,330]),
[iquote('1:MRR:4.0,330.0')] ).
cnf(341,plain,
revenge(skc39,skc45),
inference(mrr,[status(thm)],[3,330]),
[iquote('1:MRR:3.0,330.0')] ).
cnf(342,plain,
patient(skc39,skc40,skc41),
inference(mrr,[status(thm)],[28,330]),
[iquote('1:MRR:28.0,330.0')] ).
cnf(343,plain,
of(skc39,skc43,skc44),
inference(mrr,[status(thm)],[27,330]),
[iquote('1:MRR:27.0,330.0')] ).
cnf(344,plain,
agent(skc39,skc40,skc44),
inference(mrr,[status(thm)],[26,330]),
[iquote('1:MRR:26.0,330.0')] ).
cnf(345,plain,
of(skc39,skc40,skc45),
inference(mrr,[status(thm)],[25,330]),
[iquote('1:MRR:25.0,330.0')] ).
cnf(346,plain,
ssskP0(skc43,skc44,skc42,skc39),
inference(mrr,[status(thm)],[33,330]),
[iquote('1:MRR:33.0,330.0')] ).
cnf(347,plain,
( ~ member(skc39,u,skc42)
| shot(skc39,u) ),
inference(mrr,[status(thm)],[35,330]),
[iquote('1:MRR:35.1,330.0')] ).
cnf(348,plain,
( ~ actual_world(u)
| ~ cry(u,v)
| ~ revenge(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ of(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ patient(u,x1,v)
| ~ ssskP0(y,x,z,u)
| member(u,skf12(u,z),z) ),
inference(mrr,[status(thm)],[46,330]),
[iquote('1:MRR:46.17,330.0')] ).
cnf(349,plain,
( ~ actual_world(u)
| ~ cry(u,v)
| ~ revenge(u,w)
| ~ male(u,x)
| ~ man(u,x)
| ~ cannon(u,y)
| ~ six(u,z)
| ~ group(u,z)
| ~ scream(u,x1)
| ~ nonreflexive(u,x1)
| ~ present(u,x1)
| ~ event(u,x1)
| ~ shot(u,skf12(u,x2))
| ~ of(u,x1,w)
| ~ of(u,y,x)
| ~ agent(u,x1,x)
| ~ patient(u,x1,v)
| ~ ssskP0(y,x,z,u) ),
inference(mrr,[status(thm)],[47,330]),
[iquote('1:MRR:47.18,330.0')] ).
cnf(458,plain,
( ~ actual_world(skc39)
| ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ male(skc39,skc44)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,w)
| ~ nonreflexive(skc39,w)
| ~ present(skc39,w)
| ~ event(skc39,w)
| ~ of(skc39,w,v)
| ~ of(skc39,skc43,skc44)
| ~ agent(skc39,w,skc44)
| ~ patient(skc39,w,u)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(res,[status(thm),theory(equality)],[346,348]),
[iquote('1:Res:346.0,348.16')] ).
cnf(466,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ male(skc39,skc44)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,w)
| ~ nonreflexive(skc39,w)
| ~ present(skc39,w)
| ~ event(skc39,w)
| ~ of(skc39,w,v)
| ~ of(skc39,skc43,skc44)
| ~ agent(skc39,w,skc44)
| ~ patient(skc39,w,u)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(ssi,[status(thm)],[458,1]),
[iquote('1:SSi:458.0,1.0')] ).
cnf(467,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ scream(skc39,w)
| ~ nonreflexive(skc39,w)
| ~ present(skc39,w)
| ~ event(skc39,w)
| ~ of(skc39,w,v)
| ~ agent(skc39,w,skc44)
| ~ patient(skc39,w,u)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(mrr,[status(thm)],[466,332,333,334,335,336,343]),
[iquote('1:MRR:466.2,466.3,466.4,466.5,466.6,466.12,332.0,333.0,334.0,335.0,336.0,343.0')] ).
cnf(485,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,skc45)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ agent(skc39,skc40,skc44)
| ~ patient(skc39,skc40,u)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(res,[status(thm),theory(equality)],[345,467]),
[iquote('1:Res:345.0,467.6')] ).
cnf(486,plain,
( ~ cry(skc39,u)
| ~ patient(skc39,skc40,u)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(mrr,[status(thm)],[485,341,337,338,339,340,344]),
[iquote('1:MRR:485.1,485.2,485.3,485.4,485.5,485.6,341.0,337.0,338.0,339.0,340.0,344.0')] ).
cnf(490,plain,
( ~ cry(skc39,skc41)
| member(skc39,skf12(skc39,skc42),skc42) ),
inference(res,[status(thm),theory(equality)],[342,486]),
[iquote('1:Res:342.0,486.1')] ).
cnf(491,plain,
member(skc39,skf12(skc39,skc42),skc42),
inference(mrr,[status(thm)],[490,331]),
[iquote('1:MRR:490.0,331.0')] ).
cnf(499,plain,
shot(skc39,skf12(skc39,skc42)),
inference(res,[status(thm),theory(equality)],[491,347]),
[iquote('1:Res:491.0,347.0')] ).
cnf(500,plain,
( ~ actual_world(skc39)
| ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ male(skc39,w)
| ~ man(skc39,w)
| ~ cannon(skc39,x)
| ~ six(skc39,y)
| ~ group(skc39,y)
| ~ scream(skc39,z)
| ~ nonreflexive(skc39,z)
| ~ present(skc39,z)
| ~ event(skc39,z)
| ~ of(skc39,z,v)
| ~ of(skc39,x,w)
| ~ agent(skc39,z,w)
| ~ patient(skc39,z,u)
| ~ ssskP0(x,w,y,skc39) ),
inference(res,[status(thm),theory(equality)],[499,349]),
[iquote('1:Res:499.0,349.12')] ).
cnf(501,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ male(skc39,w)
| ~ man(skc39,w)
| ~ cannon(skc39,x)
| ~ six(skc39,y)
| ~ group(skc39,y)
| ~ scream(skc39,z)
| ~ nonreflexive(skc39,z)
| ~ present(skc39,z)
| ~ event(skc39,z)
| ~ of(skc39,z,v)
| ~ of(skc39,x,w)
| ~ agent(skc39,z,w)
| ~ patient(skc39,z,u)
| ~ ssskP0(x,w,y,skc39) ),
inference(ssi,[status(thm)],[500,1]),
[iquote('1:SSi:500.0,1.0')] ).
cnf(520,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ male(skc39,skc44)
| ~ man(skc39,skc44)
| ~ cannon(skc39,skc43)
| ~ six(skc39,skc42)
| ~ group(skc39,skc42)
| ~ scream(skc39,w)
| ~ nonreflexive(skc39,w)
| ~ present(skc39,w)
| ~ event(skc39,w)
| ~ of(skc39,w,v)
| ~ of(skc39,skc43,skc44)
| ~ agent(skc39,w,skc44)
| ~ patient(skc39,w,u) ),
inference(res,[status(thm),theory(equality)],[346,501]),
[iquote('1:Res:346.0,501.15')] ).
cnf(521,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,v)
| ~ scream(skc39,w)
| ~ nonreflexive(skc39,w)
| ~ present(skc39,w)
| ~ event(skc39,w)
| ~ of(skc39,w,v)
| ~ agent(skc39,w,skc44)
| ~ patient(skc39,w,u) ),
inference(mrr,[status(thm)],[520,332,333,334,335,336,343]),
[iquote('1:MRR:520.2,520.3,520.4,520.5,520.6,520.12,332.0,333.0,334.0,335.0,336.0,343.0')] ).
cnf(523,plain,
( ~ cry(skc39,u)
| ~ revenge(skc39,skc45)
| ~ scream(skc39,skc40)
| ~ nonreflexive(skc39,skc40)
| ~ present(skc39,skc40)
| ~ event(skc39,skc40)
| ~ agent(skc39,skc40,skc44)
| ~ patient(skc39,skc40,u) ),
inference(res,[status(thm),theory(equality)],[345,521]),
[iquote('1:Res:345.0,521.6')] ).
cnf(524,plain,
( ~ cry(skc39,u)
| ~ patient(skc39,skc40,u) ),
inference(mrr,[status(thm)],[523,341,337,338,339,340,344]),
[iquote('1:MRR:523.1,523.2,523.3,523.4,523.5,523.6,341.0,337.0,338.0,339.0,340.0,344.0')] ).
cnf(527,plain,
~ cry(skc39,skc41),
inference(res,[status(thm),theory(equality)],[342,524]),
[iquote('1:Res:342.0,524.1')] ).
cnf(528,plain,
$false,
inference(mrr,[status(thm)],[527,331]),
[iquote('1:MRR:527.0,331.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NLP081-1 : TPTP v8.1.0. Released v2.4.0.
% 0.04/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n008.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Fri Jul 1 08:50:53 EDT 2022
% 0.14/0.34 % CPUTime :
% 0.20/0.51
% 0.20/0.51 SPASS V 3.9
% 0.20/0.51 SPASS beiseite: Proof found.
% 0.20/0.51 % SZS status Theorem
% 0.20/0.51 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.51 SPASS derived 357 clauses, backtracked 76 clauses, performed 13 splits and kept 282 clauses.
% 0.20/0.51 SPASS allocated 76215 KBytes.
% 0.20/0.51 SPASS spent 0:00:00.15 on the problem.
% 0.20/0.51 0:00:00.04 for the input.
% 0.20/0.51 0:00:00.00 for the FLOTTER CNF translation.
% 0.20/0.51 0:00:00.01 for inferences.
% 0.20/0.51 0:00:00.00 for the backtracking.
% 0.20/0.51 0:00:00.06 for the reduction.
% 0.20/0.51
% 0.20/0.51
% 0.20/0.51 Here is a proof with depth 8, length 112 :
% 0.20/0.51 % SZS output start Refutation
% See solution above
% 0.20/0.51 Formulae used in the proof : clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause9 clause10 clause11 clause12 clause13 clause14 clause15 clause16 clause17 clause18 clause19 clause20 clause21 clause22 clause23 clause24 clause25 clause26 clause27 clause28 clause29 clause30 clause31 clause32 clause33 clause34 clause35 clause36 clause46 clause47 clause48 clause49
% 0.20/0.51
%------------------------------------------------------------------------------