%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO117-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:21:06 EDT 2024
% Result : Unsatisfiable 127.86s 128.03s
% Output : Refutation 127.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 5
% Syntax : Number of clauses : 10 ( 6 unt; 0 nHn; 9 RR)
% Number of literals : 15 ( 3 equ; 7 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-4 aty)
% Number of variables : 15 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(between_c_defn_1,axiom,
( ~ between_c(X70,X71,X69,X68)
| X71 != X68 ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-1.ax',between_c_defn_1) ).
cnf(theorem_4_4_133,negated_conjecture,
ordered_by(sk25,sk26,sk26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',theorem_4_4_133) ).
cnf(between_o_defn_5,axiom,
( ~ ordered_by(X476,X477,X475)
| ~ ordered_by(X476,X475,X474)
| between_o(X476,X477,X475,X474) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-2.ax',between_o_defn_5) ).
cnf(c1067,plain,
( ~ ordered_by(X541,X542,X542)
| between_o(X541,X542,X542,X542) ),
inference(factor,[status(thm)],[between_o_defn_5]) ).
cnf(c1182,plain,
between_o(sk25,sk26,sk26,sk26),
inference(resolution,[status(thm)],[c1067,theorem_4_4_133]) ).
cnf(o3_24,axiom,
( ~ between_o(X611,X612,X610,X609)
| between_c(ax2_sk4(X611,X609,X610,X612),X612,X610,X609) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO004-2.ax',o3_24) ).
cnf(c1363,plain,
between_c(ax2_sk4(sk25,sk26,sk26,sk26),sk26,sk26,sk26),
inference(resolution,[status(thm)],[o3_24,c1182]) ).
cnf(c116184,plain,
sk26 != sk26,
inference(resolution,[status(thm)],[c1363,between_c_defn_1]) ).
cnf(c116228,plain,
$false,
inference(resolution,[status(thm)],[c116184,reflexivity]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO117-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:10:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 127.86/128.03 % Version: 1.5
% 127.86/128.03 % SZS status Unsatisfiable
% 127.86/128.03 % SZS output start CNFRefutation
% See solution above
% 127.86/128.03
% 127.86/128.03 % Initial clauses : 139
% 127.86/128.03 % Processed clauses : 2005
% 127.86/128.03 % Factors computed : 235
% 127.86/128.03 % Resolvents computed: 115957
% 127.86/128.03 % Tautologies deleted: 51
% 127.86/128.03 % Forward subsumed : 3903
% 127.86/128.03 % Backward subsumed : 74
% 127.86/128.03 % -------- CPU Time ---------
% 127.86/128.03 % User time : 127.385 s
% 127.86/128.03 % System time : 0.291 s
% 127.86/128.03 % Total time : 127.676 s
%------------------------------------------------------------------------------