%------------------------------------------------------------------------------
% File : Waldmeister---710
% Problem : ROB006-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : woody %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 20:57:13 EDT 2022
% Result : Unsatisfiable 2.35s 2.72s
% Output : CNFRefutation 2.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : ROB006-2 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.12 % Command : woody %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 9 13:58:38 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.68/1.05 ********************************************************************************
% 0.68/1.05 * W A L D M E I S T E R \| \ / \|/ *
% 0.68/1.05 * |/ | \/ | *
% 0.68/1.05 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / *
% 0.68/1.05 * A. Jaeger and B. Loechner | | *
% 0.68/1.05 * <waldmeister@informatik.uni-kl.de> | *
% 0.68/1.05 ********************************************************************************
% 0.68/1.05
% 0.68/1.05
% 0.68/1.05 Goals:
% 0.68/1.05 ------
% 0.68/1.05
% 0.68/1.05 ( 1) true ?= false
% 0.68/1.05 using narrowing to prove x1 ?= add(x1,x1)
% 0.68/1.05
% 0.68/1.05 Detected structure: RobbinsAlgebra
% 0.68/1.05 ********************************************************************************
% 0.68/1.05 ****************************** COMPLETION - PROOF ******************************
% 0.68/1.05 ********************************************************************************
% 0.68/1.05
% 2.35/2.72 joined goal: 1 x1 ?= add(x1,x1) to false
% 2.35/2.72 goal joined
% 2.35/2.72 % SZS status Unsatisfiable
% 2.35/2.72 #START OF PROOF
% 2.35/2.72 % SZS output start CNFRefutation
% 2.35/2.72 cnf('0.1.0.0',axiom,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.1.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1.0.0']),
% 2.35/2.72 [weight('<0,0,0,[0,0,0,1]>')]).
% 2.35/2.72 cnf('0.1.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X1,negate(X2))))) = X1 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_1]).
% 2.35/2.72 cnf('0.2.0.0',axiom,
% 2.35/2.72 ( add(X1,X2) = add(X2,X1) ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.2.1.0',plain,
% 2.35/2.72 ( add(X1,X2) = add(X2,X1) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.2.0.0']),
% 2.35/2.72 [weight('<1,0,0,[0,0,0,2]>')]).
% 2.35/2.72 cnf('0.2.2.0',plain,
% 2.35/2.72 ( add(X1,X2) = add(X2,X1) ),
% 2.35/2.72 inference(activate,[status(thm)],['0.2.1.0']),
% 2.35/2.72 [equation_1]).
% 2.35/2.72 cnf('0.3.0.0',axiom,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(add(X1,X2),X3) ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.3.1.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(add(X1,X2),X3) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.3.0.0']),
% 2.35/2.72 [weight('<2,0,0,[0,0,0,3]>')]).
% 2.35/2.72 cnf('0.3.2.0',plain,
% 2.35/2.72 ( add(add(X1,X2),X3) = add(X1,add(X2,X3)) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.3.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_2]).
% 2.35/2.72 cnf('0.4.0.0',axiom,
% 2.35/2.72 ( add(c,d) = d ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.4.1.0',plain,
% 2.35/2.72 ( add(c,d) = d ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.4.0.0']),
% 2.35/2.72 [weight('<3,0,0,[0,0,0,4]>')]).
% 2.35/2.72 cnf('0.4.2.0',plain,
% 2.35/2.72 ( add(c,d) = d ),
% 2.35/2.72 inference(orient,[status(thm)],['0.4.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_3]).
% 2.35/2.72 cnf('0.5.0.0',axiom,
% 2.35/2.72 ( eq(X1,X1) = true ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.5.1.0',plain,
% 2.35/2.72 ( eq(X1,X1) = true ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.5.0.0']),
% 2.35/2.72 [weight('<4,0,0,[0,0,0,5]>')]).
% 2.35/2.72 cnf('0.5.2.0',plain,
% 2.35/2.72 ( eq(X1,X1) = true ),
% 2.35/2.72 inference(orient,[status(thm)],['0.5.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_4]).
% 2.35/2.72 cnf('0.6.0.0',axiom,
% 2.35/2.72 ( eq(X1,add(X1,X1)) = false ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023')).
% 2.35/2.72 cnf('0.6.1.0',plain,
% 2.35/2.72 ( eq(X1,add(X1,X1)) = false ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.6.0.0']),
% 2.35/2.72 [weight('<5,0,0,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.6.2.0',plain,
% 2.35/2.72 ( eq(X1,add(X1,X1)) = false ),
% 2.35/2.72 inference(orient,[status(thm)],['0.6.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_5]).
% 2.35/2.72 cnf('0.7.0.0',plain,
% 2.35/2.72 ( add(c,add(d,X1)) = add(d,X1) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.3.2.0','0.4.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1','L')]).
% 2.35/2.72 cnf('0.7.1.0',plain,
% 2.35/2.72 ( add(c,add(d,X1)) = add(d,X1) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.7.0.0']),
% 2.35/2.72 [weight('<25,4,3,[0,0,0,1]>')]).
% 2.35/2.72 cnf('0.7.2.0',plain,
% 2.35/2.72 ( add(c,add(d,X1)) = add(d,X1) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.7.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_6]).
% 2.35/2.72 cnf('0.8.0.0',plain,
% 2.35/2.72 ( add(d,X1) = add(c,add(X1,d)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.7.2.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.8.1.0',plain,
% 2.35/2.72 ( add(d,X1) = add(c,add(X1,d)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.8.0.0']),
% 2.35/2.72 [weight('<25,7,2,[1,0,0,2]>')]).
% 2.35/2.72 cnf('0.8.2.0',plain,
% 2.35/2.72 ( add(c,add(X1,d)) = add(d,X1) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.8.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_7]).
% 2.35/2.72 cnf('0.9.0.0',plain,
% 2.35/2.72 ( c = negate(add(negate(d),negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.4.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.9.1.0',plain,
% 2.35/2.72 ( c = negate(add(negate(d),negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.9.0.0']),
% 2.35/2.72 [weight('<29,4,1,[0,0,0,3]>')]).
% 2.35/2.72 cnf('0.9.2.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(c,negate(d))))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.9.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_8]).
% 2.35/2.72 cnf('0.10.0.0',plain,
% 2.35/2.72 ( add(c,add(add(X1,d),X2)) = add(add(d,X1),X2) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.3.2.0','0.8.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1','L')]).
% 2.35/2.72 cnf('0.10.0.1',plain,
% 2.35/2.72 ( add(c,add(X1,add(d,X2))) = add(add(d,X1),X2) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.10.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.10.0.2',plain,
% 2.35/2.72 ( add(c,add(X1,add(d,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.10.0.1','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.10.1.0',plain,
% 2.35/2.72 ( add(c,add(X1,add(d,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.10.0.2']),
% 2.35/2.72 [weight('<35,8,3,[0,0,0,1]>')]).
% 2.35/2.72 cnf('0.10.2.0',plain,
% 2.35/2.72 ( add(c,add(X1,add(d,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.10.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_9]).
% 2.35/2.72 cnf('0.11.0.0',plain,
% 2.35/2.72 ( add(d,add(c,X1)) = add(c,add(d,X1)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.10.2.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.11.0.1',plain,
% 2.35/2.72 ( add(d,add(c,X1)) = add(d,X1) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.11.0.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.11.1.0',plain,
% 2.35/2.72 ( add(d,add(c,X1)) = add(d,X1) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.11.0.1']),
% 2.35/2.72 [weight('<25,10,7,[1,0,0,2]>')]).
% 2.35/2.72 cnf('0.11.2.0',plain,
% 2.35/2.72 ( add(d,add(c,X1)) = add(d,X1) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.11.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_10]).
% 2.35/2.72 cnf('0.15.0.0',plain,
% 2.35/2.72 ( add(d,add(X1,add(c,X2))) = add(c,add(X1,add(d,X2))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.10.2.0','0.11.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2.2','L')]).
% 2.35/2.72 cnf('0.15.0.1',plain,
% 2.35/2.72 ( add(d,add(X1,add(c,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.15.0.0','0.10.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.15.1.0',plain,
% 2.35/2.72 ( add(d,add(X1,add(c,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.15.0.1']),
% 2.35/2.72 [weight('<35,11,10,[0,0,0,4]>')]).
% 2.35/2.72 cnf('0.15.2.0',plain,
% 2.35/2.72 ( add(d,add(X1,add(c,X2))) = add(d,add(X1,X2)) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.15.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_14]).
% 2.35/2.72 cnf('0.17.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,X1)),negate(add(X1,negate(X2))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.17.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,X1)),negate(add(X1,negate(X2))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.17.0.0']),
% 2.35/2.72 [weight('<39,2,1,[0,0,0,3]>')]).
% 2.35/2.72 cnf('0.17.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X2,negate(X1))))) = X2 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.17.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_16]).
% 2.35/2.72 cnf('0.21.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,X1)),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.17.2.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1','L')]).
% 2.35/2.72 cnf('0.21.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,X1)),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.21.0.0']),
% 2.35/2.72 [weight('<39,17,2,[1,0,0,7]>')]).
% 2.35/2.72 cnf('0.21.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(negate(X1),X2)))) = X2 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.21.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_20]).
% 2.35/2.72 cnf('0.25.0.0',plain,
% 2.35/2.72 ( negate(add(X1,X2)) = negate(add(negate(add(negate(add(X1,X2)),add(X1,negate(X2)))),X1)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.1.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.25.1.0',plain,
% 2.35/2.72 ( negate(add(X1,X2)) = negate(add(negate(add(negate(add(X1,X2)),add(X1,negate(X2)))),X1)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.25.0.0']),
% 2.35/2.72 [weight('<?,1,1,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.25.1.1',plain,
% 2.35/2.72 ( negate(add(X1,X2)) = negate(add(X1,negate(add(negate(add(X1,X2)),add(X1,negate(X2)))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.25.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.25.1.2',plain,
% 2.35/2.72 ( negate(add(X1,X2)) = negate(add(X1,negate(add(add(X1,negate(X2)),negate(add(X1,X2)))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.25.1.1','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.25.1.3',plain,
% 2.35/2.72 ( negate(add(X1,X2)) = negate(add(X1,negate(add(X1,add(negate(X2),negate(add(X1,X2))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.25.1.2','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.25.2.0',plain,
% 2.35/2.72 ( negate(add(X1,negate(add(X1,add(negate(X2),negate(add(X1,X2))))))) = negate(add(X1,X2)) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.25.1.3',theory(equality)]),
% 2.35/2.72 [x,rule_24]).
% 2.35/2.72 cnf('0.27.0.0',plain,
% 2.35/2.72 ( negate(add(c,negate(d))) = negate(add(negate(add(d,negate(add(c,negate(d))))),c)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.9.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.27.1.0',plain,
% 2.35/2.72 ( negate(add(c,negate(d))) = negate(add(negate(add(d,negate(add(c,negate(d))))),c)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.27.0.0']),
% 2.35/2.72 [weight('<39,21,9,[1,0,0,6]>')]).
% 2.35/2.72 cnf('0.27.1.1',plain,
% 2.35/2.72 ( negate(add(c,negate(d))) = negate(add(c,negate(add(d,negate(add(c,negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.27.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.27.2.0',plain,
% 2.35/2.72 ( negate(add(c,negate(add(d,negate(add(c,negate(d))))))) = negate(add(c,negate(d))) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.27.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_26]).
% 2.35/2.72 cnf('0.36.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))),negate(add(X1,X2)))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.1.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.36.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))),negate(add(X1,X2)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.36.0.0']),
% 2.35/2.72 [weight('<?,1,1,[0,0,0,9]>')]).
% 2.35/2.72 cnf('0.36.1.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.36.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.36.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(add(X2,X3)),negate(add(X2,negate(X3)))))))) = X1 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.36.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_35]).
% 2.35/2.72 cnf('0.48.0.0',plain,
% 2.35/2.72 ( add(X1,X2) = negate(add(negate(add(X1,add(X2,X3))),negate(add(add(X1,X2),negate(X3))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.48.0.1',plain,
% 2.35/2.72 ( add(X1,X2) = negate(add(negate(add(X1,add(X2,X3))),negate(add(X1,add(X2,negate(X3)))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.48.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.48.1.0',plain,
% 2.35/2.72 ( add(X1,X2) = negate(add(negate(add(X1,add(X2,X3))),negate(add(X1,add(X2,negate(X3)))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.48.0.1']),
% 2.35/2.72 [weight('<?,3,1,[0,0,0,3]>')]).
% 2.35/2.72 cnf('0.48.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,add(X2,X3))),negate(add(X1,add(X2,negate(X3)))))) = add(X1,X2) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.48.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_47]).
% 2.35/2.72 cnf('0.57.0.0',plain,
% 2.35/2.72 ( negate(add(negate(X1),X2)) = negate(add(negate(add(add(X1,X2),negate(add(negate(X1),X2)))),X2)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.21.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.57.0.1',plain,
% 2.35/2.72 ( negate(add(negate(X1),X2)) = negate(add(negate(add(X1,add(X2,negate(add(negate(X1),X2))))),X2)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.57.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.57.1.0',plain,
% 2.35/2.72 ( negate(add(negate(X1),X2)) = negate(add(negate(add(X1,add(X2,negate(add(negate(X1),X2))))),X2)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.57.0.1']),
% 2.35/2.72 [weight('<49,21,21,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.57.1.1',plain,
% 2.35/2.72 ( negate(add(negate(X1),X2)) = negate(add(X2,negate(add(X1,add(X2,negate(add(negate(X1),X2))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.57.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.57.2.0',plain,
% 2.35/2.72 ( negate(add(X1,negate(add(X2,add(X1,negate(add(negate(X2),X1))))))) = negate(add(negate(X2),X1)) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.57.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_56]).
% 2.35/2.72 cnf('0.59.0.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X3,X1)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.2.2.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('L','L')]).
% 2.35/2.72 cnf('0.59.1.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X3,X1)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.59.0.0']),
% 2.35/2.72 [weight('<?,3,2,[0,0,0,0]>')]).
% 2.35/2.72 cnf('0.59.2.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X3,X1)) ),
% 2.35/2.72 inference(activate,[status(thm)],['0.59.1.0']),
% 2.35/2.72 [equation_2]).
% 2.35/2.72 cnf('0.71.0.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(add(X2,X1),X3) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.3.2.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1','L')]).
% 2.35/2.72 cnf('0.71.0.1',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X1,X3)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.71.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.71.1.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X1,X3)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.71.0.1']),
% 2.35/2.72 [weight('<?,3,2,[1,0,0,1]>')]).
% 2.35/2.72 cnf('0.71.2.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X2,add(X1,X3)) ),
% 2.35/2.72 inference(activate,[status(thm)],['0.71.1.0']),
% 2.35/2.72 [equation_3]).
% 2.35/2.72 cnf('0.81.0.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X3,add(X2,X1)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.59.2.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.81.1.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X3,add(X2,X1)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.81.0.0']),
% 2.35/2.72 [weight('<50,59,2,[1,0,0,2]>')]).
% 2.35/2.72 cnf('0.81.2.0',plain,
% 2.35/2.72 ( add(X1,add(X2,X3)) = add(X3,add(X2,X1)) ),
% 2.35/2.72 inference(activate,[status(thm)],['0.81.1.0']),
% 2.35/2.72 [equation_4]).
% 2.35/2.72 cnf('0.90.0.0',plain,
% 2.35/2.72 ( c = negate(add(negate(add(c,add(d,negate(add(c,negate(d)))))),negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.27.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.90.0.1',plain,
% 2.35/2.72 ( c = negate(add(negate(add(d,negate(add(c,negate(d))))),negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.90.0.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.90.1.0',plain,
% 2.35/2.72 ( c = negate(add(negate(add(d,negate(add(c,negate(d))))),negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.90.0.1']),
% 2.35/2.72 [weight('<51,27,1,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.90.1.1',plain,
% 2.35/2.72 ( c = negate(add(negate(add(c,negate(d))),negate(add(d,negate(add(c,negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.90.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.90.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(c,negate(d))),negate(add(d,negate(add(c,negate(d))))))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.90.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_86]).
% 2.35/2.72 cnf('0.111.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X3,X1))),negate(add(X1,negate(add(X2,X3)))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.17.2.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.111.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X3,X1))),negate(add(X1,negate(add(X2,X3)))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.111.0.0']),
% 2.35/2.72 [weight('<59,17,3,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.111.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,add(X2,X3))),negate(add(X3,negate(add(X1,X2)))))) = X3 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.111.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_107]).
% 2.35/2.72 cnf('0.113.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X3,X1))),negate(add(negate(add(X2,X3)),X1)))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.113.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X3,X1))),negate(add(negate(add(X2,X3)),X1)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.113.0.0']),
% 2.35/2.72 [weight('<59,21,3,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.113.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,add(X2,X3))),negate(add(negate(add(X1,X2)),X3)))) = X3 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.113.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_109]).
% 2.35/2.72 cnf('0.182.0.0',plain,
% 2.35/2.72 ( c = negate(add(negate(d),negate(add(c,add(negate(add(d,X1)),negate(add(d,negate(X1)))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.36.2.0','0.4.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.182.1.0',plain,
% 2.35/2.72 ( c = negate(add(negate(d),negate(add(c,add(negate(add(d,X1)),negate(add(d,negate(X1)))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.182.0.0']),
% 2.35/2.72 [weight('<61,36,4,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.182.2.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(c,add(negate(add(d,X1)),negate(add(d,negate(X1)))))))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.182.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_178]).
% 2.35/2.72 cnf('0.205.0.0',plain,
% 2.35/2.72 ( negate(add(d,negate(add(c,negate(d))))) = negate(add(negate(add(add(c,negate(d)),negate(add(d,negate(add(c,negate(d))))))),c)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.90.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.205.0.1',plain,
% 2.35/2.72 ( negate(add(d,negate(add(c,negate(d))))) = negate(add(negate(add(c,add(negate(d),negate(add(d,negate(add(c,negate(d)))))))),c)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.205.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.205.1.0',plain,
% 2.35/2.72 ( negate(add(d,negate(add(c,negate(d))))) = negate(add(negate(add(c,add(negate(d),negate(add(d,negate(add(c,negate(d)))))))),c)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.205.0.1']),
% 2.35/2.72 [weight('<61,90,21,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.205.1.1',plain,
% 2.35/2.72 ( negate(add(d,negate(add(c,negate(d))))) = negate(add(c,negate(add(c,add(negate(d),negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.205.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.205.2.0',plain,
% 2.35/2.72 ( negate(add(c,negate(add(c,add(negate(d),negate(add(d,negate(add(c,negate(d)))))))))) = negate(add(d,negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.205.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_201]).
% 2.35/2.72 cnf('0.302.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(negate(add(X2,X3)),negate(add(X3,negate(X2)))))),negate(add(X1,X3)))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.17.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.302.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(negate(add(X2,X3)),negate(add(X3,negate(X2)))))),negate(add(X1,X3)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.302.0.0']),
% 2.35/2.72 [weight('<?,17,1,[0,0,0,9]>')]).
% 2.35/2.72 cnf('0.302.1.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,X3)),negate(add(X1,add(negate(add(X2,X3)),negate(add(X3,negate(X2)))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.302.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.302.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X1,add(negate(add(X3,X2)),negate(add(X2,negate(X3)))))))) = X1 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.302.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_298]).
% 2.35/2.72 cnf('0.312.0.0',plain,
% 2.35/2.72 ( add(X1,c) = negate(add(negate(add(X1,add(d,X2))),negate(add(X1,add(c,negate(add(d,X2))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.48.2.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1.2','L')]).
% 2.35/2.72 cnf('0.312.1.0',plain,
% 2.35/2.72 ( add(X1,c) = negate(add(negate(add(X1,add(d,X2))),negate(add(X1,add(c,negate(add(d,X2))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.312.0.0']),
% 2.35/2.72 [weight('<69,48,7,[1,0,0,5]>')]).
% 2.35/2.72 cnf('0.312.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,add(d,X2))),negate(add(X1,add(c,negate(add(d,X2))))))) = add(X1,c) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.312.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_308]).
% 2.35/2.72 cnf('0.314.0.0',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(d,X1)),negate(add(c,add(c,negate(add(d,X1))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.312.2.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.314.1.0',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(d,X1)),negate(add(c,add(c,negate(add(d,X1))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.314.0.0']),
% 2.35/2.72 [weight('<59,312,7,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.314.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(d,X1)),negate(add(c,add(c,negate(add(d,X1))))))) = add(c,c) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.314.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_310]).
% 2.35/2.72 cnf('0.435.0.0',plain,
% 2.35/2.72 ( add(c,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(add(c,X1),negate(add(d,X2)))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.111.2.0','0.15.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.435.0.1',plain,
% 2.35/2.72 ( add(c,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(c,add(X1,negate(add(d,X2))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.435.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.435.1.0',plain,
% 2.35/2.72 ( add(c,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(c,add(X1,negate(add(d,X2))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.435.0.1']),
% 2.35/2.72 [weight('<69,111,15,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.435.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(d,add(X1,X2))),negate(add(c,add(X2,negate(add(d,X1))))))) = add(c,X2) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.435.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_431]).
% 2.35/2.72 cnf('0.438.0.0',plain,
% 2.35/2.72 ( add(d,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(negate(add(c,X2)),add(d,X1))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.113.2.0','0.10.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1','L')]).
% 2.35/2.72 cnf('0.438.1.0',plain,
% 2.35/2.72 ( add(d,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(negate(add(c,X2)),add(d,X1))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.438.0.0']),
% 2.35/2.72 [weight('<69,113,10,[1,0,0,3]>')]).
% 2.35/2.72 cnf('0.438.1.1',plain,
% 2.35/2.72 ( add(d,X1) = negate(add(negate(add(d,add(X2,X1))),negate(add(d,add(negate(add(c,X2)),X1))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.438.1.0','0.71.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.438.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(d,add(X1,X2))),negate(add(d,add(negate(add(c,X1)),X2))))) = add(d,X2) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.438.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_434]).
% 2.35/2.72 cnf('0.591.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(X2,negate(add(X2,add(negate(X3),negate(add(X2,X3)))))))),negate(add(X1,negate(add(X2,X3)))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.25.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.591.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(X2,negate(add(X2,add(negate(X3),negate(add(X2,X3)))))))),negate(add(X1,negate(add(X2,X3)))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.591.0.0']),
% 2.35/2.72 [weight('<?,25,1,[0,0,0,9]>')]).
% 2.35/2.72 cnf('0.591.1.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,negate(add(X2,X3)))),negate(add(X1,add(X2,negate(add(X2,add(negate(X3),negate(add(X2,X3)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.591.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.591.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,negate(add(X2,X3)))),negate(add(X1,add(X2,negate(add(X2,add(negate(X3),negate(add(X2,X3)))))))))) = X1 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.591.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_587]).
% 2.35/2.72 cnf('0.698.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(add(X2,add(X1,negate(add(negate(X2),X1)))),X1)),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.17.2.0','0.57.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.698.0.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(add(X1,negate(add(negate(X2),X1))),X1))),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.698.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.698.0.2',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X1,add(negate(add(negate(X2),X1)),X1)))),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.698.0.1','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1.2','L')]).
% 2.35/2.72 cnf('0.698.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X2,add(X1,add(negate(add(negate(X2),X1)),X1)))),negate(add(negate(X2),X1)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.698.0.2']),
% 2.35/2.72 [weight('<71,57,17,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.698.1.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(negate(X2),X1)),negate(add(X2,add(X1,add(negate(add(negate(X2),X1)),X1)))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.698.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.698.1.2',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(negate(X2),X1)),negate(add(X2,add(X1,add(X1,negate(add(negate(X2),X1)))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.698.1.1','0.59.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2','R')]).
% 2.35/2.72 cnf('0.698.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(negate(X1),X2)),negate(add(X1,add(X2,add(X2,negate(add(negate(X1),X2)))))))) = X2 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.698.1.2',theory(equality)]),
% 2.35/2.72 [x,rule_694]).
% 2.35/2.72 cnf('0.775.0.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X2,negate(X1))))) = negate(add(negate(add(X1,X2)),negate(add(negate(add(X1,X2)),add(negate(negate(add(X2,negate(X1)))),X2))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.25.2.0','0.17.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2.2','L')]).
% 2.35/2.72 cnf('0.775.0.1',plain,
% 2.35/2.72 ( X2 = negate(add(negate(add(X1,X2)),negate(add(negate(add(X1,X2)),add(negate(negate(add(X2,negate(X1)))),X2))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.775.0.0','0.17.2.0',theory(equality)]),
% 2.35/2.72 [pos('L','L')]).
% 2.35/2.72 cnf('0.775.1.0',plain,
% 2.35/2.72 ( X2 = negate(add(negate(add(X1,X2)),negate(add(negate(add(X1,X2)),add(negate(negate(add(X2,negate(X1)))),X2))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.775.0.1']),
% 2.35/2.72 [weight('<?,25,17,[1,0,0,9]>')]).
% 2.35/2.72 cnf('0.775.1.1',plain,
% 2.35/2.72 ( X2 = negate(add(negate(add(X1,X2)),negate(add(X2,add(negate(negate(add(X2,negate(X1)))),negate(add(X1,X2))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.775.1.0','0.81.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.775.1.2',plain,
% 2.35/2.72 ( X2 = negate(add(negate(add(X1,X2)),negate(add(X2,add(negate(add(X1,X2)),negate(negate(add(X2,negate(X1))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.775.1.1','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.775.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,X2)),negate(add(X2,add(negate(add(X1,X2)),negate(negate(add(X2,negate(X1))))))))) = X2 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.775.1.2',theory(equality)]),
% 2.35/2.72 [x,rule_771]).
% 2.35/2.72 cnf('0.902.0.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(c,negate(add(d,negate(add(c,negate(d)))))))),negate(add(X1,negate(add(c,negate(d))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.27.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.902.1.0',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,add(c,negate(add(d,negate(add(c,negate(d)))))))),negate(add(X1,negate(add(c,negate(d))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.902.0.0']),
% 2.35/2.72 [weight('<?,27,1,[0,0,0,9]>')]).
% 2.35/2.72 cnf('0.902.1.1',plain,
% 2.35/2.72 ( X1 = negate(add(negate(add(X1,negate(add(c,negate(d))))),negate(add(X1,add(c,negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.902.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.902.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(X1,negate(add(c,negate(d))))),negate(add(X1,add(c,negate(add(d,negate(add(c,negate(d)))))))))) = X1 ),
% 2.35/2.72 inference(orient,[status(thm)],['0.902.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_898]).
% 2.35/2.72 cnf('0.903.0.0',plain,
% 2.35/2.72 ( negate(add(c,d)) = negate(add(c,negate(add(negate(add(c,d)),add(c,negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.902.2.0','0.1.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1','L')]).
% 2.35/2.72 cnf('0.903.0.1',plain,
% 2.35/2.72 ( negate(d) = negate(add(c,negate(add(negate(add(c,d)),add(c,negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.903.0.0','0.4.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1','L')]).
% 2.35/2.72 cnf('0.903.0.2',plain,
% 2.35/2.72 ( negate(d) = negate(add(c,negate(add(negate(d),add(c,negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.903.0.1','0.4.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.1.1','L')]).
% 2.35/2.72 cnf('0.903.1.0',plain,
% 2.35/2.72 ( negate(d) = negate(add(c,negate(add(negate(d),add(c,negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.903.0.2']),
% 2.35/2.72 [weight('<61,902,1,[1,0,0,2]>')]).
% 2.35/2.72 cnf('0.903.1.1',plain,
% 2.35/2.72 ( negate(d) = negate(add(c,negate(add(c,add(negate(d),negate(add(d,negate(add(c,negate(d)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.903.1.0','0.71.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.903.1.2',plain,
% 2.35/2.72 ( negate(d) = negate(add(d,negate(add(c,negate(d))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.903.1.1','0.205.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.903.2.0',plain,
% 2.35/2.72 ( negate(add(d,negate(add(c,negate(d))))) = negate(d) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.903.1.2',theory(equality)]),
% 2.35/2.72 [x,rule_899]).
% 2.35/2.72 cnf('0.905.0.0',plain,
% 2.35/2.72 ( d = negate(add(negate(add(add(c,negate(d)),d)),negate(d))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.17.2.0','0.903.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.905.0.1',plain,
% 2.35/2.72 ( d = negate(add(negate(add(c,add(negate(d),d))),negate(d))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.905.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.905.0.2',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(d))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.905.0.1','0.8.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.905.1.0',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(d))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.905.0.2']),
% 2.35/2.72 [weight('<29,903,17,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.905.1.1',plain,
% 2.35/2.72 ( d = negate(add(negate(d),negate(add(d,negate(d))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.905.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.905.2.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(d,negate(d))))) = d ),
% 2.35/2.72 inference(orient,[status(thm)],['0.905.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_901]).
% 2.35/2.72 cnf('0.971.0.0',plain,
% 2.35/2.72 ( d = negate(add(negate(add(add(c,negate(d)),d)),negate(add(d,add(negate(add(add(c,negate(d)),d)),negate(negate(d))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.775.2.0','0.903.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1.2.2.1','L')]).
% 2.35/2.72 cnf('0.971.0.1',plain,
% 2.35/2.72 ( d = negate(add(negate(add(c,add(negate(d),d))),negate(add(d,add(negate(add(add(c,negate(d)),d)),negate(negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.971.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.971.0.2',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(add(add(c,negate(d)),d)),negate(negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.971.0.1','0.8.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.971.0.3',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(add(c,add(negate(d),d))),negate(negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.971.0.2','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2.1.1','L')]).
% 2.35/2.72 cnf('0.971.0.4',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(add(d,negate(d))),negate(negate(d))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.971.0.3','0.8.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2.1.1','L')]).
% 2.35/2.72 cnf('0.971.1.0',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(add(d,negate(d))),negate(negate(d))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.971.0.4']),
% 2.35/2.72 [weight('<63,903,775,[0,0,0,15]>')]).
% 2.35/2.72 cnf('0.971.1.1',plain,
% 2.35/2.72 ( d = negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.971.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.971.2.0',plain,
% 2.35/2.72 ( negate(add(negate(add(d,negate(d))),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))))) = d ),
% 2.35/2.72 inference(orient,[status(thm)],['0.971.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_967]).
% 2.35/2.72 cnf('0.1232.0.0',plain,
% 2.35/2.72 ( negate(d) = negate(add(d,negate(add(negate(d),add(d,negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.591.2.0','0.905.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1','L')]).
% 2.35/2.72 cnf('0.1232.1.0',plain,
% 2.35/2.72 ( negate(d) = negate(add(d,negate(add(negate(d),add(d,negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1232.0.0']),
% 2.35/2.72 [weight('<73,905,591,[0,0,0,2]>')]).
% 2.35/2.72 cnf('0.1232.1.1',plain,
% 2.35/2.72 ( negate(d) = negate(add(d,negate(add(d,add(negate(d),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1232.1.0','0.71.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.1232.2.0',plain,
% 2.35/2.72 ( negate(add(d,negate(add(d,add(negate(d),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))))) = negate(d) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1232.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_1228]).
% 2.35/2.72 cnf('0.1258.0.0',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(add(negate(add(add(d,negate(d)),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))))),d)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.971.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.1258.0.1',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(add(negate(add(d,add(negate(d),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))),d)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1258.0.0','0.3.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.1258.1.0',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(add(negate(add(d,add(negate(d),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))),d)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1258.0.1']),
% 2.35/2.72 [weight('<73,971,21,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.1258.1.1',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(add(d,negate(add(d,add(negate(d),negate(add(d,add(negate(negate(d)),negate(add(d,negate(d))))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1258.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.1258.1.2',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(d) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1258.1.1','0.1232.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.1258.2.0',plain,
% 2.35/2.72 ( negate(add(d,add(negate(negate(d)),negate(add(d,negate(d)))))) = negate(d) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1258.1.2',theory(equality)]),
% 2.35/2.72 [u,rule_1254]).
% 2.35/2.72 cnf('0.1259.0.0',plain,
% 2.35/2.72 ( add(c,negate(add(d,negate(d)))) = negate(add(negate(d),negate(add(c,add(negate(add(d,negate(d))),negate(add(d,negate(negate(d))))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.435.2.0','0.1258.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1','L')]).
% 2.35/2.72 cnf('0.1259.0.1',plain,
% 2.35/2.72 ( add(c,negate(add(d,negate(d)))) = c ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1259.0.0','0.182.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.1259.1.0',plain,
% 2.35/2.72 ( add(c,negate(add(d,negate(d)))) = c ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1259.0.1']),
% 2.35/2.72 [weight('<27,1258,435,[0,0,0,2]>')]).
% 2.35/2.72 cnf('0.1259.2.0',plain,
% 2.35/2.72 ( add(c,negate(add(d,negate(d)))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1259.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_1255]).
% 2.35/2.72 cnf('0.1262.0.0',plain,
% 2.35/2.72 ( c = negate(add(negate(add(c,add(d,negate(d)))),negate(c))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.1.2.0','0.1259.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1','L')]).
% 2.35/2.72 cnf('0.1262.0.1',plain,
% 2.35/2.72 ( c = negate(add(negate(add(d,negate(d))),negate(c))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1262.0.0','0.7.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.1262.1.0',plain,
% 2.35/2.72 ( c = negate(add(negate(add(d,negate(d))),negate(c))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1262.0.1']),
% 2.35/2.72 [weight('<29,1259,1,[0,0,0,7]>')]).
% 2.35/2.72 cnf('0.1262.1.1',plain,
% 2.35/2.72 ( c = negate(add(negate(c),negate(add(d,negate(d))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1262.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.1262.2.0',plain,
% 2.35/2.72 ( negate(add(negate(c),negate(add(d,negate(d))))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1262.1.1',theory(equality)]),
% 2.35/2.72 [x,rule_1258]).
% 2.35/2.72 cnf('0.1263.0.0',plain,
% 2.35/2.72 ( negate(add(d,negate(d))) = negate(add(negate(add(c,negate(add(d,negate(d))))),c)) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.21.2.0','0.1262.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.1263.0.1',plain,
% 2.35/2.72 ( negate(add(d,negate(d))) = negate(add(negate(c),c)) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1263.0.0','0.1259.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1.1','L')]).
% 2.35/2.72 cnf('0.1263.1.0',plain,
% 2.35/2.72 ( negate(add(d,negate(d))) = negate(add(negate(c),c)) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1263.0.1']),
% 2.35/2.72 [weight('<17,1262,21,[0,0,0,6]>')]).
% 2.35/2.72 cnf('0.1263.1.1',plain,
% 2.35/2.72 ( negate(add(d,negate(d))) = negate(add(c,negate(c))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1263.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.1263.2.0',plain,
% 2.35/2.72 ( negate(add(d,negate(d))) = negate(add(c,negate(c))) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1263.1.1',theory(equality)]),
% 2.35/2.72 [u,rule_1259]).
% 2.35/2.72 cnf('0.1264.0.0',plain,
% 2.35/2.72 ( add(c,negate(add(d,negate(d)))) = c ),
% 2.35/2.72 inference(interreduction_right,[status(thm)],['0.1259.2.0'])).
% 2.35/2.72 cnf('0.1264.0.1',plain,
% 2.35/2.72 ( add(c,negate(add(c,negate(c)))) = c ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1264.0.0','0.1263.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.1264.1.0',plain,
% 2.35/2.72 ( add(c,negate(add(c,negate(c)))) = c ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1264.0.1']),
% 2.35/2.72 [weight('<27,1259,1263,[0,0,0,0]>')]).
% 2.35/2.72 cnf('0.1264.2.0',plain,
% 2.35/2.72 ( add(c,negate(add(c,negate(c)))) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1264.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_1260]).
% 2.35/2.72 cnf('0.1266.0.0',plain,
% 2.35/2.72 ( add(d,negate(add(c,negate(c)))) = negate(add(negate(add(d,c)),negate(add(d,add(negate(add(c,c)),negate(add(c,negate(c)))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.438.2.0','0.1264.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1.1.2','L')]).
% 2.35/2.72 cnf('0.1266.0.1',plain,
% 2.35/2.72 ( add(d,negate(add(c,negate(c)))) = d ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1266.0.0','0.302.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.1266.1.0',plain,
% 2.35/2.72 ( add(d,negate(add(c,negate(c)))) = d ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1266.0.1']),
% 2.35/2.72 [weight('<27,1264,438,[0,0,0,5]>')]).
% 2.35/2.72 cnf('0.1266.2.0',plain,
% 2.35/2.72 ( add(d,negate(add(c,negate(c)))) = d ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1266.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_1262]).
% 2.35/2.72 cnf('0.1267.0.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(d,negate(d))))) = d ),
% 2.35/2.72 inference(interreduction_right,[status(thm)],['0.905.2.0'])).
% 2.35/2.72 cnf('0.1267.0.1',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(c,negate(c))))) = d ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1267.0.0','0.1263.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2','L')]).
% 2.35/2.72 cnf('0.1267.1.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(c,negate(c))))) = d ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1267.0.1']),
% 2.35/2.72 [weight('<29,905,1263,[0,0,0,0]>')]).
% 2.35/2.72 cnf('0.1267.2.0',plain,
% 2.35/2.72 ( negate(add(negate(d),negate(add(c,negate(c))))) = d ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1267.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_1263]).
% 2.35/2.72 cnf('0.1274.0.0',plain,
% 2.35/2.72 ( add(d,add(negate(add(c,negate(c))),X1)) = add(d,X1) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.3.2.0','0.1266.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1','L')]).
% 2.35/2.72 cnf('0.1274.1.0',plain,
% 2.35/2.72 ( add(d,add(negate(add(c,negate(c))),X1)) = add(d,X1) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1274.0.0']),
% 2.35/2.72 [weight('<37,1266,3,[0,0,0,1]>')]).
% 2.35/2.72 cnf('0.1274.2.0',plain,
% 2.35/2.72 ( add(d,add(negate(add(c,negate(c))),X1)) = add(d,X1) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1274.1.0',theory(equality)]),
% 2.35/2.72 [u,rule_1270]).
% 2.35/2.72 cnf('0.1275.0.0',plain,
% 2.35/2.72 ( negate(add(c,negate(c))) = negate(add(negate(add(negate(d),negate(add(c,negate(c))))),negate(add(d,add(negate(add(c,negate(c))),negate(add(negate(d),negate(add(c,negate(c)))))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.698.2.0','0.1274.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.2.1','L')]).
% 2.35/2.72 cnf('0.1275.0.1',plain,
% 2.35/2.72 ( negate(add(c,negate(c))) = negate(add(d,negate(add(d,add(negate(add(c,negate(c))),negate(add(negate(d),negate(add(c,negate(c)))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1275.0.0','0.1267.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.1','L')]).
% 2.35/2.72 cnf('0.1275.0.2',plain,
% 2.35/2.72 ( negate(add(c,negate(c))) = negate(add(d,negate(add(d,negate(add(negate(d),negate(add(c,negate(c))))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1275.0.1','0.1274.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1','L')]).
% 2.35/2.72 cnf('0.1275.0.3',plain,
% 2.35/2.72 ( negate(add(c,negate(c))) = negate(add(d,negate(add(d,d)))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1275.0.2','0.1267.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.1275.1.0',plain,
% 2.35/2.72 ( negate(add(c,negate(c))) = negate(add(d,negate(add(d,d)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1275.0.3']),
% 2.35/2.72 [weight('<27,1274,698,[0,0,0,8]>')]).
% 2.35/2.72 cnf('0.1275.2.0',plain,
% 2.35/2.72 ( negate(add(d,negate(add(d,d)))) = negate(add(c,negate(c))) ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1275.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_1271]).
% 2.35/2.72 cnf('0.1283.0.0',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(c,negate(c))),negate(add(c,add(c,negate(add(d,negate(add(d,d))))))))) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.314.2.0','0.1275.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.1.1','L')]).
% 2.35/2.72 cnf('0.1283.0.1',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(c,negate(c))),negate(add(c,add(c,negate(add(c,negate(c)))))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1283.0.0','0.1275.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2.2','L')]).
% 2.35/2.72 cnf('0.1283.0.2',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(c,negate(c))),negate(add(c,c)))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1283.0.1','0.1264.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1.2.1.2','L')]).
% 2.35/2.72 cnf('0.1283.1.0',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(c,negate(c))),negate(add(c,c)))) ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1283.0.2']),
% 2.35/2.72 [weight('<39,1275,314,[0,0,0,2]>')]).
% 2.35/2.72 cnf('0.1283.1.1',plain,
% 2.35/2.72 ( add(c,c) = negate(add(negate(add(c,c)),negate(add(c,negate(c))))) ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1283.1.0','0.2.2.0',theory(equality)]),
% 2.35/2.72 [pos('R.1','L')]).
% 2.35/2.72 cnf('0.1283.1.2',plain,
% 2.35/2.72 ( add(c,c) = c ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1283.1.1','0.17.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.1283.2.0',plain,
% 2.35/2.72 ( add(c,c) = c ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1283.1.2',theory(equality)]),
% 2.35/2.72 [u,rule_1279]).
% 2.35/2.72 cnf('0.1285.0.0',plain,
% 2.35/2.72 ( false = eq(c,c) ),
% 2.35/2.72 inference(cp,[status(thm)],['0.6.2.0','0.1283.2.0',theory(equality)]),
% 2.35/2.72 [pos('L.2','L')]).
% 2.35/2.72 cnf('0.1285.0.1',plain,
% 2.35/2.72 ( false = true ),
% 2.35/2.72 inference(reduction,[status(thm)],['0.1285.0.0','0.5.2.0',theory(equality)]),
% 2.35/2.72 [pos('R','L')]).
% 2.35/2.72 cnf('0.1285.1.0',plain,
% 2.35/2.72 ( false = true ),
% 2.35/2.72 inference(weigh,[status(thm)],['0.1285.0.1']),
% 2.35/2.72 [weight('<5,1283,6,[0,0,0,2]>')]).
% 2.35/2.72 cnf('0.1285.2.0',plain,
% 2.35/2.72 ( true = false ),
% 2.35/2.72 inference(orient,[status(thm)],['0.1285.1.0',theory(equality)]),
% 2.35/2.72 [x,rule_1281]).
% 2.35/2.72 cnf('1.0.0.0',conjecture,
% 2.35/2.72 ( true = false ),
% 2.35/2.72 file('/tmp/WALDMEISTER_10296_n023',conjecture_1)).
% 2.35/2.72 cnf('1.0.0.1',plain,
% 2.35/2.72 ( false = false ),
% 2.35/2.72 inference(reduction,[status(thm)],['1.0.0.0','0.1285.2.0',theory(equality)]),
% 2.35/2.72 [pos('L','L')]).
% 2.35/2.72 cnf('1.0.0.2',plain,
% 2.35/2.72 ( $true ),
% 2.35/2.72 inference(trivial,[status(thm)],['1.0.0.1',theory(equality)]),
% 2.35/2.72 [conjecture_1]).
% 2.35/2.72
% 2.35/2.72 Proved Goals:
% 2.35/2.72 No. 1: true ?= false, current false ?= false
% 2.35/2.72 using narrowing to prove x1 ?= add(x1,x1)
% 2.35/2.72
% 2.35/2.72 1 goal was specified, which was proved.
% 2.35/2.72 % SZS output end CNFRefutation
% 2.35/2.72 #END OF PROOF
% 2.35/2.72
% 2.35/2.72 Problem WALDMEISTER_10296_n023
% 2.35/2.72 CPs.gen 290105
% 2.35/2.72 CPs.reexp 0
% 2.35/2.72 Select 5734
% 2.35/2.72 R 1281
% 2.35/2.72 E 4
% 2.35/2.72 vsize 9.3M
% 2.35/2.72 rss 4.9M
% 2.35/2.72 process.time 1.665s
% 2.35/2.72 wallclock.time 1.665s
% 2.35/2.72 status S
% 2.35/2.72
% 2.35/2.72
% 2.35/2.72 Waldmeister states: Goal proved.
% 2.35/2.72 % SZS status Unsatisfiable
%------------------------------------------------------------------------------