%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NLP064-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:22 EDT 2022
% Result : Satisfiable 0.18s 0.53s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 1022)
% Comments :
%------------------------------------------------------------------------------
cnf(1159,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| ssskP1(y,z,u)
| member(u,skf16(z,u,x1),z)
| from_loc(u,skf12(u,v,skf26(w,u,x),x2),skf13(u,x2,skf26(w,u,x),v)) ),
inference(res,[status(thm),theory(equality)],[15,1026]),
[iquote('0:Res:15.1,1026.1')] ).
cnf(1155,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| ssskP1(y,z,u)
| member(u,skf16(z,u,x1),z)
| patient(u,skf12(u,v,skf26(w,u,x),x2),skf26(w,u,x)) ),
inference(res,[status(thm),theory(equality)],[15,1029]),
[iquote('0:Res:15.1,1029.1')] ).
cnf(1026,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| ssskP1(y,z,u)
| member(u,skf16(z,u,x1),z)
| from_loc(u,skf12(u,v,w,x2),skf13(u,x2,w,v)) ),
inference(res,[status(thm),theory(equality)],[1023,34]),
[iquote('0:Res:1023.0,34.1')] ).
cnf(1045,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| member(u,skf11(u,v),v) ),
inference(res,[status(thm),theory(equality)],[1023,50]),
[iquote('1:Res:1023.1,50.4')] ).
cnf(1029,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| ssskP1(y,z,u)
| member(u,skf16(z,u,x1),z)
| patient(u,skf12(u,v,w,x2),w) ),
inference(res,[status(thm),theory(equality)],[1023,31]),
[iquote('0:Res:1023.0,31.1')] ).
cnf(1035,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| agent(u,skf20(u,x1,x2),skf21(u,x2,x1)) ),
inference(res,[status(thm),theory(equality)],[1023,25]),
[iquote('0:Res:1023.1,25.0')] ).
cnf(1036,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| from_loc(u,skf20(u,v,x1),skf22(u,x1,v)) ),
inference(res,[status(thm),theory(equality)],[1023,24]),
[iquote('0:Res:1023.1,24.0')] ).
cnf(1037,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| of(u,skf22(u,x1,x2),x1) ),
inference(res,[status(thm),theory(equality)],[1023,22]),
[iquote('0:Res:1023.1,22.0')] ).
cnf(1038,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| patient(u,skf20(u,v,x1),v) ),
inference(res,[status(thm),theory(equality)],[1023,23]),
[iquote('0:Res:1023.1,23.0')] ).
cnf(1039,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| man(u,skf21(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,21]),
[iquote('0:Res:1023.1,21.0')] ).
cnf(1040,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| cannon(u,skf22(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,16]),
[iquote('0:Res:1023.1,16.0')] ).
cnf(1041,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| event(u,skf20(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,17]),
[iquote('0:Res:1023.1,17.0')] ).
cnf(1042,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| present(u,skf20(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,18]),
[iquote('0:Res:1023.1,18.0')] ).
cnf(1043,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| nonreflexive(u,skf20(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,19]),
[iquote('0:Res:1023.1,19.0')] ).
cnf(1044,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| fire(u,skf20(u,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[1023,20]),
[iquote('0:Res:1023.1,20.0')] ).
cnf(1023,plain,
( ssskP0(u,v,w)
| ssskP1(x,y,w)
| member(w,skf16(y,w,z),y) ),
inference(mrr,[status(thm)],[1022,13]),
[iquote('0:MRR:1022.0,13.0')] ).
cnf(957,plain,
( ~ man(skc6,u)
| ssskP1(v,w,skc6) ),
inference(obv,[status(thm),theory(equality)],[955]),
[iquote('11:Obv:955.1')] ).
cnf(487,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| of(u,skf13(u,x1,x2,x3),x1) ),
inference(mrr,[status(thm)],[455,478]),
[iquote('1:MRR:455.7,478.0')] ).
cnf(324,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| nonreflexive(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[308,320]),
[iquote('1:MRR:308.7,320.0')] ).
cnf(281,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| fire(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[266,277]),
[iquote('1:MRR:266.7,277.0')] ).
cnf(246,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| cannon(u,skf13(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[231,242]),
[iquote('1:MRR:231.7,242.0')] ).
cnf(201,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| event(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[188,197]),
[iquote('1:MRR:188.7,197.0')] ).
cnf(162,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ssskP0(x,y,u)
| member(u,skf16(v,u,z),v)
| present(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[150,158]),
[iquote('1:MRR:150.7,158.0')] ).
cnf(512,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| from_loc(u,skf12(u,v,skf26(w,u,x),z),skf13(u,z,skf26(w,u,x),v)) ),
inference(res,[status(thm),theory(equality)],[15,119]),
[iquote('0:Res:15.1,119.1')] ).
cnf(575,plain,
( ~ man(skc6,u)
| ~ member(skc6,v,w)
| from_loc(skc6,skf12(skc6,u,v,x),skf13(skc6,x,v,u)) ),
inference(res,[status(thm),theory(equality)],[574,34]),
[iquote('11:Res:574.0,34.1')] ).
cnf(578,plain,
( ~ man(skc6,u)
| ~ member(skc6,v,w)
| patient(skc6,skf12(skc6,u,v,x),v) ),
inference(res,[status(thm),theory(equality)],[574,31]),
[iquote('11:Res:574.0,31.1')] ).
cnf(574,plain,
ssskP0(u,v,skc6),
inference(spt,[],[543]),
[iquote('11:Spt:543.0')] ).
cnf(503,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| from_loc(u,skf12(u,v,skf26(w,u,x),x1),skf13(u,x1,skf26(w,u,x),v)) ),
inference(res,[status(thm),theory(equality)],[15,118]),
[iquote('0:Res:15.1,118.1')] ).
cnf(374,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| patient(u,skf12(u,v,skf26(w,u,x),z),skf26(w,u,x)) ),
inference(res,[status(thm),theory(equality)],[15,90]),
[iquote('0:Res:15.1,90.1')] ).
cnf(325,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| patient(u,skf12(u,v,skf26(w,u,x),x1),skf26(w,u,x)) ),
inference(res,[status(thm),theory(equality)],[15,89]),
[iquote('0:Res:15.1,89.1')] ).
cnf(119,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| from_loc(u,skf12(u,v,w,z),skf13(u,z,w,v)) ),
inference(res,[status(thm),theory(equality)],[14,34]),
[iquote('0:Res:14.0,34.1')] ).
cnf(118,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| from_loc(u,skf12(u,v,w,x1),skf13(u,x1,w,v)) ),
inference(res,[status(thm),theory(equality)],[13,34]),
[iquote('0:Res:13.1,34.1')] ).
cnf(478,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| of(u,skf13(u,x1,x2,x3),x1) ),
inference(mrr,[status(thm)],[449,101]),
[iquote('0:MRR:449.4,101.0')] ).
cnf(427,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| of(u,skf13(u,z,x1,x2),z) ),
inference(res,[status(thm),theory(equality)],[15,101]),
[iquote('0:Res:15.1,101.1')] ).
cnf(420,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| agent(u,skf12(u,v,z,x1),v) ),
inference(res,[status(thm),theory(equality)],[15,94]),
[iquote('0:Res:15.1,94.1')] ).
cnf(101,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| of(u,skf13(u,z,x1,x2),z) ),
inference(res,[status(thm),theory(equality)],[14,32]),
[iquote('0:Res:14.0,32.1')] ).
cnf(94,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| agent(u,skf12(u,v,z,x1),v) ),
inference(res,[status(thm),theory(equality)],[14,33]),
[iquote('0:Res:14.0,33.1')] ).
cnf(320,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| nonreflexive(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[302,83]),
[iquote('0:MRR:302.4,83.0')] ).
cnf(277,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| fire(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[260,73]),
[iquote('0:MRR:260.4,73.0')] ).
cnf(242,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| cannon(u,skf13(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[225,69]),
[iquote('0:MRR:225.4,69.0')] ).
cnf(90,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| patient(u,skf12(u,v,w,z),w) ),
inference(res,[status(thm),theory(equality)],[14,31]),
[iquote('0:Res:14.0,31.1')] ).
cnf(197,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| event(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[182,61]),
[iquote('0:MRR:182.4,61.0')] ).
cnf(158,plain,
( ~ member(u,v,w)
| ssskP0(x,y,u)
| member(u,skf16(w,u,z),w)
| present(u,skf12(u,x1,x2,x3)) ),
inference(mrr,[status(thm)],[144,55]),
[iquote('0:MRR:144.4,55.0')] ).
cnf(339,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| of(u,skf13(u,x1,x2,x3),x1) ),
inference(res,[status(thm),theory(equality)],[15,100]),
[iquote('0:Res:15.1,100.1')] ).
cnf(332,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| agent(u,skf12(u,v,x1,x2),v) ),
inference(res,[status(thm),theory(equality)],[15,93]),
[iquote('0:Res:15.1,93.1')] ).
cnf(100,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| of(u,skf13(u,x1,x2,x3),x1) ),
inference(res,[status(thm),theory(equality)],[13,32]),
[iquote('0:Res:13.1,32.1')] ).
cnf(93,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| agent(u,skf12(u,v,x1,x2),v) ),
inference(res,[status(thm),theory(equality)],[13,33]),
[iquote('0:Res:13.1,33.1')] ).
cnf(89,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| patient(u,skf12(u,v,w,x1),w) ),
inference(res,[status(thm),theory(equality)],[13,31]),
[iquote('0:Res:13.1,31.1')] ).
cnf(282,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| nonreflexive(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[15,83]),
[iquote('0:Res:15.1,83.1')] ).
cnf(83,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| nonreflexive(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[14,26]),
[iquote('0:Res:14.0,26.1')] ).
cnf(206,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| fire(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[15,73]),
[iquote('0:Res:15.1,73.1')] ).
cnf(202,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| cannon(u,skf13(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[15,69]),
[iquote('0:Res:15.1,69.1')] ).
cnf(73,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| fire(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[14,27]),
[iquote('0:Res:14.0,27.1')] ).
cnf(69,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| cannon(u,skf13(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[14,28]),
[iquote('0:Res:14.0,28.1')] ).
cnf(165,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| event(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[15,61]),
[iquote('0:Res:15.1,61.1')] ).
cnf(61,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| event(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[14,29]),
[iquote('0:Res:14.0,29.1')] ).
cnf(40,axiom,
( ~ cannon(u,v)
| ~ event(u,w)
| ~ present(u,w)
| ~ nonreflexive(u,w)
| ~ fire(u,w)
| ~ man(u,x)
| ~ from_loc(u,w,v)
| ~ of(u,v,y)
| ~ agent(u,w,x)
| ~ patient(u,w,skf26(y,u,z))
| ssskP1(y,x1,u) ),
file('NLP064-1.p',unknown),
[] ).
cnf(128,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| member(u,skf16(x,u,y),x)
| present(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[15,55]),
[iquote('0:Res:15.1,55.1')] ).
cnf(55,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| member(u,skf16(x,u,y),x)
| present(u,skf12(u,z,x1,x2)) ),
inference(res,[status(thm),theory(equality)],[14,30]),
[iquote('0:Res:14.0,30.1')] ).
cnf(127,plain,
of(skc6,skf13(skc6,u,v,w),u),
inference(spt,[],[102]),
[iquote('9:Spt:102.3')] ).
cnf(39,axiom,
( ~ cannon(u,v)
| ~ fire(u,w)
| ~ nonreflexive(u,w)
| ~ present(u,w)
| ~ event(u,w)
| ~ of(u,v,x)
| ~ from_loc(u,w,v)
| ~ patient(u,w,skf16(y,u,x))
| ~ agent(u,w,skf19(u,y,x))
| ssskP0(x,y,u) ),
file('NLP064-1.p',unknown),
[] ).
cnf(122,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| nonreflexive(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[15,82]),
[iquote('0:Res:15.1,82.1')] ).
cnf(82,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| nonreflexive(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[13,26]),
[iquote('0:Res:13.1,26.1')] ).
cnf(115,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| fire(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[15,72]),
[iquote('0:Res:15.1,72.1')] ).
cnf(34,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| from_loc(u,skf12(u,v,y,w),skf13(u,w,y,v)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(72,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| fire(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[13,27]),
[iquote('0:Res:13.1,27.1')] ).
cnf(112,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| cannon(u,skf13(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[15,68]),
[iquote('0:Res:15.1,68.1')] ).
cnf(68,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| cannon(u,skf13(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[13,28]),
[iquote('0:Res:13.1,28.1')] ).
cnf(109,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| event(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[15,60]),
[iquote('0:Res:15.1,60.1')] ).
cnf(50,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ~ ssskP1(w,v,u)
| member(u,skf11(u,v),v) ),
inference(mrr,[status(thm)],[37,43]),
[iquote('1:MRR:37.1,43.0')] ).
cnf(60,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| event(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[13,29]),
[iquote('0:Res:13.1,29.1')] ).
cnf(106,plain,
( ~ man(u,v)
| ssskP1(w,x,u)
| man(u,skf19(u,y,z))
| present(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[15,54]),
[iquote('0:Res:15.1,54.1')] ).
cnf(54,plain,
( ~ man(u,v)
| ~ member(u,w,x)
| man(u,skf19(u,y,z))
| present(u,skf12(u,x1,x2,x3)) ),
inference(res,[status(thm),theory(equality)],[13,30]),
[iquote('0:Res:13.1,30.1')] ).
cnf(49,plain,
( ~ actual_world(u)
| ~ six(u,v)
| ~ male(u,w)
| ~ group(u,v)
| ~ shot(u,skf11(u,x))
| ~ ssskP1(w,v,u) ),
inference(mrr,[status(thm)],[38,43]),
[iquote('1:MRR:38.1,43.0')] ).
cnf(32,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| of(u,skf13(u,w,z,x1),w) ),
file('NLP064-1.p',unknown),
[] ).
cnf(98,plain,
( ~ man(skc6,u)
| agent(skc6,skf12(skc6,u,v,w),u) ),
inference(spt,[],[96]),
[iquote('7:Spt:96.0,96.2')] ).
cnf(33,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| agent(u,skf12(u,v,z,x1),v) ),
file('NLP064-1.p',unknown),
[] ).
cnf(31,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| patient(u,skf12(u,v,y,z),y) ),
file('NLP064-1.p',unknown),
[] ).
cnf(87,plain,
nonreflexive(skc6,skf12(skc6,u,v,w)),
inference(spt,[],[85]),
[iquote('6:Spt:85.2')] ).
cnf(26,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| nonreflexive(u,skf12(u,z,x1,x2)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(80,plain,
fire(skc6,skf12(skc6,u,v,w)),
inference(spt,[],[78]),
[iquote('5:Spt:78.2')] ).
cnf(77,plain,
cannon(skc6,skf13(skc6,u,v,w)),
inference(spt,[],[75]),
[iquote('4:Spt:75.2')] ).
cnf(27,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| fire(u,skf12(u,z,x1,x2)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(28,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| cannon(u,skf13(u,z,x1,x2)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(66,plain,
event(skc6,skf12(skc6,u,v,w)),
inference(spt,[],[64]),
[iquote('3:Spt:64.2')] ).
cnf(63,plain,
present(skc6,skf12(skc6,u,v,w)),
inference(spt,[],[57]),
[iquote('2:Spt:57.2')] ).
cnf(29,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| event(u,skf12(u,z,x1,x2)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ man(u,v)
| ~ ssskP0(w,x,u)
| ~ member(u,y,x)
| present(u,skf12(u,z,x1,x2)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(25,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| agent(w,skf20(w,y,z),skf21(w,z,y)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| from_loc(w,skf20(w,x,u),skf22(w,u,x)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| of(w,skf22(w,u,y),u) ),
file('NLP064-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| patient(w,skf20(w,x,y),x) ),
file('NLP064-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| man(w,skf21(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| cannon(w,skf22(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| event(w,skf20(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(18,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| present(w,skf20(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| nonreflexive(w,skf20(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ ssskP1(u,v,w)
| ~ member(w,x,v)
| fire(w,skf20(w,y,z)) ),
file('NLP064-1.p',unknown),
[] ).
cnf(51,plain,
( ssskP1(u,skc7,skc6)
| shot(skc6,skf26(u,skc6,skc7)) ),
inference(res,[status(thm),theory(equality)],[15,48]),
[iquote('1:Res:15.1,48.0')] ).
cnf(14,axiom,
( ssskP0(u,v,w)
| member(w,skf16(v,w,x),v) ),
file('NLP064-1.p',unknown),
[] ).
cnf(15,axiom,
( ssskP1(u,v,w)
| member(w,skf26(u,w,v),v) ),
file('NLP064-1.p',unknown),
[] ).
cnf(13,axiom,
( man(u,skf19(u,v,w))
| ssskP0(x,y,u) ),
file('NLP064-1.p',unknown),
[] ).
cnf(48,plain,
( ~ member(skc6,u,skc7)
| shot(skc6,u) ),
inference(mrr,[status(thm)],[12,43]),
[iquote('1:MRR:12.0,43.0')] ).
cnf(46,plain,
six(skc6,skc7),
inference(mrr,[status(thm)],[6,43]),
[iquote('1:MRR:6.0,43.0')] ).
cnf(45,plain,
group(skc6,skc7),
inference(mrr,[status(thm)],[7,43]),
[iquote('1:MRR:7.0,43.0')] ).
cnf(44,plain,
male(skc6,skc8),
inference(mrr,[status(thm)],[8,43]),
[iquote('1:MRR:8.0,43.0')] ).
cnf(1,axiom,
actual_world(skc60),
file('NLP064-1.p',unknown),
[] ).
cnf(2,axiom,
actual_world(skc6),
file('NLP064-1.p',unknown),
[] ).
cnf(43,plain,
ssskC0,
inference(spt,[],[35]),
[iquote('1:Spt:35.5')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP064-1 : TPTP v8.1.0. Released v2.4.0.
% 0.00/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Fri Jul 1 08:30:47 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.53
% 0.18/0.53 SPASS V 3.9
% 0.18/0.53 SPASS beiseite: Completion found.
% 0.18/0.53 % SZS status CounterSatisfiable
% 0.18/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.53 SPASS derived 865 clauses, backtracked 0 clauses, performed 11 splits and kept 229 clauses.
% 0.18/0.53 SPASS allocated 76809 KBytes.
% 0.18/0.53 SPASS spent 0:00:00.20 on the problem.
% 0.18/0.53 0:00:00.04 for the input.
% 0.18/0.53 0:00:00.00 for the FLOTTER CNF translation.
% 0.18/0.53 0:00:00.04 for inferences.
% 0.18/0.53 0:00:00.00 for the backtracking.
% 0.18/0.53 0:00:00.09 for the reduction.
% 0.18/0.53
% 0.18/0.53
% 0.18/0.53 The saturated set of worked-off clauses is :
% 0.18/0.53 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------