%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:59:59 AM UTC 2026
% Result : Theorem 10.11s 1.77s
% Output : CNFRefutation 10.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 9
% Syntax : Number of formulae : 124 ( 86 unt; 0 def)
% Number of atoms : 168 ( 167 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 58 ( 14 ~; 40 |; 2 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 174 ( 3 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_01,axiom,
! [A,B,C] : '+'('+'(A,B),C) = '+'(A,'+'(B,C)),
file('theBenchmark.p',sos_01) ).
fof(sos_02,axiom,
! [A,B] : '+'(A,B) = '+'(B,A),
file('theBenchmark.p',sos_02) ).
fof(sos_03,axiom,
! [A] : '+'(A,'0') = A,
file('theBenchmark.p',sos_03) ).
fof(sos_04,axiom,
! [A] : '==>'(A,A) = '0',
file('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [A] : '==>'(A,'0') = '0',
file('theBenchmark.p',sos_05) ).
fof(sos_06,axiom,
! [A] : '==>'('0',A) = A,
file('theBenchmark.p',sos_06) ).
fof(sos_07,axiom,
! [A,B,C] : '==>'('+'(A,B),C) = '==>'(A,'==>'(B,C)),
file('theBenchmark.p',sos_07) ).
fof(sos_08,axiom,
! [A,B] : '+'(A,'==>'(A,B)) = '+'(B,'==>'(B,A)),
file('theBenchmark.p',sos_08) ).
fof(goals_09,conjecture,
( ( '==>'(c,b) = '0'
& '==>'(c,a) = '0' )
<=> '==>'(c,'+'(a,'==>'(a,b))) = '0' ),
file('theBenchmark.p',goals_09) ).
fof(goals_09_neg,negated_conjecture,
~ ( ( '==>'(c,b) = '0'
& '==>'(c,a) = '0' )
<=> '==>'(c,'+'(a,'==>'(a,b))) = '0' ),
inference(assume_negation,[status(cth)],[goals_09]) ).
cnf(c_10,plain,
'+'('+'(A,B),C) = '+'(A,'+'(B,C)),
inference(clausify,[status(thm)],[sos_01]) ).
cnf(c_11,plain,
'+'(A,B) = '+'(B,A),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_12,plain,
'+'(A,'0') = A,
inference(clausify,[status(thm)],[sos_03]) ).
cnf(c_13,plain,
'==>'(A,A) = '0',
inference(clausify,[status(thm)],[sos_04]) ).
cnf(c_14,plain,
'==>'(A,'0') = '0',
inference(clausify,[status(thm)],[sos_05]) ).
cnf(c_15,plain,
'==>'('0',A) = A,
inference(clausify,[status(thm)],[sos_06]) ).
cnf(c_16,plain,
'==>'('+'(A,B),C) = '==>'(A,'==>'(B,C)),
inference(clausify,[status(thm)],[sos_07]) ).
cnf(c_17,plain,
'+'(A,'==>'(A,B)) = '+'(B,'==>'(B,A)),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_18,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) = '0'
| '==>'(c,a) = '0' ),
inference(clausify,[status(thm)],[goals_09_neg]) ).
cnf(c_19,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) = '0'
| '==>'(c,b) = '0' ),
inference(clausify,[status(thm)],[goals_09_neg]) ).
cnf(c_20,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) != '0'
| '==>'(c,b) != '0'
| '==>'(c,a) != '0' ),
inference(clausify,[status(thm)],[goals_09_neg]) ).
cnf(c_2596,plain,
'+'('+'(A,B),C) = '+'(B,'+'(A,C)),
inference(paramod,[status(thm)],[c_11,c_10]) ).
cnf(c_21,plain,
'+'(A,'+'(B,C)) = '+'(B,'+'(A,C)),
inference(paramod,[status(thm)],[c_10,c_2596]) ).
cnf(c_2597,plain,
A = '+'('0',A),
inference(paramod,[status(thm)],[c_12,c_11]) ).
cnf(c_24,plain,
'+'('0',A) = A,
inference(copy,[status(thm)],[c_2597]) ).
cnf(c_2598,plain,
'==>'('+'(A,B),C) = '==>'(B,'==>'(A,C)),
inference(paramod,[status(thm)],[c_11,c_16]) ).
cnf(c_25,plain,
'==>'(A,'==>'(B,C)) = '==>'(B,'==>'(A,C)),
inference(paramod,[status(thm)],[c_16,c_2598]) ).
cnf(c_26,plain,
'==>'(A,'==>'(B,'+'(A,B))) = '0',
inference(paramod,[status(thm)],[c_16,c_13]) ).
cnf(c_2599,plain,
'==>'('+'('==>'(A,B),A),B) = '0',
inference(paramod,[status(thm)],[c_13,c_16]) ).
cnf(c_2600,plain,
'==>'('+'(A,'==>'(A,B)),B) = '0',
inference(paramod,[status(thm)],[c_11,c_2599]) ).
cnf(c_27,plain,
'==>'(A,'==>'('==>'(A,B),B)) = '0',
inference(paramod,[status(thm)],[c_16,c_2600]) ).
cnf(c_2601,plain,
'+'('+'(A,'==>'(A,B)),C) = '+'(B,'+'('==>'(B,A),C)),
inference(paramod,[status(thm)],[c_17,c_10]) ).
cnf(c_28,plain,
'+'(A,'+'('==>'(A,B),C)) = '+'(B,'+'('==>'(B,A),C)),
inference(paramod,[status(thm)],[c_10,c_2601]) ).
cnf(c_2602,plain,
'+'(A,'==>'(A,'+'(B,C))) = '+'(B,'+'(C,'==>'('+'(B,C),A))),
inference(paramod,[status(thm)],[c_17,c_10]) ).
cnf(c_29,plain,
'+'(A,'==>'(A,'+'(B,C))) = '+'(B,'+'(C,'==>'(B,'==>'(C,A)))),
inference(paramod,[status(thm)],[c_16,c_2602]) ).
cnf(c_2603,plain,
'==>'('+'(A,'==>'(A,B)),C) = '==>'(B,'==>'('==>'(B,A),C)),
inference(paramod,[status(thm)],[c_17,c_16]) ).
cnf(c_31,plain,
'==>'(A,'==>'('==>'(A,B),C)) = '==>'(B,'==>'('==>'(B,A),C)),
inference(paramod,[status(thm)],[c_16,c_2603]) ).
cnf(c_36,plain,
'+'(A,'+'(B,'==>'(B,C))) = '+'(C,'+'(A,'==>'(C,B))),
inference(paramod,[status(thm)],[c_17,c_21]) ).
cnf(c_39,plain,
'==>'(A,'==>'('==>'(A,B),'+'(B,'==>'(B,A)))) = '0',
inference(paramod,[status(thm)],[c_17,c_26]) ).
cnf(c_2604,plain,
'==>'(A,'0') = '==>'(B,'==>'(A,B)),
inference(paramod,[status(thm)],[c_13,c_25]) ).
cnf(c_2605,plain,
'0' = '==>'(B,'==>'(A,B)),
inference(paramod,[status(thm)],[c_14,c_2604]) ).
cnf(c_44,plain,
'==>'(A,'==>'(B,A)) = '0',
inference(copy,[status(thm)],[c_2605]) ).
cnf(c_2606,plain,
'+'(A,'==>'(B,'==>'(A,C))) = '+'('==>'(B,C),'==>'('==>'(B,C),A)),
inference(paramod,[status(thm)],[c_25,c_17]) ).
cnf(c_47,plain,
'+'('==>'(A,B),'==>'('==>'(A,B),C)) = '+'(C,'==>'(A,'==>'(C,B))),
inference(copy,[status(thm)],[c_2606]) ).
cnf(c_2607,plain,
'+'(A,'==>'(A,'+'('==>'(B,A),B))) = '+'('==>'(B,A),'+'(B,'0')),
inference(paramod,[status(thm)],[c_13,c_29]) ).
cnf(c_2608,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,A)))) = '+'('==>'(B,A),'+'(B,'0')),
inference(paramod,[status(thm)],[c_11,c_2607]) ).
cnf(c_2609,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,A)))) = '+'('==>'(B,A),B),
inference(paramod,[status(thm)],[c_12,c_2608]) ).
cnf(c_166,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,A)))) = '+'(B,'==>'(B,A)),
inference(paramod,[status(thm)],[c_11,c_2609]) ).
cnf(c_2610,plain,
'+'(A,'==>'(A,'+'(A,B))) = '+'(A,'+'(B,'0')),
inference(paramod,[status(thm)],[c_44,c_29]) ).
cnf(c_181,plain,
'+'(A,'==>'(A,'+'(A,B))) = '+'(A,B),
inference(paramod,[status(thm)],[c_12,c_2610]) ).
cnf(c_190,plain,
'+'(A,'+'('==>'(A,B),'==>'('==>'(A,B),C))) = '+'(B,'==>'(B,'+'(C,A))),
inference(paramod,[status(thm)],[c_29,c_36]) ).
cnf(c_2611,plain,
'==>'('+'(A,'==>'(A,B)),C) = '==>'(B,'==>'('==>'(B,'+'(A,'==>'(A,B))),C)),
inference(paramod,[status(thm)],[c_166,c_16]) ).
cnf(c_2612,plain,
'==>'(A,'==>'('==>'(A,B),C)) = '==>'(B,'==>'('==>'(B,'+'(A,'==>'(A,B))),C)),
inference(paramod,[status(thm)],[c_16,c_2611]) ).
cnf(c_229,plain,
'==>'(A,'==>'('==>'(A,'+'(B,'==>'(B,A))),C)) = '==>'(B,'==>'('==>'(B,A),C)),
inference(copy,[status(thm)],[c_2612]) ).
cnf(c_2613,plain,
'+'('==>'(A,B),'==>'('==>'(A,B),'+'(C,'==>'(C,'==>'(A,B))))) = '+'(C,'==>'(A,'==>'(C,B))),
inference(paramod,[status(thm)],[c_25,c_166]) ).
cnf(c_2614,plain,
'+'(C,'==>'(C,'==>'(A,B))) = '+'(C,'==>'(A,'==>'(C,B))),
inference(paramod,[status(thm)],[c_166,c_2613]) ).
cnf(c_236,plain,
'+'(A,'==>'(B,'==>'(A,C))) = '+'(A,'==>'(A,'==>'(B,C))),
inference(copy,[status(thm)],[c_2614]) ).
cnf(c_310,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,C)))) = '+'(B,'+'('==>'(B,C),'==>'(C,'==>'('==>'(C,B),A)))),
inference(paramod,[status(thm)],[c_31,c_29]) ).
cnf(c_2615,plain,
'+'(A,'+'('==>'(A,B),'==>'('==>'(A,B),'==>'(C,D)))) = '+'(B,'+'('==>'(B,A),'==>'(C,'==>'('==>'(A,B),D)))),
inference(paramod,[status(thm)],[c_236,c_28]) ).
cnf(c_2616,plain,
'+'(B,'==>'(B,'+'('==>'(C,D),A))) = '+'(B,'+'('==>'(B,A),'==>'(C,'==>'('==>'(A,B),D)))),
inference(paramod,[status(thm)],[c_190,c_2615]) ).
cnf(c_338,plain,
'+'(A,'+'('==>'(A,B),'==>'(C,'==>'('==>'(B,A),D)))) = '+'(A,'==>'(A,'+'('==>'(C,D),B))),
inference(copy,[status(thm)],[c_2616]) ).
cnf(c_2617,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,C)))) = '+'(B,'==>'(B,'+'('==>'(C,A),C))),
inference(paramod,[status(thm)],[c_338,c_310]) ).
cnf(c_2618,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,C)))) = '+'(B,'==>'(B,'+'(C,'==>'(C,A)))),
inference(paramod,[status(thm)],[c_11,c_2617]) ).
cnf(c_349,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,C)))) = '+'(C,'==>'(C,'+'(A,'==>'(A,B)))),
inference(copy,[status(thm)],[c_2618]) ).
cnf(c_359,plain,
'+'(A,'==>'(A,'+'(B,'==>'(B,C)))) = '+'(B,'==>'(B,'+'(A,'==>'(A,C)))),
inference(paramod,[status(thm)],[c_17,c_349]) ).
cnf(c_2619,plain,
( '+'(c,'0') = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_18,c_349]) ).
cnf(c_2620,plain,
( '+'('0',c) = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_11,c_2619]) ).
cnf(c_2621,plain,
( c = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_24,c_2620]) ).
cnf(c_2622,plain,
( c = '+'(b,'==>'(b,'+'(a,'==>'(a,c))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_17,c_2621]) ).
cnf(c_361,plain,
( '+'(b,'==>'(b,'+'(a,'==>'(a,c)))) = c
| '==>'(c,a) = '0' ),
inference(copy,[status(thm)],[c_2622]) ).
cnf(c_2623,plain,
( '+'(a,'==>'(a,'+'(b,'==>'(b,c)))) = '+'(c,'0')
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_18,c_349]) ).
cnf(c_2624,plain,
( '+'(a,'==>'(a,'+'(c,'==>'(c,b)))) = '+'(c,'0')
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_17,c_2623]) ).
cnf(c_2625,plain,
( '+'(a,'==>'(a,'+'(c,'==>'(c,b)))) = '+'('0',c)
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_11,c_2624]) ).
cnf(c_363,plain,
( '+'(a,'==>'(a,'+'(c,'==>'(c,b)))) = c
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_24,c_2625]) ).
cnf(c_2626,plain,
( '+'(c,'0') = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_19,c_349]) ).
cnf(c_2627,plain,
( '+'('0',c) = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_11,c_2626]) ).
cnf(c_2628,plain,
( c = '+'(b,'==>'(b,'+'(c,'==>'(c,a))))
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_24,c_2627]) ).
cnf(c_2629,plain,
( c = '+'(b,'==>'(b,'+'(a,'==>'(a,c))))
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_17,c_2628]) ).
cnf(c_365,plain,
( '+'(b,'==>'(b,'+'(a,'==>'(a,c)))) = c
| '==>'(c,b) = '0' ),
inference(copy,[status(thm)],[c_2629]) ).
cnf(c_2630,plain,
( '+'(b,'==>'(b,c)) = '+'(b,'==>'(b,'+'(a,'==>'(a,c))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_361,c_181]) ).
cnf(c_2631,plain,
( '+'(c,'==>'(c,b)) = '+'(b,'==>'(b,'+'(a,'==>'(a,c))))
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_17,c_2630]) ).
cnf(c_432,plain,
( '+'(b,'==>'(b,'+'(a,'==>'(a,c)))) = '+'(c,'==>'(c,b))
| '==>'(c,a) = '0' ),
inference(copy,[status(thm)],[c_2631]) ).
cnf(c_2632,plain,
( '+'(c,'==>'(c,b)) = c
| '==>'(c,a) = '0'
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_432,c_361]) ).
cnf(c_584,plain,
( '+'(c,'==>'(c,b)) = c
| '==>'(c,a) = '0' ),
inference(copy,[status(thm)],[c_2632]) ).
cnf(c_2633,plain,
( '+'(a,'==>'(a,c)) = c
| '==>'(c,a) = '0'
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_584,c_363]) ).
cnf(c_598,plain,
( '+'(a,'==>'(a,c)) = c
| '==>'(c,a) = '0' ),
inference(copy,[status(thm)],[c_2633]) ).
cnf(c_2634,plain,
'+'('==>'(A,'+'(B,'==>'(B,A))),'==>'('==>'(A,'+'(B,'==>'(B,A))),'==>'(A,B))) = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_39,c_47]) ).
cnf(c_2635,plain,
'+'('==>'(A,'+'(B,'==>'(B,A))),'==>'(A,'==>'('==>'(A,'+'(B,'==>'(B,A))),B))) = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_25,c_2634]) ).
cnf(c_2636,plain,
'+'('==>'(A,'+'(B,'==>'(B,A))),'==>'(B,'==>'('==>'(B,A),B))) = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_229,c_2635]) ).
cnf(c_2637,plain,
'+'('==>'(A,'+'(B,'==>'(B,A))),'0') = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_44,c_2636]) ).
cnf(c_2638,plain,
'+'('0','==>'(A,'+'(B,'==>'(B,A)))) = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_11,c_2637]) ).
cnf(c_2639,plain,
'==>'(A,'+'(B,'==>'(B,A))) = '+'('==>'(A,B),'0'),
inference(paramod,[status(thm)],[c_24,c_2638]) ).
cnf(c_2640,plain,
'==>'(A,'+'(B,'==>'(B,A))) = '+'('0','==>'(A,B)),
inference(paramod,[status(thm)],[c_11,c_2639]) ).
cnf(c_2161,plain,
'==>'(A,'+'(B,'==>'(B,A))) = '==>'(A,B),
inference(paramod,[status(thm)],[c_24,c_2640]) ).
cnf(c_2190,plain,
'==>'(A,'+'(A,'==>'(A,B))) = '==>'(A,B),
inference(paramod,[status(thm)],[c_17,c_2161]) ).
cnf(c_2641,plain,
( '==>'('+'(a,'==>'(a,c)),c) = '==>'('+'(a,'==>'(a,c)),b)
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_365,c_2161]) ).
cnf(c_2642,plain,
( '==>'(a,'==>'('==>'(a,c),c)) = '==>'('+'(a,'==>'(a,c)),b)
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_16,c_2641]) ).
cnf(c_2643,plain,
( '0' = '==>'('+'(a,'==>'(a,c)),b)
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_27,c_2642]) ).
cnf(c_2644,plain,
( '0' = '==>'(a,'==>'('==>'(a,c),b))
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_16,c_2643]) ).
cnf(c_2200,plain,
( '==>'(a,'==>'('==>'(a,c),b)) = '0'
| '==>'(c,b) = '0' ),
inference(copy,[status(thm)],[c_2644]) ).
cnf(c_2645,plain,
( '==>'(c,c) = '==>'(c,a)
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_598,c_2161]) ).
cnf(c_2646,plain,
( '0' = '==>'(c,a)
| '==>'(c,a) = '0' ),
inference(paramod,[status(thm)],[c_13,c_2645]) ).
cnf(c_2647,plain,
( '==>'(c,a) = '0'
| '==>'(c,a) = '0' ),
inference(copy,[status(thm)],[c_2646]) ).
cnf(c_2205,plain,
'==>'(c,a) = '0',
inference(copy,[status(thm)],[c_2647]) ).
cnf(c_2648,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) != '0'
| '==>'(c,b) != '0'
| '0' != '0' ),
inference(paramod,[status(thm)],[c_2205,c_20]) ).
cnf(c_2213,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) != '0'
| '==>'(c,b) != '0' ),
inference(copy,[status(thm)],[c_2648]) ).
cnf(c_2649,plain,
'==>'(c,'==>'('0',A)) = '==>'(a,'==>'('==>'(a,c),A)),
inference(paramod,[status(thm)],[c_2205,c_31]) ).
cnf(c_2650,plain,
'==>'(c,A) = '==>'(a,'==>'('==>'(a,c),A)),
inference(paramod,[status(thm)],[c_15,c_2649]) ).
cnf(c_2219,plain,
'==>'(a,'==>'('==>'(a,c),A)) = '==>'(c,A),
inference(copy,[status(thm)],[c_2650]) ).
cnf(c_2651,plain,
'+'(A,'==>'(A,'+'(c,'0'))) = '+'(c,'==>'(c,'+'(A,'==>'(A,a)))),
inference(paramod,[status(thm)],[c_2205,c_359]) ).
cnf(c_2652,plain,
'+'(A,'==>'(A,'+'('0',c))) = '+'(c,'==>'(c,'+'(A,'==>'(A,a)))),
inference(paramod,[status(thm)],[c_11,c_2651]) ).
cnf(c_2653,plain,
'+'(A,'==>'(A,c)) = '+'(c,'==>'(c,'+'(A,'==>'(A,a)))),
inference(paramod,[status(thm)],[c_24,c_2652]) ).
cnf(c_2223,plain,
'+'(c,'==>'(c,'+'(A,'==>'(A,a)))) = '+'(A,'==>'(A,c)),
inference(copy,[status(thm)],[c_2653]) ).
cnf(c_2654,plain,
( '==>'(c,b) = '0'
| '==>'(c,b) = '0' ),
inference(paramod,[status(thm)],[c_2219,c_2200]) ).
cnf(c_2229,plain,
'==>'(c,b) = '0',
inference(copy,[status(thm)],[c_2654]) ).
cnf(c_2655,negated_conjecture,
( '==>'(c,'+'(a,'==>'(a,b))) != '0'
| '0' != '0' ),
inference(paramod,[status(thm)],[c_2229,c_2213]) ).
cnf(c_2230,negated_conjecture,
'==>'(c,'+'(a,'==>'(a,b))) != '0',
inference(copy,[status(thm)],[c_2655]) ).
cnf(c_2656,plain,
'==>'(c,'+'(A,'==>'(A,c))) = '==>'(c,'+'(A,'==>'(A,a))),
inference(paramod,[status(thm)],[c_2223,c_2190]) ).
cnf(c_2657,plain,
'==>'(c,A) = '==>'(c,'+'(A,'==>'(A,a))),
inference(paramod,[status(thm)],[c_2161,c_2656]) ).
cnf(c_2585,plain,
'==>'(c,'+'(A,'==>'(A,a))) = '==>'(c,A),
inference(copy,[status(thm)],[c_2657]) ).
cnf(c_2587,plain,
'==>'(c,'+'(a,'==>'(a,A))) = '==>'(c,A),
inference(paramod,[status(thm)],[c_17,c_2585]) ).
cnf(c_2658,negated_conjecture,
'==>'(c,b) != '0',
inference(paramod,[status(thm)],[c_2587,c_2230]) ).
cnf(c_2659,negated_conjecture,
'0' != '0',
inference(paramod,[status(thm)],[c_2229,c_2658]) ).
cnf(c_2595,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_2659]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n002.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 : Fri Sep 25 23:49:35 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 295380 was started by sandbox2 on n002,
% 0.11/0.38 % Fri Sep 25 23:49:35 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 10.11/1.77
% 10.11/1.77 % SZS status Theorem for theBenchmark
% 10.11/1.77
% 10.11/1.77 % Proof 1 at 1.10 (+ 0.26) seconds.
% 10.11/1.77 % Length of proof is 59.
% 10.11/1.77 % Level of proof is 15.
% 10.11/1.77 % Maximum clause weight is 69.000.
% 10.11/1.77 % Given clauses 137.
% 10.11/1.77
% 10.11/1.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------