The cat needs the squirrel. The cat visits the squirrel. The dog eats the rabbit. The dog is red. The dog needs the rabbit. The rabbit needs the cat. The squirrel visits the cat. If someone eats the rabbit then the rabbit is green. If someone is red and they visit the rabbit then they eat the cat. If someone eats the rabbit and the rabbit needs the dog then the dog visits the cat. If someone eats the rabbit then the rabbit needs the dog. If someone visits the cat then they need the dog. If someone is green then they eat the dog.
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
If someone eats the rabbit then the rabbit is green.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
If someone is red and they visit the rabbit then they eat the cat.
((("someone" "is" "red" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "cat" "+"))
If someone eats the rabbit and the rabbit needs the dog then the dog visits the cat.
((("someone" "eats" "rabbit" "+") ("rabbit" "needs" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If someone eats the rabbit then the rabbit needs the dog.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If someone visits the cat then they need the dog.
((("someone" "visits" "cat" "+")) -> ("someone" "needs" "dog" "+"))
If someone is green then they eat the dog.
((("someone" "is" "green" "+")) -> ("someone" "eats" "dog" "+"))
The cat visits the squirrel.
True
1
proof
[(triple2)]
("cat" "visits" "squirrel" "+")
triple2
The cat does not need the squirrel.
False
1
inv-proof
[(triple1)]
("cat" "needs" "squirrel" "-")
triple1
The rabbit needs the dog.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "needs" "dog" "+")
((triple3) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The squirrel does not need the dog.
False
2
inv-proof
[(((triple7) -> rule5))]
("squirrel" "needs" "dog" "-")
((triple7) -> (rule5 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog visits the cat.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule3))]
("dog" "visits" "cat" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The dog does not visit the cat.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule3))]
("dog" "visits" "cat" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The cat does not eat the dog.
Unknown
inv-rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "eats" "dog" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not need the dog.
Unknown
inv-rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat visits the rabbit.
Unknown
random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "+")
@0: The cat needs the squirrel.[(triple1)] The cat visits the squirrel.[(triple2)] The dog eats the rabbit.[(triple3)] The dog is red.[(triple4)] The dog needs the rabbit.[(triple5)] The rabbit needs the cat.[(triple6)] The squirrel visits the cat.[(triple7)] @1: The rabbit is green.[(((triple3) -> rule1))] The rabbit needs the dog.[(((triple3) -> rule4))] The squirrel needs the dog.[(((triple7) -> rule5))] @2: The dog visits the cat.[(((triple3 ((triple3) -> rule4)) -> rule3))] The rabbit eats the dog.[(((((triple3) -> rule1)) -> rule6))] @3: The dog needs the dog.[(((((triple3 ((triple3) -> rule4)) -> rule3)) -> rule5))]
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple5
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple6
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
((triple3) -> (rule1 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple3) -> (rule4 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
((triple7) -> (rule5 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple3 ((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int3