%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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 02:58:41 EDT 2022
% Result : Theorem 0.44s 1.42s
% Output : Proof 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP079+1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Fri Jul 1 09:43:24 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.44/1.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.43 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/1.43
% 0.44/1.43 %-----------------------------------------------------
% 0.44/1.43 fof(co1, conjecture, ~ ~ ((? [_103983] : (actual_world(_103983) & ? [_103998, _104001, _104004, _104007, _104010, _104013, _104016] : (male(_103983, _103998) & male(_103983, _104001) & man(_103983, _104001) & of(_103983, _104004, _104001) & cannon(_103983, _104004) & ! [_104077] : (member(_103983, _104077, _104007) => ? [_104098] : (event(_103983, _104098) & agent(_103983, _104098, _104001) & patient(_103983, _104098, _104077) & present(_103983, _104098) & nonreflexive(_103983, _104098) & fire(_103983, _104098) & from_loc(_103983, _104098, _104004))) & six(_103983, _104007) & group(_103983, _104007) & ! [_104205] : (member(_103983, _104205, _104007) => shot(_103983, _104205)) & revenge(_103983, _104010) & cry(_103983, _104013) & event(_103983, _104016) & agent(_103983, _104016, _103998) & patient(_103983, _104016, _104013) & present(_103983, _104016) & nonreflexive(_103983, _104016) & scream(_103983, _104016) & of(_103983, _104016, _104010))) => ? [_104335] : (actual_world(_104335) & ? [_104350, _104353, _104356, _104359, _104362, _104365, _104368] : (male(_104335, _104350) & male(_104335, _104353) & man(_104335, _104353) & of(_104335, _104356, _104353) & cannon(_104335, _104356) & ! [_104429] : (member(_104335, _104429, _104359) => ? [_104450] : (event(_104335, _104450) & agent(_104335, _104450, _104353) & patient(_104335, _104450, _104429) & present(_104335, _104450) & nonreflexive(_104335, _104450) & fire(_104335, _104450) & from_loc(_104335, _104450, _104356))) & six(_104335, _104359) & group(_104335, _104359) & ! [_104557] : (member(_104335, _104557, _104359) => shot(_104335, _104557)) & cry(_104335, _104362) & revenge(_104335, _104365) & event(_104335, _104368) & agent(_104335, _104368, _104350) & patient(_104335, _104368, _104362) & present(_104335, _104368) & nonreflexive(_104335, _104368) & scream(_104335, _104368) & of(_104335, _104368, _104365)))) & (? [_104335] : (actual_world(_104335) & ? [_104350, _104353, _104356, _104359, _104362, _104365, _104368] : (male(_104335, _104350) & male(_104335, _104353) & man(_104335, _104353) & of(_104335, _104356, _104353) & cannon(_104335, _104356) & ! [_104429] : (member(_104335, _104429, _104359) => ? [_104450] : (event(_104335, _104450) & agent(_104335, _104450, _104353) & patient(_104335, _104450, _104429) & present(_104335, _104450) & nonreflexive(_104335, _104450) & fire(_104335, _104450) & from_loc(_104335, _104450, _104356))) & six(_104335, _104359) & group(_104335, _104359) & ! [_104557] : (member(_104335, _104557, _104359) => shot(_104335, _104557)) & cry(_104335, _104362) & revenge(_104335, _104365) & event(_104335, _104368) & agent(_104335, _104368, _104350) & patient(_104335, _104368, _104362) & present(_104335, _104368) & nonreflexive(_104335, _104368) & scream(_104335, _104368) & of(_104335, _104368, _104365))) => ? [_103983] : (actual_world(_103983) & ? [_103998, _104001, _104004, _104007, _104010, _104013, _104016] : (male(_103983, _103998) & male(_103983, _104001) & man(_103983, _104001) & of(_103983, _104004, _104001) & cannon(_103983, _104004) & ! [_104077] : (member(_103983, _104077, _104007) => ? [_104098] : (event(_103983, _104098) & agent(_103983, _104098, _104001) & patient(_103983, _104098, _104077) & present(_103983, _104098) & nonreflexive(_103983, _104098) & fire(_103983, _104098) & from_loc(_103983, _104098, _104004))) & six(_103983, _104007) & group(_103983, _104007) & ! [_104205] : (member(_103983, _104205, _104007) => shot(_103983, _104205)) & revenge(_103983, _104010) & cry(_103983, _104013) & event(_103983, _104016) & agent(_103983, _104016, _103998) & patient(_103983, _104016, _104013) & present(_103983, _104016) & nonreflexive(_103983, _104016) & scream(_103983, _104016) & of(_103983, _104016, _104010))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.44/1.43
% 0.44/1.43 cnf(1, plain, [-(29 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503]), shot(_22503, 28 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503])], clausify(co1)).
% 0.44/1.43 cnf(2, plain, [-(29 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503]), -(member(_22503, 28 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], _23516))], clausify(co1)).
% 0.44/1.43 cnf(3, plain, [-(27 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503]), event(_22503, _31856), agent(_22503, _31856, _23033), patient(_22503, _31856, 26 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503]), present(_22503, _31856), nonreflexive(_22503, _31856), fire(_22503, _31856), from_loc(_22503, _31856, _23275)], clausify(co1)).
% 0.44/1.43 cnf(4, plain, [-(27 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503]), -(member(_22503, 26 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], _23516))], clausify(co1)).
% 0.44/1.43 cnf(5, plain, [-(25 ^ [_31254]), -(from_loc(16 ^ [], 24 ^ [_31254], 19 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(6, plain, [-(25 ^ [_31254]), -(fire(16 ^ [], 24 ^ [_31254]))], clausify(co1)).
% 0.44/1.43 cnf(7, plain, [-(25 ^ [_31254]), -(nonreflexive(16 ^ [], 24 ^ [_31254]))], clausify(co1)).
% 0.44/1.43 cnf(8, plain, [-(25 ^ [_31254]), -(present(16 ^ [], 24 ^ [_31254]))], clausify(co1)).
% 0.44/1.43 cnf(9, plain, [-(25 ^ [_31254]), -(patient(16 ^ [], 24 ^ [_31254], _31254))], clausify(co1)).
% 0.44/1.43 cnf(10, plain, [-(25 ^ [_31254]), -(agent(16 ^ [], 24 ^ [_31254], 18 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(11, plain, [-(25 ^ [_31254]), -(event(16 ^ [], 24 ^ [_31254]))], clausify(co1)).
% 0.44/1.43 cnf(12, plain, [-(30 ^ []), actual_world(_22503), male(_22503, _22790), male(_22503, _23033), man(_22503, _23033), of(_22503, _23275, _23033), cannon(_22503, _23275), 27 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], six(_22503, _23516), group(_22503, _23516), 29 ^ [_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], revenge(_22503, _23756), cry(_22503, _23995), event(_22503, _24233), agent(_22503, _24233, _22790), patient(_22503, _24233, _23995), present(_22503, _24233), nonreflexive(_22503, _24233), scream(_22503, _24233), of(_22503, _24233, _23756)], clausify(co1)).
% 0.44/1.43 cnf(13, plain, [-(30 ^ []), member(16 ^ [], _31322, 20 ^ []), -(shot(16 ^ [], _31322))], clausify(co1)).
% 0.44/1.43 cnf(14, plain, [-(30 ^ []), -(of(16 ^ [], 23 ^ [], 22 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(15, plain, [-(30 ^ []), -(scream(16 ^ [], 23 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(16, plain, [-(30 ^ []), -(nonreflexive(16 ^ [], 23 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(17, plain, [-(30 ^ []), -(present(16 ^ [], 23 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(18, plain, [-(30 ^ []), -(patient(16 ^ [], 23 ^ [], 21 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(19, plain, [-(30 ^ []), -(agent(16 ^ [], 23 ^ [], 17 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(20, plain, [-(30 ^ []), -(event(16 ^ [], 23 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(21, plain, [-(30 ^ []), -(revenge(16 ^ [], 22 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(22, plain, [-(30 ^ []), -(cry(16 ^ [], 21 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(23, plain, [-(30 ^ []), -(group(16 ^ [], 20 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(24, plain, [-(30 ^ []), -(six(16 ^ [], 20 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(25, plain, [-(30 ^ []), member(16 ^ [], _31254, 20 ^ []), 25 ^ [_31254]], clausify(co1)).
% 0.44/1.43 cnf(26, plain, [-(30 ^ []), -(cannon(16 ^ [], 19 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(27, plain, [-(30 ^ []), -(of(16 ^ [], 19 ^ [], 18 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(28, plain, [-(30 ^ []), -(man(16 ^ [], 18 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(29, plain, [-(30 ^ []), -(male(16 ^ [], 18 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(30, plain, [-(30 ^ []), -(male(16 ^ [], 17 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(31, plain, [-(30 ^ []), -(actual_world(16 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(32, plain, [-(14 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242]), shot(_13242, 13 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242])], clausify(co1)).
% 0.44/1.43 cnf(33, plain, [-(14 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242]), -(member(_13242, 13 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], _14255))], clausify(co1)).
% 0.44/1.43 cnf(34, plain, [-(12 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242]), event(_13242, _29384), agent(_13242, _29384, _13772), patient(_13242, _29384, 11 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242]), present(_13242, _29384), nonreflexive(_13242, _29384), fire(_13242, _29384), from_loc(_13242, _29384, _14014)], clausify(co1)).
% 0.44/1.43 cnf(35, plain, [-(12 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242]), -(member(_13242, 11 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], _14255))], clausify(co1)).
% 0.44/1.43 cnf(36, plain, [-(10 ^ [_28782]), -(from_loc(1 ^ [], 9 ^ [_28782], 4 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(37, plain, [-(10 ^ [_28782]), -(fire(1 ^ [], 9 ^ [_28782]))], clausify(co1)).
% 0.44/1.43 cnf(38, plain, [-(10 ^ [_28782]), -(nonreflexive(1 ^ [], 9 ^ [_28782]))], clausify(co1)).
% 0.44/1.43 cnf(39, plain, [-(10 ^ [_28782]), -(present(1 ^ [], 9 ^ [_28782]))], clausify(co1)).
% 0.44/1.43 cnf(40, plain, [-(10 ^ [_28782]), -(patient(1 ^ [], 9 ^ [_28782], _28782))], clausify(co1)).
% 0.44/1.43 cnf(41, plain, [-(10 ^ [_28782]), -(agent(1 ^ [], 9 ^ [_28782], 3 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(42, plain, [-(10 ^ [_28782]), -(event(1 ^ [], 9 ^ [_28782]))], clausify(co1)).
% 0.44/1.43 cnf(43, plain, [-(15 ^ []), actual_world(_13242), male(_13242, _13529), male(_13242, _13772), man(_13242, _13772), of(_13242, _14014, _13772), cannon(_13242, _14014), 12 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], six(_13242, _14255), group(_13242, _14255), 14 ^ [_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], cry(_13242, _14495), revenge(_13242, _14734), event(_13242, _14972), agent(_13242, _14972, _13529), patient(_13242, _14972, _14495), present(_13242, _14972), nonreflexive(_13242, _14972), scream(_13242, _14972), of(_13242, _14972, _14734)], clausify(co1)).
% 0.44/1.43 cnf(44, plain, [-(15 ^ []), member(1 ^ [], _28850, 5 ^ []), -(shot(1 ^ [], _28850))], clausify(co1)).
% 0.44/1.43 cnf(45, plain, [-(15 ^ []), -(of(1 ^ [], 8 ^ [], 6 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(46, plain, [-(15 ^ []), -(scream(1 ^ [], 8 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(47, plain, [-(15 ^ []), -(nonreflexive(1 ^ [], 8 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(48, plain, [-(15 ^ []), -(present(1 ^ [], 8 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(49, plain, [-(15 ^ []), -(patient(1 ^ [], 8 ^ [], 7 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(50, plain, [-(15 ^ []), -(agent(1 ^ [], 8 ^ [], 2 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(51, plain, [-(15 ^ []), -(event(1 ^ [], 8 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(52, plain, [-(15 ^ []), -(cry(1 ^ [], 7 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(53, plain, [-(15 ^ []), -(revenge(1 ^ [], 6 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(54, plain, [-(15 ^ []), -(group(1 ^ [], 5 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(55, plain, [-(15 ^ []), -(six(1 ^ [], 5 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(56, plain, [-(15 ^ []), member(1 ^ [], _28782, 5 ^ []), 10 ^ [_28782]], clausify(co1)).
% 0.44/1.43 cnf(57, plain, [-(15 ^ []), -(cannon(1 ^ [], 4 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(58, plain, [-(15 ^ []), -(of(1 ^ [], 4 ^ [], 3 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(59, plain, [-(15 ^ []), -(man(1 ^ [], 3 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(60, plain, [-(15 ^ []), -(male(1 ^ [], 3 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(61, plain, [-(15 ^ []), -(male(1 ^ [], 2 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(62, plain, [-(15 ^ []), -(actual_world(1 ^ []))], clausify(co1)).
% 0.44/1.43 cnf(63, plain, [15 ^ [], 30 ^ []], clausify(co1)).
% 0.44/1.43
% 0.44/1.43 cnf('1',plain,[15 ^ [], 30 ^ []],start(63)).
% 0.44/1.43 cnf('1.1',plain,[-(15 ^ []), -(agent(1 ^ [], 8 ^ [], 2 ^ []))],extension(50)).
% 0.44/1.43 cnf('1.1.1',plain,[agent(1 ^ [], 8 ^ [], 2 ^ []), -(15 ^ []), actual_world(1 ^ []), male(1 ^ [], 2 ^ []), male(1 ^ [], 3 ^ []), man(1 ^ [], 3 ^ []), of(1 ^ [], 4 ^ [], 3 ^ []), cannon(1 ^ [], 4 ^ []), 12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], six(1 ^ [], 5 ^ []), group(1 ^ [], 5 ^ []), 14 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], cry(1 ^ [], 7 ^ []), revenge(1 ^ [], 6 ^ []), event(1 ^ [], 8 ^ []), patient(1 ^ [], 8 ^ [], 7 ^ []), present(1 ^ [], 8 ^ []), nonreflexive(1 ^ [], 8 ^ []), scream(1 ^ [], 8 ^ []), of(1 ^ [], 8 ^ [], 6 ^ [])],extension(43,bind([[_14255, _14014, _13772, _13529, _14495, _13242, _14972, _14734], [5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 7 ^ [], 1 ^ [], 8 ^ [], 6 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.1',plain,[15 ^ []],reduction('1')).
% 0.44/1.43 cnf('1.1.1.2',plain,[-(actual_world(1 ^ [])), -(15 ^ [])],extension(62)).
% 0.44/1.43 cnf('1.1.1.2.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.3',plain,[-(male(1 ^ [], 2 ^ [])), -(15 ^ [])],extension(61)).
% 0.44/1.43 cnf('1.1.1.3.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.4',plain,[-(male(1 ^ [], 3 ^ [])), -(15 ^ [])],extension(60)).
% 0.44/1.43 cnf('1.1.1.4.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.5',plain,[-(man(1 ^ [], 3 ^ [])), -(15 ^ [])],extension(59)).
% 0.44/1.43 cnf('1.1.1.5.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.6',plain,[-(of(1 ^ [], 4 ^ [], 3 ^ [])), -(15 ^ [])],extension(58)).
% 0.44/1.43 cnf('1.1.1.6.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.7',plain,[-(cannon(1 ^ [], 4 ^ [])), -(15 ^ [])],extension(57)).
% 0.44/1.43 cnf('1.1.1.7.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8',plain,[-(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]), event(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]), agent(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 3 ^ []), patient(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]), present(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]), nonreflexive(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]), fire(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]), from_loc(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 4 ^ [])],extension(34,bind([[_14972, _14734, _14495, _14255, _13772, _13529, _13242, _29384, _14014], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 4 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.1',plain,[-(event(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(42,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.1.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.1.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.1.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.1.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.2',plain,[-(agent(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 3 ^ [])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(41,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.2.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.2.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.2.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.2.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.3',plain,[-(patient(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(40,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.3.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.3.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.3.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.3.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.4',plain,[-(present(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(39,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.4.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.4.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.4.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.4.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.5',plain,[-(nonreflexive(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(38,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.5.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.5.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.5.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.5.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.6',plain,[-(fire(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(37,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.6.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.6.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.6.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.6.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.7',plain,[-(from_loc(1 ^ [], 9 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], 4 ^ [])), -(10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]])],extension(36,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.7.1',plain,[10 ^ [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]], -(15 ^ []), member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(56,bind([[_28782], [11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.8.7.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.8.7.1.2',plain,[-(member(1 ^ [], 11 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(35,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.8.7.1.2.1',plain,[12 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.9',plain,[-(six(1 ^ [], 5 ^ [])), -(15 ^ [])],extension(55)).
% 0.44/1.43 cnf('1.1.1.9.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.10',plain,[-(group(1 ^ [], 5 ^ [])), -(15 ^ [])],extension(54)).
% 0.44/1.43 cnf('1.1.1.10.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.11',plain,[-(14 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]), shot(1 ^ [], 13 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(32,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.11.1',plain,[-(shot(1 ^ [], 13 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])), -(15 ^ []), member(1 ^ [], 13 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])],extension(44,bind([[_28850], [13 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]]))).
% 0.44/1.43 cnf('1.1.1.11.1.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.11.1.2',plain,[-(member(1 ^ [], 13 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []], 5 ^ [])), -(14 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []])],extension(33,bind([[_14972, _14734, _14495, _14255, _14014, _13772, _13529, _13242], [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]]))).
% 0.44/1.43 cnf('1.1.1.11.1.2.1',plain,[14 ^ [8 ^ [], 6 ^ [], 7 ^ [], 5 ^ [], 4 ^ [], 3 ^ [], 2 ^ [], 1 ^ []]],reduction('1.1.1')).
% 0.44/1.43 cnf('1.1.1.12',plain,[-(cry(1 ^ [], 7 ^ [])), -(15 ^ [])],extension(52)).
% 0.44/1.43 cnf('1.1.1.12.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.13',plain,[-(revenge(1 ^ [], 6 ^ [])), -(15 ^ [])],extension(53)).
% 0.44/1.43 cnf('1.1.1.13.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.14',plain,[-(event(1 ^ [], 8 ^ [])), -(15 ^ [])],extension(51)).
% 0.44/1.43 cnf('1.1.1.14.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.15',plain,[-(patient(1 ^ [], 8 ^ [], 7 ^ [])), -(15 ^ [])],extension(49)).
% 0.44/1.43 cnf('1.1.1.15.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.16',plain,[-(present(1 ^ [], 8 ^ [])), -(15 ^ [])],extension(48)).
% 0.44/1.43 cnf('1.1.1.16.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.17',plain,[-(nonreflexive(1 ^ [], 8 ^ [])), -(15 ^ [])],extension(47)).
% 0.44/1.43 cnf('1.1.1.17.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.18',plain,[-(scream(1 ^ [], 8 ^ [])), -(15 ^ [])],extension(46)).
% 0.44/1.43 cnf('1.1.1.18.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.1.1.19',plain,[-(of(1 ^ [], 8 ^ [], 6 ^ [])), -(15 ^ [])],extension(45)).
% 0.44/1.43 cnf('1.1.1.19.1',plain,[15 ^ []],lemmata('1.1.1')).
% 0.44/1.43 cnf('1.2',plain,[-(30 ^ []), -(agent(16 ^ [], 23 ^ [], 17 ^ []))],extension(19)).
% 0.44/1.43 cnf('1.2.1',plain,[agent(16 ^ [], 23 ^ [], 17 ^ []), -(30 ^ []), actual_world(16 ^ []), male(16 ^ [], 17 ^ []), male(16 ^ [], 18 ^ []), man(16 ^ [], 18 ^ []), of(16 ^ [], 19 ^ [], 18 ^ []), cannon(16 ^ [], 19 ^ []), 27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], six(16 ^ [], 20 ^ []), group(16 ^ [], 20 ^ []), 29 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], revenge(16 ^ [], 22 ^ []), cry(16 ^ [], 21 ^ []), event(16 ^ [], 23 ^ []), patient(16 ^ [], 23 ^ [], 21 ^ []), present(16 ^ [], 23 ^ []), nonreflexive(16 ^ [], 23 ^ []), scream(16 ^ [], 23 ^ []), of(16 ^ [], 23 ^ [], 22 ^ [])],extension(12,bind([[_23516, _23275, _23033, _22790, _23995, _22503, _24233, _23756], [20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 21 ^ [], 16 ^ [], 23 ^ [], 22 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.1',plain,[30 ^ []],reduction('1')).
% 0.44/1.43 cnf('1.2.1.2',plain,[-(actual_world(16 ^ [])), -(30 ^ [])],extension(31)).
% 0.44/1.43 cnf('1.2.1.2.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.3',plain,[-(male(16 ^ [], 17 ^ [])), -(30 ^ [])],extension(30)).
% 0.44/1.43 cnf('1.2.1.3.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.4',plain,[-(male(16 ^ [], 18 ^ [])), -(30 ^ [])],extension(29)).
% 0.44/1.43 cnf('1.2.1.4.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.5',plain,[-(man(16 ^ [], 18 ^ [])), -(30 ^ [])],extension(28)).
% 0.44/1.43 cnf('1.2.1.5.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.6',plain,[-(of(16 ^ [], 19 ^ [], 18 ^ [])), -(30 ^ [])],extension(27)).
% 0.44/1.43 cnf('1.2.1.6.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.7',plain,[-(cannon(16 ^ [], 19 ^ [])), -(30 ^ [])],extension(26)).
% 0.44/1.43 cnf('1.2.1.7.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8',plain,[-(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]), event(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]), agent(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 18 ^ []), patient(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]), present(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]), nonreflexive(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]), fire(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]), from_loc(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 19 ^ [])],extension(3,bind([[_24233, _23995, _23756, _23516, _23033, _22790, _22503, _31856, _23275], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 18 ^ [], 17 ^ [], 16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 19 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.1',plain,[-(event(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(11,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.1.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.1.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.1.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.1.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.2',plain,[-(agent(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 18 ^ [])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(10,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.2.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.2.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.2.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.2.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.3',plain,[-(patient(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(9,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.3.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.3.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.3.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.3.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.4',plain,[-(present(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(8,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.4.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.4.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.4.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.4.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.5',plain,[-(nonreflexive(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(7,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.5.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.5.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.5.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.5.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.6',plain,[-(fire(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(6,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.6.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.6.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.6.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.6.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.7',plain,[-(from_loc(16 ^ [], 24 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], 19 ^ [])), -(25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]])],extension(5,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.7.1',plain,[25 ^ [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]], -(30 ^ []), member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(25,bind([[_31254], [26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.8.7.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.8.7.1.2',plain,[-(member(16 ^ [], 26 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(4,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.8.7.1.2.1',plain,[27 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.9',plain,[-(six(16 ^ [], 20 ^ [])), -(30 ^ [])],extension(24)).
% 0.44/1.43 cnf('1.2.1.9.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.10',plain,[-(group(16 ^ [], 20 ^ [])), -(30 ^ [])],extension(23)).
% 0.44/1.43 cnf('1.2.1.10.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.11',plain,[-(29 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]), shot(16 ^ [], 28 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(1,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.11.1',plain,[-(shot(16 ^ [], 28 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])), -(30 ^ []), member(16 ^ [], 28 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])],extension(13,bind([[_31322], [28 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]]))).
% 0.44/1.43 cnf('1.2.1.11.1.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.11.1.2',plain,[-(member(16 ^ [], 28 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []], 20 ^ [])), -(29 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []])],extension(2,bind([[_24233, _23995, _23756, _23516, _23275, _23033, _22790, _22503], [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]]))).
% 0.44/1.43 cnf('1.2.1.11.1.2.1',plain,[29 ^ [23 ^ [], 21 ^ [], 22 ^ [], 20 ^ [], 19 ^ [], 18 ^ [], 17 ^ [], 16 ^ []]],reduction('1.2.1')).
% 0.44/1.43 cnf('1.2.1.12',plain,[-(revenge(16 ^ [], 22 ^ [])), -(30 ^ [])],extension(21)).
% 0.44/1.43 cnf('1.2.1.12.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.13',plain,[-(cry(16 ^ [], 21 ^ [])), -(30 ^ [])],extension(22)).
% 0.44/1.43 cnf('1.2.1.13.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.14',plain,[-(event(16 ^ [], 23 ^ [])), -(30 ^ [])],extension(20)).
% 0.44/1.43 cnf('1.2.1.14.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.15',plain,[-(patient(16 ^ [], 23 ^ [], 21 ^ [])), -(30 ^ [])],extension(18)).
% 0.44/1.43 cnf('1.2.1.15.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.16',plain,[-(present(16 ^ [], 23 ^ [])), -(30 ^ [])],extension(17)).
% 0.44/1.43 cnf('1.2.1.16.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.17',plain,[-(nonreflexive(16 ^ [], 23 ^ [])), -(30 ^ [])],extension(16)).
% 0.44/1.43 cnf('1.2.1.17.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.18',plain,[-(scream(16 ^ [], 23 ^ [])), -(30 ^ [])],extension(15)).
% 0.44/1.43 cnf('1.2.1.18.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 cnf('1.2.1.19',plain,[-(of(16 ^ [], 23 ^ [], 22 ^ [])), -(30 ^ [])],extension(14)).
% 0.44/1.43 cnf('1.2.1.19.1',plain,[30 ^ []],lemmata('1.2.1')).
% 0.44/1.43 %-----------------------------------------------------
% 0.44/1.44
% 0.44/1.44 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------