WATCH: 0.00 CPU 0.01 WC

/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p is a Theorem
Start of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p
%-----------------------------------------------------
fof(thm147,conjecture,~ (! [_7242, _7245] : (~ a_truth(_7242) ; a_truth(_7245) ; ~ a_truth(implies(_7242, _7245))) & ! [_7242, _7245] : a_truth(implies(_7242, implies(_7245, _7242))) & ? [_7315] : ~ a_truth(implies(_7315, _7315)) & ! [_7242, _7245] : a_truth(implies(implies(not _7242, not _7245), implies(_7245, _7242))) & ! [_7242, _7245, _7388] : a_truth(implies(implies(_7242, implies(_7245, _7388)), implies(implies(_7242, _7245), implies(_7242, _7388))))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p',thm147)).

cnf(1, plain, [-(a_truth(implies(_3528, implies(_3572, _3528))))], clausify(thm147)).
cnf(2, plain, [a_truth(implies(1 ^ [], 1 ^ []))], clausify(thm147)).
cnf(3, plain, [-(a_truth(implies(implies(_4164, implies(_4225, _4285)), implies(implies(_4164, _4225), implies(_4164, _4285)))))], clausify(thm147)).
cnf(4, plain, [a_truth(_3192), -(a_truth(_3247)), a_truth(implies(_3192, _3247))], clausify(thm147)).

cnf('1',plain,[a_truth(implies(1 ^ [], 1 ^ []))],start(2)).
cnf('1.1',plain,[-(a_truth(implies(1 ^ [], 1 ^ []))), a_truth(implies(1 ^ [], implies(_5278, 1 ^ []))), a_truth(implies(implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ [])))],extension(4,bind([[_3192, _3247], [implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ [])]]))).
cnf('1.1.1',plain,[-(a_truth(implies(1 ^ [], implies(_5278, 1 ^ []))))],extension(1,bind([[_3572, _3528], [_5278, 1 ^ []]]))).
cnf('1.1.2',plain,[-(a_truth(implies(implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ [])))), a_truth(implies(1 ^ [], implies(implies(_5278, 1 ^ []), 1 ^ []))), a_truth(implies(implies(1 ^ [], implies(implies(_5278, 1 ^ []), 1 ^ [])), implies(implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ []))))],extension(4,bind([[_3192, _3247], [implies(1 ^ [], implies(implies(_5278, 1 ^ []), 1 ^ [])), implies(implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ []))]]))).
cnf('1.1.2.1',plain,[-(a_truth(implies(1 ^ [], implies(implies(_5278, 1 ^ []), 1 ^ []))))],extension(1,bind([[_3572, _3528], [implies(_5278, 1 ^ []), 1 ^ []]]))).
cnf('1.1.2.2',plain,[-(a_truth(implies(implies(1 ^ [], implies(implies(_5278, 1 ^ []), 1 ^ [])), implies(implies(1 ^ [], implies(_5278, 1 ^ [])), implies(1 ^ [], 1 ^ [])))))],extension(3,bind([[_4225, _4164, _4285], [implies(_5278, 1 ^ []), 1 ^ [], 1 ^ []]]))).
%-----------------------------------------------------
End of proof for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p

WATCH: 0.07 CPU 1.06 WC

FINAL WATCH: 0.07 CPU 1.06 WC