The dog eats the rabbit. The dog eats the squirrel. The dog is not round. The dog needs the rabbit. The dog does not visit the tiger. The rabbit needs the dog. The rabbit needs the squirrel. The rabbit visits the squirrel. The squirrel eats the dog. The tiger needs the dog. The tiger does not need the rabbit. The tiger visits the rabbit. If the tiger does not need the dog and the dog does not visit the tiger then the tiger is young. If someone eats the tiger and the tiger eats the dog then the dog is round. If the dog needs the rabbit then the rabbit is not cold. If someone eats the dog then the dog needs the squirrel. If someone visits the dog then the dog is not young. If someone needs the squirrel and they are not round then they do not visit the dog.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is not round.
("dog" "is" "round" "-")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the tiger does not need the dog and the dog does not visit the tiger then the tiger is young.
((("tiger" "needs" "dog" "~") ("dog" "visits" "tiger" "~")) -> ("tiger" "is" "young" "+"))
If someone eats the tiger and the tiger eats the dog then the dog is round.
((("someone" "eats" "tiger" "+") ("tiger" "eats" "dog" "+")) -> ("dog" "is" "round" "+"))
If the dog needs the rabbit then the rabbit is not cold.
((("dog" "needs" "rabbit" "+")) -> ("rabbit" "is" "cold" "-"))
If someone eats the dog then the dog needs the squirrel.
((("someone" "eats" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
If someone visits the dog then the dog is not young.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "young" "-"))
If someone needs the squirrel and they are not round then they do not visit the dog.
((("someone" "needs" "squirrel" "+") ("someone" "is" "round" "~")) -> ("someone" "visits" "dog" "-"))
The tiger visits the rabbit.
True
1
proof
[(triple12)]
("tiger" "visits" "rabbit" "+")
triple12
The tiger does not need the dog.
False
1
inv-proof
[(triple10)]
("tiger" "needs" "dog" "-")
triple10
The rabbit is not cold.
True
2
proof
[(((triple4) -> rule3))]
("rabbit" "is" "cold" "-")
((triple4) -> (rule3 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The dog does not need the squirrel.
False
2
inv-proof
[(((triple9) -> rule4))]
("dog" "needs" "squirrel" "-")
((triple9) -> (rule4 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The dog does not visit the dog.
True
4
proof
[(((((triple9) -> rule4) triple3) -> rule6))]
("dog" "visits" "dog" "-")
((((triple9) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The dog visits the dog.
False
4
inv-proof
[(((((triple9) -> rule4) triple3) -> rule6))]
("dog" "visits" "dog" "+")
((((triple9) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "young" "-")
The rabbit visits the tiger.
Unknown
random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The tiger does not visit the dog.
Unknown
inv-random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The dog does not visit the tiger.[(triple5)] The dog eats the rabbit.[(triple1)] The dog eats the squirrel.[(triple2)] The dog is not round.[(triple3)] The dog needs the rabbit.[(triple4)] The rabbit needs the dog.[(triple6)] The rabbit needs the squirrel.[(triple7)] The rabbit visits the squirrel.[(triple8)] The squirrel eats the dog.[(triple9)] The tiger does not need the rabbit.[(triple11)] The tiger needs the dog.[(triple10)] The tiger visits the rabbit.[(triple12)] @1: The dog needs the squirrel.[(((triple9) -> rule4))] The rabbit is not cold.[(((triple4) -> rule3))] @2: The dog does not visit the dog.[(((((triple9) -> rule4) triple3) -> rule6))]
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
triple5
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple2
The dog is not round.
("dog" "is" "round" "-")
triple3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple4
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple8
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
triple9
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple11
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple10
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple12
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
((triple9) -> (rule4 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The rabbit is not cold.
("rabbit" "is" "cold" "-")
((triple4) -> (rule3 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The dog does not visit the dog.
("dog" "visits" "dog" "-")
((((triple9) -> (rule4 % int2)) triple3) -> (rule6 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int2