%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEV668+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 08:50:24 AM UTC 2026
% Result : Theorem 173.62s 106.68s
% Output : CNFRefutation 173.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEV668+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 11:34:47 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 2030799 was started by sandbox2 on n005,
% 0.11/0.38 % Sat Sep 26 11:34:47 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 92.95/93.22
% 92.95/93.22 % From the command line: assign(max_seconds, 300).
% 92.95/93.22
% 92.95/93.22 % SInE: 4 to sos, 2816 to usable, of 2820 axioms (tolerance 2.00, depth 0 fixpoint).
% 173.62/106.68
% 173.62/106.68 % SZS status Theorem for theBenchmark
% 173.62/106.68
% 173.62/106.68 % Proof 1 at 7.51 (+ 2.65) seconds.
% 173.62/106.68 % Length of proof is 5.
% 173.62/106.68 % Level of proof is 2.
% 173.62/106.68 % Maximum clause weight is 8.000.
% 173.62/106.68 % Given clauses 0.
% 173.62/106.68
% 173.62/106.68 % SZS output start CNFRefutation for theBenchmark
% 173.62/106.68 fof($_discrim_Redblack.TREES.E$Redblack.TREES.T, axiom, ! [Vvar__0___24Anonymous__3183,Vvar__1___24Anonymous__3184,Vvar__2___24Anonymous__3185,Vvar__3___24Anonymous__3186,Vvar__4___24Anonymous__3187] : ~ (cRedblack_2eTREES_2eE = cRedblack_2eTREES_2eT___24a5(Vvar__0___24Anonymous__3183,Vvar__1___24Anonymous__3184,Vvar__2___24Anonymous__3185,Vvar__3___24Anonymous__3186,Vvar__4___24Anonymous__3187)), file('theBenchmark.p',$_discrim_Redblack.TREES.E$Redblack.TREES.T)).
% 173.62/106.68 fof(_HAMMER_GOAL, conjecture, ! [V0__c] : (cRedblack_2ecolor___24t(V0__c) => ! [V1__l] : (cRedblack_2eTREES_2etree___24t(V1__l) => ! [V2__k] : (cRedblack_2ekey___24t(V2__k) => ! [V3__v] : (cV___24t(V3__v) => ! [V4__r] : (cRedblack_2eTREES_2etree___24t(V4__r) => ~ (cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) = cRedblack_2eTREES_2eE)))))), file('theBenchmark.p',_HAMMER_GOAL)).
% 173.62/106.68 fof(_HAMMER_GOAL_neg, negated_conjecture, ~(! [V0__c] : (cRedblack_2ecolor___24t(V0__c) => ! [V1__l] : (cRedblack_2eTREES_2etree___24t(V1__l) => ! [V2__k] : (cRedblack_2ekey___24t(V2__k) => ! [V3__v] : (cV___24t(V3__v) => ! [V4__r] : (cRedblack_2eTREES_2etree___24t(V4__r) => ~ (cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) = cRedblack_2eTREES_2eE))))))), inference(assume_negation, [status(cth)], [_HAMMER_GOAL])).
% 173.62/106.68 cnf(c_29391, plain, cRedblack_2eTREES_2eT___24a5(A,B,C,D,E) != cRedblack_2eTREES_2eE, inference(clausify, [status(thm)], [$_discrim_Redblack.TREES.E$Redblack.TREES.T])).
% 173.62/106.68 fof(nnf_2359, plain, ? [V0__c] : (cRedblack_2ecolor___24t(V0__c) & ? [V1__l] : (cRedblack_2eTREES_2etree___24t(V1__l) & ? [V2__k] : (cRedblack_2ekey___24t(V2__k) & ? [V3__v] : (cV___24t(V3__v) & ? [V4__r] : (cRedblack_2eTREES_2etree___24t(V4__r) & cRedblack_2eTREES_2eT___24a5(V0__c,V1__l,V2__k,V3__v,V4__r) = cRedblack_2eTREES_2eE))))), inference(fof_nnf, [status(thm)], [_HAMMER_GOAL_neg])).
% 173.62/106.68 fof(sk__HAMMER_GOAL_neg, plain, (cRedblack_2ecolor___24t(sK0) & cRedblack_2eTREES_2etree___24t(sK1) & cRedblack_2ekey___24t(sK2) & cV___24t(sK3) & cRedblack_2eTREES_2etree___24t(sK4) & cRedblack_2eTREES_2eT___24a5(sK0,sK1,sK2,sK3,sK4) = cRedblack_2eTREES_2eE), inference(skolemize, [status(esa), new_symbols(skolem, [sK0,sK1,sK2,sK3,sK4]), skolemize(V0__c,sK0), skolemize(V1__l,sK1), skolemize(V2__k,sK2), skolemize(V3__v,sK3), skolemize(V4__r,sK4)], [nnf_2359])).
% 173.62/106.68 cnf(c_29415, negated_conjecture, cRedblack_2eTREES_2eT___24a5(sK0,sK1,sK2,sK3,sK4) = cRedblack_2eTREES_2eE, inference(split_conjunct, [status(thm)], [sk__HAMMER_GOAL_neg])).
% 173.62/106.68 cnf(c_29417, negated_conjecture, cRedblack_2eTREES_2eE = cRedblack_2eTREES_2eT___24a5(sK0,sK1,sK2,sK3,sK4),
% 173.62/106.68 inference(copy, [status(thm)], [c_29415])).
% 173.62/106.68 cnf(c_29416, negated_conjecture, $false,
% 173.62/106.68 inference(resolve, [status(thm)], [c_29391, c_29417])).
% 173.62/106.68 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------