%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG440-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 06:50:12 AM UTC 2026
% Result : Unsatisfiable 7.85s 1.43s
% Output : CNFRefutation 7.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG440-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n006.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 22:01:11 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 2212218 was started by sandbox on n006,
% 0.11/0.37 % Sat Sep 26 22:01:11 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 7.85/1.43
% 7.85/1.43 % SZS status Unsatisfiable for theBenchmark
% 7.85/1.43
% 7.85/1.43 % Proof 1 at 0.66 (+ 0.21) seconds.
% 7.85/1.43 % Length of proof is 31.
% 7.85/1.43 % Level of proof is 7.
% 7.85/1.43 % Maximum clause weight is 29.000.
% 7.85/1.43 % Given clauses 36.
% 7.85/1.43
% 7.85/1.43 % SZS output start CNFRefutation for theBenchmark
% 7.85/1.43 fof(sos, axiom, ! [VAR_0,VAR_1] : (m(VAR_0,VAR_0,VAR_1) = VAR_1), file('theBenchmark.p',sos)).
% 7.85/1.43 cnf(c_1, plain, m(A,A,B) = B, inference(clausify, [status(thm)], [sos])).
% 7.85/1.43 fof(sos_001, axiom, ! [VAR_0,VAR_1] : (m(VAR_0,VAR_1,VAR_1) = VAR_0), file('theBenchmark.p',sos_001)).
% 7.85/1.43 cnf(c_2, plain, m(A,B,B) = A, inference(clausify, [status(thm)], [sos_001])).
% 7.85/1.43 fof(sos_002, axiom, ! [VAR_0] : (u(VAR_0,VAR_0,VAR_0) = VAR_0), file('theBenchmark.p',sos_002)).
% 7.85/1.43 cnf(c_3, plain, u(A,A,A) = A, inference(clausify, [status(thm)], [sos_002])).
% 7.85/1.43 fof(sos_004, axiom, ! [VAR_0,VAR_1] : (u(VAR_0,VAR_0,VAR_1) = u(VAR_0,VAR_1,VAR_0)), file('theBenchmark.p',sos_004)).
% 7.85/1.43 cnf(c_5, plain, u(A,A,B) = u(A,B,A), inference(clausify, [status(thm)], [sos_004])).
% 7.85/1.43 cnf(c_6, plain, u(A,B,A) = u(A,A,B),
% 7.85/1.43 inference(copy, [status(thm)], [c_5])).
% 7.85/1.43 fof(sos_005, axiom, ! [VAR_0,VAR_1] : (u(VAR_0,VAR_0,VAR_1) = u(VAR_1,VAR_0,VAR_0)), file('theBenchmark.p',sos_005)).
% 7.85/1.43 cnf(c_7, plain, u(A,A,B) = u(B,A,A), inference(clausify, [status(thm)], [sos_005])).
% 7.85/1.43 cnf(c_8, plain, u(A,B,B) = u(B,B,A),
% 7.85/1.43 inference(copy, [status(thm)], [c_7])).
% 7.85/1.43 fof(sos_006, axiom, ! [VAR_0,VAR_1] : (VAR_0 v VAR_1 = VAR_1 v VAR_0), file('theBenchmark.p',sos_006)).
% 7.85/1.43 cnf(c_9, plain, A v B = B v A, inference(clausify, [status(thm)], [sos_006])).
% 7.85/1.43 fof(sos_007, axiom, ! [VAR_0,VAR_1] : (u(VAR_0,VAR_0,VAR_1) = VAR_0 v VAR_1), file('theBenchmark.p',sos_007)).
% 7.85/1.43 cnf(c_10, plain, u(A,A,B) = A v B, inference(clausify, [status(thm)], [sos_007])).
% 7.85/1.43 cnf(c_11, plain, A v B = u(A,A,B),
% 7.85/1.43 inference(copy, [status(thm)], [c_10])).
% 7.85/1.43 fof(sos_008, axiom, ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] : (~ (r(VAR_0,VAR_1,VAR_2)) | ~ (r(VAR_3,VAR_4,VAR_5)) | ~ (r(VAR_6,VAR_7,VAR_8)) | r(m(VAR_0,VAR_3,VAR_6),m(VAR_1,VAR_4,VAR_7),m(VAR_2,VAR_5,VAR_8))), file('theBenchmark.p',sos_008)).
% 7.85/1.43 cnf(c_12, plain, ~r(A,B,C) | ~r(D,E,F) | ~r(V6,V7,V8) | r(m(A,D,V6),m(B,E,V7),m(C,F,V8)), inference(clausify, [status(thm)], [sos_008])).
% 7.85/1.43 fof(sos_009, axiom, ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] : (~ (r(VAR_0,VAR_1,VAR_2)) | ~ (r(VAR_3,VAR_4,VAR_5)) | ~ (r(VAR_6,VAR_7,VAR_8)) | r(u(VAR_0,VAR_3,VAR_6),u(VAR_1,VAR_4,VAR_7),u(VAR_2,VAR_5,VAR_8))), file('theBenchmark.p',sos_009)).
% 7.85/1.43 cnf(c_13, plain, ~r(A,B,C) | ~r(D,E,F) | ~r(V6,V7,V8) | r(u(A,D,V6),u(B,E,V7),u(C,F,V8)), inference(clausify, [status(thm)], [sos_009])).
% 7.85/1.43 fof(sos_010, axiom, ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] : (~ (r(VAR_0,VAR_1,VAR_2)) | ~ (r(VAR_3,VAR_4,VAR_5)) | r(VAR_0 v VAR_3,VAR_1 v VAR_4,VAR_2 v VAR_5)), file('theBenchmark.p',sos_010)).
% 7.85/1.43 cnf(c_14, plain, ~r(A,B,C) | ~r(D,E,F) | r(A v D,B v E,C v F), inference(clausify, [status(thm)], [sos_010])).
% 7.85/1.43 cnf(c_4305, plain, ~r(A,B,C) | ~r(D,E,F) | r(u(A,A,D),B v E,C v F),
% 7.85/1.43 inference(paramod, [status(thm)], [c_11, c_14])).
% 7.85/1.43 cnf(c_4306, plain, ~r(A,B,C) | ~r(D,E,F) | r(u(A,A,D),u(B,B,E),C v F),
% 7.85/1.43 inference(paramod, [status(thm)], [c_11, c_4305])).
% 7.85/1.43 cnf(c_15, plain, ~r(A,B,C) | ~r(D,E,F) | r(u(A,A,D),u(B,B,E),u(C,C,F)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_11, c_4306])).
% 7.85/1.43 fof(sos_011, axiom, (r(a,a,b)), file('theBenchmark.p',sos_011)).
% 7.85/1.43 cnf(c_16, plain, r(a,a,b), inference(clausify, [status(thm)], [sos_011])).
% 7.85/1.43 fof(sos_012, axiom, (r(a,b,a)), file('theBenchmark.p',sos_012)).
% 7.85/1.43 cnf(c_17, plain, r(a,b,a), inference(clausify, [status(thm)], [sos_012])).
% 7.85/1.43 fof(sos_013, axiom, (r(b,a,a)), file('theBenchmark.p',sos_013)).
% 7.85/1.43 cnf(c_18, plain, r(b,a,a), inference(clausify, [status(thm)], [sos_013])).
% 7.85/1.43 fof(goals, axiom, (~ (r(a,a,a))), file('theBenchmark.p',goals)).
% 7.85/1.43 cnf(c_19, plain, ~r(a,a,a), inference(clausify, [status(thm)], [goals])).
% 7.85/1.43 cnf(c_4307, plain, u(A,A,B) = B v A,
% 7.85/1.43 inference(paramod, [status(thm)], [c_11, c_9])).
% 7.85/1.43 cnf(c_20, plain, u(A,A,B) = u(B,B,A),
% 7.85/1.43 inference(paramod, [status(thm)], [c_11, c_4307])).
% 7.85/1.43 cnf(c_4308, plain, u(A,B,A) = u(B,A,A),
% 7.85/1.43 inference(paramod, [status(thm)], [c_8, c_6])).
% 7.85/1.43 cnf(c_21, plain, u(A,B,B) = u(B,A,B),
% 7.85/1.43 inference(copy, [status(thm)], [c_4308])).
% 7.85/1.43 cnf(c_4309, plain, ~r(A,B,C) | r(u(a,a,A),u(b,b,B),u(a,a,C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_15, c_17])).
% 7.85/1.43 cnf(c_4310, plain, r(u(a,a,a),u(b,b,a),u(a,a,b)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4309, c_16])).
% 7.85/1.43 cnf(c_4311, plain, r(a,u(b,b,a),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_3, c_4310])).
% 7.85/1.43 cnf(c_4312, plain, r(a,u(b,a,b),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_6, c_4311])).
% 7.85/1.43 cnf(c_23, plain, r(a,u(a,b,b),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_21, c_4312])).
% 7.85/1.43 cnf(c_4313, plain, ~r(A,B,C) | r(u(b,b,A),u(a,a,B),u(a,a,C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_15, c_18])).
% 7.85/1.43 cnf(c_4314, plain, r(u(b,b,a),u(a,a,b),u(a,a,a)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4313, c_17])).
% 7.85/1.43 cnf(c_4315, plain, r(u(b,a,b),u(a,a,b),u(a,a,a)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_6, c_4314])).
% 7.85/1.43 cnf(c_4316, plain, r(u(a,b,b),u(a,a,b),u(a,a,a)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_21, c_4315])).
% 7.85/1.43 cnf(c_28, plain, r(u(a,b,b),u(a,a,b),a),
% 7.85/1.43 inference(paramod, [status(thm)], [c_3, c_4316])).
% 7.85/1.43 cnf(c_4317, plain, ~r(A,B,C) | r(u(b,b,A),u(a,a,B),u(a,a,C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_15, c_18])).
% 7.85/1.43 cnf(c_4318, plain, r(u(b,b,a),u(a,a,a),u(a,a,b)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4317, c_16])).
% 7.85/1.43 cnf(c_4319, plain, r(u(b,a,b),u(a,a,a),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_6, c_4318])).
% 7.85/1.43 cnf(c_4320, plain, r(u(a,b,b),u(a,a,a),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_21, c_4319])).
% 7.85/1.43 cnf(c_29, plain, r(u(a,b,b),a,u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_3, c_4320])).
% 7.85/1.43 cnf(c_4321, plain, ~r(A,B,C) | ~r(D,E,F) | r(u(a,A,D),u(b,B,E),u(a,C,F)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_13, c_17])).
% 7.85/1.43 cnf(c_4322, plain, ~r(A,B,C) | r(u(a,a,A),u(b,a,B),u(a,b,C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4321, c_16])).
% 7.85/1.43 cnf(c_4323, plain, r(u(a,a,b),u(b,a,a),u(a,b,a)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4322, c_18])).
% 7.85/1.43 cnf(c_4324, plain, r(u(a,a,b),u(a,a,b),u(a,b,a)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_8, c_4323])).
% 7.85/1.43 cnf(c_30, plain, r(u(a,a,b),u(a,a,b),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_6, c_4324])).
% 7.85/1.43 cnf(c_39, plain, u(A,B,B) = u(A,A,B),
% 7.85/1.43 inference(paramod, [status(thm)], [c_20, c_8])).
% 7.85/1.43 cnf(c_40, plain, r(u(a,a,b),a,u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_39, c_29])).
% 7.85/1.43 cnf(c_41, plain, r(u(a,a,b),u(a,a,b),a),
% 7.85/1.43 inference(paramod, [status(thm)], [c_39, c_28])).
% 7.85/1.43 cnf(c_42, plain, r(a,u(a,a,b),u(a,a,b)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_39, c_23])).
% 7.85/1.43 cnf(c_4325, plain, ~r(A,B,C) | ~r(D,E,F) | r(m(u(a,a,b),A,D),m(a,B,E),m(u(a,a,b),C,F)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_12, c_40])).
% 7.85/1.43 cnf(c_4326, plain, ~r(A,B,C) | r(m(u(a,a,b),u(a,a,b),A),m(a,u(a,a,b),B),m(u(a,a,b),u(a,a,b),C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4325, c_30])).
% 7.85/1.43 cnf(c_4327, plain, r(m(u(a,a,b),u(a,a,b),u(a,a,b)),m(a,u(a,a,b),u(a,a,b)),m(u(a,a,b),u(a,a,b),a)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4326, c_41])).
% 7.85/1.43 cnf(c_4328, plain, r(u(a,a,b),m(a,u(a,a,b),u(a,a,b)),m(u(a,a,b),u(a,a,b),a)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_1, c_4327])).
% 7.85/1.43 cnf(c_4329, plain, r(u(a,a,b),a,m(u(a,a,b),u(a,a,b),a)),
% 7.85/1.43 inference(paramod, [status(thm)], [c_2, c_4328])).
% 7.85/1.43 cnf(c_3170, plain, r(u(a,a,b),a,a),
% 7.85/1.43 inference(paramod, [status(thm)], [c_1, c_4329])).
% 7.85/1.43 cnf(c_4330, plain, ~r(A,B,C) | ~r(D,E,F) | r(m(u(a,a,b),A,D),m(a,B,E),m(a,C,F)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_12, c_3170])).
% 7.85/1.43 cnf(c_4331, plain, ~r(A,B,C) | r(m(u(a,a,b),u(a,a,b),A),m(a,u(a,a,b),B),m(a,u(a,a,b),C)),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4330, c_30])).
% 7.85/1.43 cnf(c_4332, plain, r(m(u(a,a,b),u(a,a,b),a),m(a,u(a,a,b),u(a,a,b)),m(a,u(a,a,b),u(a,a,b))),
% 7.85/1.43 inference(resolve, [status(thm)], [c_4331, c_42])).
% 7.85/1.43 cnf(c_4333, plain, r(a,m(a,u(a,a,b),u(a,a,b)),m(a,u(a,a,b),u(a,a,b))),
% 7.85/1.43 inference(paramod, [status(thm)], [c_1, c_4332])).
% 7.85/1.43 cnf(c_4334, plain, r(a,a,m(a,u(a,a,b),u(a,a,b))),
% 7.85/1.43 inference(paramod, [status(thm)], [c_2, c_4333])).
% 7.85/1.43 cnf(c_4303, plain, r(a,a,a),
% 7.85/1.43 inference(paramod, [status(thm)], [c_2, c_4334])).
% 7.85/1.43 cnf(c_4304, plain, $false,
% 7.85/1.43 inference(resolve, [status(thm)], [c_4303, c_19])).
% 7.85/1.43 % SZS output end CNFRefutation for theBenchmark
%------------------------------------------------------------------------------