%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYO582+1 : TPTP v8.1.2. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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 : 300s
% DateTime : Thu May 9 17:50:55 EDT 2024
% Result : CounterSatisfiable 3.37s 3.53s
% Output : Saturation 3.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYO582+1 : TPTP v8.1.2. Released v5.5.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n015.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 : 300
% 0.12/0.34 % DateTime : Wed May 8 17:51:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 3.37/3.53 % Version: 1.5
% 3.37/3.53 % SZS status CounterSatisfiable
% 3.37/3.53 % SZS output start Saturation
% 3.37/3.53 fof(sos_15,axiom,((![X19]:(k04_buttercup10516(X19)=>b48_buttercup10417(X19)))&(?[X20]:(b48_buttercup10417(X20)&(~k04_buttercup10516(X20))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_15)).
% 3.37/3.53 fof(c106,plain,((![X19]:(k04_buttercup10516(X19)=>b48_buttercup10417(X19)))&(?[X20]:(b48_buttercup10417(X20)&~k04_buttercup10516(X20)))),inference(fof_simplification,[status(thm)],[sos_15])).
% 3.37/3.53 fof(c107,plain,((![X19]:(~k04_buttercup10516(X19)|b48_buttercup10417(X19)))&(?[X20]:(b48_buttercup10417(X20)&~k04_buttercup10516(X20)))),inference(fof_nnf,[status(thm)],[c106])).
% 3.37/3.53 fof(c108,plain,((![X37]:(~k04_buttercup10516(X37)|b48_buttercup10417(X37)))&(?[X38]:(b48_buttercup10417(X38)&~k04_buttercup10516(X38)))),inference(variable_rename,[status(thm)],[c107])).
% 3.37/3.53 fof(c110,plain,(![X37]:((~k04_buttercup10516(X37)|b48_buttercup10417(X37))&(b48_buttercup10417(skolem0027)&~k04_buttercup10516(skolem0027)))),inference(shift_quantors,[status(thm)],[fof(c109,plain,((![X37]:(~k04_buttercup10516(X37)|b48_buttercup10417(X37)))&(b48_buttercup10417(skolem0027)&~k04_buttercup10516(skolem0027))),inference(skolemize,[status(esa)],[c108])).])).
% 3.37/3.53 cnf(c111,plain,~k04_buttercup10516(X68)|b48_buttercup10417(X68),inference(split_conjunct,[status(thm)],[c110])).
% 3.37/3.53 fof(sos_17,axiom,((![X23]:(b48_buttercup10515(X23)=>k04_buttercup10516(X23)))&(?[X24]:(k04_buttercup10516(X24)&(~b48_buttercup10515(X24))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_17)).
% 3.37/3.53 fof(c90,plain,((![X23]:(b48_buttercup10515(X23)=>k04_buttercup10516(X23)))&(?[X24]:(k04_buttercup10516(X24)&~b48_buttercup10515(X24)))),inference(fof_simplification,[status(thm)],[sos_17])).
% 3.37/3.53 fof(c91,plain,((![X23]:(~b48_buttercup10515(X23)|k04_buttercup10516(X23)))&(?[X24]:(k04_buttercup10516(X24)&~b48_buttercup10515(X24)))),inference(fof_nnf,[status(thm)],[c90])).
% 3.37/3.53 fof(c92,plain,((![X33]:(~b48_buttercup10515(X33)|k04_buttercup10516(X33)))&(?[X34]:(k04_buttercup10516(X34)&~b48_buttercup10515(X34)))),inference(variable_rename,[status(thm)],[c91])).
% 3.37/3.53 fof(c94,plain,(![X33]:((~b48_buttercup10515(X33)|k04_buttercup10516(X33))&(k04_buttercup10516(skolem0025)&~b48_buttercup10515(skolem0025)))),inference(shift_quantors,[status(thm)],[fof(c93,plain,((![X33]:(~b48_buttercup10515(X33)|k04_buttercup10516(X33)))&(k04_buttercup10516(skolem0025)&~b48_buttercup10515(skolem0025))),inference(skolemize,[status(esa)],[c92])).])).
% 3.37/3.53 cnf(c95,plain,~b48_buttercup10515(X66)|k04_buttercup10516(X66),inference(split_conjunct,[status(thm)],[c94])).
% 3.37/3.53 fof(sos_03,axiom,(![X2]:(b48_buttercup10519(X2)=>b48_buttercup10515(X2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_03)).
% 3.37/3.53 fof(c168,plain,(![X2]:(~b48_buttercup10519(X2)|b48_buttercup10515(X2))),inference(fof_nnf,[status(thm)],[sos_03])).
% 3.37/3.53 fof(c169,plain,(![X55]:(~b48_buttercup10519(X55)|b48_buttercup10515(X55))),inference(variable_rename,[status(thm)],[c168])).
% 3.37/3.53 cnf(c170,plain,~b48_buttercup10519(X79)|b48_buttercup10515(X79),inference(split_conjunct,[status(thm)],[c169])).
% 3.37/3.53 fof(goals_38,conjecture,((((![X48]:(k04_buttercup10225(X48)<=>b48_buttercup10519(X48)))|((![X49]:(b48_buttercup10519(X49)=>k04_buttercup10225(X49)))&(?[X50]:(k04_buttercup10225(X50)&(~b48_buttercup10519(X50))))))|(?[X51]:(?[X52]:(?[X53]:(((((k04_buttercup10225(X51)&b48_buttercup10519(X51))&k04_buttercup10225(X52))&(~b48_buttercup10519(X52)))&(~k04_buttercup10225(X53)))&b48_buttercup10519(X53))))))|(![X54]:(k04_buttercup10225(X54)=>(~b48_buttercup10519(X54))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals_38)).
% 3.37/3.53 fof(c0,negated_conjecture,(~((((![X48]:(k04_buttercup10225(X48)<=>b48_buttercup10519(X48)))|((![X49]:(b48_buttercup10519(X49)=>k04_buttercup10225(X49)))&(?[X50]:(k04_buttercup10225(X50)&(~b48_buttercup10519(X50))))))|(?[X51]:(?[X52]:(?[X53]:(((((k04_buttercup10225(X51)&b48_buttercup10519(X51))&k04_buttercup10225(X52))&(~b48_buttercup10519(X52)))&(~k04_buttercup10225(X53)))&b48_buttercup10519(X53))))))|(![X54]:(k04_buttercup10225(X54)=>(~b48_buttercup10519(X54)))))),inference(assume_negation,[status(cth)],[goals_38])).
% 3.37/3.53 fof(c1,negated_conjecture,(~((((![X48]:(k04_buttercup10225(X48)<=>b48_buttercup10519(X48)))|((![X49]:(b48_buttercup10519(X49)=>k04_buttercup10225(X49)))&(?[X50]:(k04_buttercup10225(X50)&~b48_buttercup10519(X50)))))|(?[X51]:(?[X52]:(?[X53]:(((((k04_buttercup10225(X51)&b48_buttercup10519(X51))&k04_buttercup10225(X52))&~b48_buttercup10519(X52))&~k04_buttercup10225(X53))&b48_buttercup10519(X53))))))|(![X54]:(k04_buttercup10225(X54)=>~b48_buttercup10519(X54))))),inference(fof_simplification,[status(thm)],[c0])).
% 3.37/3.53 fof(c2,negated_conjecture,((((?[X48]:((~k04_buttercup10225(X48)|~b48_buttercup10519(X48))&(k04_buttercup10225(X48)|b48_buttercup10519(X48))))&((?[X49]:(b48_buttercup10519(X49)&~k04_buttercup10225(X49)))|(![X50]:(~k04_buttercup10225(X50)|b48_buttercup10519(X50)))))&(![X51]:(![X52]:(![X53]:(((((~k04_buttercup10225(X51)|~b48_buttercup10519(X51))|~k04_buttercup10225(X52))|b48_buttercup10519(X52))|k04_buttercup10225(X53))|~b48_buttercup10519(X53))))))&(?[X54]:(k04_buttercup10225(X54)&b48_buttercup10519(X54)))),inference(fof_nnf,[status(thm)],[c1])).
% 3.37/3.53 fof(c3,negated_conjecture,((((?[X2]:((~k04_buttercup10225(X2)|~b48_buttercup10519(X2))&(k04_buttercup10225(X2)|b48_buttercup10519(X2))))&((?[X3]:(b48_buttercup10519(X3)&~k04_buttercup10225(X3)))|(![X4]:(~k04_buttercup10225(X4)|b48_buttercup10519(X4)))))&(![X5]:(![X6]:(![X7]:(((((~k04_buttercup10225(X5)|~b48_buttercup10519(X5))|~k04_buttercup10225(X6))|b48_buttercup10519(X6))|k04_buttercup10225(X7))|~b48_buttercup10519(X7))))))&(?[X8]:(k04_buttercup10225(X8)&b48_buttercup10519(X8)))),inference(variable_rename,[status(thm)],[c2])).
% 3.37/3.53 fof(c5,negated_conjecture,(![X4]:(![X5]:(![X6]:(![X7]:(((((~k04_buttercup10225(skolem0001)|~b48_buttercup10519(skolem0001))&(k04_buttercup10225(skolem0001)|b48_buttercup10519(skolem0001)))&((b48_buttercup10519(skolem0002)&~k04_buttercup10225(skolem0002))|(~k04_buttercup10225(X4)|b48_buttercup10519(X4))))&(((((~k04_buttercup10225(X5)|~b48_buttercup10519(X5))|~k04_buttercup10225(X6))|b48_buttercup10519(X6))|k04_buttercup10225(X7))|~b48_buttercup10519(X7)))&(k04_buttercup10225(skolem0003)&b48_buttercup10519(skolem0003))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((~k04_buttercup10225(skolem0001)|~b48_buttercup10519(skolem0001))&(k04_buttercup10225(skolem0001)|b48_buttercup10519(skolem0001)))&((b48_buttercup10519(skolem0002)&~k04_buttercup10225(skolem0002))|(![X4]:(~k04_buttercup10225(X4)|b48_buttercup10519(X4)))))&(![X5]:(![X6]:(![X7]:(((((~k04_buttercup10225(X5)|~b48_buttercup10519(X5))|~k04_buttercup10225(X6))|b48_buttercup10519(X6))|k04_buttercup10225(X7))|~b48_buttercup10519(X7))))))&(k04_buttercup10225(skolem0003)&b48_buttercup10519(skolem0003))),inference(skolemize,[status(esa)],[c3])).])).
% 3.37/3.53 fof(c6,negated_conjecture,(![X4]:(![X5]:(![X6]:(![X7]:(((((~k04_buttercup10225(skolem0001)|~b48_buttercup10519(skolem0001))&(k04_buttercup10225(skolem0001)|b48_buttercup10519(skolem0001)))&((b48_buttercup10519(skolem0002)|(~k04_buttercup10225(X4)|b48_buttercup10519(X4)))&(~k04_buttercup10225(skolem0002)|(~k04_buttercup10225(X4)|b48_buttercup10519(X4)))))&(((((~k04_buttercup10225(X5)|~b48_buttercup10519(X5))|~k04_buttercup10225(X6))|b48_buttercup10519(X6))|k04_buttercup10225(X7))|~b48_buttercup10519(X7)))&(k04_buttercup10225(skolem0003)&b48_buttercup10519(skolem0003))))))),inference(distribute,[status(thm)],[c5])).
% 3.37/3.53 cnf(c12,negated_conjecture,k04_buttercup10225(skolem0003),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c13,negated_conjecture,b48_buttercup10519(skolem0003),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 fof(sos_30,axiom,(?[X40]:b48_buttercup10229(X40)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_30)).
% 3.37/3.53 fof(c35,plain,(?[X16]:b48_buttercup10229(X16)),inference(variable_rename,[status(thm)],[sos_30])).
% 3.37/3.53 fof(c36,plain,b48_buttercup10229(skolem0011),inference(skolemize,[status(esa)],[c35])).
% 3.37/3.53 cnf(c37,plain,b48_buttercup10229(skolem0011),inference(split_conjunct,[status(thm)],[c36])).
% 3.37/3.53 fof(sos_16,axiom,((![X21]:(b48_buttercup10229(X21)=>k04_buttercup10225(X21)))&(?[X22]:(k04_buttercup10225(X22)&(~b48_buttercup10229(X22))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_16)).
% 3.37/3.53 fof(c98,plain,((![X21]:(b48_buttercup10229(X21)=>k04_buttercup10225(X21)))&(?[X22]:(k04_buttercup10225(X22)&~b48_buttercup10229(X22)))),inference(fof_simplification,[status(thm)],[sos_16])).
% 3.37/3.53 fof(c99,plain,((![X21]:(~b48_buttercup10229(X21)|k04_buttercup10225(X21)))&(?[X22]:(k04_buttercup10225(X22)&~b48_buttercup10229(X22)))),inference(fof_nnf,[status(thm)],[c98])).
% 3.37/3.53 fof(c100,plain,((![X35]:(~b48_buttercup10229(X35)|k04_buttercup10225(X35)))&(?[X36]:(k04_buttercup10225(X36)&~b48_buttercup10229(X36)))),inference(variable_rename,[status(thm)],[c99])).
% 3.37/3.53 fof(c102,plain,(![X35]:((~b48_buttercup10229(X35)|k04_buttercup10225(X35))&(k04_buttercup10225(skolem0026)&~b48_buttercup10229(skolem0026)))),inference(shift_quantors,[status(thm)],[fof(c101,plain,((![X35]:(~b48_buttercup10229(X35)|k04_buttercup10225(X35)))&(k04_buttercup10225(skolem0026)&~b48_buttercup10229(skolem0026))),inference(skolemize,[status(esa)],[c100])).])).
% 3.37/3.53 cnf(c103,plain,~b48_buttercup10229(X67)|k04_buttercup10225(X67),inference(split_conjunct,[status(thm)],[c102])).
% 3.37/3.53 cnf(c205,plain,k04_buttercup10225(skolem0011),inference(resolution,[status(thm)],[c103, c37])).
% 3.37/3.53 cnf(c8,negated_conjecture,k04_buttercup10225(skolem0001)|b48_buttercup10519(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c11,negated_conjecture,~k04_buttercup10225(X61)|~b48_buttercup10519(X61)|~k04_buttercup10225(X60)|b48_buttercup10519(X60)|k04_buttercup10225(X62)|~b48_buttercup10519(X62),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c187,plain,~k04_buttercup10225(X86)|~b48_buttercup10519(X86)|~k04_buttercup10225(X87)|b48_buttercup10519(X87)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c11, c8])).
% 3.37/3.53 cnf(c295,plain,~k04_buttercup10225(X130)|~b48_buttercup10519(X130)|b48_buttercup10519(skolem0011)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c187, c205])).
% 3.37/3.53 cnf(c988,plain,~k04_buttercup10225(skolem0003)|b48_buttercup10519(skolem0011)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c295, c13])).
% 3.37/3.53 cnf(c2735,plain,b48_buttercup10519(skolem0011)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c988, c12])).
% 3.37/3.53 cnf(c2736,plain,k04_buttercup10225(skolem0001)|b48_buttercup10515(skolem0011),inference(resolution,[status(thm)],[c2735, c170])).
% 3.37/3.53 cnf(c2786,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0011),inference(resolution,[status(thm)],[c2736, c95])).
% 3.37/3.53 cnf(c2862,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0011),inference(resolution,[status(thm)],[c2786, c111])).
% 3.37/3.53 cnf(c7,negated_conjecture,~k04_buttercup10225(skolem0001)|~b48_buttercup10519(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c10,negated_conjecture,~k04_buttercup10225(skolem0002)|~k04_buttercup10225(X59)|b48_buttercup10519(X59),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c184,plain,~k04_buttercup10225(skolem0002)|b48_buttercup10519(skolem0001),inference(resolution,[status(thm)],[c10, c8])).
% 3.37/3.53 cnf(c9,negated_conjecture,b48_buttercup10519(skolem0002)|~k04_buttercup10225(X58)|b48_buttercup10519(X58),inference(split_conjunct,[status(thm)],[c6])).
% 3.37/3.53 cnf(c179,plain,b48_buttercup10519(skolem0002)|b48_buttercup10519(skolem0001),inference(resolution,[status(thm)],[c9, c8])).
% 3.37/3.53 cnf(c246,plain,b48_buttercup10519(skolem0001)|~k04_buttercup10225(X90)|~b48_buttercup10519(X90)|~k04_buttercup10225(X91)|b48_buttercup10519(X91)|k04_buttercup10225(skolem0002),inference(resolution,[status(thm)],[c179, c11])).
% 3.37/3.53 cnf(c333,plain,b48_buttercup10519(skolem0001)|~k04_buttercup10225(X158)|~b48_buttercup10519(X158)|k04_buttercup10225(skolem0002),inference(resolution,[status(thm)],[c246, c8])).
% 3.37/3.53 cnf(c2060,plain,b48_buttercup10519(skolem0001)|~k04_buttercup10225(skolem0003)|k04_buttercup10225(skolem0002),inference(resolution,[status(thm)],[c333, c13])).
% 3.37/3.53 cnf(c3675,plain,b48_buttercup10519(skolem0001)|k04_buttercup10225(skolem0002),inference(resolution,[status(thm)],[c2060, c12])).
% 3.37/3.53 cnf(c3698,plain,b48_buttercup10519(skolem0001),inference(resolution,[status(thm)],[c3675, c184])).
% 3.37/3.53 cnf(c3710,plain,~k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c3698, c7])).
% 3.37/3.53 cnf(c3736,plain,b48_buttercup10417(skolem0011),inference(resolution,[status(thm)],[c3710, c2862])).
% 3.37/3.53 fof(sos_12,axiom,((![X12]:(b48_buttercup10227(X12)=>k04_buttercup10225(X12)))&(?[X13]:(k04_buttercup10225(X13)&(~b48_buttercup10227(X13))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_12)).
% 3.37/3.53 fof(c131,plain,((![X12]:(b48_buttercup10227(X12)=>k04_buttercup10225(X12)))&(?[X13]:(k04_buttercup10225(X13)&~b48_buttercup10227(X13)))),inference(fof_simplification,[status(thm)],[sos_12])).
% 3.37/3.53 fof(c132,plain,((![X12]:(~b48_buttercup10227(X12)|k04_buttercup10225(X12)))&(?[X13]:(k04_buttercup10225(X13)&~b48_buttercup10227(X13)))),inference(fof_nnf,[status(thm)],[c131])).
% 3.37/3.53 fof(c133,plain,((![X44]:(~b48_buttercup10227(X44)|k04_buttercup10225(X44)))&(?[X45]:(k04_buttercup10225(X45)&~b48_buttercup10227(X45)))),inference(variable_rename,[status(thm)],[c132])).
% 3.37/3.53 fof(c135,plain,(![X44]:((~b48_buttercup10227(X44)|k04_buttercup10225(X44))&(k04_buttercup10225(skolem0032)&~b48_buttercup10227(skolem0032)))),inference(shift_quantors,[status(thm)],[fof(c134,plain,((![X44]:(~b48_buttercup10227(X44)|k04_buttercup10225(X44)))&(k04_buttercup10225(skolem0032)&~b48_buttercup10227(skolem0032))),inference(skolemize,[status(esa)],[c133])).])).
% 3.37/3.53 cnf(c137,plain,k04_buttercup10225(skolem0032),inference(split_conjunct,[status(thm)],[c135])).
% 3.37/3.53 cnf(c293,plain,~k04_buttercup10225(X128)|~b48_buttercup10519(X128)|b48_buttercup10519(skolem0032)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c187, c137])).
% 3.37/3.53 cnf(c880,plain,~k04_buttercup10225(skolem0003)|b48_buttercup10519(skolem0032)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c293, c13])).
% 3.37/3.53 cnf(c2175,plain,b48_buttercup10519(skolem0032)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c880, c12])).
% 3.37/3.53 cnf(c2176,plain,k04_buttercup10225(skolem0001)|b48_buttercup10515(skolem0032),inference(resolution,[status(thm)],[c2175, c170])).
% 3.37/3.53 cnf(c2262,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0032),inference(resolution,[status(thm)],[c2176, c95])).
% 3.37/3.53 cnf(c2293,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0032),inference(resolution,[status(thm)],[c2262, c111])).
% 3.37/3.53 cnf(c3735,plain,b48_buttercup10417(skolem0032),inference(resolution,[status(thm)],[c3710, c2293])).
% 3.37/3.53 fof(sos_29,axiom,(?[X39]:b48_buttercup10227(X39)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_29)).
% 3.37/3.53 fof(c38,plain,(?[X17]:b48_buttercup10227(X17)),inference(variable_rename,[status(thm)],[sos_29])).
% 3.37/3.53 fof(c39,plain,b48_buttercup10227(skolem0012),inference(skolemize,[status(esa)],[c38])).
% 3.37/3.53 cnf(c40,plain,b48_buttercup10227(skolem0012),inference(split_conjunct,[status(thm)],[c39])).
% 3.37/3.53 cnf(c136,plain,~b48_buttercup10227(X70)|k04_buttercup10225(X70),inference(split_conjunct,[status(thm)],[c135])).
% 3.37/3.53 cnf(c213,plain,k04_buttercup10225(skolem0012),inference(resolution,[status(thm)],[c136, c40])).
% 3.37/3.53 cnf(c294,plain,~k04_buttercup10225(X129)|~b48_buttercup10519(X129)|b48_buttercup10519(skolem0012)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c187, c213])).
% 3.37/3.53 cnf(c933,plain,~k04_buttercup10225(skolem0003)|b48_buttercup10519(skolem0012)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c294, c13])).
% 3.37/3.53 cnf(c2515,plain,b48_buttercup10519(skolem0012)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c933, c12])).
% 3.37/3.53 cnf(c2516,plain,k04_buttercup10225(skolem0001)|b48_buttercup10515(skolem0012),inference(resolution,[status(thm)],[c2515, c170])).
% 3.37/3.53 cnf(c2569,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0012),inference(resolution,[status(thm)],[c2516, c95])).
% 3.37/3.53 cnf(c2669,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0012),inference(resolution,[status(thm)],[c2569, c111])).
% 3.37/3.53 cnf(c3734,plain,b48_buttercup10417(skolem0012),inference(resolution,[status(thm)],[c3710, c2669])).
% 3.37/3.53 cnf(c3733,plain,b48_buttercup10519(skolem0032),inference(resolution,[status(thm)],[c3710, c2175])).
% 3.37/3.53 cnf(c104,plain,k04_buttercup10225(skolem0026),inference(split_conjunct,[status(thm)],[c102])).
% 3.37/3.53 cnf(c298,plain,~k04_buttercup10225(X133)|~b48_buttercup10519(X133)|b48_buttercup10519(skolem0026)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c187, c104])).
% 3.37/3.53 cnf(c1098,plain,~k04_buttercup10225(skolem0003)|b48_buttercup10519(skolem0026)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c298, c13])).
% 3.37/3.53 cnf(c3331,plain,b48_buttercup10519(skolem0026)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c1098, c12])).
% 3.37/3.53 cnf(c3383,plain,k04_buttercup10225(skolem0001)|b48_buttercup10515(skolem0026),inference(resolution,[status(thm)],[c3331, c170])).
% 3.37/3.53 cnf(c3732,plain,b48_buttercup10515(skolem0026),inference(resolution,[status(thm)],[c3710, c3383])).
% 3.37/3.53 cnf(c3731,plain,k04_buttercup10516(skolem0011),inference(resolution,[status(thm)],[c3710, c2786])).
% 3.37/3.53 cnf(c3730,plain,b48_buttercup10515(skolem0011),inference(resolution,[status(thm)],[c3710, c2736])).
% 3.37/3.53 cnf(c3436,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0026),inference(resolution,[status(thm)],[c3383, c95])).
% 3.37/3.53 cnf(c3729,plain,k04_buttercup10516(skolem0026),inference(resolution,[status(thm)],[c3710, c3436])).
% 3.37/3.53 cnf(c3728,plain,b48_buttercup10519(skolem0026),inference(resolution,[status(thm)],[c3710, c3331])).
% 3.37/3.53 fof(sos_22,axiom,(?[X32]:k04_buttercup10225(X32)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_22)).
% 3.37/3.53 fof(c59,plain,(?[X24]:k04_buttercup10225(X24)),inference(variable_rename,[status(thm)],[sos_22])).
% 3.37/3.53 fof(c60,plain,k04_buttercup10225(skolem0019),inference(skolemize,[status(esa)],[c59])).
% 3.37/3.53 cnf(c61,plain,k04_buttercup10225(skolem0019),inference(split_conjunct,[status(thm)],[c60])).
% 3.37/3.53 cnf(c297,plain,~k04_buttercup10225(X132)|~b48_buttercup10519(X132)|b48_buttercup10519(skolem0019)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c187, c61])).
% 3.37/3.53 cnf(c1044,plain,~k04_buttercup10225(skolem0003)|b48_buttercup10519(skolem0019)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c297, c13])).
% 3.37/3.53 cnf(c3097,plain,b48_buttercup10519(skolem0019)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c1044, c12])).
% 3.37/3.53 cnf(c3098,plain,k04_buttercup10225(skolem0001)|b48_buttercup10515(skolem0019),inference(resolution,[status(thm)],[c3097, c170])).
% 3.37/3.53 cnf(c3727,plain,b48_buttercup10515(skolem0019),inference(resolution,[status(thm)],[c3710, c3098])).
% 3.37/3.53 cnf(c3726,plain,b48_buttercup10515(skolem0012),inference(resolution,[status(thm)],[c3710, c2516])).
% 3.37/3.53 cnf(c3540,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0026),inference(resolution,[status(thm)],[c3436, c111])).
% 3.37/3.53 cnf(c3725,plain,b48_buttercup10417(skolem0026),inference(resolution,[status(thm)],[c3710, c3540])).
% 3.37/3.53 cnf(c3152,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0019),inference(resolution,[status(thm)],[c3098, c95])).
% 3.37/3.53 cnf(c3724,plain,k04_buttercup10516(skolem0019),inference(resolution,[status(thm)],[c3710, c3152])).
% 3.37/3.53 cnf(c3723,plain,b48_buttercup10519(skolem0019),inference(resolution,[status(thm)],[c3710, c3097])).
% 3.37/3.53 cnf(c3256,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0019),inference(resolution,[status(thm)],[c3152, c111])).
% 3.37/3.53 cnf(c3722,plain,b48_buttercup10417(skolem0019),inference(resolution,[status(thm)],[c3710, c3256])).
% 3.37/3.53 cnf(c3720,plain,k04_buttercup10516(skolem0032),inference(resolution,[status(thm)],[c3710, c2262])).
% 3.37/3.53 cnf(c3719,plain,b48_buttercup10515(skolem0032),inference(resolution,[status(thm)],[c3710, c2176])).
% 3.37/3.53 cnf(c3718,plain,b48_buttercup10519(skolem0011),inference(resolution,[status(thm)],[c3710, c2735])).
% 3.37/3.53 cnf(c3717,plain,k04_buttercup10516(skolem0012),inference(resolution,[status(thm)],[c3710, c2569])).
% 3.37/3.53 cnf(c3716,plain,b48_buttercup10519(skolem0012),inference(resolution,[status(thm)],[c3710, c2515])).
% 3.37/3.53 cnf(c231,plain,b48_buttercup10515(skolem0001)|k04_buttercup10225(skolem0001),inference(resolution,[status(thm)],[c170, c8])).
% 3.37/3.53 cnf(c283,plain,k04_buttercup10225(skolem0001)|k04_buttercup10516(skolem0001),inference(resolution,[status(thm)],[c231, c95])).
% 3.37/3.53 cnf(c354,plain,k04_buttercup10225(skolem0001)|b48_buttercup10417(skolem0001),inference(resolution,[status(thm)],[c283, c111])).
% 3.37/3.53 cnf(c3715,plain,b48_buttercup10417(skolem0001),inference(resolution,[status(thm)],[c3710, c354])).
% 3.37/3.53 cnf(c3708,plain,b48_buttercup10515(skolem0001),inference(resolution,[status(thm)],[c3698, c170])).
% 3.37/3.53 cnf(c3714,plain,k04_buttercup10516(skolem0001),inference(resolution,[status(thm)],[c3708, c95])).
% 3.37/3.53 fof(sos_01,axiom,(![X0]:(k04_buttercup10517(X0)=>k04_buttercup10516(X0))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_01)).
% 3.37/3.53 fof(c174,plain,(![X0]:(~k04_buttercup10517(X0)|k04_buttercup10516(X0))),inference(fof_nnf,[status(thm)],[sos_01])).
% 3.37/3.53 fof(c175,plain,(![X57]:(~k04_buttercup10517(X57)|k04_buttercup10516(X57))),inference(variable_rename,[status(thm)],[c174])).
% 3.37/3.53 cnf(c176,plain,~k04_buttercup10517(X81)|k04_buttercup10516(X81),inference(split_conjunct,[status(thm)],[c175])).
% 3.37/3.53 fof(sos_20,axiom,(![X28]:(k04_buttercup10517(X28)<=>b48_buttercup10421(X28))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_20)).
% 3.37/3.53 fof(c71,plain,(![X28]:((~k04_buttercup10517(X28)|b48_buttercup10421(X28))&(~b48_buttercup10421(X28)|k04_buttercup10517(X28)))),inference(fof_nnf,[status(thm)],[sos_20])).
% 3.37/3.53 fof(c72,plain,((![X28]:(~k04_buttercup10517(X28)|b48_buttercup10421(X28)))&(![X28]:(~b48_buttercup10421(X28)|k04_buttercup10517(X28)))),inference(shift_quantors,[status(thm)],[c71])).
% 3.37/3.53 fof(c74,plain,(![X28]:(![X29]:((~k04_buttercup10517(X28)|b48_buttercup10421(X28))&(~b48_buttercup10421(X29)|k04_buttercup10517(X29))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X28]:(~k04_buttercup10517(X28)|b48_buttercup10421(X28)))&(![X29]:(~b48_buttercup10421(X29)|k04_buttercup10517(X29)))),inference(variable_rename,[status(thm)],[c72])).])).
% 3.37/3.53 cnf(c76,plain,~b48_buttercup10421(X64)|k04_buttercup10517(X64),inference(split_conjunct,[status(thm)],[c74])).
% 3.37/3.53 fof(sos_19,axiom,(~(![X27]:(k04_buttercup10419(X27)<=>b48_buttercup10421(X27)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_19)).
% 3.37/3.53 fof(c77,plain,(?[X27]:((~k04_buttercup10419(X27)|~b48_buttercup10421(X27))&(k04_buttercup10419(X27)|b48_buttercup10421(X27)))),inference(fof_nnf,[status(thm)],[sos_19])).
% 3.37/3.53 fof(c78,plain,(?[X30]:((~k04_buttercup10419(X30)|~b48_buttercup10421(X30))&(k04_buttercup10419(X30)|b48_buttercup10421(X30)))),inference(variable_rename,[status(thm)],[c77])).
% 3.37/3.53 fof(c79,plain,((~k04_buttercup10419(skolem0023)|~b48_buttercup10421(skolem0023))&(k04_buttercup10419(skolem0023)|b48_buttercup10421(skolem0023))),inference(skolemize,[status(esa)],[c78])).
% 3.37/3.53 cnf(c81,plain,k04_buttercup10419(skolem0023)|b48_buttercup10421(skolem0023),inference(split_conjunct,[status(thm)],[c79])).
% 3.37/3.53 cnf(c196,plain,k04_buttercup10419(skolem0023)|k04_buttercup10517(skolem0023),inference(resolution,[status(thm)],[c81, c76])).
% 3.37/3.53 cnf(c263,plain,k04_buttercup10419(skolem0023)|k04_buttercup10516(skolem0023),inference(resolution,[status(thm)],[c196, c176])).
% 3.37/3.53 fof(sos_06,axiom,(![X5]:(b48_buttercup10421(X5)=>b48_buttercup10417(X5))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_06)).
% 3.37/3.53 fof(c159,plain,(![X5]:(~b48_buttercup10421(X5)|b48_buttercup10417(X5))),inference(fof_nnf,[status(thm)],[sos_06])).
% 3.37/3.53 fof(c160,plain,(![X52]:(~b48_buttercup10421(X52)|b48_buttercup10417(X52))),inference(variable_rename,[status(thm)],[c159])).
% 3.37/3.53 cnf(c161,plain,~b48_buttercup10421(X76)|b48_buttercup10417(X76),inference(split_conjunct,[status(thm)],[c160])).
% 3.37/3.53 cnf(c223,plain,b48_buttercup10417(skolem0023)|k04_buttercup10419(skolem0023),inference(resolution,[status(thm)],[c161, c81])).
% 3.37/3.53 fof(sos_35,axiom,(?[X45]:b48_buttercup10519(X45)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_35)).
% 3.37/3.53 fof(c20,plain,(?[X11]:b48_buttercup10519(X11)),inference(variable_rename,[status(thm)],[sos_35])).
% 3.37/3.53 fof(c21,plain,b48_buttercup10519(skolem0006),inference(skolemize,[status(esa)],[c20])).
% 3.37/3.53 cnf(c22,plain,b48_buttercup10519(skolem0006),inference(split_conjunct,[status(thm)],[c21])).
% 3.37/3.53 cnf(c186,plain,~k04_buttercup10225(X84)|~b48_buttercup10519(X84)|~k04_buttercup10225(X85)|b48_buttercup10519(X85)|k04_buttercup10225(skolem0006),inference(resolution,[status(thm)],[c11, c22])).
% 3.37/3.53 cnf(c181,plain,~k04_buttercup10225(skolem0002)|b48_buttercup10519(skolem0002),inference(factor,[status(thm)],[c10])).
% 3.37/3.53 fof(sos_28,axiom,(?[X38]:b48_buttercup10421(X38)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_28)).
% 3.37/3.53 fof(c41,plain,(?[X18]:b48_buttercup10421(X18)),inference(variable_rename,[status(thm)],[sos_28])).
% 3.37/3.53 fof(c42,plain,b48_buttercup10421(skolem0013),inference(skolemize,[status(esa)],[c41])).
% 3.37/3.53 cnf(c43,plain,b48_buttercup10421(skolem0013),inference(split_conjunct,[status(thm)],[c42])).
% 3.37/3.53 cnf(c192,plain,k04_buttercup10517(skolem0013),inference(resolution,[status(thm)],[c76, c43])).
% 3.37/3.53 cnf(c242,plain,k04_buttercup10516(skolem0013),inference(resolution,[status(thm)],[c176, c192])).
% 3.37/3.53 fof(sos_23,axiom,(?[X33]:k04_buttercup10517(X33)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_23)).
% 3.37/3.53 fof(c56,plain,(?[X23]:k04_buttercup10517(X23)),inference(variable_rename,[status(thm)],[sos_23])).
% 3.37/3.53 fof(c57,plain,k04_buttercup10517(skolem0018),inference(skolemize,[status(esa)],[c56])).
% 3.37/3.53 cnf(c58,plain,k04_buttercup10517(skolem0018),inference(split_conjunct,[status(thm)],[c57])).
% 3.37/3.53 cnf(c241,plain,k04_buttercup10516(skolem0018),inference(resolution,[status(thm)],[c176, c58])).
% 3.37/3.53 fof(sos_36,axiom,(?[X46]:b48_buttercup10518(X46)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_36)).
% 3.37/3.53 fof(c17,plain,(?[X10]:b48_buttercup10518(X10)),inference(variable_rename,[status(thm)],[sos_36])).
% 3.37/3.53 fof(c18,plain,b48_buttercup10518(skolem0005),inference(skolemize,[status(esa)],[c17])).
% 3.37/3.53 cnf(c19,plain,b48_buttercup10518(skolem0005),inference(split_conjunct,[status(thm)],[c18])).
% 3.37/3.53 fof(sos_02,axiom,(![X1]:(b48_buttercup10518(X1)=>b48_buttercup10515(X1))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 3.37/3.53 fof(c171,plain,(![X1]:(~b48_buttercup10518(X1)|b48_buttercup10515(X1))),inference(fof_nnf,[status(thm)],[sos_02])).
% 3.37/3.53 fof(c172,plain,(![X56]:(~b48_buttercup10518(X56)|b48_buttercup10515(X56))),inference(variable_rename,[status(thm)],[c171])).
% 3.37/3.53 cnf(c173,plain,~b48_buttercup10518(X80)|b48_buttercup10515(X80),inference(split_conjunct,[status(thm)],[c172])).
% 3.37/3.53 cnf(c237,plain,b48_buttercup10515(skolem0005),inference(resolution,[status(thm)],[c173, c19])).
% 3.37/3.53 cnf(c239,plain,k04_buttercup10516(skolem0005),inference(resolution,[status(thm)],[c237, c95])).
% 3.37/3.53 cnf(c240,plain,b48_buttercup10417(skolem0005),inference(resolution,[status(thm)],[c239, c111])).
% 3.37/3.53 cnf(c232,plain,b48_buttercup10515(skolem0003),inference(resolution,[status(thm)],[c170, c13])).
% 3.37/3.53 cnf(c235,plain,k04_buttercup10516(skolem0003),inference(resolution,[status(thm)],[c232, c95])).
% 3.37/3.53 cnf(c238,plain,b48_buttercup10417(skolem0003),inference(resolution,[status(thm)],[c235, c111])).
% 3.37/3.53 cnf(c230,plain,b48_buttercup10515(skolem0006),inference(resolution,[status(thm)],[c170, c22])).
% 3.37/3.53 cnf(c234,plain,k04_buttercup10516(skolem0006),inference(resolution,[status(thm)],[c230, c95])).
% 3.37/3.53 cnf(c236,plain,b48_buttercup10417(skolem0006),inference(resolution,[status(thm)],[c234, c111])).
% 3.37/3.53 fof(sos_37,axiom,(?[X47]:b48_buttercup10520(X47)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_37)).
% 3.37/3.53 fof(c14,plain,(?[X9]:b48_buttercup10520(X9)),inference(variable_rename,[status(thm)],[sos_37])).
% 3.37/3.53 fof(c15,plain,b48_buttercup10520(skolem0004),inference(skolemize,[status(esa)],[c14])).
% 3.37/3.53 cnf(c16,plain,b48_buttercup10520(skolem0004),inference(split_conjunct,[status(thm)],[c15])).
% 3.37/3.53 fof(sos_04,axiom,(![X3]:(b48_buttercup10520(X3)=>b48_buttercup10515(X3))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 3.37/3.53 fof(c165,plain,(![X3]:(~b48_buttercup10520(X3)|b48_buttercup10515(X3))),inference(fof_nnf,[status(thm)],[sos_04])).
% 3.37/3.53 fof(c166,plain,(![X54]:(~b48_buttercup10520(X54)|b48_buttercup10515(X54))),inference(variable_rename,[status(thm)],[c165])).
% 3.37/3.53 cnf(c167,plain,~b48_buttercup10520(X78)|b48_buttercup10515(X78),inference(split_conjunct,[status(thm)],[c166])).
% 3.37/3.53 cnf(c228,plain,b48_buttercup10515(skolem0004),inference(resolution,[status(thm)],[c167, c16])).
% 3.37/3.53 cnf(c229,plain,k04_buttercup10516(skolem0004),inference(resolution,[status(thm)],[c228, c95])).
% 3.37/3.53 cnf(c233,plain,b48_buttercup10417(skolem0004),inference(resolution,[status(thm)],[c229, c111])).
% 3.37/3.53 fof(sos_26,axiom,(?[X36]:b48_buttercup10521(X36)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_26)).
% 3.37/3.53 fof(c47,plain,(?[X20]:b48_buttercup10521(X20)),inference(variable_rename,[status(thm)],[sos_26])).
% 3.37/3.53 fof(c48,plain,b48_buttercup10521(skolem0015),inference(skolemize,[status(esa)],[c47])).
% 3.37/3.53 cnf(c49,plain,b48_buttercup10521(skolem0015),inference(split_conjunct,[status(thm)],[c48])).
% 3.37/3.53 fof(sos_05,axiom,(![X4]:(b48_buttercup10521(X4)=>b48_buttercup10515(X4))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_05)).
% 3.37/3.53 fof(c162,plain,(![X4]:(~b48_buttercup10521(X4)|b48_buttercup10515(X4))),inference(fof_nnf,[status(thm)],[sos_05])).
% 3.37/3.53 fof(c163,plain,(![X53]:(~b48_buttercup10521(X53)|b48_buttercup10515(X53))),inference(variable_rename,[status(thm)],[c162])).
% 3.37/3.53 cnf(c164,plain,~b48_buttercup10521(X77)|b48_buttercup10515(X77),inference(split_conjunct,[status(thm)],[c163])).
% 3.37/3.53 cnf(c225,plain,b48_buttercup10515(skolem0015),inference(resolution,[status(thm)],[c164, c49])).
% 3.37/3.53 cnf(c226,plain,k04_buttercup10516(skolem0015),inference(resolution,[status(thm)],[c225, c95])).
% 3.37/3.53 cnf(c227,plain,b48_buttercup10417(skolem0015),inference(resolution,[status(thm)],[c226, c111])).
% 3.37/3.53 cnf(c75,plain,~k04_buttercup10517(X63)|b48_buttercup10421(X63),inference(split_conjunct,[status(thm)],[c74])).
% 3.37/3.53 cnf(c191,plain,b48_buttercup10421(skolem0018),inference(resolution,[status(thm)],[c75, c58])).
% 3.37/3.53 cnf(c224,plain,b48_buttercup10417(skolem0018),inference(resolution,[status(thm)],[c161, c191])).
% 3.37/3.53 cnf(c222,plain,b48_buttercup10417(skolem0013),inference(resolution,[status(thm)],[c161, c43])).
% 3.37/3.53 fof(sos_27,axiom,(?[X37]:b48_buttercup10422(X37)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_27)).
% 3.37/3.53 fof(c44,plain,(?[X19]:b48_buttercup10422(X19)),inference(variable_rename,[status(thm)],[sos_27])).
% 3.37/3.53 fof(c45,plain,b48_buttercup10422(skolem0014),inference(skolemize,[status(esa)],[c44])).
% 3.37/3.53 cnf(c46,plain,b48_buttercup10422(skolem0014),inference(split_conjunct,[status(thm)],[c45])).
% 3.37/3.53 fof(sos_07,axiom,(![X6]:(b48_buttercup10422(X6)=>b48_buttercup10417(X6))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 3.37/3.53 fof(c156,plain,(![X6]:(~b48_buttercup10422(X6)|b48_buttercup10417(X6))),inference(fof_nnf,[status(thm)],[sos_07])).
% 3.37/3.53 fof(c157,plain,(![X51]:(~b48_buttercup10422(X51)|b48_buttercup10417(X51))),inference(variable_rename,[status(thm)],[c156])).
% 3.37/3.53 cnf(c158,plain,~b48_buttercup10422(X75)|b48_buttercup10417(X75),inference(split_conjunct,[status(thm)],[c157])).
% 3.37/3.53 cnf(c221,plain,b48_buttercup10417(skolem0014),inference(resolution,[status(thm)],[c158, c46])).
% 3.37/3.53 fof(sos_08,axiom,(![X7]:(b48_buttercup10227(X7)=>b48_buttercup10222(X7))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 3.37/3.53 fof(c153,plain,(![X7]:(~b48_buttercup10227(X7)|b48_buttercup10222(X7))),inference(fof_nnf,[status(thm)],[sos_08])).
% 3.37/3.53 fof(c154,plain,(![X50]:(~b48_buttercup10227(X50)|b48_buttercup10222(X50))),inference(variable_rename,[status(thm)],[c153])).
% 3.37/3.53 cnf(c155,plain,~b48_buttercup10227(X74)|b48_buttercup10222(X74),inference(split_conjunct,[status(thm)],[c154])).
% 3.37/3.53 fof(sos_34,axiom,(?[X44]:b48_buttercup10228(X44)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_34)).
% 3.37/3.53 fof(c23,plain,(?[X12]:b48_buttercup10228(X12)),inference(variable_rename,[status(thm)],[sos_34])).
% 3.37/3.53 fof(c24,plain,b48_buttercup10228(skolem0007),inference(skolemize,[status(esa)],[c23])).
% 3.37/3.53 cnf(c25,plain,b48_buttercup10228(skolem0007),inference(split_conjunct,[status(thm)],[c24])).
% 3.37/3.53 fof(sos_09,axiom,(![X8]:(b48_buttercup10228(X8)=>b48_buttercup10222(X8))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_09)).
% 3.37/3.53 fof(c150,plain,(![X8]:(~b48_buttercup10228(X8)|b48_buttercup10222(X8))),inference(fof_nnf,[status(thm)],[sos_09])).
% 3.37/3.53 fof(c151,plain,(![X49]:(~b48_buttercup10228(X49)|b48_buttercup10222(X49))),inference(variable_rename,[status(thm)],[c150])).
% 3.37/3.53 cnf(c152,plain,~b48_buttercup10228(X73)|b48_buttercup10222(X73),inference(split_conjunct,[status(thm)],[c151])).
% 3.37/3.53 cnf(c219,plain,b48_buttercup10222(skolem0007),inference(resolution,[status(thm)],[c152, c25])).
% 3.37/3.53 fof(sos_11,axiom,((![X10]:(b48_buttercup10422(X10)=>k04_buttercup10419(X10)))&(?[X11]:(k04_buttercup10419(X11)&(~b48_buttercup10422(X11))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_11)).
% 3.37/3.53 fof(c139,plain,((![X10]:(b48_buttercup10422(X10)=>k04_buttercup10419(X10)))&(?[X11]:(k04_buttercup10419(X11)&~b48_buttercup10422(X11)))),inference(fof_simplification,[status(thm)],[sos_11])).
% 3.37/3.53 fof(c140,plain,((![X10]:(~b48_buttercup10422(X10)|k04_buttercup10419(X10)))&(?[X11]:(k04_buttercup10419(X11)&~b48_buttercup10422(X11)))),inference(fof_nnf,[status(thm)],[c139])).
% 3.37/3.53 fof(c141,plain,((![X46]:(~b48_buttercup10422(X46)|k04_buttercup10419(X46)))&(?[X47]:(k04_buttercup10419(X47)&~b48_buttercup10422(X47)))),inference(variable_rename,[status(thm)],[c140])).
% 3.37/3.53 fof(c143,plain,(![X46]:((~b48_buttercup10422(X46)|k04_buttercup10419(X46))&(k04_buttercup10419(skolem0033)&~b48_buttercup10422(skolem0033)))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X46]:(~b48_buttercup10422(X46)|k04_buttercup10419(X46)))&(k04_buttercup10419(skolem0033)&~b48_buttercup10422(skolem0033))),inference(skolemize,[status(esa)],[c141])).])).
% 3.37/3.53 cnf(c144,plain,~b48_buttercup10422(X71)|k04_buttercup10419(X71),inference(split_conjunct,[status(thm)],[c143])).
% 3.37/3.53 cnf(c217,plain,k04_buttercup10419(skolem0014),inference(resolution,[status(thm)],[c144, c46])).
% 3.37/3.53 fof(sos_10,axiom,(![X9]:(b48_buttercup10229(X9)=>b48_buttercup10222(X9))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_10)).
% 3.37/3.53 fof(c147,plain,(![X9]:(~b48_buttercup10229(X9)|b48_buttercup10222(X9))),inference(fof_nnf,[status(thm)],[sos_10])).
% 3.37/3.53 fof(c148,plain,(![X48]:(~b48_buttercup10229(X48)|b48_buttercup10222(X48))),inference(variable_rename,[status(thm)],[c147])).
% 3.37/3.53 cnf(c149,plain,~b48_buttercup10229(X72)|b48_buttercup10222(X72),inference(split_conjunct,[status(thm)],[c148])).
% 3.37/3.53 fof(sos_18,axiom,((![X25]:(k04_buttercup10225(X25)=>b48_buttercup10222(X25)))&(?[X26]:(b48_buttercup10222(X26)&(~k04_buttercup10225(X26))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_18)).
% 3.37/3.53 fof(c82,plain,((![X25]:(k04_buttercup10225(X25)=>b48_buttercup10222(X25)))&(?[X26]:(b48_buttercup10222(X26)&~k04_buttercup10225(X26)))),inference(fof_simplification,[status(thm)],[sos_18])).
% 3.37/3.53 fof(c83,plain,((![X25]:(~k04_buttercup10225(X25)|b48_buttercup10222(X25)))&(?[X26]:(b48_buttercup10222(X26)&~k04_buttercup10225(X26)))),inference(fof_nnf,[status(thm)],[c82])).
% 3.37/3.53 fof(c84,plain,((![X31]:(~k04_buttercup10225(X31)|b48_buttercup10222(X31)))&(?[X32]:(b48_buttercup10222(X32)&~k04_buttercup10225(X32)))),inference(variable_rename,[status(thm)],[c83])).
% 3.37/3.53 fof(c86,plain,(![X31]:((~k04_buttercup10225(X31)|b48_buttercup10222(X31))&(b48_buttercup10222(skolem0024)&~k04_buttercup10225(skolem0024)))),inference(shift_quantors,[status(thm)],[fof(c85,plain,((![X31]:(~k04_buttercup10225(X31)|b48_buttercup10222(X31)))&(b48_buttercup10222(skolem0024)&~k04_buttercup10225(skolem0024))),inference(skolemize,[status(esa)],[c84])).])).
% 3.37/3.53 cnf(c87,plain,~k04_buttercup10225(X65)|b48_buttercup10222(X65),inference(split_conjunct,[status(thm)],[c86])).
% 3.37/3.53 cnf(c214,plain,b48_buttercup10222(skolem0012),inference(resolution,[status(thm)],[c213, c87])).
% 3.37/3.53 fof(sos_13,axiom,((![X14]:(b48_buttercup10228(X14)=>k04_buttercup10419(X14)))&(?[X15]:(k04_buttercup10419(X15)&(~b48_buttercup10228(X15))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_13)).
% 3.37/3.53 fof(c123,plain,((![X14]:(b48_buttercup10228(X14)=>k04_buttercup10419(X14)))&(?[X15]:(k04_buttercup10419(X15)&~b48_buttercup10228(X15)))),inference(fof_simplification,[status(thm)],[sos_13])).
% 3.37/3.53 fof(c124,plain,((![X14]:(~b48_buttercup10228(X14)|k04_buttercup10419(X14)))&(?[X15]:(k04_buttercup10419(X15)&~b48_buttercup10228(X15)))),inference(fof_nnf,[status(thm)],[c123])).
% 3.37/3.53 fof(c125,plain,((![X42]:(~b48_buttercup10228(X42)|k04_buttercup10419(X42)))&(?[X43]:(k04_buttercup10419(X43)&~b48_buttercup10228(X43)))),inference(variable_rename,[status(thm)],[c124])).
% 3.37/3.53 fof(c127,plain,(![X42]:((~b48_buttercup10228(X42)|k04_buttercup10419(X42))&(k04_buttercup10419(skolem0031)&~b48_buttercup10228(skolem0031)))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((![X42]:(~b48_buttercup10228(X42)|k04_buttercup10419(X42)))&(k04_buttercup10419(skolem0031)&~b48_buttercup10228(skolem0031))),inference(skolemize,[status(esa)],[c125])).])).
% 3.37/3.53 cnf(c128,plain,~b48_buttercup10228(X69)|k04_buttercup10419(X69),inference(split_conjunct,[status(thm)],[c127])).
% 3.37/3.53 cnf(c212,plain,k04_buttercup10419(skolem0007),inference(resolution,[status(thm)],[c128, c25])).
% 3.37/3.53 cnf(c209,plain,b48_buttercup10222(skolem0011),inference(resolution,[status(thm)],[c205, c87])).
% 3.37/3.53 cnf(c96,plain,k04_buttercup10516(skolem0025),inference(split_conjunct,[status(thm)],[c94])).
% 3.37/3.53 cnf(c208,plain,b48_buttercup10417(skolem0025),inference(resolution,[status(thm)],[c111, c96])).
% 3.37/3.53 fof(sos_24,axiom,(?[X34]:k04_buttercup10516(X34)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_24)).
% 3.37/3.53 fof(c53,plain,(?[X22]:k04_buttercup10516(X22)),inference(variable_rename,[status(thm)],[sos_24])).
% 3.37/3.53 fof(c54,plain,k04_buttercup10516(skolem0017),inference(skolemize,[status(esa)],[c53])).
% 3.37/3.53 cnf(c55,plain,k04_buttercup10516(skolem0017),inference(split_conjunct,[status(thm)],[c54])).
% 3.37/3.53 cnf(c207,plain,b48_buttercup10417(skolem0017),inference(resolution,[status(thm)],[c111, c55])).
% 3.37/3.53 fof(sos_33,axiom,(?[X43]:b48_buttercup10515(X43)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_33)).
% 3.37/3.53 fof(c26,plain,(?[X13]:b48_buttercup10515(X13)),inference(variable_rename,[status(thm)],[sos_33])).
% 3.37/3.53 fof(c27,plain,b48_buttercup10515(skolem0008),inference(skolemize,[status(esa)],[c26])).
% 3.37/3.53 cnf(c28,plain,b48_buttercup10515(skolem0008),inference(split_conjunct,[status(thm)],[c27])).
% 3.37/3.53 cnf(c204,plain,k04_buttercup10516(skolem0008),inference(resolution,[status(thm)],[c95, c28])).
% 3.37/3.53 cnf(c206,plain,b48_buttercup10417(skolem0008),inference(resolution,[status(thm)],[c111, c204])).
% 3.37/3.53 cnf(c202,plain,b48_buttercup10222(skolem0026),inference(resolution,[status(thm)],[c87, c104])).
% 3.37/3.53 cnf(c201,plain,b48_buttercup10222(skolem0019),inference(resolution,[status(thm)],[c87, c61])).
% 3.37/3.53 cnf(c200,plain,b48_buttercup10222(skolem0003),inference(resolution,[status(thm)],[c87, c12])).
% 3.37/3.53 cnf(c199,plain,b48_buttercup10222(skolem0032),inference(resolution,[status(thm)],[c87, c137])).
% 3.37/3.53 cnf(c146,plain,~b48_buttercup10422(skolem0033),inference(split_conjunct,[status(thm)],[c143])).
% 3.37/3.53 cnf(c145,plain,k04_buttercup10419(skolem0033),inference(split_conjunct,[status(thm)],[c143])).
% 3.37/3.53 cnf(c138,plain,~b48_buttercup10227(skolem0032),inference(split_conjunct,[status(thm)],[c135])).
% 3.37/3.53 cnf(c80,plain,~k04_buttercup10419(skolem0023)|~b48_buttercup10421(skolem0023),inference(split_conjunct,[status(thm)],[c79])).
% 3.37/3.53 cnf(c130,plain,~b48_buttercup10228(skolem0031),inference(split_conjunct,[status(thm)],[c127])).
% 3.37/3.53 cnf(c129,plain,k04_buttercup10419(skolem0031),inference(split_conjunct,[status(thm)],[c127])).
% 3.37/3.53 fof(sos_14,axiom,(?[X16]:(?[X17]:(?[X18]:(((((k04_buttercup10419(X16)&b48_buttercup10222(X16))&k04_buttercup10419(X17))&(~b48_buttercup10222(X17)))&(~k04_buttercup10419(X18)))&b48_buttercup10222(X18))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_14)).
% 3.37/3.53 fof(c114,plain,(?[X16]:(?[X17]:(?[X18]:(((((k04_buttercup10419(X16)&b48_buttercup10222(X16))&k04_buttercup10419(X17))&~b48_buttercup10222(X17))&~k04_buttercup10419(X18))&b48_buttercup10222(X18))))),inference(fof_simplification,[status(thm)],[sos_14])).
% 3.37/3.53 fof(c115,plain,(?[X39]:(?[X40]:(?[X41]:(((((k04_buttercup10419(X39)&b48_buttercup10222(X39))&k04_buttercup10419(X40))&~b48_buttercup10222(X40))&~k04_buttercup10419(X41))&b48_buttercup10222(X41))))),inference(variable_rename,[status(thm)],[c114])).
% 3.37/3.53 fof(c116,plain,(((((k04_buttercup10419(skolem0028)&b48_buttercup10222(skolem0028))&k04_buttercup10419(skolem0029))&~b48_buttercup10222(skolem0029))&~k04_buttercup10419(skolem0030))&b48_buttercup10222(skolem0030)),inference(skolemize,[status(esa)],[c115])).
% 3.37/3.53 cnf(c122,plain,b48_buttercup10222(skolem0030),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c121,plain,~k04_buttercup10419(skolem0030),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c120,plain,~b48_buttercup10222(skolem0029),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c119,plain,k04_buttercup10419(skolem0029),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c118,plain,b48_buttercup10222(skolem0028),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c117,plain,k04_buttercup10419(skolem0028),inference(split_conjunct,[status(thm)],[c116])).
% 3.37/3.53 cnf(c113,plain,~k04_buttercup10516(skolem0027),inference(split_conjunct,[status(thm)],[c110])).
% 3.37/3.53 cnf(c112,plain,b48_buttercup10417(skolem0027),inference(split_conjunct,[status(thm)],[c110])).
% 3.37/3.53 cnf(c105,plain,~b48_buttercup10229(skolem0026),inference(split_conjunct,[status(thm)],[c102])).
% 3.37/3.53 cnf(c97,plain,~b48_buttercup10515(skolem0025),inference(split_conjunct,[status(thm)],[c94])).
% 3.37/3.53 cnf(c89,plain,~k04_buttercup10225(skolem0024),inference(split_conjunct,[status(thm)],[c86])).
% 3.37/3.53 cnf(c88,plain,b48_buttercup10222(skolem0024),inference(split_conjunct,[status(thm)],[c86])).
% 3.37/3.53 fof(sos_21,axiom,(?[X29]:(?[X30]:(?[X31]:(((((k04_buttercup10419(X29)&b48_buttercup10417(X29))&k04_buttercup10419(X30))&(~b48_buttercup10417(X30)))&(~k04_buttercup10419(X31)))&b48_buttercup10417(X31))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_21)).
% 3.37/3.53 fof(c62,plain,(?[X29]:(?[X30]:(?[X31]:(((((k04_buttercup10419(X29)&b48_buttercup10417(X29))&k04_buttercup10419(X30))&~b48_buttercup10417(X30))&~k04_buttercup10419(X31))&b48_buttercup10417(X31))))),inference(fof_simplification,[status(thm)],[sos_21])).
% 3.37/3.53 fof(c63,plain,(?[X25]:(?[X26]:(?[X27]:(((((k04_buttercup10419(X25)&b48_buttercup10417(X25))&k04_buttercup10419(X26))&~b48_buttercup10417(X26))&~k04_buttercup10419(X27))&b48_buttercup10417(X27))))),inference(variable_rename,[status(thm)],[c62])).
% 3.37/3.53 fof(c64,plain,(((((k04_buttercup10419(skolem0020)&b48_buttercup10417(skolem0020))&k04_buttercup10419(skolem0021))&~b48_buttercup10417(skolem0021))&~k04_buttercup10419(skolem0022))&b48_buttercup10417(skolem0022)),inference(skolemize,[status(esa)],[c63])).
% 3.37/3.53 cnf(c70,plain,b48_buttercup10417(skolem0022),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 cnf(c69,plain,~k04_buttercup10419(skolem0022),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 cnf(c68,plain,~b48_buttercup10417(skolem0021),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 cnf(c67,plain,k04_buttercup10419(skolem0021),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 cnf(c66,plain,b48_buttercup10417(skolem0020),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 cnf(c65,plain,k04_buttercup10419(skolem0020),inference(split_conjunct,[status(thm)],[c64])).
% 3.37/3.53 fof(sos_25,axiom,(?[X35]:k04_buttercup10419(X35)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_25)).
% 3.37/3.53 fof(c50,plain,(?[X21]:k04_buttercup10419(X21)),inference(variable_rename,[status(thm)],[sos_25])).
% 3.37/3.53 fof(c51,plain,k04_buttercup10419(skolem0016),inference(skolemize,[status(esa)],[c50])).
% 3.37/3.53 cnf(c52,plain,k04_buttercup10419(skolem0016),inference(split_conjunct,[status(thm)],[c51])).
% 3.37/3.53 fof(sos_31,axiom,(?[X41]:b48_buttercup10417(X41)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_31)).
% 3.37/3.53 fof(c32,plain,(?[X15]:b48_buttercup10417(X15)),inference(variable_rename,[status(thm)],[sos_31])).
% 3.37/3.53 fof(c33,plain,b48_buttercup10417(skolem0010),inference(skolemize,[status(esa)],[c32])).
% 3.37/3.53 cnf(c34,plain,b48_buttercup10417(skolem0010),inference(split_conjunct,[status(thm)],[c33])).
% 3.37/3.53 fof(sos_32,axiom,(?[X42]:b48_buttercup10222(X42)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 3.37/3.53 fof(c29,plain,(?[X14]:b48_buttercup10222(X14)),inference(variable_rename,[status(thm)],[sos_32])).
% 3.37/3.53 fof(c30,plain,b48_buttercup10222(skolem0009),inference(skolemize,[status(esa)],[c29])).
% 3.37/3.53 cnf(c31,plain,b48_buttercup10222(skolem0009),inference(split_conjunct,[status(thm)],[c30])).
% 3.37/3.53 % SZS output end Saturation
% 3.37/3.53
% 3.37/3.53 % Initial clauses : 70
% 3.37/3.53 % Processed clauses : 399
% 3.37/3.53 % Factors computed : 22
% 3.37/3.53 % Resolvents computed: 3568
% 3.37/3.53 % Tautologies deleted: 475
% 3.37/3.53 % Forward subsumed : 2786
% 3.37/3.53 % Backward subsumed : 263
% 3.37/3.53 % -------- CPU Time ---------
% 3.37/3.53 % User time : 3.165 s
% 3.37/3.53 % System time : 0.027 s
% 3.37/3.53 % Total time : 3.192 s
%------------------------------------------------------------------------------