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