%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO214+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:26:07 PM UTC 2026
% Result : CounterSatisfiable 0.08s 0.56s
% Output : Saturation 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f36,conjecture,
! [L,M] :
( not_orthogonal_lines(L,M)
=> not_orthogonal_lines(M,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
~ ! [L,M] :
( not_orthogonal_lines(L,M)
=> not_orthogonal_lines(M,L) ),
inference(negated_conjecture,[status(cth)],[f36]) ).
fof(f127,plain,
? [L,M] :
( ~ not_orthogonal_lines(M,L)
& not_orthogonal_lines(L,M) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f128,plain,
( ~ not_orthogonal_lines(sK1_skl,sK0_skl)
& not_orthogonal_lines(sK0_skl,sK1_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(L,sK0_skl),skolemize(M,sK1_skl)],[f127]) ).
fof(f129,plain,
not_orthogonal_lines(sK0_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
~ not_orthogonal_lines(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f128]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO214+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.52 % Computer : n009.cluster.edu
% 0.08/0.52 % Model : x86_64 x86_64
% 0.08/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.52 % Memory : 8046.5625MB
% 0.08/0.52 % OS : Linux 6.8.0-71-generic
% 0.08/0.52 % CPULimit : 300
% 0.08/0.52 % WCLimit : 300
% 0.08/0.52 % DateTime : Sun Sep 20 13:28:29 UTC 2026
% 0.08/0.53 % CPUTime :
% 0.08/0.54 % Drodi V4.1.1
% 0.08/0.56 % SZS status CounterSatisfiable for theBenchmark: Theorem is counter-satisfiable, conjecture is false
% 0.08/0.56 % SZS output start Saturation for theBenchmark
% See solution above
% 0.12/0.59 % Elapsed time: 0.045899 seconds
% 0.12/0.59 % CPU time: 0.109681 seconds
% 0.12/0.59 % Total memory used: 17.919 MB
% 0.12/0.59 % Net memory used: 17.078 MB
%------------------------------------------------------------------------------