%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN726+1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:48:44 EDT 2024
% Result : Theorem 0.48s 0.69s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SYN726+1 : TPTP v8.1.2. Released v2.5.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 20:24:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.48/0.69 % Version: 1.5
% 0.48/0.69 % SZS status Theorem
% 0.48/0.69 % SZS output start CNFRefutation
% 0.48/0.69 fof(thm400,conjecture,((((((![X]:(![Y]:(![Z]:((p(X,Y)&p(Y,Z))=>p(X,Z)))))&(![X]:(![Y]:(![Z]:((q(X,Y)&q(Y,Z))=>q(X,Z))))))&(![X]:(![Y]:(q(X,Y)=>q(Y,X)))))&(![X]:(![Y]:(p(X,Y)|q(X,Y)))))=>(![X]:(![Y]:p(X,Y))))|(![X]:(![Y]:q(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thm400)).
% 0.48/0.69 fof(c0,negated_conjecture,(~((((((![X]:(![Y]:(![Z]:((p(X,Y)&p(Y,Z))=>p(X,Z)))))&(![X]:(![Y]:(![Z]:((q(X,Y)&q(Y,Z))=>q(X,Z))))))&(![X]:(![Y]:(q(X,Y)=>q(Y,X)))))&(![X]:(![Y]:(p(X,Y)|q(X,Y)))))=>(![X]:(![Y]:p(X,Y))))|(![X]:(![Y]:q(X,Y))))),inference(assume_negation,[status(cth)],[thm400])).
% 0.48/0.69 fof(c1,negated_conjecture,((((((![X]:(![Y]:(![Z]:((~p(X,Y)|~p(Y,Z))|p(X,Z)))))&(![X]:(![Y]:(![Z]:((~q(X,Y)|~q(Y,Z))|q(X,Z))))))&(![X]:(![Y]:(~q(X,Y)|q(Y,X)))))&(![X]:(![Y]:(p(X,Y)|q(X,Y)))))&(?[X]:(?[Y]:~p(X,Y))))&(?[X]:(?[Y]:~q(X,Y)))),inference(fof_nnf,[status(thm)],[c0])).
% 0.48/0.69 fof(c2,negated_conjecture,((((((![X2]:(![X3]:(![X4]:((~p(X2,X3)|~p(X3,X4))|p(X2,X4)))))&(![X5]:(![X6]:(![X7]:((~q(X5,X6)|~q(X6,X7))|q(X5,X7))))))&(![X8]:(![X9]:(~q(X8,X9)|q(X9,X8)))))&(![X10]:(![X11]:(p(X10,X11)|q(X10,X11)))))&(?[X12]:(?[X13]:~p(X12,X13))))&(?[X14]:(?[X15]:~q(X14,X15)))),inference(variable_rename,[status(thm)],[c1])).
% 0.48/0.69 fof(c4,negated_conjecture,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(((((((~p(X2,X3)|~p(X3,X4))|p(X2,X4))&((~q(X5,X6)|~q(X6,X7))|q(X5,X7)))&(~q(X8,X9)|q(X9,X8)))&(p(X10,X11)|q(X10,X11)))&~p(skolem0001,skolem0002))&~q(skolem0003,skolem0004)))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,((((((![X2]:(![X3]:(![X4]:((~p(X2,X3)|~p(X3,X4))|p(X2,X4)))))&(![X5]:(![X6]:(![X7]:((~q(X5,X6)|~q(X6,X7))|q(X5,X7))))))&(![X8]:(![X9]:(~q(X8,X9)|q(X9,X8)))))&(![X10]:(![X11]:(p(X10,X11)|q(X10,X11)))))&~p(skolem0001,skolem0002))&~q(skolem0003,skolem0004)),inference(skolemize,[status(esa)],[c2])).])).
% 0.48/0.69 cnf(c10,negated_conjecture,~q(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c7,negated_conjecture,~q(X17,X16)|q(X16,X17),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c9,negated_conjecture,~p(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c8,negated_conjecture,p(X19,X18)|q(X19,X18),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c11,plain,q(skolem0001,skolem0002),inference(resolution,[status(thm)],[c8, c9])).
% 0.48/0.69 cnf(c14,plain,q(skolem0002,skolem0001),inference(resolution,[status(thm)],[c11, c7])).
% 0.48/0.69 cnf(c6,negated_conjecture,~q(X26,X25)|~q(X25,X27)|q(X26,X27),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c27,plain,~q(X37,skolem0002)|q(X37,skolem0001),inference(resolution,[status(thm)],[c6, c14])).
% 0.48/0.69 cnf(c12,plain,p(X24,X23)|q(X23,X24),inference(resolution,[status(thm)],[c8, c7])).
% 0.48/0.69 cnf(c5,negated_conjecture,~p(X20,X21)|~p(X21,X22)|p(X20,X22),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.69 cnf(c16,plain,~p(X35,X33)|p(X35,X34)|q(X33,X34),inference(resolution,[status(thm)],[c5, c8])).
% 0.48/0.69 cnf(c34,plain,p(X53,X54)|q(X55,X54)|q(X55,X53),inference(resolution,[status(thm)],[c16, c12])).
% 0.48/0.69 cnf(c118,plain,q(X121,skolem0002)|q(X121,skolem0001),inference(resolution,[status(thm)],[c34, c9])).
% 0.48/0.69 cnf(c448,plain,q(X122,skolem0001),inference(resolution,[status(thm)],[c118, c27])).
% 0.48/0.69 cnf(c459,plain,q(skolem0001,X126),inference(resolution,[status(thm)],[c448, c7])).
% 0.48/0.69 cnf(c485,plain,~q(X153,skolem0001)|q(X153,X154),inference(resolution,[status(thm)],[c459, c6])).
% 0.48/0.69 cnf(c590,plain,q(X156,X155),inference(resolution,[status(thm)],[c485, c448])).
% 0.48/0.69 cnf(c596,plain,$false,inference(resolution,[status(thm)],[c590, c10])).
% 0.48/0.69 % SZS output end CNFRefutation
% 0.48/0.69
% 0.48/0.69 % Initial clauses : 6
% 0.48/0.69 % Processed clauses : 69
% 0.48/0.69 % Factors computed : 10
% 0.48/0.69 % Resolvents computed: 576
% 0.48/0.69 % Tautologies deleted: 6
% 0.48/0.69 % Forward subsumed : 55
% 0.48/0.69 % Backward subsumed : 61
% 0.48/0.69 % -------- CPU Time ---------
% 0.48/0.69 % User time : 0.302 s
% 0.48/0.69 % System time : 0.023 s
% 0.48/0.69 % Total time : 0.325 s
%------------------------------------------------------------------------------