%------------------------------------------------------------------------------
% File : Waldmeister---710
% Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : woody %s
% Computer : n029.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 : 300s
% DateTime : Tue May 5 07:08:10 PM UTC 2026
% Result : Unsatisfiable 19.63s 20.11s
% Output : CNFRefutation 19.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX239-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : woody %s
% 0.16/0.34 % Computer : n029.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 13:19:44 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.62/1.04 ********************************************************************************
% 0.62/1.04 * W A L D M E I S T E R \| \ / \|/ *
% 0.62/1.04 * |/ | \/ | *
% 0.62/1.04 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / *
% 0.62/1.04 * A. Jaeger and B. Loechner | | *
% 0.62/1.04 * <waldmeister@informatik.uni-kl.de> | *
% 0.62/1.04 ********************************************************************************
% 0.62/1.04
% 0.62/1.04
% 0.62/1.04 Goals:
% 0.62/1.04 ------
% 0.62/1.04
% 0.62/1.04 ( 1) true ?= false
% 0.62/1.04 using narrowing to prove btrue ?= eq2(prop_same(x2,x1),bfalse)
% 0.62/1.04
% 0.62/1.04 Detected structure: Orkus
% 0.62/1.04 ********************************************************************************
% 0.62/1.04 ****************************** COMPLETION - PROOF ******************************
% 0.62/1.04 ********************************************************************************
% 0.62/1.04
% 19.63/20.11 joined goal: 1 btrue ?= eq2(prop_same(x2,x1),bfalse) to false
% 19.63/20.11 goal joined
% 19.63/20.11 % SZS status Unsatisfiable
% 19.63/20.11 #START OF PROOF
% 19.63/20.11 % SZS output start CNFRefutation
% 19.63/20.11 cnf('0.4.0.0',axiom,
% 19.63/20.11 ( X1 = andb(btrue,X1) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.4.1.0',plain,
% 19.63/20.11 ( X1 = andb(btrue,X1) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.4.0.0']),
% 19.63/20.11 [weight('<3,0,0,[0,0,0,4]>')]).
% 19.63/20.11 cnf('0.4.2.0',plain,
% 19.63/20.11 ( andb(btrue,X1) = X1 ),
% 19.63/20.11 inference(orient,[status(thm)],['0.4.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_4]).
% 19.63/20.11 cnf('0.53.0.0',axiom,
% 19.63/20.11 ( y(step(X1,X2),star(X1)) = step(star(X1),X2) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.53.1.0',plain,
% 19.63/20.11 ( y(step(X1,X2),star(X1)) = step(star(X1),X2) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.53.0.0']),
% 19.63/20.11 [weight('<52,0,0,[0,0,0,53]>')]).
% 19.63/20.11 cnf('0.53.2.0',plain,
% 19.63/20.11 ( y(step(X1,X2),star(X1)) = step(star(X1),X2) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.53.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_53]).
% 19.63/20.11 cnf('0.59.0.0',axiom,
% 19.63/20.11 ( eps = aux(X1,X2,btrue) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.59.1.0',plain,
% 19.63/20.11 ( eps = aux(X1,X2,btrue) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.59.0.0']),
% 19.63/20.11 [weight('<58,0,0,[0,0,0,59]>')]).
% 19.63/20.11 cnf('0.59.2.0',plain,
% 19.63/20.11 ( aux(X1,X2,btrue) = eps ),
% 19.63/20.11 inference(orient,[status(thm)],['0.59.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_59]).
% 19.63/20.11 cnf('0.74.0.0',axiom,
% 19.63/20.11 ( bfalse = eq2(btrue,bfalse) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.74.1.0',plain,
% 19.63/20.11 ( bfalse = eq2(btrue,bfalse) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.74.0.0']),
% 19.63/20.11 [weight('<73,0,0,[0,0,0,74]>')]).
% 19.63/20.11 cnf('0.74.2.0',plain,
% 19.63/20.11 ( eq2(btrue,bfalse) = bfalse ),
% 19.63/20.11 inference(orient,[status(thm)],['0.74.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_74]).
% 19.63/20.11 cnf('0.76.0.0',axiom,
% 19.63/20.11 ( bfalse = notb(btrue) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.76.1.0',plain,
% 19.63/20.11 ( bfalse = notb(btrue) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.76.0.0']),
% 19.63/20.11 [weight('<75,0,0,[0,0,0,76]>')]).
% 19.63/20.11 cnf('0.76.2.0',plain,
% 19.63/20.11 ( notb(btrue) = bfalse ),
% 19.63/20.11 inference(orient,[status(thm)],['0.76.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_76]).
% 19.63/20.11 cnf('0.77.0.0',axiom,
% 19.63/20.11 ( bfalse = aux3(X1,X2,X3,bfalse) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.77.1.0',plain,
% 19.63/20.11 ( bfalse = aux3(X1,X2,X3,bfalse) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.77.0.0']),
% 19.63/20.11 [weight('<76,0,0,[0,0,0,77]>')]).
% 19.63/20.11 cnf('0.77.2.0',plain,
% 19.63/20.11 ( aux3(X1,X2,X3,bfalse) = bfalse ),
% 19.63/20.11 inference(orient,[status(thm)],['0.77.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_77]).
% 19.63/20.11 cnf('0.88.0.0',axiom,
% 19.63/20.11 ( btrue = eps2(star(X1)) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.88.1.0',plain,
% 19.63/20.11 ( btrue = eps2(star(X1)) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.88.0.0']),
% 19.63/20.11 [weight('<87,0,0,[0,0,0,88]>')]).
% 19.63/20.11 cnf('0.88.2.0',plain,
% 19.63/20.11 ( eps2(star(X1)) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.88.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_88]).
% 19.63/20.11 cnf('0.89.0.0',axiom,
% 19.63/20.11 ( btrue = eps2(eps) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.89.1.0',plain,
% 19.63/20.11 ( btrue = eps2(eps) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.89.0.0']),
% 19.63/20.11 [weight('<88,0,0,[0,0,0,89]>')]).
% 19.63/20.11 cnf('0.89.2.0',plain,
% 19.63/20.11 ( eps2(eps) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.89.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_89]).
% 19.63/20.11 cnf('0.90.0.0',axiom,
% 19.63/20.11 ( btrue = eq(X1,X1) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.90.1.0',plain,
% 19.63/20.11 ( btrue = eq(X1,X1) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.90.0.0']),
% 19.63/20.11 [weight('<89,0,0,[0,0,0,90]>')]).
% 19.63/20.11 cnf('0.90.2.0',plain,
% 19.63/20.11 ( eq(X1,X1) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.90.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_90]).
% 19.63/20.11 cnf('0.92.0.0',axiom,
% 19.63/20.11 ( btrue = eq2(X1,X1) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.92.1.0',plain,
% 19.63/20.11 ( btrue = eq2(X1,X1) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.92.0.0']),
% 19.63/20.11 [weight('<91,0,0,[0,0,0,92]>')]).
% 19.63/20.11 cnf('0.92.2.0',plain,
% 19.63/20.11 ( eq2(X1,X1) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.92.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_92]).
% 19.63/20.11 cnf('0.96.0.0',axiom,
% 19.63/20.11 ( reck2(star(X1),cons2(X2,X3)) = aux3(X1,X2,X3,notb(eps2(X1))) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.96.1.0',plain,
% 19.63/20.11 ( reck2(star(X1),cons2(X2,X3)) = aux3(X1,X2,X3,notb(eps2(X1))) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.96.0.0']),
% 19.63/20.11 [weight('<95,0,0,[0,0,0,96]>')]).
% 19.63/20.11 cnf('0.96.2.0',plain,
% 19.63/20.11 ( aux3(X1,X2,X3,notb(eps2(X1))) = reck2(star(X1),cons2(X2,X3)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.96.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_96]).
% 19.63/20.11 cnf('0.98.0.0',axiom,
% 19.63/20.11 ( eps2(X1) = rec(X1,nil2) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.98.1.0',plain,
% 19.63/20.11 ( eps2(X1) = rec(X1,nil2) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.98.0.0']),
% 19.63/20.11 [weight('<97,0,0,[0,0,0,98]>')]).
% 19.63/20.11 cnf('0.98.2.0',plain,
% 19.63/20.11 ( rec(X1,nil2) = eps2(X1) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.98.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_98]).
% 19.63/20.11 cnf('0.100.0.0',axiom,
% 19.63/20.11 ( eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.100.1.0',plain,
% 19.63/20.11 ( eps2(y(X1,X2)) = andb(eps2(X1),eps2(X2)) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.100.0.0']),
% 19.63/20.11 [weight('<99,0,0,[0,0,0,100]>')]).
% 19.63/20.11 cnf('0.100.2.0',plain,
% 19.63/20.11 ( andb(eps2(X1),eps2(X2)) = eps2(y(X1,X2)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.100.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_100]).
% 19.63/20.11 cnf('0.102.0.0',axiom,
% 19.63/20.11 ( step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.102.1.0',plain,
% 19.63/20.11 ( step(atom(X1),X2) = aux(X2,X1,eq(X1,X2)) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.102.0.0']),
% 19.63/20.11 [weight('<101,0,0,[0,0,0,102]>')]).
% 19.63/20.11 cnf('0.102.2.0',plain,
% 19.63/20.11 ( aux(X1,X2,eq(X2,X1)) = step(atom(X2),X1) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.102.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_102]).
% 19.63/20.11 cnf('0.103.0.0',axiom,
% 19.63/20.11 ( rec(X1,cons2(X2,X3)) = rec(step(X1,X2),X3) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.103.1.0',plain,
% 19.63/20.11 ( rec(X1,cons2(X2,X3)) = rec(step(X1,X2),X3) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.103.0.0']),
% 19.63/20.11 [weight('<102,0,0,[0,0,0,103]>')]).
% 19.63/20.11 cnf('0.103.2.0',plain,
% 19.63/20.11 ( rec(step(X1,X2),X3) = rec(X1,cons2(X2,X3)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.103.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_103]).
% 19.63/20.11 cnf('0.110.0.0',axiom,
% 19.63/20.11 ( eq2(rec(X1,X2),reck2(X1,X2)) = prop_same(X1,X2) ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.110.1.0',plain,
% 19.63/20.11 ( eq2(rec(X1,X2),reck2(X1,X2)) = prop_same(X1,X2) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.110.0.0']),
% 19.63/20.11 [weight('<109,0,0,[0,0,0,110]>')]).
% 19.63/20.11 cnf('0.110.2.0',plain,
% 19.63/20.11 ( eq2(rec(X1,X2),reck2(X1,X2)) = prop_same(X1,X2) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.110.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_110]).
% 19.63/20.11 cnf('0.113.0.0',axiom,
% 19.63/20.11 ( eq1(X1,X1) = true ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.113.1.0',plain,
% 19.63/20.11 ( eq1(X1,X1) = true ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.113.0.0']),
% 19.63/20.11 [weight('<112,0,0,[0,0,0,113]>')]).
% 19.63/20.11 cnf('0.113.2.0',plain,
% 19.63/20.11 ( eq1(X1,X1) = true ),
% 19.63/20.11 inference(orient,[status(thm)],['0.113.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_113]).
% 19.63/20.11 cnf('0.114.0.0',axiom,
% 19.63/20.11 ( eq1(btrue,eq2(prop_same(X2,X1),bfalse)) = false ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029')).
% 19.63/20.11 cnf('0.114.1.0',plain,
% 19.63/20.11 ( eq1(btrue,eq2(prop_same(X2,X1),bfalse)) = false ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.114.0.0']),
% 19.63/20.11 [weight('<113,0,0,[0,0,0,114]>')]).
% 19.63/20.11 cnf('0.114.2.0',plain,
% 19.63/20.11 ( eq1(btrue,eq2(prop_same(X1,X2),bfalse)) = false ),
% 19.63/20.11 inference(orient,[status(thm)],['0.114.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_114]).
% 19.63/20.11 cnf('0.124.0.0',plain,
% 19.63/20.11 ( step(atom(X1),X1) = aux(X1,X1,btrue) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.102.2.0','0.90.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.3','L')]).
% 19.63/20.11 cnf('0.124.0.1',plain,
% 19.63/20.11 ( step(atom(X1),X1) = eps ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.124.0.0','0.59.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.124.1.0',plain,
% 19.63/20.11 ( step(atom(X1),X1) = eps ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.124.0.1']),
% 19.63/20.11 [weight('<29,102,90,[1,0,0,3]>')]).
% 19.63/20.11 cnf('0.124.2.0',plain,
% 19.63/20.11 ( step(atom(X1),X1) = eps ),
% 19.63/20.11 inference(orient,[status(thm)],['0.124.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_124]).
% 19.63/20.11 cnf('0.189.0.0',plain,
% 19.63/20.11 ( eps2(y(X1,star(X2))) = andb(eps2(X1),btrue) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.100.2.0','0.88.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.2','L')]).
% 19.63/20.11 cnf('0.189.1.0',plain,
% 19.63/20.11 ( eps2(y(X1,star(X2))) = andb(eps2(X1),btrue) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.189.0.0']),
% 19.63/20.11 [weight('<59,100,88,[1,0,0,3]>')]).
% 19.63/20.11 cnf('0.189.2.0',plain,
% 19.63/20.11 ( eps2(y(X1,star(X2))) = andb(eps2(X1),btrue) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.189.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_189]).
% 19.63/20.11 cnf('0.190.0.0',plain,
% 19.63/20.11 ( rec(X1,cons2(X2,nil2)) = eps2(step(X1,X2)) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.103.2.0','0.98.2.0',theory(equality)]),
% 19.63/20.11 [pos('L','L')]).
% 19.63/20.11 cnf('0.190.1.0',plain,
% 19.63/20.11 ( rec(X1,cons2(X2,nil2)) = eps2(step(X1,X2)) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.190.0.0']),
% 19.63/20.11 [weight('<59,103,98,[1,0,0,0]>')]).
% 19.63/20.11 cnf('0.190.2.0',plain,
% 19.63/20.11 ( rec(X1,cons2(X2,nil2)) = eps2(step(X1,X2)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.190.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_190]).
% 19.63/20.11 cnf('0.272.0.0',plain,
% 19.63/20.11 ( reck2(star(star(X1)),cons2(X2,X3)) = aux3(star(X1),X2,X3,notb(btrue)) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.96.2.0','0.88.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.4.1','L')]).
% 19.63/20.11 cnf('0.272.0.1',plain,
% 19.63/20.11 ( reck2(star(star(X1)),cons2(X2,X3)) = aux3(star(X1),X2,X3,bfalse) ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.272.0.0','0.76.2.0',theory(equality)]),
% 19.63/20.11 [pos('R.4','L')]).
% 19.63/20.11 cnf('0.272.0.2',plain,
% 19.63/20.11 ( reck2(star(star(X1)),cons2(X2,X3)) = bfalse ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.272.0.1','0.77.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.272.1.0',plain,
% 19.63/20.11 ( reck2(star(star(X1)),cons2(X2,X3)) = bfalse ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.272.0.2']),
% 19.63/20.11 [weight('<71,96,88,[1,0,0,5]>')]).
% 19.63/20.11 cnf('0.272.2.0',plain,
% 19.63/20.11 ( reck2(star(star(X1)),cons2(X2,X3)) = bfalse ),
% 19.63/20.11 inference(orient,[status(thm)],['0.272.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_272]).
% 19.63/20.11 cnf('0.433.0.0',plain,
% 19.63/20.11 ( andb(eps2(step(X1,X2)),btrue) = eps2(step(star(X1),X2)) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.189.2.0','0.53.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.1','L')]).
% 19.63/20.11 cnf('0.433.1.0',plain,
% 19.63/20.11 ( andb(eps2(step(X1,X2)),btrue) = eps2(step(star(X1),X2)) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.433.0.0']),
% 19.63/20.11 [weight('<83,189,53,[1,0,0,1]>')]).
% 19.63/20.11 cnf('0.433.2.0',plain,
% 19.63/20.11 ( andb(eps2(step(X1,X2)),btrue) = eps2(step(star(X1),X2)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.433.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_427]).
% 19.63/20.11 cnf('0.434.0.0',plain,
% 19.63/20.11 ( eps2(step(star(atom(X1)),X1)) = andb(eps2(eps),btrue) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.433.2.0','0.124.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.1.1','L')]).
% 19.63/20.11 cnf('0.434.0.1',plain,
% 19.63/20.11 ( eps2(step(star(atom(X1)),X1)) = andb(btrue,btrue) ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.434.0.0','0.89.2.0',theory(equality)]),
% 19.63/20.11 [pos('R.1','L')]).
% 19.63/20.11 cnf('0.434.0.2',plain,
% 19.63/20.11 ( eps2(step(star(atom(X1)),X1)) = btrue ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.434.0.1','0.4.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.434.1.0',plain,
% 19.63/20.11 ( eps2(step(star(atom(X1)),X1)) = btrue ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.434.0.2']),
% 19.63/20.11 [weight('<55,433,124,[1,0,0,2]>')]).
% 19.63/20.11 cnf('0.434.2.0',plain,
% 19.63/20.11 ( eps2(step(star(atom(X1)),X1)) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.434.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_428]).
% 19.63/20.11 cnf('0.442.0.0',plain,
% 19.63/20.11 ( eps2(step(star(star(atom(X1))),X1)) = andb(btrue,btrue) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.433.2.0','0.434.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.1','L')]).
% 19.63/20.11 cnf('0.442.0.1',plain,
% 19.63/20.11 ( eps2(step(star(star(atom(X1))),X1)) = btrue ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.442.0.0','0.4.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.442.1.0',plain,
% 19.63/20.11 ( eps2(step(star(star(atom(X1))),X1)) = btrue ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.442.0.1']),
% 19.63/20.11 [weight('<71,434,433,[0,0,0,1]>')]).
% 19.63/20.11 cnf('0.442.2.0',plain,
% 19.63/20.11 ( eps2(step(star(star(atom(X1))),X1)) = btrue ),
% 19.63/20.11 inference(orient,[status(thm)],['0.442.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_436]).
% 19.63/20.11 cnf('0.17070.0.0',plain,
% 19.63/20.11 ( prop_same(star(star(X1)),cons2(X2,X3)) = eq2(rec(star(star(X1)),cons2(X2,X3)),bfalse) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.110.2.0','0.272.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.2','L')]).
% 19.63/20.11 cnf('0.17070.1.0',plain,
% 19.63/20.11 ( prop_same(star(star(X1)),cons2(X2,X3)) = eq2(rec(star(star(X1)),cons2(X2,X3)),bfalse) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.17070.0.0']),
% 19.63/20.11 [weight('<169,272,110,[0,0,0,4]>')]).
% 19.63/20.11 cnf('0.17070.2.0',plain,
% 19.63/20.11 ( eq2(rec(star(star(X1)),cons2(X2,X3)),bfalse) = prop_same(star(star(X1)),cons2(X2,X3)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.17070.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_17026]).
% 19.63/20.11 cnf('0.17071.0.0',plain,
% 19.63/20.11 ( prop_same(star(star(X1)),cons2(X2,nil2)) = eq2(eps2(step(star(star(X1)),X2)),bfalse) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.17070.2.0','0.190.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.1','L')]).
% 19.63/20.11 cnf('0.17071.1.0',plain,
% 19.63/20.11 ( prop_same(star(star(X1)),cons2(X2,nil2)) = eq2(eps2(step(star(star(X1)),X2)),bfalse) ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.17071.0.0']),
% 19.63/20.11 [weight('<143,17070,190,[1,0,0,1]>')]).
% 19.63/20.11 cnf('0.17071.2.0',plain,
% 19.63/20.11 ( eq2(eps2(step(star(star(X1)),X2)),bfalse) = prop_same(star(star(X1)),cons2(X2,nil2)) ),
% 19.63/20.11 inference(orient,[status(thm)],['0.17071.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_17027]).
% 19.63/20.11 cnf('0.17079.0.0',plain,
% 19.63/20.11 ( prop_same(star(star(atom(X1))),cons2(X1,nil2)) = eq2(btrue,bfalse) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.17071.2.0','0.442.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.1','L')]).
% 19.63/20.11 cnf('0.17079.0.1',plain,
% 19.63/20.11 ( prop_same(star(star(atom(X1))),cons2(X1,nil2)) = bfalse ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.17079.0.0','0.74.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.17079.1.0',plain,
% 19.63/20.11 ( prop_same(star(star(atom(X1))),cons2(X1,nil2)) = bfalse ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.17079.0.1']),
% 19.63/20.11 [weight('<89,17071,442,[1,0,0,1]>')]).
% 19.63/20.11 cnf('0.17079.2.0',plain,
% 19.63/20.11 ( prop_same(star(star(atom(X1))),cons2(X1,nil2)) = bfalse ),
% 19.63/20.11 inference(orient,[status(thm)],['0.17079.1.0',theory(equality)]),
% 19.63/20.11 [u,rule_17035]).
% 19.63/20.11 cnf('0.17080.0.0',plain,
% 19.63/20.11 ( false = eq1(btrue,eq2(bfalse,bfalse)) ),
% 19.63/20.11 inference(cp,[status(thm)],['0.114.2.0','0.17079.2.0',theory(equality)]),
% 19.63/20.11 [pos('L.2.1','L')]).
% 19.63/20.11 cnf('0.17080.0.1',plain,
% 19.63/20.11 ( false = eq1(btrue,btrue) ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.17080.0.0','0.92.2.0',theory(equality)]),
% 19.63/20.11 [pos('R.2','L')]).
% 19.63/20.11 cnf('0.17080.0.2',plain,
% 19.63/20.11 ( false = true ),
% 19.63/20.11 inference(reduction,[status(thm)],['0.17080.0.1','0.113.2.0',theory(equality)]),
% 19.63/20.11 [pos('R','L')]).
% 19.63/20.11 cnf('0.17080.1.0',plain,
% 19.63/20.11 ( false = true ),
% 19.63/20.11 inference(weigh,[status(thm)],['0.17080.0.2']),
% 19.63/20.11 [weight('<5,17079,114,[0,0,0,3]>')]).
% 19.63/20.11 cnf('0.17080.2.0',plain,
% 19.63/20.11 ( true = false ),
% 19.63/20.11 inference(orient,[status(thm)],['0.17080.1.0',theory(equality)]),
% 19.63/20.11 [x,rule_17036]).
% 19.63/20.11 cnf('1.0.0.0',conjecture,
% 19.63/20.11 ( true = false ),
% 19.63/20.11 file('/tmp/WALDMEISTER_15088_n029',conjecture_1)).
% 19.63/20.11 cnf('1.0.0.1',plain,
% 19.63/20.11 ( false = false ),
% 19.63/20.11 inference(reduction,[status(thm)],['1.0.0.0','0.17080.2.0',theory(equality)]),
% 19.63/20.11 [pos('L','L')]).
% 19.63/20.11 cnf('1.0.0.2',plain,
% 19.63/20.11 ( $true ),
% 19.63/20.11 inference(trivial,[status(thm)],['1.0.0.1',theory(equality)]),
% 19.63/20.11 [conjecture_1]).
% 19.63/20.11
% 19.63/20.11 Proved Goals:
% 19.63/20.11 No. 1: true ?= false, current false ?= false
% 19.63/20.11 using narrowing to prove btrue ?= eq2(prop_same(x2,x1),bfalse)
% 19.63/20.11
% 19.63/20.11 1 goal was specified, which was proved.
% 19.63/20.11 % SZS output end CNFRefutation
% 19.63/20.11 #END OF PROOF
% 19.63/20.11
% 19.63/20.11 Problem WALDMEISTER_15088_n029
% 19.63/20.11 CPs.gen 2998818
% 19.63/20.11 CPs.reexp 0
% 19.63/20.11 Select 37446
% 19.63/20.11 R 17036
% 19.63/20.11 E 44
% 19.63/20.11 vsize 21.3M
% 19.63/20.11 rss 16.6M
% 19.63/20.11 process.time 19.071s
% 19.63/20.11 wallclock.time 19.070s
% 19.63/20.11 status S
% 19.63/20.11
% 19.63/20.11
% 19.63/20.11 Waldmeister states: Goal proved.
% 19.63/20.11 % SZS status Unsatisfiable
%------------------------------------------------------------------------------