The cat is big. The dog is rough. The dog does not like the cat. The mouse is not blue. The mouse is nice. The mouse likes the cat. The mouse visits the cat. If the mouse likes the cat then the cat is not nice. If someone likes the dog then the dog does not eat the mouse. If the dog visits the cat then the dog eats the mouse. If someone is nice and big then they like the cat. Rough people are nice. If someone is nice then they do not like the dog. If the dog is not big and the dog does not like the cat then the dog is young. If someone is rough and they do not like the dog then the dog eats the cat.
The cat is big.
("cat" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog does not like the cat.
("dog" "likes" "cat" "-")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If the mouse likes the cat then the cat is not nice.
((("mouse" "likes" "cat" "+")) -> ("cat" "is" "nice" "-"))
If someone likes the dog then the dog does not eat the mouse.
((("someone" "likes" "dog" "+")) -> ("dog" "eats" "mouse" "-"))
If the dog visits the cat then the dog eats the mouse.
((("dog" "visits" "cat" "+")) -> ("dog" "eats" "mouse" "+"))
If someone is nice and big then they like the cat.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "cat" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they do not like the dog.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "dog" "-"))
If the dog is not big and the dog does not like the cat then the dog is young.
((("dog" "is" "big" "~") ("dog" "likes" "cat" "~")) -> ("dog" "is" "young" "+"))
If someone is rough and they do not like the dog then the dog eats the cat.
((("someone" "is" "rough" "+") ("someone" "likes" "dog" "~")) -> ("dog" "eats" "cat" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The mouse does not like the cat.
False
1
inv-proof
[(triple6)]
("mouse" "likes" "cat" "-")
triple6
The dog is nice.
True
2
proof
[(((triple2) -> rule5))]
("dog" "is" "nice" "+")
((triple2) -> (rule5 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The cat is nice.
False
2
inv-proof
[(((triple6) -> rule1))]
("cat" "is" "nice" "+")
((triple6) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The dog does not like the dog.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("dog" "likes" "dog" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The dog does not like the dog.
("dog" "likes" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog likes the dog.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("dog" "likes" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The dog does not like the dog.
("dog" "likes" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog eats the cat.
True
5
proof
[(((triple2 ((((triple2) -> rule5)) -> rule6)) -> rule8))]
("dog" "eats" "cat" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog does not like the dog.
("dog" "likes" "dog" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The dog does not eat the cat.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule5)) -> rule6)) -> rule8))]
("dog" "eats" "cat" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog does not like the dog.
("dog" "likes" "dog" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "likes" "cat" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "young" "+")
The dog does not eat the mouse.
Unknown
inv-rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "mouse" "-")
The mouse visits the dog.
Unknown
random
[@0: The mouse visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "dog" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The mouse does not eat the dog.
Unknown
inv-random
[@0: The mouse eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "dog" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat is big.[(triple1)] The dog does not like the cat.[(triple3)] The dog is rough.[(triple2)] The mouse is nice.[(triple5)] The mouse is not blue.[(triple4)] The mouse likes the cat.[(triple6)] The mouse visits the cat.[(triple7)] @1: The cat is not nice.[(((triple6) -> rule1))] The dog is nice.[(((triple2) -> rule5))] The mouse does not like the dog.[(((triple5) -> rule6))] @2: The dog does not like the dog.[(((((triple2) -> rule5)) -> rule6))] @3: The dog eats the cat.[(((triple2 ((((triple2) -> rule5)) -> rule6)) -> rule8))]
The cat is big.
("cat" "is" "big" "+")
triple1
The dog does not like the cat.
("dog" "likes" "cat" "-")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse is not blue.
("mouse" "is" "blue" "-")
triple4
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple6
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple7
The cat is not nice.
("cat" "is" "nice" "-")
((triple6) -> (rule1 % int1))
The cat is not nice.
("cat" "is" "nice" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple2) -> (rule5 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
((triple5) -> (rule6 % int1))
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
int1
The dog does not like the dog.
("dog" "likes" "dog" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The dog does not like the dog.
("dog" "likes" "dog" "-")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog does not like the dog.
("dog" "likes" "dog" "-")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3