The cat is round. The cat likes the tiger. The cow likes the cat. The cow needs the squirrel. The squirrel eats the tiger. The squirrel likes the cat. The tiger eats the cow. If something eats the tiger and it likes the tiger then it likes the cow. If something likes the cat then it likes the tiger.
The cat is round.
("cat" "is" "round" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If something eats the tiger and it likes the tiger then it likes the cow.
((("something" "eats" "tiger" "+") ("something" "likes" "tiger" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cat then it likes the tiger.
((("something" "likes" "cat" "+")) -> ("something" "likes" "tiger" "+"))
The cow needs the squirrel.
True
1
proof
[(triple4)]
("cow" "needs" "squirrel" "+")
triple4
The cow does not like the cat.
False
1
inv-proof
[(triple3)]
("cow" "likes" "cat" "-")
triple3
The cow likes the tiger.
True
2
proof
[(((triple3) -> rule2))]
("cow" "likes" "tiger" "+")
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "likes" "tiger" "-")
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The squirrel likes the cow.
True
4
proof
[(((triple5 ((triple6) -> rule2)) -> rule1))]
("squirrel" "likes" "cow" "+")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The squirrel does not like the cow.
False
4
inv-proof
[(((triple5 ((triple6) -> rule2)) -> rule1))]
("squirrel" "likes" "cow" "-")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2
The cat does not like the cow.
Unknown
inv-rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "cow" "-")
The tiger likes the cow.
Unknown
rconc
[@1: The tiger likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "cow" "+")
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The cat is round.[(triple1)] The cat likes the tiger.[(triple2)] The cow likes the cat.[(triple3)] The cow needs the squirrel.[(triple4)] The squirrel eats the tiger.[(triple5)] The squirrel likes the cat.[(triple6)] The tiger eats the cow.[(triple7)] @1: The cow likes the tiger.[(((triple3) -> rule2))] The squirrel likes the tiger.[(((triple6) -> rule2))] @2: The squirrel likes the cow.[(((triple5 ((triple6) -> rule2)) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple6
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple7
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple3) -> (rule2 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((triple6) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int2