%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO094-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:25:45 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO094-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 10:41:08 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.09/0.53 % Refutation found
% 0.09/0.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.53 fof(f1,axiom,(
% 0.09/0.53 (![A,B,C]: (( ~ part_of(A,B)| ~ incident_c(C,A)| incident_c(C,B) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f14,axiom,(
% 0.09/0.53 (![A,B,C,D]: (( ~ end_point(A,B)| ~ part_of(C,B)| ~ part_of(D,B)| ~ incident_c(A,C)| ~ incident_c(A,D)| part_of(C,D)| part_of(D,C) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f21,axiom,(
% 0.09/0.53 (![A,B]: (( ~ inner_point(A,B)| incident_c(A,B) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f22,axiom,(
% 0.09/0.53 (![A,B]: (( ~ inner_point(A,B)| ~ end_point(A,B) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f24,axiom,(
% 0.09/0.53 (![A,B,C]: (( ~ meet(A,B,C)| incident_c(A,B) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f25,axiom,(
% 0.09/0.53 (![A,B,C]: (( ~ meet(A,B,C)| incident_c(A,C) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f26,axiom,(
% 0.09/0.53 (![A,B,C,D]: (( ~ meet(A,B,C)| ~ incident_c(D,B)| ~ incident_c(D,C)| end_point(D,B) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f27,axiom,(
% 0.09/0.53 (![A,B,C,D]: (( ~ meet(A,B,C)| ~ incident_c(D,B)| ~ incident_c(D,C)| end_point(D,C) ) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f37,axiom,(
% 0.09/0.53 (![A]: (inner_point(ax0_sk8(A),A) ))),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f49,negated_conjecture,(
% 0.09/0.53 meet(sk17,sk15,sk16) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f50,negated_conjecture,(
% 0.09/0.53 part_of(sk15,sk14) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f51,negated_conjecture,(
% 0.09/0.53 part_of(sk16,sk14) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f52,negated_conjecture,(
% 0.09/0.53 end_point(sk17,sk14) ),
% 0.09/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.53 fof(f53,plain,(
% 0.09/0.53 ![B,C]: ((![A]: (~part_of(A,B)|~incident_c(C,A)))|incident_c(C,B))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f1])).
% 0.09/0.53 fof(f54,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~part_of(X0,X1)|~incident_c(X2,X0)|incident_c(X2,X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f53])).
% 0.09/0.53 fof(f70,plain,(
% 0.09/0.53 ![C,D]: (((![A]: (((![B]: ((~end_point(A,B)|~part_of(C,B))|~part_of(D,B)))|~incident_c(A,C))|~incident_c(A,D)))|part_of(C,D))|part_of(D,C))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f14])).
% 0.09/0.53 fof(f71,plain,(
% 0.09/0.53 ![X0,X1,X2,X3]: (~end_point(X0,X1)|~part_of(X2,X1)|~part_of(X3,X1)|~incident_c(X0,X2)|~incident_c(X0,X3)|part_of(X2,X3)|part_of(X3,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f70])).
% 0.09/0.53 fof(f78,plain,(
% 0.09/0.53 ![X0,X1]: (~inner_point(X0,X1)|incident_c(X0,X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f21])).
% 0.09/0.53 fof(f79,plain,(
% 0.09/0.53 ![X0,X1]: (~inner_point(X0,X1)|~end_point(X0,X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f22])).
% 0.09/0.53 fof(f81,plain,(
% 0.09/0.53 ![A,B]: ((![C]: ~meet(A,B,C))|incident_c(A,B))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f24])).
% 0.09/0.53 fof(f82,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~meet(X0,X1,X2)|incident_c(X0,X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f81])).
% 0.09/0.53 fof(f83,plain,(
% 0.09/0.53 ![A,C]: ((![B]: ~meet(A,B,C))|incident_c(A,C))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f25])).
% 0.09/0.53 fof(f84,plain,(
% 0.09/0.53 ![X0,X1,X2]: (~meet(X0,X1,X2)|incident_c(X0,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f83])).
% 0.09/0.53 fof(f85,plain,(
% 0.09/0.53 ![B,D]: ((![C]: (((![A]: ~meet(A,B,C))|~incident_c(D,B))|~incident_c(D,C)))|end_point(D,B))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f26])).
% 0.09/0.53 fof(f86,plain,(
% 0.09/0.53 ![X0,X1,X2,X3]: (~meet(X0,X1,X2)|~incident_c(X3,X1)|~incident_c(X3,X2)|end_point(X3,X1))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f85])).
% 0.09/0.53 fof(f87,plain,(
% 0.09/0.53 ![C,D]: (((![B]: ((![A]: ~meet(A,B,C))|~incident_c(D,B)))|~incident_c(D,C))|end_point(D,C))),
% 0.09/0.53 inference(miniscoping,[status(thm)],[f27])).
% 0.09/0.53 fof(f88,plain,(
% 0.09/0.53 ![X0,X1,X2,X3]: (~meet(X0,X1,X2)|~incident_c(X3,X1)|~incident_c(X3,X2)|end_point(X3,X2))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f87])).
% 0.09/0.53 fof(f102,plain,(
% 0.09/0.53 ![X0]: (inner_point(ax0_sk8(X0),X0))),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f37])).
% 0.09/0.53 fof(f117,plain,(
% 0.09/0.53 meet(sk17,sk15,sk16)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f49])).
% 0.09/0.53 fof(f118,plain,(
% 0.09/0.53 part_of(sk15,sk14)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f50])).
% 0.09/0.53 fof(f119,plain,(
% 0.09/0.53 part_of(sk16,sk14)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f51])).
% 0.09/0.53 fof(f120,plain,(
% 0.09/0.53 end_point(sk17,sk14)),
% 0.09/0.53 inference(cnf_transformation,[status(thm)],[f52])).
% 0.09/0.53 fof(f125,plain,(
% 0.09/0.53 incident_c(sk17,sk15)),
% 0.09/0.53 inference(resolution,[status(thm)],[f82,f117])).
% 0.09/0.53 fof(f126,plain,(
% 0.09/0.53 incident_c(sk17,sk16)),
% 0.09/0.53 inference(resolution,[status(thm)],[f84,f117])).
% 0.09/0.53 fof(f127,plain,(
% 0.09/0.53 ![X0]: (~incident_c(X0,sk15)|~incident_c(X0,sk16)|end_point(X0,sk15))),
% 0.09/0.53 inference(resolution,[status(thm)],[f86,f117])).
% 0.09/0.53 fof(f129,plain,(
% 0.09/0.53 ![X0,X1]: (~incident_c(X0,sk15)|end_point(X0,sk15)|~part_of(X1,sk16)|~incident_c(X0,X1))),
% 0.09/0.53 inference(resolution,[status(thm)],[f127,f54])).
% 0.09/0.53 fof(f130,definition,(
% 0.09/0.53 sQ0_spl <=> (incident_c(sk17,sk15))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f132,plain,(
% 0.09/0.53 ~incident_c(sk17,sk15)|sQ0_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f130])).
% 0.09/0.53 fof(f137,plain,(
% 0.09/0.53 $false|sQ0_spl),
% 0.09/0.53 inference(forward_subsumption_resolution,[status(thm)],[f132,f125])).
% 0.09/0.53 fof(f138,plain,(
% 0.09/0.53 sQ0_spl),
% 0.09/0.53 inference(contradiction_clause,[status(thm)],[f137])).
% 0.09/0.53 fof(f139,plain,(
% 0.09/0.53 ![X0]: (~incident_c(X0,sk15)|~incident_c(X0,sk16)|end_point(X0,sk16))),
% 0.09/0.53 inference(resolution,[status(thm)],[f88,f117])).
% 0.09/0.53 fof(f150,plain,(
% 0.09/0.53 ![X0,X1]: (~end_point(X0,sk14)|~part_of(X1,sk14)|~incident_c(X0,X1)|~incident_c(X0,sk16)|part_of(X1,sk16)|part_of(sk16,X1))),
% 0.09/0.53 inference(resolution,[status(thm)],[f71,f119])).
% 0.09/0.53 fof(f174,plain,(
% 0.09/0.53 ![X0]: (incident_c(ax0_sk8(X0),X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f78,f102])).
% 0.09/0.53 fof(f193,plain,(
% 0.09/0.53 ![X0]: (~part_of(X0,sk14)|~incident_c(sk17,X0)|~incident_c(sk17,sk16)|part_of(X0,sk16)|part_of(sk16,X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f150,f120])).
% 0.09/0.53 fof(f194,definition,(
% 0.09/0.53 ![X0]: (sQ9_spl <=> (~part_of(X0,sk14)|~incident_c(sk17,X0)|part_of(X0,sk16)|part_of(sk16,X0)))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f195,plain,(
% 0.09/0.53 ![X0]: (~part_of(X0,sk14)|~incident_c(sk17,X0)|part_of(X0,sk16)|part_of(sk16,X0)|~sQ9_spl)),
% 0.09/0.53 inference(component_clause,[status(thm)],[f194])).
% 0.09/0.53 fof(f197,definition,(
% 0.09/0.53 sQ10_spl <=> (incident_c(sk17,sk16))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f199,plain,(
% 0.09/0.53 ~incident_c(sk17,sk16)|sQ10_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f197])).
% 0.09/0.53 fof(f200,plain,(
% 0.09/0.53 sQ9_spl|~sQ10_spl),
% 0.09/0.53 inference(split_clause,[status(thm)],[f193,f194,f197])).
% 0.09/0.53 fof(f206,plain,(
% 0.09/0.53 ~incident_c(ax0_sk8(sk16),sk15)|end_point(ax0_sk8(sk16),sk16)),
% 0.09/0.53 inference(resolution,[status(thm)],[f174,f139])).
% 0.09/0.53 fof(f209,definition,(
% 0.09/0.53 sQ12_spl <=> (incident_c(ax0_sk8(sk16),sk15))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f211,plain,(
% 0.09/0.53 ~incident_c(ax0_sk8(sk16),sk15)|sQ12_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f209])).
% 0.09/0.53 fof(f212,definition,(
% 0.09/0.53 sQ13_spl <=> (end_point(ax0_sk8(sk16),sk16))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f213,plain,(
% 0.09/0.53 end_point(ax0_sk8(sk16),sk16)|~sQ13_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f212])).
% 0.09/0.53 fof(f215,plain,(
% 0.09/0.53 ~sQ12_spl|sQ13_spl),
% 0.09/0.53 inference(split_clause,[status(thm)],[f206,f209,f212])).
% 0.09/0.53 fof(f223,plain,(
% 0.09/0.53 ![X0]: (~end_point(ax0_sk8(X0),X0))),
% 0.09/0.53 inference(resolution,[status(thm)],[f79,f102])).
% 0.09/0.53 fof(f225,plain,(
% 0.09/0.53 ![X0]: (~part_of(X0,sk15)|~incident_c(ax0_sk8(sk16),X0)|sQ12_spl)),
% 0.09/0.53 inference(resolution,[status(thm)],[f211,f54])).
% 0.09/0.53 fof(f240,plain,(
% 0.09/0.53 ~incident_c(sk17,sk15)|part_of(sk15,sk16)|part_of(sk16,sk15)|~sQ9_spl),
% 0.09/0.53 inference(resolution,[status(thm)],[f195,f118])).
% 0.09/0.53 fof(f242,definition,(
% 0.09/0.53 sQ15_spl <=> (part_of(sk15,sk16))),
% 0.09/0.53 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.53 fof(f243,plain,(
% 0.09/0.53 part_of(sk15,sk16)|~sQ15_spl),
% 0.09/0.53 inference(component_clause,[status(thm)],[f242])).
% 0.09/0.54 fof(f245,definition,(
% 0.09/0.54 sQ16_spl <=> (part_of(sk16,sk15))),
% 0.09/0.54 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.54 fof(f246,plain,(
% 0.09/0.54 part_of(sk16,sk15)|~sQ16_spl),
% 0.09/0.54 inference(component_clause,[status(thm)],[f245])).
% 0.09/0.54 fof(f248,plain,(
% 0.09/0.54 ~sQ0_spl|sQ15_spl|sQ16_spl|~sQ9_spl),
% 0.09/0.54 inference(split_clause,[status(thm)],[f240,f130,f242,f245,f194])).
% 0.09/0.54 fof(f249,plain,(
% 0.09/0.54 $false|sQ10_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f199,f126])).
% 0.09/0.54 fof(f250,plain,(
% 0.09/0.54 sQ10_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f249])).
% 0.09/0.54 fof(f264,plain,(
% 0.09/0.54 ![X0]: (~incident_c(X0,sk15)|end_point(X0,sk15)|~incident_c(X0,sk15)|~sQ15_spl)),
% 0.09/0.54 inference(resolution,[status(thm)],[f243,f129])).
% 0.09/0.54 fof(f271,plain,(
% 0.09/0.54 ![X0]: (~incident_c(X0,sk15)|end_point(X0,sk15)|~sQ15_spl)),
% 0.09/0.54 inference(duplicate_literals_removal,[status(thm)],[f264])).
% 0.09/0.54 fof(f289,plain,(
% 0.09/0.54 ~incident_c(ax0_sk8(sk16),sk16)|~sQ16_spl|sQ12_spl),
% 0.09/0.54 inference(resolution,[status(thm)],[f246,f225])).
% 0.09/0.54 fof(f295,plain,(
% 0.09/0.54 $false|~sQ16_spl|sQ12_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f289,f174])).
% 0.09/0.54 fof(f296,plain,(
% 0.09/0.54 ~sQ16_spl|sQ12_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f295])).
% 0.09/0.54 fof(f297,plain,(
% 0.09/0.54 $false|~sQ13_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f213,f223])).
% 0.09/0.54 fof(f298,plain,(
% 0.09/0.54 ~sQ13_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f297])).
% 0.09/0.54 fof(f309,plain,(
% 0.09/0.54 end_point(ax0_sk8(sk15),sk15)|~sQ15_spl),
% 0.09/0.54 inference(resolution,[status(thm)],[f271,f174])).
% 0.09/0.54 fof(f315,plain,(
% 0.09/0.54 $false|~sQ15_spl),
% 0.09/0.54 inference(forward_subsumption_resolution,[status(thm)],[f309,f223])).
% 0.09/0.54 fof(f316,plain,(
% 0.09/0.54 ~sQ15_spl),
% 0.09/0.54 inference(contradiction_clause,[status(thm)],[f315])).
% 0.09/0.54 fof(f317,plain,(
% 0.09/0.54 $false),
% 0.09/0.54 inference(sat_refutation,[status(thm)],[f138,f200,f215,f248,f250,f296,f298,f316])).
% 0.09/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.73/0.56 % Elapsed time: 0.164418 seconds
% 0.73/0.56 % CPU time: 1.064302 seconds
% 0.73/0.56 % Total memory used: 92.607 MB
% 0.73/0.56 % Net memory used: 91.213 MB
%------------------------------------------------------------------------------