%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n020.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 : Wed Jul 27 13:24:53 EDT 2022
% Result : Theorem 96.27s 96.42s
% Output : Refutation 96.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 14
% Syntax : Number of clauses : 211 ( 16 unt; 149 nHn; 210 RR)
% Number of literals : 612 ( 611 equ; 212 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 115 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( dollar_c1 = f(g(dollar_c1))
| A != g(f(A))
| B != g(f(B))
| A = B ),
file('SYN551+1.p',unknown),
[] ).
cnf(2,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A
| g(f(B)) != B
| A = B ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[1])])])]),
[iquote('copy,1,flip.1,flip.2,flip.3')] ).
cnf(3,axiom,
( A != f(g(A))
| B != f(g(B))
| A = B
| dollar_c2 = g(f(dollar_c2)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(4,plain,
( f(g(A)) != A
| f(g(B)) != B
| A = B
| g(f(dollar_c2)) = dollar_c2 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[3])])])]),
[iquote('copy,3,flip.1,flip.2,flip.4')] ).
cnf(5,axiom,
( A != f(g(A))
| B != f(g(B))
| A = B
| C != g(f(C))
| D != g(f(D))
| C = D ),
file('SYN551+1.p',unknown),
[] ).
cnf(6,plain,
( f(g(A)) != A
| f(g(B)) != B
| A = B
| g(f(C)) != C
| g(f(D)) != D
| C = D ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[5])])])])]),
[iquote('copy,5,flip.1,flip.2,flip.4,flip.5')] ).
cnf(7,axiom,
( A != f(g(A))
| dollar_c4 = f(g(dollar_c4))
| B != g(f(B))
| dollar_c6 = g(f(dollar_c6)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(8,plain,
( f(g(A)) != A
| f(g(dollar_c4)) = dollar_c4
| g(f(B)) != B
| g(f(dollar_c6)) = dollar_c6 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[7])])])])]),
[iquote('copy,7,flip.1,flip.2,flip.3,flip.4')] ).
cnf(9,axiom,
( A != f(g(A))
| dollar_c4 = f(g(dollar_c4))
| B != g(f(B))
| dollar_c5 = g(f(dollar_c5)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(10,plain,
( f(g(A)) != A
| f(g(dollar_c4)) = dollar_c4
| g(f(B)) != B
| g(f(dollar_c5)) = dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[9])])])])]),
[iquote('copy,9,flip.1,flip.2,flip.3,flip.4')] ).
cnf(11,axiom,
( A != f(g(A))
| dollar_c4 = f(g(dollar_c4))
| B != g(f(B))
| dollar_c6 != dollar_c5 ),
file('SYN551+1.p',unknown),
[] ).
cnf(12,plain,
( f(g(A)) != A
| f(g(dollar_c4)) = dollar_c4
| g(f(B)) != B
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[11])])])]),
[iquote('copy,11,flip.1,flip.2,flip.3')] ).
cnf(13,axiom,
( A != f(g(A))
| dollar_c3 = f(g(dollar_c3))
| B != g(f(B))
| dollar_c6 = g(f(dollar_c6)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(14,plain,
( f(g(A)) != A
| f(g(dollar_c3)) = dollar_c3
| g(f(B)) != B
| g(f(dollar_c6)) = dollar_c6 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[13])])])])]),
[iquote('copy,13,flip.1,flip.2,flip.3,flip.4')] ).
cnf(15,axiom,
( A != f(g(A))
| dollar_c3 = f(g(dollar_c3))
| B != g(f(B))
| dollar_c5 = g(f(dollar_c5)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(16,plain,
( f(g(A)) != A
| f(g(dollar_c3)) = dollar_c3
| g(f(B)) != B
| g(f(dollar_c5)) = dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[15])])])])]),
[iquote('copy,15,flip.1,flip.2,flip.3,flip.4')] ).
cnf(17,axiom,
( A != f(g(A))
| dollar_c3 = f(g(dollar_c3))
| B != g(f(B))
| dollar_c6 != dollar_c5 ),
file('SYN551+1.p',unknown),
[] ).
cnf(18,plain,
( f(g(A)) != A
| f(g(dollar_c3)) = dollar_c3
| g(f(B)) != B
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[17])])])]),
[iquote('copy,17,flip.1,flip.2,flip.3')] ).
cnf(19,axiom,
( A != f(g(A))
| dollar_c4 != dollar_c3
| B != g(f(B))
| dollar_c6 = g(f(dollar_c6)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(20,plain,
( f(g(A)) != A
| dollar_c4 != dollar_c3
| g(f(B)) != B
| g(f(dollar_c6)) = dollar_c6 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[19])])])]),
[iquote('copy,19,flip.1,flip.3,flip.4')] ).
cnf(21,axiom,
( A != f(g(A))
| dollar_c4 != dollar_c3
| B != g(f(B))
| dollar_c5 = g(f(dollar_c5)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(22,plain,
( f(g(A)) != A
| dollar_c4 != dollar_c3
| g(f(B)) != B
| g(f(dollar_c5)) = dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[21])])])]),
[iquote('copy,21,flip.1,flip.3,flip.4')] ).
cnf(23,axiom,
( A != f(g(A))
| dollar_c4 != dollar_c3
| B != g(f(B))
| dollar_c6 != dollar_c5 ),
file('SYN551+1.p',unknown),
[] ).
cnf(24,plain,
( f(g(A)) != A
| dollar_c4 != dollar_c3
| g(f(B)) != B
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[23])])]),
[iquote('copy,23,flip.1,flip.3')] ).
cnf(34,axiom,
A = A,
file('SYN551+1.p',unknown),
[] ).
cnf(35,axiom,
( dollar_c1 = f(g(dollar_c1))
| dollar_c2 = g(f(dollar_c2)) ),
file('SYN551+1.p',unknown),
[] ).
cnf(36,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(dollar_c2)) = dollar_c2 ),
inference(flip,[status(thm),theory(equality)],[inference(flip,[status(thm),theory(equality)],[inference(copy,[status(thm)],[35])])]),
[iquote('copy,35,flip.1,flip.2')] ).
cnf(57,plain,
( f(g(A)) != A
| A = dollar_c1
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,4]),34])]),
[iquote('para_from,36.1.1,4.2.1,unit_del,34,factor_simp')] ).
cnf(59,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,24]),34]),
[iquote('para_from,36.1.1,24.1.1,unit_del,34')] ).
cnf(60,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,22]),34]),
[iquote('para_from,36.1.1,22.1.1,unit_del,34')] ).
cnf(61,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,20]),34]),
[iquote('para_from,36.1.1,20.1.1,unit_del,34')] ).
cnf(62,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,18]),34]),
[iquote('para_from,36.1.1,18.1.1,unit_del,34')] ).
cnf(63,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,16]),34]),
[iquote('para_from,36.1.1,16.1.1,unit_del,34')] ).
cnf(64,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,14]),34]),
[iquote('para_from,36.1.1,14.1.1,unit_del,34')] ).
cnf(65,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,12]),34]),
[iquote('para_from,36.1.1,12.1.1,unit_del,34')] ).
cnf(66,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,10]),34]),
[iquote('para_from,36.1.1,10.1.1,unit_del,34')] ).
cnf(67,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,8]),34]),
[iquote('para_from,36.1.1,8.1.1,unit_del,34')] ).
cnf(69,plain,
( f(g(A)) != A
| dollar_c1 = A
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,4]),34])]),
[iquote('para_from,36.1.1,4.1.1,unit_del,34,factor_simp')] ).
cnf(85,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,16]),34]),
[iquote('para_from,36.2.1,16.1.1.1,unit_del,34')] ).
cnf(86,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6
| f(g(dollar_c1)) = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,14]),34]),
[iquote('para_from,36.2.1,14.1.1.1,unit_del,34')] ).
cnf(88,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,10]),34]),
[iquote('para_from,36.2.1,10.1.1.1,unit_del,34')] ).
cnf(89,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6
| f(g(dollar_c1)) = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,8]),34]),
[iquote('para_from,36.2.1,8.1.1.1,unit_del,34')] ).
cnf(100,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A
| A = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,2]),34])]),
[iquote('para_from,36.2.1,2.3.1,unit_del,34,factor_simp')] ).
cnf(102,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A
| dollar_c2 = A ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[36,2]),34])]),
[iquote('para_from,36.2.1,2.2.1,unit_del,34,factor_simp')] ).
cnf(108,plain,
( f(dollar_c6) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| f(g(A)) != A
| f(g(dollar_c3)) = dollar_c3
| g(f(B)) != B ),
inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[57,14]),34]),
[iquote('para_into,57.1.1.1,14.4.1,unit_del,34')] ).
cnf(427,plain,
( f(g(A)) != A
| A = dollar_c1
| g(f(B)) != B
| g(f(C)) != C
| B = C
| g(f(D)) != D
| D = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[100,6]),34]),
[iquote('para_from,100.1.1,6.2.1,unit_del,34')] ).
cnf(506,plain,
( f(g(A)) != A
| A = dollar_c1
| g(f(B)) != B
| g(f(dollar_c2)) != dollar_c2
| B = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor,[status(thm)],[427])]),
[iquote('factor,427.5.7,factor_simp')] ).
cnf(753,plain,
( f(g(A)) != A
| dollar_c1 = A
| g(f(B)) != B
| g(f(C)) != C
| B = C
| g(f(D)) != D
| dollar_c2 = D ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[102,6]),34]),
[iquote('para_from,102.1.1,6.1.1,unit_del,34')] ).
cnf(771,plain,
( f(g(A)) != A
| dollar_c1 = A
| g(f(dollar_c2)) != dollar_c2
| g(f(B)) != B
| dollar_c2 = B ),
inference(factor_simp,[status(thm)],[inference(factor,[status(thm)],[753])]),
[iquote('factor,753.5.7,factor_simp')] ).
cnf(1459,plain,
( dollar_c4 != dollar_c3
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[59,36]),34])]),
[iquote('para_into,59.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(1474,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1459,24]),34])])]),
[iquote('para_from,1459.3.1,24.1.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(1519,plain,
( dollar_c4 != dollar_c3
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1474,1459]),34])])]),
[iquote('para_into,1474.2.1,1459.3.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(1536,plain,
( dollar_c4 != dollar_c3
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[60,36]),34])]),
[iquote('para_into,60.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(1559,plain,
( f(dollar_c5) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1536,69]),34])]),
[iquote('para_from,1536.2.1,69.1.1.1,unit_del,34,factor_simp')] ).
cnf(1564,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1536,22]),34])])]),
[iquote('para_from,1536.3.1,22.1.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(1592,plain,
( dollar_c4 != dollar_c3
| g(dollar_c1) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1559,1536])])]),
[iquote('para_from,1559.1.1,1536.2.1.1,factor_simp,factor_simp')] ).
cnf(1654,plain,
( dollar_c4 != dollar_c3
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[61,36]),34])]),
[iquote('para_into,61.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(1672,plain,
( dollar_c4 != dollar_c3
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1564,1536]),34])])]),
[iquote('para_into,1564.2.1,1536.3.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(1705,plain,
( dollar_c4 != dollar_c3
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1672,20]),34])]),
[iquote('para_from,1672.2.1,20.1.1.1,unit_del,34,factor_simp')] ).
cnf(1711,plain,
( f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1672,102]),34])]),
[iquote('para_from,1672.2.1,102.2.1,unit_del,34,flip.2')] ).
cnf(1760,plain,
( f(dollar_c6) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1654,69]),34])]),
[iquote('para_from,1654.2.1,69.1.1.1,unit_del,34,factor_simp')] ).
cnf(1774,plain,
( f(g(dollar_c3)) = dollar_c3
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[62,36]),34])]),
[iquote('para_into,62.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(1805,plain,
( dollar_c4 != dollar_c3
| g(dollar_c1) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1760,1654])])]),
[iquote('para_from,1760.1.1,1654.2.1.1,factor_simp,factor_simp')] ).
cnf(1821,plain,
( dollar_c4 != dollar_c3
| dollar_c6 = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1805,1592])])]),
[iquote('para_into,1805.2.1,1592.2.1,factor_simp,factor_simp')] ).
cnf(1889,plain,
( dollar_c4 != dollar_c3
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1821,1519]),34])]),
[iquote('para_from,1821.2.1,1519.2.1,unit_del,34,factor_simp')] ).
cnf(1902,plain,
( dollar_c3 != dollar_c1
| g(f(dollar_c2)) = dollar_c2
| f(g(dollar_c4)) != dollar_c4 ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1889,57])]),
[iquote('para_into,1889.1.1,57.2.1,factor_simp')] ).
cnf(1938,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[63,36]),34])]),
[iquote('para_into,63.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(1954,plain,
( dollar_c4 != dollar_c3
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1705,1889]),34])]),
[iquote('para_into,1705.2.1,1889.2.1,unit_del,34,factor_simp')] ).
cnf(1991,plain,
( f(g(dollar_c1)) = dollar_c1
| dollar_c6 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1954,102]),34])]),
[iquote('para_from,1954.2.1,102.2.1,unit_del,34,flip.2')] ).
cnf(2025,plain,
( dollar_c4 != dollar_c3
| dollar_c5 != dollar_c2
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1991,1519])]),
[iquote('para_from,1991.2.1,1519.2.1,factor_simp')] ).
cnf(2033,plain,
( dollar_c4 != dollar_c3
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2025,1711]),34])])]),
[iquote('para_into,2025.2.1,1711.2.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(2058,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[64,36]),34])]),
[iquote('para_into,64.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(2108,plain,
( dollar_c3 = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1774,69]),34])]),
[iquote('para_from,1774.1.1,69.1.1,unit_del,34,factor_simp')] ).
cnf(2113,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1774,18]),34])])]),
[iquote('para_from,1774.3.1,18.1.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(2150,plain,
( g(f(dollar_c2)) = dollar_c2
| f(g(dollar_c4)) != dollar_c4
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[1902,2108]),34])]),
[iquote('para_into,1902.1.1,2108.1.1,unit_del,34,factor_simp')] ).
cnf(2218,plain,
( f(g(dollar_c4)) = dollar_c4
| dollar_c6 != dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[65,1774]),34])])]),
[iquote('para_into,65.2.1.1,1774.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(2339,plain,
( f(g(dollar_c3)) = dollar_c3
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2113,1774]),34])])]),
[iquote('para_into,2113.2.1,1774.3.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(2361,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2339,12]),34])]),
[iquote('para_from,2339.1.1,12.1.1,unit_del,34,factor_simp')] ).
cnf(2367,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2339,102]),34])]),
[iquote('para_from,2339.1.1,102.2.1.1,unit_del,34,flip.2')] ).
cnf(2380,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[66,36]),34])]),
[iquote('para_into,66.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(2424,plain,
( f(dollar_c2) = dollar_c3
| dollar_c6 != dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2367,2339])]),
[iquote('para_from,2367.2.1,2339.1.1.1,factor_simp')] ).
cnf(2585,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[67,36]),34])]),
[iquote('para_into,67.2.1.1,36.1.1,unit_del,34,factor_simp')] ).
cnf(2602,plain,
( g(f(dollar_c2)) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2218,2150]),34])])]),
[iquote('para_from,2218.1.1,2150.2.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(2648,plain,
( f(g(dollar_c4)) = dollar_c4
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2361,2339]),34])]),
[iquote('para_into,2361.2.1.1,2339.1.1,unit_del,34,factor_simp')] ).
cnf(2674,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c4) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2648,102]),34])]),
[iquote('para_from,2648.1.1,102.2.1.1,unit_del,34,flip.2')] ).
cnf(2678,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c5)) = dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[85,36])]),
[iquote('hyper,85,36,factor_simp')] ).
cnf(2713,plain,
( f(dollar_c2) = dollar_c4
| dollar_c6 != dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2674,2648])]),
[iquote('para_from,2674.2.1,2648.1.1.1,factor_simp')] ).
cnf(2717,plain,
( dollar_c4 = dollar_c3
| dollar_c6 != dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2713,2424])])]),
[iquote('para_into,2713.1.1,2424.1.1,factor_simp,factor_simp')] ).
cnf(2789,plain,
( f(g(dollar_c1)) = dollar_c1
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2717,2033]),34])]),
[iquote('para_from,2717.1.1,2033.1.1,unit_del,34,factor_simp')] ).
cnf(2811,plain,
( f(g(dollar_c1)) = dollar_c1
| dollar_c5 != dollar_c2
| g(f(dollar_c6)) != dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2789,100])]),
[iquote('para_into,2789.2.1,100.3.1,factor_simp')] ).
cnf(2829,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c6)) = dollar_c6
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[86,36])]),
[iquote('hyper,86,36,factor_simp')] ).
cnf(2951,plain,
( g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1938,69])]),
[iquote('hyper,1938,69,factor_simp')] ).
cnf(2974,plain,
( f(dollar_c5) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| f(g(dollar_c3)) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1938,69]),34])]),
[iquote('para_from,1938.2.1,69.1.1.1,unit_del,34,factor_simp')] ).
cnf(2979,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[1938,16]),34])])]),
[iquote('para_from,1938.3.1,16.1.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(3018,plain,
( f(dollar_c5) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2951,69]),34])]),
[iquote('para_from,2951.1.1,69.1.1.1,unit_del,34,factor_simp')] ).
cnf(3040,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c5)) = dollar_c5
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[88,36])]),
[iquote('hyper,88,36,factor_simp')] ).
cnf(3066,plain,
( g(dollar_c1) = dollar_c5
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3018,2951])])]),
[iquote('para_from,3018.1.1,2951.1.1.1,factor_simp,factor_simp')] ).
cnf(3173,plain,
( f(g(dollar_c3)) = dollar_c3
| g(dollar_c1) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2974,1938])])]),
[iquote('para_from,2974.1.1,1938.2.1.1,factor_simp,factor_simp')] ).
cnf(3245,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c6)) = dollar_c6
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[89,36])]),
[iquote('hyper,89,36,factor_simp')] ).
cnf(3695,plain,
( f(dollar_c6) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| f(g(dollar_c3)) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[108,36,1938])])])]),
[iquote('hyper,108,36,1938,factor_simp,factor_simp,factor_simp')] ).
cnf(3697,plain,
( f(dollar_c6) = dollar_c1
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3695,69])]),
[iquote('hyper,3695,69,factor_simp')] ).
cnf(3720,plain,
( g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[2058,69])]),
[iquote('hyper,2058,69,factor_simp')] ).
cnf(3727,plain,
( f(g(dollar_c3)) = dollar_c3
| g(dollar_c1) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[2058,3695])])]),
[iquote('para_into,2058.2.1.1,3695.1.1,factor_simp,factor_simp')] ).
cnf(3733,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[2058,14]),34])])]),
[iquote('para_from,2058.3.1,14.1.1.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(3738,plain,
( g(dollar_c1) = dollar_c6
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3720,3697])])]),
[iquote('para_into,3720.1.1.1,3697.1.1,factor_simp,factor_simp')] ).
cnf(3753,plain,
( dollar_c6 = dollar_c5
| g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3738,3066])])]),
[iquote('para_into,3738.1.1,3066.1.1,factor_simp,factor_simp')] ).
cnf(3759,plain,
( g(f(dollar_c2)) = dollar_c2
| dollar_c3 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3753,2602])]),
[iquote('hyper,3753,2602,factor_simp')] ).
cnf(3760,plain,
( g(f(dollar_c2)) = dollar_c2
| f(g(dollar_c4)) != dollar_c4 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3759,1902]),34])]),
[iquote('para_from,3759.2.1,1902.1.1,unit_del,34,factor_simp')] ).
cnf(3771,plain,
( f(g(dollar_c3)) = dollar_c3
| dollar_c6 = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3727,3173])])]),
[iquote('para_into,3727.2.1,3173.2.1,factor_simp,factor_simp')] ).
cnf(3778,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3771,2602])]),
[iquote('hyper,3771,2602,factor_simp')] ).
cnf(3785,plain,
( f(g(A)) != A
| dollar_c3 = A
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3778,4]),34])]),
[iquote('para_from,3778.1.1,4.1.1,unit_del,34,factor_simp')] ).
cnf(3811,plain,
( g(f(dollar_c5)) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[2380,3760])]),
[iquote('hyper,2380,3760,factor_simp')] ).
cnf(3820,plain,
( f(dollar_c5) = dollar_c3
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3811,3785]),34])]),
[iquote('para_from,3811.1.1,3785.1.1.1,unit_del,34,factor_simp')] ).
cnf(3825,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3811,10]),34])]),
[iquote('para_from,3811.2.1,10.1.1.1,unit_del,34,factor_simp')] ).
cnf(3830,plain,
( g(dollar_c3) = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3820,3811])]),
[iquote('para_from,3820.1.1,3811.1.1.1,factor_simp')] ).
cnf(3887,plain,
( g(f(dollar_c6)) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[2585,3760])]),
[iquote('hyper,2585,3760,factor_simp')] ).
cnf(3902,plain,
( f(dollar_c6) = dollar_c3
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3887,3785]),34])]),
[iquote('para_from,3887.1.1,3785.1.1.1,unit_del,34,factor_simp')] ).
cnf(3907,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(A)) != A
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3887,8]),34])]),
[iquote('para_from,3887.2.1,8.1.1.1,unit_del,34,factor_simp')] ).
cnf(3913,plain,
( g(dollar_c3) = dollar_c6
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3902,3887])]),
[iquote('para_from,3902.1.1,3887.1.1.1,factor_simp')] ).
cnf(3922,plain,
( dollar_c6 = dollar_c5
| g(f(dollar_c2)) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3913,3830])]),
[iquote('para_into,3913.1.1,3830.1.1,factor_simp')] ).
cnf(3928,plain,
g(f(dollar_c2)) = dollar_c2,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3922,2602])]),
[iquote('hyper,3922,2602,factor_simp')] ).
cnf(3933,plain,
( f(g(A)) != A
| dollar_c1 = A
| g(f(B)) != B
| dollar_c2 = B ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[771]),3928]),34]),
[iquote('back_demod,771,demod,3928,unit_del,34')] ).
cnf(3937,plain,
( f(g(A)) != A
| A = dollar_c1
| g(f(B)) != B
| B = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[506]),3928]),34]),
[iquote('back_demod,506,demod,3928,unit_del,34')] ).
cnf(3942,plain,
( f(g(dollar_c3)) = dollar_c3
| f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[2678,102])]),
[iquote('hyper,2678,102,factor_simp')] ).
cnf(3982,plain,
( f(g(dollar_c3)) = dollar_c3
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[2829,2811,3942])])])]),
[iquote('hyper,2829,2811,3942,factor_simp,factor_simp,factor_simp')] ).
cnf(3988,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3982,102]),34])]),
[iquote('para_from,3982.1.1,102.2.1.1,unit_del,34,factor_simp')] ).
cnf(3990,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A
| g(dollar_c3) = A ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3982,2]),34])]),
[iquote('para_from,3982.1.1,2.2.1.1,unit_del,34,factor_simp')] ).
cnf(3993,plain,
( f(dollar_c2) = dollar_c3
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[3988,3982])]),
[iquote('para_from,3988.2.1,3982.1.1.1,factor_simp')] ).
cnf(3995,plain,
( f(A) = dollar_c3
| f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3993,102])]),
[iquote('para_into,3993.1.1.1,102.3.1,factor_simp')] ).
cnf(4012,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c5)) = dollar_c5 ),
inference(hyper,[status(thm)],[2979,3928]),
[iquote('hyper,2979,3927')] ).
cnf(4013,plain,
( f(g(dollar_c4)) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| f(dollar_c5) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3040,3995])]),
[iquote('hyper,3040,3995,factor_simp')] ).
cnf(4014,plain,
( f(g(dollar_c4)) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3040,3990])]),
[iquote('hyper,3040,3990,factor_simp')] ).
cnf(4016,plain,
( f(g(dollar_c4)) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3040,102])]),
[iquote('hyper,3040,102,factor_simp')] ).
cnf(4034,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c4) = dollar_c2
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4016,102]),34])]),
[iquote('para_from,4016.1.1,102.2.1.1,unit_del,34,factor_simp')] ).
cnf(4038,plain,
( f(dollar_c2) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4034,4016])])]),
[iquote('para_from,4034.2.1,4016.1.1.1,factor_simp,factor_simp')] ).
cnf(4042,plain,
( dollar_c4 = dollar_c3
| f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[4038,3995]),3928]),34])]),
[iquote('para_into,4038.1.1,3995.1.1,demod,3928,unit_del,34,factor_simp')] ).
cnf(4046,plain,
( f(g(dollar_c1)) = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4042,2033])]),
[iquote('hyper,4042,2033,factor_simp')] ).
cnf(4047,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(dollar_c6)) != dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4046,2811]),34])]),
[iquote('para_from,4046.2.1,2811.2.1,unit_del,34,factor_simp')] ).
cnf(4056,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c4) = dollar_c2
| f(dollar_c5) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4013,102]),34])]),
[iquote('para_from,4013.1.1,102.2.1.1,unit_del,34,factor_simp')] ).
cnf(4059,plain,
( f(dollar_c2) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| f(dollar_c5) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4056,4013])])]),
[iquote('para_from,4056.2.1,4013.1.1.1,factor_simp,factor_simp')] ).
cnf(4063,plain,
( dollar_c4 = dollar_c3
| f(g(dollar_c1)) = dollar_c1
| f(dollar_c5) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[4059,3995]),3928]),34])]),
[iquote('para_into,4059.1.1,3995.1.1,demod,3928,unit_del,34,factor_simp')] ).
cnf(4065,plain,
( f(g(dollar_c1)) = dollar_c1
| f(dollar_c5) = dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4063,2033])]),
[iquote('hyper,4063,2033,factor_simp')] ).
cnf(4075,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c4) = dollar_c2
| g(dollar_c3) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4014,102]),34])]),
[iquote('para_from,4014.1.1,102.2.1.1,unit_del,34,factor_simp')] ).
cnf(4081,plain,
( f(dollar_c2) = dollar_c4
| f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4075,4014])])]),
[iquote('para_from,4075.2.1,4014.1.1.1,factor_simp,factor_simp')] ).
cnf(4087,plain,
( dollar_c4 = dollar_c3
| f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[4081,3995]),3928]),34])]),
[iquote('para_into,4081.1.1,3995.1.1,demod,3928,unit_del,34,factor_simp')] ).
cnf(4093,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c3) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4087,2033])]),
[iquote('hyper,4087,2033,factor_simp')] ).
cnf(4097,plain,
( f(g(dollar_c1)) = dollar_c1
| g(f(A)) != A
| dollar_c5 = A ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4093,3990])]),
[iquote('para_from,4093.2.1,3990.3.1,factor_simp')] ).
cnf(4126,plain,
( f(g(dollar_c4)) = dollar_c4
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3245,4047])]),
[iquote('hyper,3245,4047,factor_simp')] ).
cnf(4138,plain,
( f(g(dollar_c1)) = dollar_c1
| g(dollar_c4) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4126,4097]),34])]),
[iquote('para_from,4126.1.1,4097.2.1.1,unit_del,34,factor_simp')] ).
cnf(4148,plain,
( f(dollar_c5) = dollar_c4
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4138,4126])]),
[iquote('para_from,4138.2.1,4126.1.1.1,factor_simp')] ).
cnf(4156,plain,
( dollar_c4 = dollar_c3
| f(g(dollar_c1)) = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4148,4065])]),
[iquote('para_into,4148.1.1,4065.2.1,factor_simp')] ).
cnf(4159,plain,
f(g(dollar_c1)) = dollar_c1,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4156,2033])]),
[iquote('hyper,4156,2033,factor_simp')] ).
cnf(4164,plain,
( f(g(dollar_c3)) = dollar_c3
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3733,4012])]),
[iquote('hyper,3733,4012,factor_simp')] ).
cnf(4165,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c5)) = dollar_c5 ),
inference(hyper,[status(thm)],[3825,3928]),
[iquote('hyper,3825,3927')] ).
cnf(4167,plain,
( f(g(dollar_c4)) = dollar_c4
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[3907,4165])]),
[iquote('hyper,3907,4165,factor_simp')] ).
cnf(4172,plain,
( f(dollar_c2) = dollar_c1
| g(f(A)) != A
| dollar_c2 = A ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,3928]),34])]),
[iquote('para_into,3933.1.1.1,3927.1.1,unit_del,34,flip.1')] ).
cnf(4175,plain,
( dollar_c4 = dollar_c1
| g(f(A)) != A
| dollar_c2 = A
| g(f(dollar_c6)) = dollar_c6 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,4167]),34])]),
[iquote('para_into,3933.1.1,4167.1.1,unit_del,34,flip.1')] ).
cnf(4176,plain,
( dollar_c4 = dollar_c1
| g(f(A)) != A
| dollar_c2 = A
| g(f(dollar_c5)) = dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,4165]),34])]),
[iquote('para_into,3933.1.1,4165.1.1,unit_del,34,flip.1')] ).
cnf(4179,plain,
( dollar_c4 = dollar_c1
| g(f(A)) != A
| dollar_c2 = A
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,2648]),34])]),
[iquote('para_into,3933.1.1,2648.1.1,unit_del,34,flip.1')] ).
cnf(4180,plain,
( dollar_c3 = dollar_c1
| g(f(A)) != A
| dollar_c2 = A
| dollar_c6 != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,2339]),34])]),
[iquote('para_into,3933.1.1,2339.1.1,unit_del,34,flip.1')] ).
cnf(4192,plain,
( f(g(A)) != A
| dollar_c1 = A
| dollar_c6 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,1954]),34])]),
[iquote('para_into,3933.3.1,1954.2.1,unit_del,34,flip.3')] ).
cnf(4193,plain,
( f(g(A)) != A
| dollar_c1 = A
| dollar_c5 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[3933,1672]),34])]),
[iquote('para_into,3933.3.1,1672.2.1,unit_del,34,flip.3')] ).
cnf(4203,plain,
( f(dollar_c2) = dollar_c1
| g(dollar_c1) = dollar_c2 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4172,4159]),34])]),
[iquote('para_into,4172.2.1.1,4159.1.1,unit_del,34,flip.2')] ).
cnf(4215,plain,
g(dollar_c1) = dollar_c2,
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4203,3928])]),
[iquote('para_from,4203.1.1,3927.1.1.1,factor_simp')] ).
cnf(4217,plain,
f(dollar_c2) = dollar_c1,
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4203,4159])]),
[iquote('para_from,4203.2.1,4159.1.1.1,factor_simp')] ).
cnf(4225,plain,
( dollar_c4 = dollar_c1
| g(dollar_c4) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4179,2648]),34])]),
[iquote('para_into,4179.2.1.1,2648.1.1,unit_del,34,factor_simp')] ).
cnf(4234,plain,
( dollar_c4 = dollar_c1
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4225,2648]),4217])])]),
[iquote('para_from,4225.2.1,2648.1.1.1,demod,4217,factor_simp,factor_simp')] ).
cnf(4237,plain,
( dollar_c3 != dollar_c1
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4234,1519])]),
[iquote('para_from,4234.1.1,1519.1.1,factor_simp')] ).
cnf(4243,plain,
( dollar_c3 = dollar_c1
| g(dollar_c3) = dollar_c2
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4180,2339]),34])]),
[iquote('para_into,4180.2.1.1,2339.1.1,unit_del,34,factor_simp')] ).
cnf(4250,plain,
( dollar_c3 = dollar_c1
| dollar_c6 != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4243,2339]),4217])])]),
[iquote('para_from,4243.2.1,2339.1.1.1,demod,4217,factor_simp,factor_simp')] ).
cnf(4251,plain,
dollar_c6 != dollar_c5,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4250,4237]),34])]),
[iquote('para_from,4250.1.1,4237.1.1,unit_del,34,factor_simp')] ).
cnf(4256,plain,
( f(dollar_c6) = dollar_c1
| dollar_c6 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4192,1954]),34])]),
[iquote('para_into,4192.1.1.1,1954.2.1,unit_del,34,factor_simp')] ).
cnf(4262,plain,
( dollar_c4 != dollar_c3
| dollar_c6 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4256,1954]),4215])])]),
[iquote('para_from,4256.1.1,1954.2.1.1,demod,4215,factor_simp,factor_simp')] ).
cnf(4264,plain,
( dollar_c5 != dollar_c2
| dollar_c4 != dollar_c3 ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4262,4251])]),
[iquote('para_from,4262.2.1,4251.1.1,flip.1')] ).
cnf(4270,plain,
( f(dollar_c5) = dollar_c1
| dollar_c5 = dollar_c2
| dollar_c4 != dollar_c3 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4193,1672]),34])]),
[iquote('para_into,4193.1.1.1,1672.2.1,unit_del,34,factor_simp')] ).
cnf(4276,plain,
( dollar_c4 != dollar_c3
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4270,1672]),4215])])]),
[iquote('para_from,4270.1.1,1672.2.1.1,demod,4215,factor_simp,factor_simp')] ).
cnf(4278,plain,
dollar_c4 != dollar_c3,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4276,4264]),34])]),
[iquote('para_from,4276.2.1,4264.1.1,unit_del,34,factor_simp')] ).
cnf(4295,plain,
( dollar_c4 = dollar_c1
| g(dollar_c4) = dollar_c2
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4175,4167]),34])]),
[iquote('para_into,4175.2.1.1,4167.1.1,unit_del,34,factor_simp')] ).
cnf(4301,plain,
( dollar_c4 = dollar_c1
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4295,4167]),4217])])]),
[iquote('para_from,4295.2.1,4167.1.1.1,demod,4217,factor_simp,factor_simp')] ).
cnf(4305,plain,
( f(g(A)) != A
| A = dollar_c1
| dollar_c6 = dollar_c2
| dollar_c4 = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4301,3937]),34]),
[iquote('para_from,4301.2.1,3937.3.1,unit_del,34')] ).
cnf(4307,plain,
( f(g(dollar_c4)) != dollar_c4
| dollar_c4 = dollar_c1
| dollar_c6 = dollar_c2 ),
inference(factor,[status(thm)],[4305]),
[iquote('factor,4305.2.4')] ).
cnf(4315,plain,
( dollar_c5 != dollar_c2
| f(g(dollar_c4)) != dollar_c4
| dollar_c4 = dollar_c1 ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4307,4251])]),
[iquote('para_from,4307.3.1,4251.1.1,flip.1')] ).
cnf(4318,plain,
( f(g(dollar_c4)) != dollar_c4
| dollar_c4 = dollar_c1
| g(f(dollar_c5)) != dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4315,3937]),34])])]),
[iquote('para_into,4315.1.1,3937.4.1,unit_del,34,factor_simp,factor_simp')] ).
cnf(4320,plain,
( dollar_c3 != dollar_c1
| f(g(dollar_c4)) != dollar_c4
| g(f(dollar_c5)) != dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4318,4278])]),
[iquote('para_from,4318.2.1,4278.1.1,flip.1')] ).
cnf(4334,plain,
( f(dollar_c6) = dollar_c1
| dollar_c6 = dollar_c2
| dollar_c4 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4305,4301]),34])]),
[iquote('para_into,4305.1.1.1,4301.2.1,unit_del,34,factor_simp')] ).
cnf(4350,plain,
( dollar_c4 = dollar_c1
| dollar_c6 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4334,4301]),4215])])]),
[iquote('para_from,4334.1.1,4301.2.1.1,demod,4215,factor_simp,factor_simp')] ).
cnf(4354,plain,
( dollar_c5 != dollar_c2
| dollar_c4 = dollar_c1 ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4350,4251])]),
[iquote('para_from,4350.2.1,4251.1.1,flip.1')] ).
cnf(4376,plain,
( dollar_c4 = dollar_c1
| g(dollar_c4) = dollar_c2
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4176,4165]),34])]),
[iquote('para_into,4176.2.1.1,4165.1.1,unit_del,34,factor_simp')] ).
cnf(4379,plain,
( dollar_c4 = dollar_c1
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4376,4165]),4217])])]),
[iquote('para_from,4376.2.1,4165.1.1.1,demod,4217,factor_simp,factor_simp')] ).
cnf(4382,plain,
( dollar_c3 != dollar_c1
| g(f(dollar_c5)) = dollar_c5 ),
inference(flip,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4379,4278])]),
[iquote('para_from,4379.1.1,4278.1.1,flip.1')] ).
cnf(4386,plain,
( f(g(A)) != A
| A = dollar_c1
| dollar_c5 = dollar_c2
| dollar_c4 = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4379,3937]),34]),
[iquote('para_from,4379.2.1,3937.3.1,unit_del,34')] ).
cnf(4388,plain,
( dollar_c3 != dollar_c1
| f(g(dollar_c4)) != dollar_c4 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[4382,4320]),34])]),
[iquote('para_from,4382.2.1,4320.3.1,unit_del,34,factor_simp')] ).
cnf(4394,plain,
( f(dollar_c5) = dollar_c1
| dollar_c5 = dollar_c2
| dollar_c4 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4386,4379]),34])]),
[iquote('para_into,4386.1.1.1,4379.2.1,unit_del,34,factor_simp')] ).
cnf(4403,plain,
( f(dollar_c5) = dollar_c1
| dollar_c4 = dollar_c1 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4394,4354])]),
[iquote('hyper,4394,4354,factor_simp')] ).
cnf(4405,plain,
( dollar_c4 = dollar_c1
| dollar_c5 = dollar_c2 ),
inference(factor_simp,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4403,4379]),4215])]),
[iquote('para_from,4403.1.1,4379.2.1.1,demod,4215,factor_simp')] ).
cnf(4408,plain,
dollar_c4 = dollar_c1,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[4405,4354])]),
[iquote('hyper,4405,4354,factor_simp')] ).
cnf(4409,plain,
dollar_c3 != dollar_c1,
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[4388]),4408,4215,4217,4408]),34]),
[iquote('back_demod,4388,demod,4408,4215,4217,4408,unit_del,34')] ).
cnf(4410,plain,
( f(g(dollar_c3)) != dollar_c3
| g(f(A)) != A
| A = dollar_c2 ),
inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4409,3937]),34]),
[iquote('para_into,4409.1.1,3937.2.1,unit_del,34')] ).
cnf(4412,plain,
( g(f(A)) != A
| A = dollar_c2
| g(f(dollar_c6)) = dollar_c6 ),
inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4410,4164]),34]),
[iquote('para_into,4410.1.1,4164.1.1,unit_del,34')] ).
cnf(4413,plain,
( g(f(A)) != A
| A = dollar_c2
| g(f(dollar_c5)) = dollar_c5 ),
inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4410,4012]),34]),
[iquote('para_into,4410.1.1,4012.1.1,unit_del,34')] ).
cnf(4422,plain,
( g(dollar_c3) = dollar_c2
| g(f(dollar_c6)) = dollar_c6 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4412,4164]),34])]),
[iquote('para_into,4412.1.1.1,4164.1.1,unit_del,34,factor_simp')] ).
cnf(4431,plain,
g(f(dollar_c6)) = dollar_c6,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4422,4164]),4217]),4409])]),
[iquote('para_from,4422.1.1,4164.1.1.1,demod,4217,unit_del,4409,factor_simp')] ).
cnf(4442,plain,
( dollar_c6 = dollar_c2
| g(f(A)) != A
| A = dollar_c2 ),
inference(flip,[status(thm),theory(equality)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[4431,3937]),4215,4431]),34])]),
[iquote('para_into,4430.1.1.1,3937.2.1,demod,4215,4431,unit_del,34,flip.1')] ).
cnf(4445,plain,
dollar_c6 = dollar_c2,
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(factor,[status(thm)],[4442]),4431]),34]),
[iquote('factor,4442.1.3,demod,4431,unit_del,34')] ).
cnf(4446,plain,
dollar_c5 != dollar_c2,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[4251]),4445])]),
[iquote('back_demod,4251,demod,4445,flip.1')] ).
cnf(4448,plain,
( g(dollar_c3) = dollar_c2
| g(f(dollar_c5)) = dollar_c5 ),
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4413,4012]),34])]),
[iquote('para_into,4413.1.1.1,4012.1.1,unit_del,34,factor_simp')] ).
cnf(4452,plain,
g(f(dollar_c5)) = dollar_c5,
inference(factor_simp,[status(thm)],[inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[4448,4012]),4217]),4409])]),
[iquote('para_from,4448.1.1,4012.1.1.1,demod,4217,unit_del,4409,factor_simp')] ).
cnf(4457,plain,
( f(g(A)) != A
| A = dollar_c1 ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_into,[status(thm),theory(equality)],[4452,3937]),4217,4215,4452]),4446,34]),
[iquote('para_into,4451.1.1.1.1,3937.4.1,demod,4217,4215,4452,unit_del,4446,34')] ).
cnf(4462,plain,
f(dollar_c5) = dollar_c1,
inference(unit_del,[status(thm)],[inference(para_into,[status(thm),theory(equality)],[4457,4452]),34]),
[iquote('para_into,4457.1.1.1,4451.1.1,unit_del,34')] ).
cnf(4463,plain,
dollar_c5 = dollar_c2,
inference(flip,[status(thm),theory(equality)],[inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[4452]),4462,4215])]),
[iquote('back_demod,4451,demod,4462,4215,flip.1')] ).
cnf(4465,plain,
$false,
inference(binary,[status(thm)],[4463,4446]),
[iquote('binary,4463.1,4446.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SYN551+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% 0.11/0.13 % Command : otter-tptp-script %s
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Jul 27 11:16:08 EDT 2022
% 0.14/0.35 % CPUTime :
% 11.37/11.56 ----- Otter 3.3f, August 2004 -----
% 11.37/11.56 The process was started by sandbox2 on n020.cluster.edu,
% 11.37/11.56 Wed Jul 27 11:16:08 2022
% 11.37/11.56 The command was "./otter". The process ID is 32556.
% 11.37/11.56
% 11.37/11.56 set(prolog_style_variables).
% 11.37/11.56 set(auto).
% 11.37/11.56 dependent: set(auto1).
% 11.37/11.56 dependent: set(process_input).
% 11.37/11.56 dependent: clear(print_kept).
% 11.37/11.56 dependent: clear(print_new_demod).
% 11.37/11.56 dependent: clear(print_back_demod).
% 11.37/11.56 dependent: clear(print_back_sub).
% 11.37/11.56 dependent: set(control_memory).
% 11.37/11.56 dependent: assign(max_mem, 12000).
% 11.37/11.56 dependent: assign(pick_given_ratio, 4).
% 11.37/11.56 dependent: assign(stats_level, 1).
% 11.37/11.56 dependent: assign(max_seconds, 10800).
% 11.37/11.56 clear(print_given).
% 11.37/11.56
% 11.37/11.56 formula_list(usable).
% 11.37/11.56 all A (A=A).
% 11.37/11.56 -((exists X (X=f(g(X))))& (all Y Z (Y=f(g(Y))&Z=f(g(Z))->Y=Z))<-> (exists X (X=g(f(X))))& (all Y Z (Y=g(f(Y))&Z=g(f(Z))->Y=Z))).
% 11.37/11.56 end_of_list.
% 11.37/11.56
% 11.37/11.56 -------> usable clausifies to:
% 11.37/11.56
% 11.37/11.56 list(usable).
% 11.37/11.56 0 [] A=A.
% 11.37/11.56 0 [] $c1=f(g($c1))|$c2=g(f($c2)).
% 11.37/11.56 0 [] $c1=f(g($c1))|X1!=g(f(X1))|X2!=g(f(X2))|X1=X2.
% 11.37/11.56 0 [] Y!=f(g(Y))|Z!=f(g(Z))|Y=Z|$c2=g(f($c2)).
% 11.37/11.56 0 [] Y!=f(g(Y))|Z!=f(g(Z))|Y=Z|X1!=g(f(X1))|X2!=g(f(X2))|X1=X2.
% 11.37/11.56 0 [] X!=f(g(X))|$c4=f(g($c4))|X3!=g(f(X3))|$c6=g(f($c6)).
% 11.37/11.56 0 [] X!=f(g(X))|$c4=f(g($c4))|X3!=g(f(X3))|$c5=g(f($c5)).
% 11.37/11.56 0 [] X!=f(g(X))|$c4=f(g($c4))|X3!=g(f(X3))|$c6!=$c5.
% 11.37/11.56 0 [] X!=f(g(X))|$c3=f(g($c3))|X3!=g(f(X3))|$c6=g(f($c6)).
% 11.37/11.56 0 [] X!=f(g(X))|$c3=f(g($c3))|X3!=g(f(X3))|$c5=g(f($c5)).
% 11.37/11.56 0 [] X!=f(g(X))|$c3=f(g($c3))|X3!=g(f(X3))|$c6!=$c5.
% 11.37/11.56 0 [] X!=f(g(X))|$c4!=$c3|X3!=g(f(X3))|$c6=g(f($c6)).
% 11.37/11.56 0 [] X!=f(g(X))|$c4!=$c3|X3!=g(f(X3))|$c5=g(f($c5)).
% 11.37/11.56 0 [] X!=f(g(X))|$c4!=$c3|X3!=g(f(X3))|$c6!=$c5.
% 11.37/11.56 end_of_list.
% 11.37/11.56
% 11.37/11.56 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6.
% 11.37/11.56
% 11.37/11.56 This ia a non-Horn set with equality. The strategy will be
% 11.37/11.56 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 11.37/11.56 deletion, with positive clauses in sos and nonpositive
% 11.37/11.56 clauses in usable.
% 11.37/11.56
% 11.37/11.56 dependent: set(knuth_bendix).
% 11.37/11.56 dependent: set(anl_eq).
% 11.37/11.56 dependent: set(para_from).
% 11.37/11.56 dependent: set(para_into).
% 11.37/11.56 dependent: clear(para_from_right).
% 11.37/11.56 dependent: clear(para_into_right).
% 11.37/11.56 dependent: set(para_from_vars).
% 11.37/11.56 dependent: set(eq_units_both_ways).
% 11.37/11.56 dependent: set(dynamic_demod_all).
% 11.37/11.56 dependent: set(dynamic_demod).
% 11.37/11.56 dependent: set(order_eq).
% 11.37/11.56 dependent: set(back_demod).
% 11.37/11.56 dependent: set(lrpo).
% 11.37/11.56 dependent: set(hyper_res).
% 11.37/11.56 dependent: set(unit_deletion).
% 11.37/11.56 dependent: set(factor).
% 11.37/11.56
% 11.37/11.56 ------------> process usable:
% 11.37/11.56 ** KEPT (pick-wt=18): 2 [copy,1,flip.1,flip.2,flip.3] f(g($c1))=$c1|g(f(A))!=A|g(f(B))!=B|A=B.
% 11.37/11.56 ** KEPT (pick-wt=18): 4 [copy,3,flip.1,flip.2,flip.4] f(g(A))!=A|f(g(B))!=B|A=B|g(f($c2))=$c2.
% 11.37/11.56 ** KEPT (pick-wt=26): 6 [copy,5,flip.1,flip.2,flip.4,flip.5] f(g(A))!=A|f(g(B))!=B|A=B|g(f(C))!=C|g(f(D))!=D|C=D.
% 11.37/11.56 ** KEPT (pick-wt=20): 8 [copy,7,flip.1,flip.2,flip.3,flip.4] f(g(A))!=A|f(g($c4))=$c4|g(f(B))!=B|g(f($c6))=$c6.
% 11.37/11.56 ** KEPT (pick-wt=20): 10 [copy,9,flip.1,flip.2,flip.3,flip.4] f(g(A))!=A|f(g($c4))=$c4|g(f(B))!=B|g(f($c5))=$c5.
% 11.37/11.56 ** KEPT (pick-wt=18): 12 [copy,11,flip.1,flip.2,flip.3] f(g(A))!=A|f(g($c4))=$c4|g(f(B))!=B|$c6!=$c5.
% 11.37/11.56 ** KEPT (pick-wt=20): 14 [copy,13,flip.1,flip.2,flip.3,flip.4] f(g(A))!=A|f(g($c3))=$c3|g(f(B))!=B|g(f($c6))=$c6.
% 11.37/11.56 ** KEPT (pick-wt=20): 16 [copy,15,flip.1,flip.2,flip.3,flip.4] f(g(A))!=A|f(g($c3))=$c3|g(f(B))!=B|g(f($c5))=$c5.
% 11.37/11.56 ** KEPT (pick-wt=18): 18 [copy,17,flip.1,flip.2,flip.3] f(g(A))!=A|f(g($c3))=$c3|g(f(B))!=B|$c6!=$c5.
% 11.37/11.56 ** KEPT (pick-wt=18): 20 [copy,19,flip.1,flip.3,flip.4] f(g(A))!=A|$c4!=$c3|g(f(B))!=B|g(f($c6))=$c6.
% 11.37/11.56 ** KEPT (pick-wt=18): 22 [copy,21,flip.1,flip.3,flip.4] f(g(A))!=A|$c4!=$c3|g(f(B))!=B|g(f($c5))=$c5.
% 11.37/11.56 ** KEPT (pick-wt=16): 24 [copy,23,flip.1,flip.3] f(g(A))!=A|$c4!=$c3|g(f(B))!=B|$c6!=$c5.
% 11.37/11.56
% 11.37/11.56 ------------> process sos:
% 11.37/11.56 ** KEPT (pick-wt=3): 34 [] A=A.
% 11.37/11.56 ** KEPT (pick-wt=10): 36 [copy,35,flip.1,flip.2] f(g($c1))=$c1|g(f($c2))=$c2.
% 11.37/11.56 Following clause subsumed by 34 during input processing: 0 [copy,34,flip.1] A=A.
% 11.37/11.56 34 back subsumes 33.
% 11.37/11.56 34 back subsumes 32.
% 11.37/11.56 34 back subsumes 31.
% 11.37/11.56 34 back subsumes 29.
% 11.37/11.56 34 back subsumes 27.
% 11.37/11.56 34 back subsumes 26.
% 11.37/11.56
% 11.37/11.56 ======= end of input processing =======
% 11.37/11.56
% 11.37/11.56 =========== start of search ===========
% 11.37/11.56
% 11.37/11.56
% 11.37/11.56 Resetting weight limit to 20.
% 11.37/11.56
% 11.37/11.56
% 11.37/11.56 Resetting weight limit to 20.
% 96.27/96.42
% 96.27/96.42 sos_size=1812
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 19.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 19.
% 96.27/96.42
% 96.27/96.42 sos_size=1743
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 18.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 18.
% 96.27/96.42
% 96.27/96.42 sos_size=972
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 16.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 16.
% 96.27/96.42
% 96.27/96.42 sos_size=280
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 15.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 15.
% 96.27/96.42
% 96.27/96.42 sos_size=144
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 12.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Resetting weight limit to 12.
% 96.27/96.42
% 96.27/96.42 sos_size=71
% 96.27/96.42
% 96.27/96.42 -- HEY sandbox2, WE HAVE A PROOF!! --
% 96.27/96.42
% 96.27/96.42 ----> UNIT CONFLICT at 94.25 sec ----> 4465 [binary,4463.1,4446.1] $F.
% 96.27/96.42
% 96.27/96.42 Length of proof is 196. Level of proof is 46.
% 96.27/96.42
% 96.27/96.42 ---------------- PROOF ----------------
% 96.27/96.42 % SZS status Theorem
% 96.27/96.42 % SZS output start Refutation
% See solution above
% 96.27/96.42 ------------ end of proof -------------
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Search stopped by max_proofs option.
% 96.27/96.42
% 96.27/96.42
% 96.27/96.42 Search stopped by max_proofs option.
% 96.27/96.42
% 96.27/96.42 ============ end of search ============
% 96.27/96.42
% 96.27/96.42 -------------- statistics -------------
% 96.27/96.42 clauses given 352
% 96.27/96.42 clauses generated 248548
% 96.27/96.42 clauses kept 4441
% 96.27/96.42 clauses forward subsumed 31302
% 96.27/96.42 clauses back subsumed 2936
% 96.27/96.42 Kbytes malloced 4882
% 96.27/96.42
% 96.27/96.42 ----------- times (seconds) -----------
% 96.27/96.42 user CPU time 94.25 (0 hr, 1 min, 34 sec)
% 96.27/96.42 system CPU time 0.01 (0 hr, 0 min, 0 sec)
% 96.27/96.42 wall-clock time 96 (0 hr, 1 min, 36 sec)
% 96.27/96.42
% 96.27/96.42 That finishes the proof of the theorem.
% 96.27/96.42
% 96.27/96.42 Process 32556 finished Wed Jul 27 11:17:44 2022
% 96.27/96.42 Otter interrupted
% 96.27/96.42 PROOF FOUND
%------------------------------------------------------------------------------