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