%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN170-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 09:37:12 AM UTC 2026
% Result : Unsatisfiable 3.26s 0.88s
% Output : CNFRefutation 3.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 10
% Syntax : Number of formulae : 85 ( 85 unt; 0 def)
% Number of atoms : 85 ( 84 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 119 ( 27 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(axiom_1,axiom,
s0(d) = true,
file('theBenchmark.p',axiom_1) ).
cnf(c_2,plain,
s0(d) = true,
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_3,plain,
true = s0(d),
inference(copy,[status(thm)],[c_2]) ).
fof(axiom_5,axiom,
s0(b) = true,
file('theBenchmark.p',axiom_5) ).
cnf(c_10,plain,
s0(b) = true,
inference(clausify,[status(thm)],[axiom_5]) ).
cnf(c_3692,plain,
s0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_11,plain,
s0(d) = s0(b),
inference(copy,[status(thm)],[c_3692]) ).
fof(axiom_9,axiom,
r0(b) = true,
file('theBenchmark.p',axiom_9) ).
cnf(c_18,plain,
r0(b) = true,
inference(clausify,[status(thm)],[axiom_9]) ).
cnf(c_3693,plain,
r0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_18]) ).
cnf(c_3694,plain,
r0(b) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3693]) ).
cnf(c_19,plain,
s0(b) = r0(b),
inference(copy,[status(thm)],[c_3694]) ).
fof(axiom_19,axiom,
! [VAR_0,VAR_1] : m0(VAR_0,d,VAR_1) = true,
file('theBenchmark.p',axiom_19) ).
cnf(c_38,plain,
m0(A,d,B) = true,
inference(clausify,[status(thm)],[axiom_19]) ).
cnf(c_3695,plain,
m0(A,d,B) = s0(d),
inference(paramod,[status(thm)],[c_3,c_38]) ).
cnf(c_3696,plain,
m0(A,d,B) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3695]) ).
cnf(c_39,plain,
m0(A,d,B) = r0(b),
inference(paramod,[status(thm)],[c_19,c_3696]) ).
fof(rule_107,axiom,
! [VAR_0] : ifeq(m0(e,d,VAR_0),true,ifeq(m0(VAR_0,d,VAR_0),true,q1(e,VAR_0,VAR_0),true),true) = true,
file('theBenchmark.p',rule_107) ).
cnf(c_279,plain,
ifeq(m0(e,d,A),true,ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true,
inference(clausify,[status(thm)],[rule_107]) ).
cnf(c_3697,plain,
ifeq(r0(b),true,ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_39,c_279]) ).
cnf(c_3698,plain,
ifeq(r0(b),s0(d),ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3697]) ).
cnf(c_3699,plain,
ifeq(r0(b),s0(b),ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_11,c_3698]) ).
cnf(c_3700,plain,
ifeq(r0(b),r0(b),ifeq(m0(A,d,A),true,q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_19,c_3699]) ).
cnf(c_3701,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),true,q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_39,c_3700]) ).
cnf(c_3702,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),s0(d),q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_3701]) ).
cnf(c_3703,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),s0(b),q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_11,c_3702]) ).
cnf(c_3704,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),r0(b),q1(e,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_19,c_3703]) ).
cnf(c_3705,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),r0(b),q1(e,A,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_3704]) ).
cnf(c_3706,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),r0(b),q1(e,A,A),s0(b)),true) = true,
inference(paramod,[status(thm)],[c_11,c_3705]) ).
cnf(c_3707,plain,
ifeq(r0(b),r0(b),ifeq(r0(b),r0(b),q1(e,A,A),r0(b)),true) = true,
inference(paramod,[status(thm)],[c_19,c_3706]) ).
cnf(c_3708,plain,
ifeq(r0(b),r0(b),q1(e,A,A),true) = true,
inference(paramod,[status(thm)],[c_1,c_3707]) ).
cnf(c_3709,plain,
ifeq(r0(b),r0(b),q1(e,A,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3708]) ).
cnf(c_3710,plain,
ifeq(r0(b),r0(b),q1(e,A,A),s0(b)) = true,
inference(paramod,[status(thm)],[c_11,c_3709]) ).
cnf(c_3711,plain,
ifeq(r0(b),r0(b),q1(e,A,A),r0(b)) = true,
inference(paramod,[status(thm)],[c_19,c_3710]) ).
cnf(c_3712,plain,
q1(e,A,A) = true,
inference(paramod,[status(thm)],[c_1,c_3711]) ).
cnf(c_3713,plain,
q1(e,A,A) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3712]) ).
cnf(c_3714,plain,
q1(e,A,A) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3713]) ).
cnf(c_280,plain,
q1(e,A,A) = r0(b),
inference(paramod,[status(thm)],[c_19,c_3714]) ).
fof(rule_129,axiom,
! [VAR_0,VAR_1] : ifeq(q1(VAR_0,VAR_1,VAR_1),true,k2(VAR_1,VAR_1),true) = true,
file('theBenchmark.p',rule_129) ).
cnf(c_321,plain,
ifeq(q1(A,B,B),true,k2(B,B),true) = true,
inference(clausify,[status(thm)],[rule_129]) ).
cnf(c_3715,plain,
ifeq(q1(A,B,B),s0(d),k2(B,B),true) = true,
inference(paramod,[status(thm)],[c_3,c_321]) ).
cnf(c_3716,plain,
ifeq(q1(A,B,B),s0(b),k2(B,B),true) = true,
inference(paramod,[status(thm)],[c_11,c_3715]) ).
cnf(c_3717,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),true) = true,
inference(paramod,[status(thm)],[c_19,c_3716]) ).
cnf(c_3718,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3717]) ).
cnf(c_3719,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),s0(b)) = true,
inference(paramod,[status(thm)],[c_11,c_3718]) ).
cnf(c_3720,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),r0(b)) = true,
inference(paramod,[status(thm)],[c_19,c_3719]) ).
cnf(c_3721,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),r0(b)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3720]) ).
cnf(c_3722,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),r0(b)) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3721]) ).
cnf(c_322,plain,
ifeq(q1(A,B,B),r0(b),k2(B,B),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_19,c_3722]) ).
fof(rule_194,axiom,
! [VAR_0,VAR_1] : ifeq(k2(VAR_0,VAR_1),true,k3(VAR_1,VAR_1,VAR_0),true) = true,
file('theBenchmark.p',rule_194) ).
cnf(c_449,plain,
ifeq(k2(A,B),true,k3(B,B,A),true) = true,
inference(clausify,[status(thm)],[rule_194]) ).
cnf(c_3723,plain,
ifeq(k2(A,B),s0(d),k3(B,B,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_449]) ).
cnf(c_3724,plain,
ifeq(k2(A,B),s0(b),k3(B,B,A),true) = true,
inference(paramod,[status(thm)],[c_11,c_3723]) ).
cnf(c_3725,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),true) = true,
inference(paramod,[status(thm)],[c_19,c_3724]) ).
cnf(c_3726,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3725]) ).
cnf(c_3727,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),s0(b)) = true,
inference(paramod,[status(thm)],[c_11,c_3726]) ).
cnf(c_3728,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),r0(b)) = true,
inference(paramod,[status(thm)],[c_19,c_3727]) ).
cnf(c_3729,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),r0(b)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3728]) ).
cnf(c_3730,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),r0(b)) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3729]) ).
cnf(c_450,plain,
ifeq(k2(A,B),r0(b),k3(B,B,A),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_19,c_3730]) ).
fof(rule_287,axiom,
! [VAR_0,VAR_1] : ifeq(k3(VAR_0,VAR_0,VAR_1),true,p4(VAR_0,VAR_1,VAR_0),true) = true,
file('theBenchmark.p',rule_287) ).
cnf(c_627,plain,
ifeq(k3(A,A,B),true,p4(A,B,A),true) = true,
inference(clausify,[status(thm)],[rule_287]) ).
cnf(c_3731,plain,
ifeq(k3(A,A,B),s0(d),p4(A,B,A),true) = true,
inference(paramod,[status(thm)],[c_3,c_627]) ).
cnf(c_3732,plain,
ifeq(k3(A,A,B),s0(b),p4(A,B,A),true) = true,
inference(paramod,[status(thm)],[c_11,c_3731]) ).
cnf(c_3733,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),true) = true,
inference(paramod,[status(thm)],[c_19,c_3732]) ).
cnf(c_3734,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_3733]) ).
cnf(c_3735,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),s0(b)) = true,
inference(paramod,[status(thm)],[c_11,c_3734]) ).
cnf(c_3736,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),r0(b)) = true,
inference(paramod,[status(thm)],[c_19,c_3735]) ).
cnf(c_3737,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),r0(b)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_3736]) ).
cnf(c_3738,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),r0(b)) = s0(b),
inference(paramod,[status(thm)],[c_11,c_3737]) ).
cnf(c_628,plain,
ifeq(k3(A,A,B),r0(b),p4(A,B,A),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_19,c_3738]) ).
fof(prove_this,axiom,
! [VAR_0,VAR_1] : p4(VAR_0,c,VAR_1) != true,
file('theBenchmark.p',prove_this) ).
cnf(c_715,plain,
p4(A,c,B) != true,
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_3739,plain,
p4(A,c,B) != s0(d),
inference(paramod,[status(thm)],[c_3,c_715]) ).
cnf(c_3740,plain,
p4(A,c,B) != s0(b),
inference(paramod,[status(thm)],[c_11,c_3739]) ).
cnf(c_716,plain,
p4(A,c,B) != r0(b),
inference(paramod,[status(thm)],[c_19,c_3740]) ).
cnf(c_3741,plain,
ifeq(r0(b),r0(b),k2(A,A),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_280,c_322]) ).
cnf(c_993,plain,
k2(A,A) = r0(b),
inference(paramod,[status(thm)],[c_1,c_3741]) ).
cnf(c_3742,plain,
ifeq(r0(b),r0(b),k3(A,A,A),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_993,c_450]) ).
cnf(c_1962,plain,
k3(A,A,A) = r0(b),
inference(paramod,[status(thm)],[c_1,c_3742]) ).
cnf(c_3743,plain,
ifeq(r0(b),r0(b),p4(A,A,A),r0(b)) = r0(b),
inference(paramod,[status(thm)],[c_1962,c_628]) ).
cnf(c_3690,plain,
p4(A,A,A) = r0(b),
inference(paramod,[status(thm)],[c_1,c_3743]) ).
cnf(c_3691,plain,
$false,
inference(resolve,[status(thm)],[c_3690,c_716]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN170-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /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 : Sat Sep 26 17:17:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3233083 was started by sandbox on n013,
% 0.09/0.37 % Sat Sep 26 17:17:21 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 3.26/0.88
% 3.26/0.88 % SZS status Unsatisfiable for theBenchmark
% 3.26/0.88
% 3.26/0.88 % Proof 1 at 0.35 (+ 0.09) seconds.
% 3.26/0.88 % Length of proof is 23.
% 3.26/0.88 % Level of proof is 9.
% 3.26/0.88 % Maximum clause weight is 31.000.
% 3.26/0.88 % Given clauses 341.
% 3.26/0.88
% 3.26/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------