%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV253-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 09:07:09 AM UTC 2026
% Result : Unsatisfiable 26.00s 9.13s
% Output : CNFRefutation 26.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 3
% Syntax : Number of formulae : 18 ( 5 unt; 0 def)
% Number of atoms : 31 ( 30 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 13 ~; 13 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-1 aty)
% Number of variables : 2 ( 0 sgn 1 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_Message_OinvKey_A_IinvKey_Ay_J_A_61_61_Ay_0,axiom,
! [VAR_0] : c_Message_OinvKey(c_Message_OinvKey(VAR_0)) = VAR_0,
file('theBenchmark.p',cls_Message_OinvKey_A_IinvKey_Ay_J_A_61_61_Ay_0) ).
cnf(c_2639,plain,
c_Message_OinvKey(c_Message_OinvKey(A)) = A,
inference(clausify,[status(thm)],[cls_Message_OinvKey_A_IinvKey_Ay_J_A_61_61_Ay_0]) ).
fof(cls_conjecture_0,axiom,
( c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K_H)
| v_K != v_K_H ),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_2661,plain,
( c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K_H)
| v_K != v_K_H ),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
cnf(c_7793,plain,
( c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K_H)
| v_K_H != v_K ),
inference(copy,[status(thm)],[c_2661]) ).
cnf(c_2662,plain,
( c_Message_OinvKey(v_K_H) != c_Message_OinvKey(v_K)
| v_K_H != v_K ),
inference(copy,[status(thm)],[c_7793]) ).
fof(cls_conjecture_1,axiom,
( v_K = v_K_H
| c_Message_OinvKey(v_K) = c_Message_OinvKey(v_K_H) ),
file('theBenchmark.p',cls_conjecture_1) ).
cnf(c_2663,plain,
( v_K = v_K_H
| c_Message_OinvKey(v_K) = c_Message_OinvKey(v_K_H) ),
inference(clausify,[status(thm)],[cls_conjecture_1]) ).
cnf(c_7794,plain,
( v_K = v_K_H
| c_Message_OinvKey(v_K_H) = c_Message_OinvKey(v_K) ),
inference(copy,[status(thm)],[c_2663]) ).
cnf(c_2664,plain,
( v_K_H = v_K
| c_Message_OinvKey(v_K_H) = c_Message_OinvKey(v_K) ),
inference(copy,[status(thm)],[c_7794]) ).
cnf(c_7795,plain,
( c_Message_OinvKey(c_Message_OinvKey(v_K)) = v_K_H
| v_K_H = v_K ),
inference(paramod,[status(thm)],[c_2664,c_2639]) ).
cnf(c_7796,plain,
( v_K = v_K_H
| v_K_H = v_K ),
inference(paramod,[status(thm)],[c_2639,c_7795]) ).
cnf(c_7797,plain,
( v_K_H = v_K
| v_K_H = v_K ),
inference(copy,[status(thm)],[c_7796]) ).
cnf(c_7791,plain,
v_K_H = v_K,
inference(copy,[status(thm)],[c_7797]) ).
cnf(c_7798,plain,
( c_Message_OinvKey(v_K_H) != c_Message_OinvKey(v_K)
| v_K != v_K ),
inference(paramod,[status(thm)],[c_7791,c_2662]) ).
cnf(c_7799,plain,
( c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K)
| v_K != v_K ),
inference(paramod,[status(thm)],[c_7791,c_7798]) ).
cnf(c_7800,plain,
c_Message_OinvKey(v_K) != c_Message_OinvKey(v_K),
inference(copy,[status(thm)],[c_7799]) ).
cnf(c_7792,plain,
$false,
inference(copy,[status(thm)],[c_7800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV253-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.08 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.45 % Computer : n003.cluster.edu
% 0.11/0.45 % Model : x86_64 x86_64
% 0.11/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.45 % Memory : 8046.5625MB
% 0.11/0.45 % OS : Linux 6.8.0-71-generic
% 0.11/0.45 % CPULimit : 300
% 0.11/0.45 % WCLimit : 300
% 0.11/0.45 % DateTime : Sat Sep 26 13:24:24 UTC 2026
% 0.11/0.46 % CPUTime :
% 0.11/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.46 % Process 2996061 was started by sandbox on n003,
% 0.11/0.46 % Sat Sep 26 13:24:24 2026
% 0.11/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.51
% 0.14/0.51 % From the command line: assign(max_seconds, 300).
% 26.00/9.13
% 26.00/9.13 % given #500 (I,wt=4): 564 -class_Ring__and__Field_Opordered__comm__ring(A) | class_HOL_Ozero(A) # tptp_name(clsrel_Ring__and__Field_Opordered__comm__ring_14) # clausal_fof(1). [assumption].
% 26.00/9.13
% 26.00/9.13 % given #1000 (I,wt=10): 1281 c_less(c_0,c_Nat_Osize(A,tc_List_Olist(B)),tc_nat) | c_List_Olist_ONil = A. [copy(1280),flip(b)].
% 26.00/9.13
% 26.00/9.13 % given #1500 (I,wt=7): 2019 -class_OrderedGroup_Oab__group__add(A) | c_uminus(c_0,A) = c_0. [copy(2018),flip(b)].
% 26.00/9.13
% 26.00/9.13 % SZS status Unsatisfiable for theBenchmark
% 26.00/9.13
% 26.00/9.13 % Proof 1 at 3.59 (+ 0.33) seconds.
% 26.00/9.13 % Length of proof is 7.
% 26.00/9.13 % Level of proof is 3.
% 26.00/9.13 % Maximum clause weight is 8.000.
% 26.00/9.13 % Given clauses 1956.
% 26.00/9.13
% 26.00/9.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------