The dog eats the squirrel. The dog is red. The dog needs the rabbit. The dog sees the rabbit. The rabbit is not rough. The rabbit needs the dog. The rabbit sees the squirrel. The squirrel eats the rabbit. The squirrel is big. The squirrel does not see the rabbit. If something sees the squirrel then it does not need the rabbit. If something is big then it eats the rabbit. If something is green and it sees the squirrel then it does not need the dog.
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
If something sees the squirrel then it does not need the rabbit.
((("something" "sees" "squirrel" "+")) -> ("something" "needs" "rabbit" "-"))
If something is big then it eats the rabbit.
((("something" "is" "big" "+")) -> ("something" "eats" "rabbit" "+"))
If something is green and it sees the squirrel then it does not need the dog.
((("something" "is" "green" "+") ("something" "sees" "squirrel" "+")) -> ("something" "needs" "dog" "-"))
The rabbit needs the dog.
True
1
proof
[(triple6)]
("rabbit" "needs" "dog" "+")
triple6
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule2))]
("squirrel" "eats" "rabbit" "-")
triple8
((triple9) -> (rule2 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The rabbit does not need the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The rabbit needs the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The dog eats the squirrel.[(triple1)] The dog is red.[(triple2)] The dog needs the rabbit.[(triple3)] The dog sees the rabbit.[(triple4)] The rabbit is not rough.[(triple5)] The rabbit needs the dog.[(triple6)] The rabbit sees the squirrel.[(triple7)] The squirrel does not see the rabbit.[(triple10)] The squirrel eats the rabbit.[(triple8 OR ((triple9) -> rule2))] The squirrel is big.[(triple9)] @1: The rabbit does not need the rabbit.[(((triple7) -> rule1))]
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple5
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple7
The squirrel does not see the rabbit.
("squirrel" "sees" "rabbit" "-")
triple10
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple8
((triple9) -> (rule2 % int1))
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit does not need the rabbit.
("rabbit" "needs" "rabbit" "-")
int1