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