%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO024-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:20:48 EDT 2024
% Result : Unsatisfiable 14.68s 14.88s
% Output : Refutation 14.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of clauses : 23 ( 12 unt; 0 nHn; 13 RR)
% Number of literals : 45 ( 21 equ; 23 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-4 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-4 aty)
% Number of variables : 90 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_congruence,negated_conjecture,
~ equidistant(u,u,v,v),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_congruence) ).
cnf(transitivity_for_equidistance,axiom,
( ~ equidistant(X8,X10,X9,X5)
| ~ equidistant(X8,X10,X7,X6)
| equidistant(X9,X5,X7,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',transitivity_for_equidistance) ).
cnf(segment_construction2,axiom,
equidistant(X25,extension(X26,X25,X27,X24),X27,X24),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',segment_construction2) ).
cnf(c11,plain,
( ~ equidistant(X280,extension(X279,X280,X284,X281),X282,X283)
| equidistant(X282,X283,X284,X281) ),
inference(resolution,[status(thm)],[segment_construction2,transitivity_for_equidistance]) ).
cnf(symmetry,axiom,
( X12 != X11
| X11 = X12 ),
theory(equality) ).
cnf(identity_for_equidistance,axiom,
( ~ equidistant(X18,X17,X16,X16)
| X18 = X17 ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).
cnf(c12,plain,
X28 = extension(X30,X28,X29,X29),
inference(resolution,[status(thm)],[segment_construction2,identity_for_equidistance]) ).
cnf(c13,plain,
extension(X31,X32,X33,X33) = X32,
inference(resolution,[status(thm)],[c12,symmetry]) ).
cnf(c7,plain,
( ~ equidistant(X54,X51,X52,X53)
| equidistant(X52,X53,X52,X53) ),
inference(factor,[status(thm)],[transitivity_for_equidistance]) ).
cnf(c24,plain,
equidistant(X56,X55,X56,X55),
inference(resolution,[status(thm)],[c7,segment_construction2]) ).
cnf(c28,plain,
( ~ equidistant(X105,X103,X104,X102)
| equidistant(X104,X102,X105,X103) ),
inference(resolution,[status(thm)],[c24,transitivity_for_equidistance]) ).
cnf(c54,plain,
equidistant(X111,X110,X113,extension(X112,X113,X111,X110)),
inference(resolution,[status(thm)],[c28,segment_construction2]) ).
cnf(c154,plain,
equidistant(X310,extension(X308,X310,X307,extension(X312,X307,X311,X309)),X311,X309),
inference(resolution,[status(thm)],[c11,c54]) ).
cnf(c179,plain,
X318 = extension(X317,X318,X319,extension(X321,X319,X320,X320)),
inference(resolution,[status(thm)],[c154,identity_for_equidistance]) ).
cnf(c183,plain,
extension(X322,X324,X323,extension(X326,X323,X325,X325)) = X324,
inference(resolution,[status(thm)],[c179,symmetry]) ).
cnf(c5,axiom,
( X405 != X402
| X403 != X408
| X401 != X407
| X406 != X404
| ~ equidistant(X405,X403,X401,X406)
| equidistant(X402,X408,X407,X404) ),
theory(equality) ).
cnf(c261,plain,
( X5769 != X5768
| extension(X5767,X5769,X5773,extension(X5775,X5773,X5771,X5766)) != X5772
| X5771 != X5774
| X5766 != X5770
| equidistant(X5768,X5772,X5774,X5770) ),
inference(resolution,[status(thm)],[c5,c154]) ).
cnf(c13293,plain,
( X5859 != X5862
| X5861 != X5860
| X5861 != X5858
| equidistant(X5862,X5859,X5860,X5858) ),
inference(resolution,[status(thm)],[c261,c183]) ).
cnf(c13479,plain,
( X5865 != X5863
| X5865 != X5864
| equidistant(X5863,X5865,X5864,X5863) ),
inference(factor,[status(thm)],[c13293]) ).
cnf(c13568,plain,
( X5872 != X5873
| equidistant(X5873,X5872,X5873,X5873) ),
inference(factor,[status(thm)],[c13479]) ).
cnf(c13811,plain,
equidistant(X5879,extension(X5877,X5879,X5878,X5878),X5879,X5879),
inference(resolution,[status(thm)],[c13568,c13]) ).
cnf(c13837,plain,
equidistant(X5881,X5881,X5880,X5880),
inference(resolution,[status(thm)],[c13811,c11]) ).
cnf(c13871,plain,
$false,
inference(resolution,[status(thm)],[c13837,prove_congruence]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GEO024-2 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 07:48:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 14.68/14.88 % Version: 1.5
% 14.68/14.88 % SZS status Unsatisfiable
% 14.68/14.88 % SZS output start CNFRefutation
% See solution above
% 14.68/14.88
% 14.68/14.88 % Initial clauses : 29
% 14.68/14.88 % Processed clauses : 380
% 14.68/14.88 % Factors computed : 321
% 14.68/14.88 % Resolvents computed: 13654
% 14.68/14.88 % Tautologies deleted: 2
% 14.68/14.88 % Forward subsumed : 662
% 14.68/14.88 % Backward subsumed : 4
% 14.68/14.88 % -------- CPU Time ---------
% 14.68/14.88 % User time : 14.486 s
% 14.68/14.88 % System time : 0.046 s
% 14.68/14.88 % Total time : 14.532 s
%------------------------------------------------------------------------------