Equation comparison seems to be missing some matches

[Chris Warburton]

Running QuickSpec on list-full.smt, we get the following:

{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> Integer -> List Integer -> Integer","symbol":"foldl"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"variable","type":"Integer","id":0}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"Integer","id":0}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"variable","type":"List Integer","id":3}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":3}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Integer","symbol":"destructorhead"},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"constant","type":"Integer","symbol":"undefined"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"constant","type":"List Integer","symbol":"undefined"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}},"rhs":{"role":"constant","type":"Nat","symbol":"constructorZ"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"Nat -> Nat","symbol":"destructorp"},"rhs":{"role":"constant","type":"Nat","symbol":"constructorZ"}},"rhs":{"role":"constant","type":"Nat","symbol":"undefined"}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> Integer -> List Integer -> Integer","symbol":"foldl"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> Integer -> List Integer -> Integer","symbol":"foldl"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> Integer -> List Integer -> Integer","symbol":"foldl"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"variable","type":"Integer","id":0}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}},"rhs":{"role":"variable","type":"List Integer","id":5}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"variable","type":"List Integer","id":5}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Integer","symbol":"destructorhead"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"Integer","id":0}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"List Integer","id":3}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":1}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"variable","type":"List Integer","id":3}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Integer","symbol":"destructorhead"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Integer","symbol":"destructorhead"},"rhs":{"role":"variable","type":"List Integer","id":3}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"List Integer","id":3}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"variable","type":"List Integer","id":3}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"Nat -> Nat","symbol":"destructorp"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"Nat -> Nat","symbol":"destructorp"},"rhs":{"role":"application","lhs":{"role":"constant","type":"Nat -> Nat","symbol":"constructorS"},"rhs":{"role":"variable","type":"Nat","id":6}}},"rhs":{"role":"variable","type":"Nat","id":6}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"Nat -> Nat","symbol":"constructorS"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> Nat","symbol":"length"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"destructortail"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"variable","type":"List Integer","id":4}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"variable","type":"Integer -> Integer","id":9}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":4}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}},"rhs":{"role":"variable","type":"Integer","id":1}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> Integer -> List Integer -> Integer","symbol":"foldl"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":1}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":4}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"variable","type":"List Integer","id":4}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"List Integer","id":3}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer) -> List Integer -> List Integer","symbol":"map"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"(Integer -> Integer -> Integer) -> List Integer -> Integer -> Integer","symbol":"foldr"},"rhs":{"role":"variable","type":"Integer -> Integer -> Integer","id":12}},"rhs":{"role":"variable","type":"List Integer","id":3}},"rhs":{"role":"variable","type":"Integer","id":0}}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer -> List Integer","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"variable","type":"List Integer","id":3}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"constant","type":"List Integer","symbol":"constructorNil"}}},"rhs":{"role":"application","lhs":{"role":"constant","type":"List Integer -> List Integer","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"constant","type":"Integer -> List Integer -> List Integer","symbol":"constructorCons"},"rhs":{"role":"variable","type":"Integer","id":0}},"rhs":{"role":"variable","type":"List Integer","id":3}}}}

The ground-truth theorems for list-full.smt2 are the following:

{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List t)","role":"variable","id":0}},"rhs":{"type":"unknown","role":"constant","symbol":"constructorNil"}},"rhs":{"type":"(List t)","role":"variable","id":0}}
{"relation":"~=","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"type":"(List t)","role":"variable","id":0}}},"rhs":{"type":"(List t)","role":"variable","id":0}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"map"},"rhs":{"type":"(=> i o)","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"type":"(List i)","role":"variable","id":0}}},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"map"},"rhs":{"type":"(=> i o)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":0}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldl"},"rhs":{"type":"(=> o (=> i o))","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldl"},"rhs":{"type":"(=> o (=> i o))","role":"variable","id":0}},"rhs":{"type":"o","role":"variable","id":0}},"rhs":{"type":"(List o)","role":"variable","id":0}}},"rhs":{"type":"(List i)","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldl"},"rhs":{"type":"(=> o (=> i o))","role":"variable","id":0}},"rhs":{"type":"o","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List o)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":0}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"length"},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"type":"(List t)","role":"variable","id":0}}},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"length"},"rhs":{"type":"(List t)","role":"variable","id":0}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List t)","role":"variable","id":0}},"rhs":{"type":"(List t)","role":"variable","id":1}}},"rhs":{"type":"(List t)","role":"variable","id":2}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List t)","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List t)","role":"variable","id":1}},"rhs":{"type":"(List t)","role":"variable","id":2}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"type":"(List t)","role":"variable","id":0}}},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"type":"(List t)","role":"variable","id":1}}},"rhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"reverse"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List t)","role":"variable","id":1}},"rhs":{"type":"(List t)","role":"variable","id":0}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"map"},"rhs":{"type":"(=> i o)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":0}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"map"},"rhs":{"type":"(=> i o)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":1}}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"map"},"rhs":{"type":"(=> i o)","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List i)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":1}}}}
{"relation":"~=","lhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldr"},"rhs":{"type":"(=> i (=> o o))","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"append"},"rhs":{"type":"(List i)","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":1}}},"rhs":{"type":"o","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldr"},"rhs":{"type":"(=> i (=> o o))","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":0}},"rhs":{"role":"application","lhs":{"role":"application","lhs":{"role":"application","lhs":{"type":"unknown","role":"constant","symbol":"foldr"},"rhs":{"type":"(=> i (=> o o))","role":"variable","id":0}},"rhs":{"type":"(List i)","role":"variable","id":1}},"rhs":{"type":"o","role":"variable","id":0}}}}

When pretty-printed, these are the found ones:

((foldl iii12) i0) constructorNil ~= i0
((foldr iii12) constructorNil) i0 ~= i0
(append li3) constructorNil ~= li3
(map ii9) constructorNil ~= constructorNil
(append constructorNil) li3 ~= li3
destructorhead constructorNil ~= undefined
reverse constructorNil ~= constructorNil
destructortail constructorNil ~= undefined
length constructorNil ~= constructorZ
destructorp constructorZ ~= undefined
((foldl iii12) (((foldl iii12) i0) li3)) li4 ~= ((foldl iii12) i0) ((append li3) li4)
((foldr iii12) ((append li3) li4)) i0 ~= ((foldr iii12) li3) (((foldr iii12) li4) i0)
(append ((constructorCons i0) li3)) li4 ~= (constructorCons i0) ((append li3) li4)
(append ((append li3) li4)) li5 ~= (append li3) ((append li4) li5)
destructorhead ((constructorCons i0) li3) ~= i0
destructortail ((constructorCons i0) li3) ~= li3
length ((constructorCons i1) li3) ~= length ((constructorCons i0) li3)
length ((append li4) li3) ~= length ((append li3) li4)
length ((map ii9) li3) ~= length li3
(map ii9) (reverse li3) ~= reverse ((map ii9) li3)
(map ii9) (destructortail li3) ~= destructortail ((map ii9) li3)
destructorhead ((append li3) li3) ~= destructorhead li3
reverse (reverse li3) ~= li3
length (reverse li3) ~= length li3
destructorp (length li3) ~= length (destructortail li3)
destructorp (constructorS n6) ~= n6
constructorS (length li3) ~= length ((constructorCons i0) li3)
(append (destructortail li3)) li3 ~= destructortail ((append li3) li3)
(append ((map ii9) li3)) ((map ii9) li4) ~= (map ii9) ((append li3) li4)
((foldr iii12) ((constructorCons i0) constructorNil)) i1 ~= ((foldl iii12) i0) ((constructorCons i1) constructorNil)
(append (reverse li3)) (reverse li4) ~= reverse ((append li4) li3)
(map ((foldr iii12) constructorNil)) li3 ~= li3
reverse ((constructorCons i0) constructorNil) ~= (constructorCons i0) constructorNil
(map ((foldr iii12) li3)) ((constructorCons i0) constructorNil) ~= (constructorCons (((foldr iii12) li3) i0)) constructorNil
(append (reverse li3)) ((constructorCons i0) constructorNil) ~= reverse ((constructorCons i0) li3)

These are the ground truths:

(append l0) constructorNil ~= l0
reverse (reverse l0) ~= l0
(map 0) (reverse l0) ~= reverse ((map 0) l0)
((foldl 0) (((foldl 0) 0) l0)) l0 ~= ((foldl 0) 0) ((append l0) l0)
length (reverse l0) ~= length l0
(append ((append l0) l1)) l2 ~= (append l0) ((append l1) l2)
(append (reverse l0)) (reverse l1) ~= reverse ((append l1) l0)
(append ((map 0) l0)) ((map 0) l1) ~= (map 0) ((append l0) l1)
((foldr 0) ((append l0) l1)) 0 ~= ((foldr 0) l0) (((foldr 0) l1) 0)

It looks like (almost?) all of the ground truths appear, just with
different variable names. Yet the precision and recall for this come out
at 0 and 0.