%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN348-1 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:47:59 EDT 2024
% Result : Satisfiable 0.45s 0.65s
% Output : Saturation 0.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause16,negated_conjecture,
( ~ f(X65,g(X65,X64))
| ~ f(g(X65,X64),X64)
| ~ f(X64,g(X65,X64))
| ~ f(g(X65,X64),X65)
| ~ f(w(X65),g(X65,X64))
| ~ f(g(X65,X64),w(X65)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c85,plain,
( ~ f(X67,g(X67,w(X67)))
| ~ f(g(X67,w(X67)),w(X67))
| ~ f(w(X67),g(X67,w(X67)))
| ~ f(g(X67,w(X67)),X67) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(clause15,negated_conjecture,
( ~ f(X58,g(X58,X57))
| ~ f(g(X58,X57),X57)
| ~ f(X57,g(X58,X57))
| ~ f(g(X58,X57),X58)
| f(w(X58),g(X58,X57))
| f(g(X58,X57),w(X58)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c77,plain,
( ~ f(X59,g(X59,X59))
| ~ f(g(X59,X59),X59)
| f(w(X59),g(X59,X59))
| f(g(X59,X59),w(X59)) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(clause14,negated_conjecture,
( f(X56,g(X56,X55))
| f(g(X56,X55),X55)
| ~ f(X55,g(X56,X55))
| ~ f(g(X56,X55),X56)
| f(w(X56),g(X56,X55))
| ~ f(g(X56,X55),w(X56)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,negated_conjecture,
( f(X50,g(X50,X49))
| f(g(X50,X49),X49)
| ~ f(X49,g(X50,X49))
| ~ f(g(X50,X49),X50)
| ~ f(w(X50),g(X50,X49))
| f(g(X50,X49),w(X50)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c65,plain,
( f(X53,g(X53,w(X53)))
| f(g(X53,w(X53)),w(X53))
| ~ f(w(X53),g(X53,w(X53)))
| ~ f(g(X53,w(X53)),X53) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(clause12,negated_conjecture,
( f(X46,g(X46,X45))
| ~ f(g(X46,X45),X45)
| f(X45,g(X46,X45))
| ~ f(g(X46,X45),X46)
| f(w(X46),g(X46,X45))
| ~ f(g(X46,X45),w(X46)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c57,plain,
( f(X48,g(X48,w(X48)))
| ~ f(g(X48,w(X48)),w(X48))
| f(w(X48),g(X48,w(X48)))
| ~ f(g(X48,w(X48)),X48) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(clause11,negated_conjecture,
( f(X43,g(X43,X42))
| ~ f(g(X43,X42),X42)
| f(X42,g(X43,X42))
| ~ f(g(X43,X42),X43)
| ~ f(w(X43),g(X43,X42))
| f(g(X43,X42),w(X43)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,negated_conjecture,
( ~ f(X41,g(X41,X40))
| f(g(X41,X40),X40)
| f(X40,g(X41,X40))
| ~ f(g(X41,X40),X41)
| ~ f(w(X41),g(X41,X40))
| ~ f(g(X41,X40),w(X41)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(clause8,negated_conjecture,
( ~ f(X31,g(X31,X30))
| ~ f(g(X31,X30),X30)
| f(X30,g(X31,X30))
| f(g(X31,X30),X31)
| f(w(X31),g(X31,X30))
| ~ f(g(X31,X30),w(X31)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c37,plain,
( ~ f(X37,g(X37,w(X37)))
| ~ f(g(X37,w(X37)),w(X37))
| f(w(X37),g(X37,w(X37)))
| f(g(X37,w(X37)),X37) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(clause9,negated_conjecture,
( ~ f(X34,g(X34,X33))
| f(g(X34,X33),X33)
| f(X33,g(X34,X33))
| ~ f(g(X34,X33),X34)
| f(w(X34),g(X34,X33))
| f(g(X34,X33),w(X34)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause7,negated_conjecture,
( ~ f(X26,g(X26,X25))
| ~ f(g(X26,X25),X25)
| f(X25,g(X26,X25))
| f(g(X26,X25),X26)
| ~ f(w(X26),g(X26,X25))
| f(g(X26,X25),w(X26)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause5,negated_conjecture,
( f(X12,g(X12,X11))
| f(g(X12,X11),X11)
| f(X11,g(X12,X11))
| f(g(X12,X11),X12)
| f(w(X12),g(X12,X11))
| f(g(X12,X11),w(X12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c4,plain,
( f(X23,g(X23,w(X23)))
| f(g(X23,w(X23)),w(X23))
| f(w(X23),g(X23,w(X23)))
| f(g(X23,w(X23)),X23) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(clause4,negated_conjecture,
( f(X10,g(X10,X9))
| ~ f(g(X10,X9),X9)
| ~ f(X9,g(X10,X9))
| f(g(X10,X9),X10)
| ~ f(w(X10),g(X10,X9))
| ~ f(g(X10,X9),w(X10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c1,plain,
( f(X22,g(X22,w(X22)))
| ~ f(g(X22,w(X22)),w(X22))
| ~ f(w(X22),g(X22,w(X22)))
| f(g(X22,w(X22)),X22) ),
inference(factor,[status(thm)],[clause4]) ).
cnf(clause6,negated_conjecture,
( f(X19,g(X19,X18))
| f(g(X19,X18),X18)
| f(X18,g(X19,X18))
| f(g(X19,X18),X19)
| ~ f(w(X19),g(X19,X18))
| ~ f(g(X19,X18),w(X19)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c2,plain,
( f(X13,g(X13,X13))
| f(g(X13,X13),X13)
| f(w(X13),g(X13,X13))
| f(g(X13,X13),w(X13)) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(clause3,negated_conjecture,
( f(X8,g(X8,X7))
| ~ f(g(X8,X7),X7)
| ~ f(X7,g(X8,X7))
| f(g(X8,X7),X8)
| f(w(X8),g(X8,X7))
| f(g(X8,X7),w(X8)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(clause2,negated_conjecture,
( ~ f(X6,g(X6,X5))
| f(g(X6,X5),X5)
| ~ f(X5,g(X6,X5))
| f(g(X6,X5),X6)
| f(w(X6),g(X6,X5))
| ~ f(g(X6,X5),w(X6)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,negated_conjecture,
( ~ f(X3,g(X3,X2))
| f(g(X3,X2),X2)
| ~ f(X2,g(X3,X2))
| f(g(X3,X2),X3)
| ~ f(w(X3),g(X3,X2))
| f(g(X3,X2),w(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(c0,plain,
( ~ f(X4,g(X4,w(X4)))
| f(g(X4,w(X4)),w(X4))
| ~ f(w(X4),g(X4,w(X4)))
| f(g(X4,w(X4)),X4) ),
inference(factor,[status(thm)],[clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN348-1 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 20:31:23 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.45/0.65 % Version: 1.5
% 0.45/0.65 % SZS status Satisfiable
% 0.45/0.65 % SZS output start Saturation
% See solution above
% 0.45/0.65
% 0.45/0.65 % Initial clauses : 16
% 0.45/0.65 % Processed clauses : 25
% 0.45/0.65 % Factors computed : 11
% 0.45/0.65 % Resolvents computed: 82
% 0.45/0.65 % Tautologies deleted: 82
% 0.45/0.65 % Forward subsumed : 2
% 0.45/0.65 % Backward subsumed : 0
% 0.45/0.65 % -------- CPU Time ---------
% 0.45/0.65 % User time : 0.275 s
% 0.45/0.65 % System time : 0.019 s
% 0.45/0.65 % Total time : 0.294 s
%------------------------------------------------------------------------------