%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN714-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 03:20:24 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN714-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 11:13:34 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.40 % Refutation found
% 0.10/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.40 fof(f22,negated_conjecture,(
% 0.10/0.40 p51(c66,c67) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f23,negated_conjecture,(
% 0.10/0.40 p53(c68,f17(c66)) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f24,negated_conjecture,(
% 0.10/0.40 ~ p16(f17(c66),c65) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f28,negated_conjecture,(
% 0.10/0.40 p52(f20(f21(c62,c64)),c66) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f33,negated_conjecture,(
% 0.10/0.40 ~ p50(c66,f25(f27(c59,c68),c67),c60) ),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f64,negated_conjecture,(
% 0.10/0.40 (![X160]: (( p50(c66,f25(f27(c59,X160),c67),c62)| ~ p53(X160,f17(c66)) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f87,negated_conjecture,(
% 0.10/0.40 (![X165,X166,X167,X168]: (( p51(X165,f25(f27(X166,X167),X168))| ~ p51(X165,X168)| ~ p53(X167,f17(X165)) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f98,negated_conjecture,(
% 0.10/0.40 (![X15,X16]: (( p16(f17(X15),c65)| p50(X15,X16,c60)| ~ p51(X15,X16)| ~ p50(X15,X16,c62)| ~ p52(f20(f21(c62,c64)),X15) ) ))),
% 0.10/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.40 fof(f127,plain,(
% 0.10/0.40 p51(c66,c67)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.40 fof(f128,plain,(
% 0.10/0.40 p53(c68,f17(c66))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.40 fof(f129,plain,(
% 0.10/0.40 ~p16(f17(c66),c65)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.40 fof(f133,plain,(
% 0.10/0.40 p52(f20(f21(c62,c64)),c66)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f28])).
% 0.10/0.40 fof(f138,plain,(
% 0.10/0.40 ~p50(c66,f25(f27(c59,c68),c67),c60)),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f33])).
% 0.10/0.40 fof(f188,plain,(
% 0.10/0.40 ![X0]: (p50(c66,f25(f27(c59,X0),c67),c62)|~p53(X0,f17(c66)))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f64])).
% 0.10/0.40 fof(f233,plain,(
% 0.10/0.40 ![X165,X167]: ((![X168]: ((![X166]: p51(X165,f25(f27(X166,X167),X168)))|~p51(X165,X168)))|~p53(X167,f17(X165)))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f87])).
% 0.10/0.40 fof(f234,plain,(
% 0.10/0.40 ![X0,X1,X2,X3]: (p51(X0,f25(f27(X1,X2),X3))|~p51(X0,X3)|~p53(X2,f17(X0)))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f233])).
% 0.10/0.40 fof(f250,plain,(
% 0.10/0.40 ![X15]: ((![X16]: (((p16(f17(X15),c65)|p50(X15,X16,c60))|~p51(X15,X16))|~p50(X15,X16,c62)))|~p52(f20(f21(c62,c64)),X15))),
% 0.10/0.40 inference(miniscoping,[status(thm)],[f98])).
% 0.10/0.40 fof(f251,plain,(
% 0.10/0.40 ![X0,X1]: (p16(f17(X0),c65)|p50(X0,X1,c60)|~p51(X0,X1)|~p50(X0,X1,c62)|~p52(f20(f21(c62,c64)),X0))),
% 0.10/0.40 inference(cnf_transformation,[status(thm)],[f250])).
% 0.10/0.40 fof(f320,plain,(
% 0.10/0.40 p50(c66,f25(f27(c59,c68),c67),c62)),
% 0.10/0.40 inference(resolution,[status(thm)],[f188,f128])).
% 0.10/0.40 fof(f349,plain,(
% 0.10/0.40 ![X0,X1]: (p51(c66,f25(f27(X0,X1),c67))|~p53(X1,f17(c66)))),
% 0.10/0.40 inference(resolution,[status(thm)],[f234,f127])).
% 0.10/0.40 fof(f384,plain,(
% 0.10/0.40 p16(f17(c66),c65)|p50(c66,f25(f27(c59,c68),c67),c60)|~p51(c66,f25(f27(c59,c68),c67))|~p52(f20(f21(c62,c64)),c66)),
% 0.10/0.40 inference(resolution,[status(thm)],[f320,f251])).
% 0.10/0.40 fof(f385,definition,(
% 0.10/0.40 sQ4_spl <=> (p16(f17(c66),c65))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f386,plain,(
% 0.10/0.40 p16(f17(c66),c65)|~sQ4_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f385])).
% 0.10/0.40 fof(f388,definition,(
% 0.10/0.40 sQ5_spl <=> (p50(c66,f25(f27(c59,c68),c67),c60))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f389,plain,(
% 0.10/0.40 p50(c66,f25(f27(c59,c68),c67),c60)|~sQ5_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f388])).
% 0.10/0.40 fof(f391,definition,(
% 0.10/0.40 sQ6_spl <=> (p51(c66,f25(f27(c59,c68),c67)))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f393,plain,(
% 0.10/0.40 ~p51(c66,f25(f27(c59,c68),c67))|sQ6_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f391])).
% 0.10/0.40 fof(f394,definition,(
% 0.10/0.40 sQ7_spl <=> (p52(f20(f21(c62,c64)),c66))),
% 0.10/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.40 fof(f396,plain,(
% 0.10/0.40 ~p52(f20(f21(c62,c64)),c66)|sQ7_spl),
% 0.10/0.40 inference(component_clause,[status(thm)],[f394])).
% 0.10/0.40 fof(f397,plain,(
% 0.10/0.40 sQ4_spl|sQ5_spl|~sQ6_spl|~sQ7_spl),
% 0.10/0.40 inference(split_clause,[status(thm)],[f384,f385,f388,f391,f394])).
% 0.10/0.40 fof(f398,plain,(
% 0.10/0.40 $false|sQ7_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f396,f133])).
% 0.10/0.40 fof(f399,plain,(
% 0.10/0.40 sQ7_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f398])).
% 0.10/0.40 fof(f419,plain,(
% 0.10/0.40 ![X0]: (p51(c66,f25(f27(X0,c68),c67)))),
% 0.10/0.40 inference(resolution,[status(thm)],[f349,f128])).
% 0.10/0.40 fof(f448,plain,(
% 0.10/0.40 $false|sQ6_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f393,f419])).
% 0.10/0.40 fof(f449,plain,(
% 0.10/0.40 sQ6_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f448])).
% 0.10/0.40 fof(f450,plain,(
% 0.10/0.40 $false|~sQ4_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f386,f129])).
% 0.10/0.40 fof(f451,plain,(
% 0.10/0.40 ~sQ4_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f450])).
% 0.10/0.40 fof(f452,plain,(
% 0.10/0.40 $false|~sQ5_spl),
% 0.10/0.40 inference(forward_subsumption_resolution,[status(thm)],[f389,f138])).
% 0.10/0.40 fof(f453,plain,(
% 0.10/0.40 ~sQ5_spl),
% 0.10/0.40 inference(contradiction_clause,[status(thm)],[f452])).
% 0.10/0.40 fof(f454,plain,(
% 0.10/0.40 $false),
% 0.10/0.40 inference(sat_refutation,[status(thm)],[f397,f399,f449,f451,f453])).
% 0.10/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.43 % Elapsed time: 0.046686 seconds
% 0.10/0.43 % CPU time: 0.139080 seconds
% 0.10/0.43 % Total memory used: 21.699 MB
% 0.10/0.43 % Net memory used: 21.480 MB
%------------------------------------------------------------------------------