The cat sees the dog. The cat does not see the rabbit. The dog eats the cat. The dog is big. The dog is cold. The dog is green. The dog sees the cat. The dog does not see the rabbit. The dog visits the cat. The rabbit eats the cat. The rabbit eats the dog. The rabbit is cold. The rabbit is green. The rabbit is young. The rabbit sees the dog. If someone eats the dog and the dog is young then they visit the dog. If someone is kind and they see the dog then the dog visits the rabbit. If the dog is big and the dog visits the cat then the dog visits the rabbit. If the rabbit eats the dog and the dog is not cold then the dog eats the cat. If someone eats the rabbit and they see the cat then they are young. If someone is big and they see the cat then they eat the rabbit.
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
The dog visits the cat.
("dog" "visits" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone eats the dog and the dog is young then they visit the dog.
((("someone" "eats" "dog" "+") ("dog" "is" "young" "+")) -> ("someone" "visits" "dog" "+"))
If someone is kind and they see the dog then the dog visits the rabbit.
((("someone" "is" "kind" "+") ("someone" "sees" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If the dog is big and the dog visits the cat then the dog visits the rabbit.
((("dog" "is" "big" "+") ("dog" "visits" "cat" "+")) -> ("dog" "visits" "rabbit" "+"))
If the rabbit eats the dog and the dog is not cold then the dog eats the cat.
((("rabbit" "eats" "dog" "+") ("dog" "is" "cold" "~")) -> ("dog" "eats" "cat" "+"))
If someone eats the rabbit and they see the cat then they are young.
((("someone" "eats" "rabbit" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "young" "+"))
If someone is big and they see the cat then they eat the rabbit.
((("someone" "is" "big" "+") ("someone" "sees" "cat" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit is young.
True
1
proof
[(triple14)]
("rabbit" "is" "young" "+")
triple14
The dog does not eat the cat.
False
1
inv-proof
[(triple3)]
("dog" "eats" "cat" "-")
triple3
The dog visits the rabbit.
True
3
proof
[(((triple4 triple9) -> rule3))]
("dog" "visits" "rabbit" "+")
((triple4 triple9) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The dog does not visit the rabbit.
False
3
inv-proof
[(((triple4 triple9) -> rule3))]
("dog" "visits" "rabbit" "-")
((triple4 triple9) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The dog is young.
True
5
proof
[(((((triple4 triple7) -> rule6) triple7) -> rule5))]
("dog" "is" "young" "+")
((((triple4 triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog is not young.
False
5
inv-proof
[(((((triple4 triple7) -> rule6) triple7) -> rule5))]
("dog" "is" "young" "-")
((((triple4 triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit visits the dog.
True
7
proof
[(((triple11 ((((triple4 triple7) -> rule6) triple7) -> rule5)) -> rule1))]
("rabbit" "visits" "dog" "+")
((triple11 ((((triple4 triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The rabbit does not visit the dog.
False
7
inv-proof
[(((triple11 ((((triple4 triple7) -> rule6) triple7) -> rule5)) -> rule1))]
("rabbit" "visits" "dog" "-")
((triple11 ((((triple4 triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "young" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The cat does not visit the dog.
Unknown
inv-rconc
[@1: The cat visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "dog" "-")
The cat eats the rabbit.
Unknown
rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "eats" "rabbit" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat does not visit the rabbit.
Unknown
inv-random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
@0: The cat does not see the rabbit.[(triple2)] The cat sees the dog.[(triple1)] The dog does not see the rabbit.[(triple8)] The dog eats the cat.[(triple3)] The dog is big.[(triple4)] The dog is cold.[(triple5)] The dog is green.[(triple6)] The dog sees the cat.[(triple7)] The dog visits the cat.[(triple9)] The rabbit eats the cat.[(triple10)] The rabbit eats the dog.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is green.[(triple13)] The rabbit is young.[(triple14)] The rabbit sees the dog.[(triple15)] @1: The dog eats the rabbit.[(((triple4 triple7) -> rule6))] The dog visits the rabbit.[(((triple4 triple9) -> rule3))] @2: The dog is young.[(((((triple4 triple7) -> rule6) triple7) -> rule5))] @3: The rabbit visits the dog.[(((triple11 ((((triple4 triple7) -> rule6) triple7) -> rule5)) -> rule1))]
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
triple8
The dog eats the cat.
("dog" "eats" "cat" "+")
triple3
The dog is big.
("dog" "is" "big" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog sees the cat.
("dog" "sees" "cat" "+")
triple7
The dog visits the cat.
("dog" "visits" "cat" "+")
triple9
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple10
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is green.
("rabbit" "is" "green" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple15
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple4 triple7) -> (rule6 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple4 triple9) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple4 triple7) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple11 ((((triple4 triple7) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3