The rabbit eats the squirrel. The squirrel chases the rabbit. If something eats the squirrel and the squirrel likes the rabbit then the squirrel eats the rabbit. If something eats the squirrel then the squirrel likes the rabbit. If something eats the rabbit and it likes the rabbit then it does not chase the squirrel.
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
If something eats the squirrel and the squirrel likes the rabbit then the squirrel eats the rabbit.
((("something" "eats" "squirrel" "+") ("squirrel" "likes" "rabbit" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If something eats the squirrel then the squirrel likes the rabbit.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If something eats the rabbit and it likes the rabbit then it does not chase the squirrel.
((("something" "eats" "rabbit" "+") ("something" "likes" "rabbit" "+")) -> ("something" "chases" "squirrel" "-"))
The rabbit eats the squirrel.
True
1
proof
[(triple1)]
("rabbit" "eats" "squirrel" "+")
triple1
The squirrel does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "rabbit" "-")
triple2
The squirrel likes the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule2))]
("squirrel" "likes" "rabbit" "-")
((triple1) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel eats the rabbit.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("squirrel" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel does not eat the rabbit.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("squirrel" "eats" "rabbit" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel does not chase the squirrel.
True
7
proof
[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("squirrel" "chases" "squirrel" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The squirrel chases the squirrel.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
("squirrel" "chases" "squirrel" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The rabbit eats the squirrel.[(triple1)] The squirrel chases the rabbit.[(triple2)] @1: The squirrel likes the rabbit.[(((triple1) -> rule2))] @2: The squirrel eats the rabbit.[(((triple1 ((triple1) -> rule2)) -> rule1))] @3: The squirrel does not chase the squirrel.[(((((triple1 ((triple1) -> rule2)) -> rule1) ((triple1) -> rule2)) -> rule3))]
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((triple1) -> (rule2 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int2
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple1) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel does not chase the squirrel.
("squirrel" "chases" "squirrel" "-")
int1
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int2
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int3