%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWC002-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 07:32:06 AM UTC 2026
% Result : Unsatisfiable 0.09s 15.64s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 9
% Syntax : Number of formulae : 52 ( 52 unt; 0 def)
% Number of atoms : 52 ( 42 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-4 aty)
% Number of variables : 140 ( 1 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(and_definition1,axiom,
and(n0,n0) = n0,
file('theBenchmark.p',and_definition1) ).
cnf(c_1,plain,
and(n0,n0) = n0,
inference(clausify,[status(thm)],[and_definition1]) ).
fof(and_definition2,axiom,
and(n0,n1) = n0,
file('theBenchmark.p',and_definition2) ).
cnf(c_2,plain,
and(n0,n1) = n0,
inference(clausify,[status(thm)],[and_definition2]) ).
fof(subsume_symmetric,axiom,
! [VAR_0,VAR_1] : circuit(top(VAR_0),VAR_1,bottom(VAR_0)),
file('theBenchmark.p',subsume_symmetric) ).
cnf(c_26,plain,
circuit(top(A),B,bottom(A)),
inference(clausify,[status(thm)],[subsume_symmetric]) ).
fof(and_table_definition,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7] : and(table(VAR_0,VAR_1,VAR_2,VAR_3),table(VAR_4,VAR_5,VAR_6,VAR_7)) = table(and(VAR_0,VAR_4),and(VAR_1,VAR_5),and(VAR_2,VAR_6),and(VAR_3,VAR_7)),
file('theBenchmark.p',and_table_definition) ).
cnf(c_27,plain,
and(table(A,B,C,D),table(E,F,V6,V7)) = table(and(A,E),and(B,F),and(C,V6),and(D,V7)),
inference(clausify,[status(thm)],[and_table_definition]) ).
cnf(c_28,plain,
table(and(A,B),and(C,D),and(E,F),and(V6,V7)) = and(table(A,C,E,V6),table(B,D,F,V7)),
inference(copy,[status(thm)],[c_27]) ).
fof(and_definition5,axiom,
! [VAR_0] : and(nil,VAR_0) = VAR_0,
file('theBenchmark.p',and_definition5) ).
cnf(c_29,plain,
and(nil,A) = A,
inference(clausify,[status(thm)],[and_definition5]) ).
fof(empty_table,axiom,
table(n0,n0,n0,n0) = nil,
file('theBenchmark.p',empty_table) ).
cnf(c_36,plain,
table(n0,n0,n0,n0) = nil,
inference(clausify,[status(thm)],[empty_table]) ).
fof(full_table,axiom,
table(n1,n1,n1,n1) = nil,
file('theBenchmark.p',full_table) ).
cnf(c_37,plain,
table(n1,n1,n1,n1) = nil,
inference(clausify,[status(thm)],[full_table]) ).
fof(connect_definition1,axiom,
! [VAR_0] : connect(nil,VAR_0) = VAR_0,
file('theBenchmark.p',connect_definition1) ).
cnf(c_38,plain,
connect(nil,A) = A,
inference(clausify,[status(thm)],[connect_definition1]) ).
fof(prove_output_configuration,axiom,
~ circuit(top(connect(table(n0,n1,n0,n1),nil)),nil,bottom(connect(table(n0,n0,n1,n1),nil))),
file('theBenchmark.p',prove_output_configuration) ).
cnf(c_41,plain,
~ circuit(top(connect(table(n0,n1,n0,n1),nil)),nil,bottom(connect(table(n0,n0,n1,n1),nil))),
inference(clausify,[status(thm)],[prove_output_configuration]) ).
cnf(c_42,plain,
table(n0,and(A,B),and(C,D),and(E,F)) = and(table(n0,A,C,E),table(n0,B,D,F)),
inference(paramod,[status(thm)],[c_1,c_28]) ).
cnf(c_43,plain,
table(and(A,B),n0,and(C,D),and(E,F)) = and(table(A,n0,C,E),table(B,n0,D,F)),
inference(paramod,[status(thm)],[c_1,c_28]) ).
cnf(c_44,plain,
table(and(A,B),and(C,D),n0,and(E,F)) = and(table(A,C,n0,E),table(B,D,n0,F)),
inference(paramod,[status(thm)],[c_1,c_28]) ).
cnf(c_267,plain,
table(n0,and(A,B),and(C,D),and(E,F)) = and(table(n0,A,C,E),table(n1,B,D,F)),
inference(paramod,[status(thm)],[c_2,c_28]) ).
cnf(c_268,plain,
and(table(n0,A,C,E),table(n0,B,D,F)) = and(table(n0,A,C,E),table(n1,B,D,F)),
inference(paramod,[status(thm)],[c_42,c_267]) ).
cnf(c_46,plain,
and(table(n0,A,B,C),table(n1,D,E,F)) = and(table(n0,A,B,C),table(n0,D,E,F)),
inference(copy,[status(thm)],[c_268]) ).
cnf(c_269,plain,
table(and(A,B),n0,and(C,D),and(E,F)) = and(table(A,n0,C,E),table(B,n1,D,F)),
inference(paramod,[status(thm)],[c_2,c_28]) ).
cnf(c_270,plain,
and(table(A,n0,C,E),table(B,n0,D,F)) = and(table(A,n0,C,E),table(B,n1,D,F)),
inference(paramod,[status(thm)],[c_43,c_269]) ).
cnf(c_47,plain,
and(table(A,n0,B,C),table(D,n1,E,F)) = and(table(A,n0,B,C),table(D,n0,E,F)),
inference(copy,[status(thm)],[c_270]) ).
cnf(c_271,plain,
table(and(A,B),and(C,D),n0,and(E,F)) = and(table(A,C,n0,E),table(B,D,n1,F)),
inference(paramod,[status(thm)],[c_2,c_28]) ).
cnf(c_272,plain,
and(table(A,C,n0,E),table(B,D,n0,F)) = and(table(A,C,n0,E),table(B,D,n1,F)),
inference(paramod,[status(thm)],[c_44,c_271]) ).
cnf(c_48,plain,
and(table(A,B,n0,C),table(D,E,n1,F)) = and(table(A,B,n0,C),table(D,E,n0,F)),
inference(copy,[status(thm)],[c_272]) ).
cnf(c_273,plain,
and(nil,table(n1,A,B,C)) = and(table(n0,n0,n0,n0),table(n0,A,B,C)),
inference(paramod,[status(thm)],[c_36,c_46]) ).
cnf(c_274,plain,
table(n1,A,B,C) = and(table(n0,n0,n0,n0),table(n0,A,B,C)),
inference(paramod,[status(thm)],[c_29,c_273]) ).
cnf(c_275,plain,
table(n1,A,B,C) = and(nil,table(n0,A,B,C)),
inference(paramod,[status(thm)],[c_36,c_274]) ).
cnf(c_169,plain,
table(n1,A,B,C) = table(n0,A,B,C),
inference(paramod,[status(thm)],[c_29,c_275]) ).
cnf(c_172,plain,
table(n0,n1,n1,n1) = nil,
inference(paramod,[status(thm)],[c_169,c_37]) ).
cnf(c_276,plain,
and(nil,table(A,n1,B,C)) = and(table(n0,n0,n0,n0),table(A,n0,B,C)),
inference(paramod,[status(thm)],[c_36,c_47]) ).
cnf(c_277,plain,
table(A,n1,B,C) = and(table(n0,n0,n0,n0),table(A,n0,B,C)),
inference(paramod,[status(thm)],[c_29,c_276]) ).
cnf(c_278,plain,
table(A,n1,B,C) = and(nil,table(A,n0,B,C)),
inference(paramod,[status(thm)],[c_36,c_277]) ).
cnf(c_202,plain,
table(A,n1,B,C) = table(A,n0,B,C),
inference(paramod,[status(thm)],[c_29,c_278]) ).
cnf(c_233,plain,
table(n0,n0,n1,n1) = nil,
inference(paramod,[status(thm)],[c_202,c_172]) ).
cnf(c_279,plain,
~ circuit(top(connect(table(n0,n0,n0,n1),nil)),nil,bottom(connect(table(n0,n0,n1,n1),nil))),
inference(paramod,[status(thm)],[c_202,c_41]) ).
cnf(c_280,plain,
~ circuit(top(connect(table(n0,n0,n0,n1),nil)),nil,bottom(connect(nil,nil))),
inference(paramod,[status(thm)],[c_233,c_279]) ).
cnf(c_237,plain,
~ circuit(top(connect(table(n0,n0,n0,n1),nil)),nil,bottom(nil)),
inference(paramod,[status(thm)],[c_38,c_280]) ).
cnf(c_281,plain,
and(nil,table(A,B,n1,C)) = and(table(n0,n0,n0,n0),table(A,B,n0,C)),
inference(paramod,[status(thm)],[c_36,c_48]) ).
cnf(c_282,plain,
table(A,B,n1,C) = and(table(n0,n0,n0,n0),table(A,B,n0,C)),
inference(paramod,[status(thm)],[c_29,c_281]) ).
cnf(c_283,plain,
table(A,B,n1,C) = and(nil,table(A,B,n0,C)),
inference(paramod,[status(thm)],[c_36,c_282]) ).
cnf(c_253,plain,
table(A,B,n1,C) = table(A,B,n0,C),
inference(paramod,[status(thm)],[c_29,c_283]) ).
cnf(c_261,plain,
table(n0,n0,n0,n1) = nil,
inference(paramod,[status(thm)],[c_253,c_233]) ).
cnf(c_284,plain,
~ circuit(top(connect(nil,nil)),nil,bottom(nil)),
inference(paramod,[status(thm)],[c_261,c_237]) ).
cnf(c_285,plain,
~ circuit(top(nil),nil,bottom(nil)),
inference(paramod,[status(thm)],[c_38,c_284]) ).
cnf(c_266,plain,
$false,
inference(resolve,[status(thm)],[c_26,c_285]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWC002-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/15.61 % CPULimit : 300
% 0.09/15.61 % WCLimit : 300
% 0.09/15.61 % DateTime : Fri Sep 25 15:58:49 UTC 2026
% 0.09/15.61 % CPUTime :
% 0.09/15.61 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/15.61 % Process 618384 was started by sandbox on n014,
% 0.09/15.61 % Fri Sep 25 15:58:49 2026
% 0.09/15.61 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/15.62
% 0.09/15.62 % From the command line: assign(max_seconds, 300).
% 0.09/15.64
% 0.09/15.64 % SZS status Unsatisfiable for theBenchmark
% 0.09/15.64
% 0.09/15.64 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.09/15.64 % Length of proof is 24.
% 0.09/15.64 % Level of proof is 8.
% 0.09/15.64 % Maximum clause weight is 40.000.
% 0.09/15.64 % Given clauses 54.
% 0.09/15.64
% 0.09/15.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------