WATCH: 0.00 CPU 0.01 WC

/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p is a Theorem
Start of proof for /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p
%-----------------------------------------------------
fof(pel52,conjecture,? [_17801] : ! [_17809] : (? [_17817] : ! [_17825] : (_17825 = _17817 <=> big_f(_17825, _17809)) <=> _17809 = _17801),file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p',pel52)).
fof(pel52_1,axiom,? [_18140, _18143] : ! [_18151, _18154] : (_18154 = _18143 & _18140 = _18151 <=> big_f(_18151, _18154)),file('/CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p',pel52_1)).

cnf(1, plain, [-(8 ^ [_6595, _5410]), 6 ^ [_6595, _5410] = _6595], clausify(pel52)).
cnf(2, plain, [-(8 ^ [_6595, _5410]), -(big_f(6 ^ [_6595, _5410], 3 ^ [_5410]))], clausify(pel52)).
cnf(3, plain, [-(7 ^ [_6595, _5410]), big_f(6 ^ [_6595, _5410], 3 ^ [_5410])], clausify(pel52)).
cnf(4, plain, [-(7 ^ [_6595, _5410]), -(6 ^ [_6595, _5410] = _6595)], clausify(pel52)).
cnf(5, plain, [-(9 ^ [_5410]), 7 ^ [_6595, _5410], 8 ^ [_6595, _5410]], clausify(pel52)).
cnf(6, plain, [-(9 ^ [_5410]), -(3 ^ [_5410] = _5410)], clausify(pel52)).
cnf(7, plain, [-(5 ^ [_5410]), -(_6670 = 4 ^ [_5410]), big_f(_6670, 3 ^ [_5410])], clausify(pel52)).
cnf(8, plain, [-(5 ^ [_5410]), _6670 = 4 ^ [_5410], -(big_f(_6670, 3 ^ [_5410]))], clausify(pel52)).
cnf(9, plain, [-(5 ^ [_5410]), 3 ^ [_5410] = _5410], clausify(pel52)).
cnf(10, plain, [9 ^ [_5410], 5 ^ [_5410]], clausify(pel52)).
cnf(11, plain, [-(_6272 = 2 ^ []), big_f(_6267, _6272)], clausify(pel52_1)).
cnf(12, plain, [-(1 ^ [] = _6267), big_f(_6267, _6272)], clausify(pel52_1)).
cnf(13, plain, [-(big_f(_6267, _6272)), _6272 = 2 ^ [], 1 ^ [] = _6267], clausify(pel52_1)).
cnf(14, plain, [-(_3307 = _3307)], theory(equality)).
cnf(15, plain, [_3460 = _3505, -(_3505 = _3460)], theory(equality)).

cnf('1',plain,[9 ^ [2 ^ []], 5 ^ [2 ^ []]],start(10,bind([[_5410], [2 ^ []]]))).
cnf('1.1',plain,[-(9 ^ [2 ^ []]), 7 ^ [1 ^ [], 2 ^ []], 8 ^ [1 ^ [], 2 ^ []]],extension(5,bind([[_6595, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.1.1',plain,[-(7 ^ [1 ^ [], 2 ^ []]), big_f(6 ^ [1 ^ [], 2 ^ []], 3 ^ [2 ^ []])],extension(3,bind([[_6595, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.1.1.1',plain,[-(big_f(6 ^ [1 ^ [], 2 ^ []], 3 ^ [2 ^ []])), 3 ^ [2 ^ []] = 2 ^ [], 1 ^ [] = 6 ^ [1 ^ [], 2 ^ []]],extension(13,bind([[_6272, _6267], [3 ^ [2 ^ []], 6 ^ [1 ^ [], 2 ^ []]]]))).
cnf('1.1.1.1.1',plain,[-(3 ^ [2 ^ []] = 2 ^ []), -(9 ^ [2 ^ []])],extension(6,bind([[_5410], [2 ^ []]]))).
cnf('1.1.1.1.1.1',plain,[9 ^ [2 ^ []]],reduction('1')).
cnf('1.1.1.1.2',plain,[-(1 ^ [] = 6 ^ [1 ^ [], 2 ^ []]), 6 ^ [1 ^ [], 2 ^ []] = 1 ^ []],extension(15,bind([[_3460, _3505], [6 ^ [1 ^ [], 2 ^ []], 1 ^ []]]))).
cnf('1.1.1.1.2.1',plain,[-(6 ^ [1 ^ [], 2 ^ []] = 1 ^ []), -(7 ^ [1 ^ [], 2 ^ []])],extension(4,bind([[_6595, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.1.1.1.2.1.1',plain,[7 ^ [1 ^ [], 2 ^ []]],reduction('1.1')).
cnf('1.1.2',plain,[-(8 ^ [1 ^ [], 2 ^ []]), 6 ^ [1 ^ [], 2 ^ []] = 1 ^ []],extension(1,bind([[_5410, _6595], [2 ^ [], 1 ^ []]]))).
cnf('1.1.2.1',plain,[-(6 ^ [1 ^ [], 2 ^ []] = 1 ^ []), 1 ^ [] = 6 ^ [1 ^ [], 2 ^ []]],extension(15,bind([[_3460, _3505], [1 ^ [], 6 ^ [1 ^ [], 2 ^ []]]]))).
cnf('1.1.2.1.1',plain,[-(1 ^ [] = 6 ^ [1 ^ [], 2 ^ []]), big_f(6 ^ [1 ^ [], 2 ^ []], 3 ^ [2 ^ []])],extension(12,bind([[_6267, _6272], [6 ^ [1 ^ [], 2 ^ []], 3 ^ [2 ^ []]]]))).
cnf('1.1.2.1.1.1',plain,[-(big_f(6 ^ [1 ^ [], 2 ^ []], 3 ^ [2 ^ []])), -(8 ^ [1 ^ [], 2 ^ []])],extension(2,bind([[_6595, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.1.2.1.1.1.1',plain,[8 ^ [1 ^ [], 2 ^ []]],reduction('1.1')).
cnf('1.2',plain,[-(5 ^ [2 ^ []]), -(1 ^ [] = 4 ^ [2 ^ []]), big_f(1 ^ [], 3 ^ [2 ^ []])],extension(7,bind([[_6670, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.2.1',plain,[1 ^ [] = 4 ^ [2 ^ []], -(5 ^ [2 ^ []]), -(big_f(1 ^ [], 3 ^ [2 ^ []]))],extension(8,bind([[_6670, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.2.1.1',plain,[5 ^ [2 ^ []]],reduction('1')).
cnf('1.2.1.2',plain,[big_f(1 ^ [], 3 ^ [2 ^ []]), -(3 ^ [2 ^ []] = 2 ^ [])],extension(11,bind([[_6267, _6272], [1 ^ [], 3 ^ [2 ^ []]]]))).
cnf('1.2.1.2.1',plain,[3 ^ [2 ^ []] = 2 ^ [], -(5 ^ [2 ^ []])],extension(9,bind([[_5410], [2 ^ []]]))).
cnf('1.2.1.2.1.1',plain,[5 ^ [2 ^ []]],lemmata('1.2.1')).
cnf('1.2.2',plain,[-(big_f(1 ^ [], 3 ^ [2 ^ []])), -(5 ^ [2 ^ []]), 1 ^ [] = 4 ^ [2 ^ []]],extension(8,bind([[_6670, _5410], [1 ^ [], 2 ^ []]]))).
cnf('1.2.2.1',plain,[5 ^ [2 ^ []]],reduction('1')).
cnf('1.2.2.2',plain,[-(1 ^ [] = 4 ^ [2 ^ []]), big_f(4 ^ [2 ^ []], 3 ^ [2 ^ []])],extension(12,bind([[_6267, _6272], [4 ^ [2 ^ []], 3 ^ [2 ^ []]]]))).
cnf('1.2.2.2.1',plain,[-(big_f(4 ^ [2 ^ []], 3 ^ [2 ^ []])), -(5 ^ [2 ^ []]), 4 ^ [2 ^ []] = 4 ^ [2 ^ []]],extension(8,bind([[_6670, _5410], [4 ^ [2 ^ []], 2 ^ []]]))).
cnf('1.2.2.2.1.1',plain,[5 ^ [2 ^ []]],lemmata('1.2.2')).
cnf('1.2.2.2.1.2',plain,[-(4 ^ [2 ^ []] = 4 ^ [2 ^ []])],extension(14,bind([[_3307], [4 ^ [2 ^ []]]]))).
%-----------------------------------------------------
End of proof for /CW/home-0/sutcliff/CASC/23/Problems/FEQ/FEQ005.p

WATCH: 0.08 CPU 1.07 WC

FINAL WATCH: 0.08 CPU 1.07 WC