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