The cat is young. The dog needs the cat. The rabbit sees the dog. If someone needs the cat then the cat visits the dog. If someone sees the cat and the cat is blue then they need the rabbit. If the cat is young and the cat needs the dog then the dog visits the rabbit. If the cat visits the dog then the cat needs the dog. If the rabbit is red and the rabbit visits the dog then the dog sees the rabbit. If someone visits the rabbit and the rabbit needs the dog then the dog visits the cat.
The cat is young.
("cat" "is" "young" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone needs the cat then the cat visits the dog.
((("someone" "needs" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If someone sees the cat and the cat is blue then they need the rabbit.
((("someone" "sees" "cat" "+") ("cat" "is" "blue" "+")) -> ("someone" "needs" "rabbit" "+"))
If the cat is young and the cat needs the dog then the dog visits the rabbit.
((("cat" "is" "young" "+") ("cat" "needs" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If the cat visits the dog then the cat needs the dog.
((("cat" "visits" "dog" "+")) -> ("cat" "needs" "dog" "+"))
If the rabbit is red and the rabbit visits the dog then the dog sees the rabbit.
((("rabbit" "is" "red" "+") ("rabbit" "visits" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
If someone visits the rabbit and the rabbit needs the dog then the dog visits the cat.
((("someone" "visits" "rabbit" "+") ("rabbit" "needs" "dog" "+")) -> ("dog" "visits" "cat" "+"))
The dog needs the cat.
True
1
proof
[(triple2)]
("dog" "needs" "cat" "+")
triple2
The dog does not need the cat.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cat" "-")
triple2
The cat visits the dog.
True
2
proof
[(((triple2) -> rule1))]
("cat" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "visits" "dog" "-")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat needs the dog.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("cat" "needs" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat does not need the dog.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("cat" "needs" "dog" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog visits the rabbit.
True
5
proof
[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule3))]
("dog" "visits" "rabbit" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The dog does not visit the rabbit.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule3))]
("dog" "visits" "rabbit" "-")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The dog visits the cat.
Unknown
rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "cat" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The dog sees the rabbit.
Unknown
rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "rabbit" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The cat is young.[(triple1)] The dog needs the cat.[(triple2)] The rabbit sees the dog.[(triple3)] @1: The cat visits the dog.[(((triple2) -> rule1))] @2: The cat needs the dog.[(((((triple2) -> rule1)) -> rule4))] @3: The dog visits the rabbit.[(((triple1 ((((triple2) -> rule1)) -> rule4)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple2) -> (rule1 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple1 ((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3