%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN090-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:15:12 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.38s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 32
% Syntax : Number of formulae : 122 ( 36 unt; 0 def)
% Number of atoms : 264 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 287 ( 145 ~; 142 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 32 ( 31 usr; 32 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ q_0
| ~ p_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( ~ q_2
| ~ q_1
| p_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( ~ q_3
| ~ q_2
| p_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( ~ q_4
| ~ q_3
| p_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
( ~ q_5
| ~ q_4
| p_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( ~ q_6
| ~ q_5
| p_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
( ~ q_7
| ~ q_6
| p_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
( ~ q_8
| ~ q_7
| p_6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( ~ q_9
| ~ q_8
| p_7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
( ~ q_10
| ~ q_9
| p_8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( ~ q_11
| ~ q_10
| p_9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( ~ q_12
| ~ q_11
| p_10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
( ~ q_13
| ~ q_12
| p_11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
( ~ p_14
| ~ p_13
| p_12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
( ~ p_15
| ~ p_14
| p_13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
( ~ q_2
| ~ p_1
| q_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
( ~ q_3
| ~ p_2
| q_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
( ~ q_4
| ~ p_3
| q_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
( ~ q_5
| ~ p_4
| q_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
( ~ q_6
| ~ p_5
| q_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
( ~ q_7
| ~ p_6
| q_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
( ~ q_8
| ~ p_7
| q_6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
( ~ q_9
| ~ p_8
| q_7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
( ~ q_10
| ~ p_9
| q_8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
( ~ q_11
| ~ p_10
| q_9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
( ~ q_12
| ~ p_11
| q_10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,axiom,
( ~ q_13
| ~ p_12
| q_11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
( ~ p_14
| ~ q_13
| q_12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
( ~ q_15
| ~ p_14
| q_13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
p_14,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
p_15,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
q_15,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,plain,
( ~ q_0
| ~ p_0 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f68,plain,
( ~ q_2
| ~ q_1
| p_0 ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f70,plain,
( ~ q_3
| ~ q_2
| p_1 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f72,plain,
( ~ q_4
| ~ q_3
| p_2 ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f74,plain,
( ~ q_5
| ~ q_4
| p_3 ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f76,plain,
( ~ q_6
| ~ q_5
| p_4 ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f78,plain,
( ~ q_7
| ~ q_6
| p_5 ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f80,plain,
( ~ q_8
| ~ q_7
| p_6 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f82,plain,
( ~ q_9
| ~ q_8
| p_7 ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f84,plain,
( ~ q_10
| ~ q_9
| p_8 ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f86,plain,
( ~ q_11
| ~ q_10
| p_9 ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f88,plain,
( ~ q_12
| ~ q_11
| p_10 ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f90,plain,
( ~ q_13
| ~ q_12
| p_11 ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f91,plain,
( ~ p_14
| ~ p_13
| p_12 ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f93,plain,
( ~ p_15
| ~ p_14
| p_13 ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f95,plain,
( ~ q_2
| ~ p_1
| q_0 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f97,plain,
( ~ q_3
| ~ p_2
| q_1 ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f99,plain,
( ~ q_4
| ~ p_3
| q_2 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f101,plain,
( ~ q_5
| ~ p_4
| q_3 ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f103,plain,
( ~ q_6
| ~ p_5
| q_4 ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f105,plain,
( ~ q_7
| ~ p_6
| q_5 ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f107,plain,
( ~ q_8
| ~ p_7
| q_6 ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f109,plain,
( ~ q_9
| ~ p_8
| q_7 ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f111,plain,
( ~ q_10
| ~ p_9
| q_8 ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f113,plain,
( ~ q_11
| ~ p_10
| q_9 ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f115,plain,
( ~ q_12
| ~ p_11
| q_10 ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f117,plain,
( ~ q_13
| ~ p_12
| q_11 ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f120,plain,
( ~ p_14
| ~ q_13
| q_12 ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f121,plain,
( ~ q_15
| ~ p_14
| q_13 ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f127,plain,
p_14,
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f128,plain,
p_15,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f130,plain,
q_15,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f131,plain,
( ~ q_15
| q_13 ),
inference(backward_subsumption_resolution,[status(thm)],[f121,f127]) ).
fof(f132,plain,
( ~ q_13
| q_12 ),
inference(backward_subsumption_resolution,[status(thm)],[f120,f127]) ).
fof(f133,plain,
( ~ p_15
| p_13 ),
inference(backward_subsumption_resolution,[status(thm)],[f93,f127]) ).
fof(f134,plain,
( ~ p_13
| p_12 ),
inference(backward_subsumption_resolution,[status(thm)],[f91,f127]) ).
fof(f139,plain,
( ~ p_12
| q_11 ),
inference(backward_subsumption_resolution,[status(thm)],[f117,f141]) ).
fof(f140,plain,
( ~ q_12
| p_11 ),
inference(backward_subsumption_resolution,[status(thm)],[f90,f141]) ).
fof(f141,plain,
q_13,
inference(forward_subsumption_resolution,[status(thm)],[f131,f130]) ).
fof(f143,plain,
( ~ p_11
| q_10 ),
inference(backward_subsumption_resolution,[status(thm)],[f115,f145]) ).
fof(f144,plain,
( ~ q_11
| p_10 ),
inference(backward_subsumption_resolution,[status(thm)],[f88,f145]) ).
fof(f145,plain,
q_12,
inference(forward_subsumption_resolution,[status(thm)],[f132,f141]) ).
fof(f147,plain,
p_13,
inference(forward_subsumption_resolution,[status(thm)],[f133,f128]) ).
fof(f150,plain,
p_12,
inference(forward_subsumption_resolution,[status(thm)],[f134,f147]) ).
fof(f151,plain,
( ~ p_10
| q_9 ),
inference(backward_subsumption_resolution,[status(thm)],[f113,f153]) ).
fof(f152,plain,
( ~ q_10
| p_9 ),
inference(backward_subsumption_resolution,[status(thm)],[f86,f153]) ).
fof(f153,plain,
q_11,
inference(forward_subsumption_resolution,[status(thm)],[f139,f150]) ).
fof(f156,plain,
p_11,
inference(forward_subsumption_resolution,[status(thm)],[f140,f145]) ).
fof(f157,plain,
( ~ p_9
| q_8 ),
inference(backward_subsumption_resolution,[status(thm)],[f111,f159]) ).
fof(f158,plain,
( ~ q_9
| p_8 ),
inference(backward_subsumption_resolution,[status(thm)],[f84,f159]) ).
fof(f159,plain,
q_10,
inference(forward_subsumption_resolution,[status(thm)],[f143,f156]) ).
fof(f162,plain,
p_10,
inference(forward_subsumption_resolution,[status(thm)],[f144,f153]) ).
fof(f163,plain,
( ~ p_8
| q_7 ),
inference(backward_subsumption_resolution,[status(thm)],[f109,f165]) ).
fof(f164,plain,
( ~ q_8
| p_7 ),
inference(backward_subsumption_resolution,[status(thm)],[f82,f165]) ).
fof(f165,plain,
q_9,
inference(forward_subsumption_resolution,[status(thm)],[f151,f162]) ).
fof(f168,plain,
p_9,
inference(forward_subsumption_resolution,[status(thm)],[f152,f159]) ).
fof(f170,plain,
( ~ p_7
| q_6 ),
inference(backward_subsumption_resolution,[status(thm)],[f107,f172]) ).
fof(f171,plain,
( ~ q_7
| p_6 ),
inference(backward_subsumption_resolution,[status(thm)],[f80,f172]) ).
fof(f172,plain,
q_8,
inference(forward_subsumption_resolution,[status(thm)],[f157,f168]) ).
fof(f176,plain,
p_8,
inference(forward_subsumption_resolution,[status(thm)],[f158,f165]) ).
fof(f177,plain,
( ~ p_6
| q_5 ),
inference(backward_subsumption_resolution,[status(thm)],[f105,f179]) ).
fof(f178,plain,
( ~ q_6
| p_5 ),
inference(backward_subsumption_resolution,[status(thm)],[f78,f179]) ).
fof(f179,plain,
q_7,
inference(forward_subsumption_resolution,[status(thm)],[f163,f176]) ).
fof(f182,plain,
p_7,
inference(forward_subsumption_resolution,[status(thm)],[f164,f172]) ).
fof(f183,plain,
( ~ p_5
| q_4 ),
inference(backward_subsumption_resolution,[status(thm)],[f103,f185]) ).
fof(f184,plain,
( ~ q_5
| p_4 ),
inference(backward_subsumption_resolution,[status(thm)],[f76,f185]) ).
fof(f185,plain,
q_6,
inference(forward_subsumption_resolution,[status(thm)],[f170,f182]) ).
fof(f188,plain,
p_6,
inference(forward_subsumption_resolution,[status(thm)],[f171,f179]) ).
fof(f189,plain,
( ~ p_4
| q_3 ),
inference(backward_subsumption_resolution,[status(thm)],[f101,f191]) ).
fof(f190,plain,
( ~ q_4
| p_3 ),
inference(backward_subsumption_resolution,[status(thm)],[f74,f191]) ).
fof(f191,plain,
q_5,
inference(forward_subsumption_resolution,[status(thm)],[f177,f188]) ).
fof(f194,plain,
p_5,
inference(forward_subsumption_resolution,[status(thm)],[f178,f185]) ).
fof(f195,plain,
( ~ p_3
| q_2 ),
inference(backward_subsumption_resolution,[status(thm)],[f99,f197]) ).
fof(f196,plain,
( ~ q_3
| p_2 ),
inference(backward_subsumption_resolution,[status(thm)],[f72,f197]) ).
fof(f197,plain,
q_4,
inference(forward_subsumption_resolution,[status(thm)],[f183,f194]) ).
fof(f200,plain,
p_4,
inference(forward_subsumption_resolution,[status(thm)],[f184,f191]) ).
fof(f201,plain,
( ~ p_2
| q_1 ),
inference(backward_subsumption_resolution,[status(thm)],[f97,f203]) ).
fof(f202,plain,
( ~ q_2
| p_1 ),
inference(backward_subsumption_resolution,[status(thm)],[f70,f203]) ).
fof(f203,plain,
q_3,
inference(forward_subsumption_resolution,[status(thm)],[f189,f200]) ).
fof(f206,plain,
p_3,
inference(forward_subsumption_resolution,[status(thm)],[f190,f197]) ).
fof(f207,plain,
( ~ p_1
| q_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f95,f209]) ).
fof(f208,plain,
( ~ q_1
| p_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f68,f209]) ).
fof(f209,plain,
q_2,
inference(forward_subsumption_resolution,[status(thm)],[f195,f206]) ).
fof(f212,plain,
p_2,
inference(forward_subsumption_resolution,[status(thm)],[f196,f203]) ).
fof(f213,plain,
q_1,
inference(forward_subsumption_resolution,[status(thm)],[f201,f212]) ).
fof(f214,plain,
p_1,
inference(forward_subsumption_resolution,[status(thm)],[f202,f209]) ).
fof(f215,plain,
~ p_0,
inference(backward_subsumption_resolution,[status(thm)],[f66,f216]) ).
fof(f216,plain,
q_0,
inference(forward_subsumption_resolution,[status(thm)],[f207,f214]) ).
fof(f217,plain,
p_0,
inference(forward_subsumption_resolution,[status(thm)],[f208,f213]) ).
fof(f218,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f215,f217]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN090-1.008 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 10:42:52 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.38 % Refutation found
% 0.08/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.42 % Elapsed time: 0.049097 seconds
% 0.13/0.42 % CPU time: 0.141857 seconds
% 0.13/0.42 % Total memory used: 56.699 MB
% 0.13/0.42 % Net memory used: 56.697 MB
%------------------------------------------------------------------------------