The dog is kind. The dog is young. The dog visits the mouse. The mouse eats the dog. The mouse is rough. The mouse likes the dog. The mouse visits the dog. If something eats the mouse then it likes the mouse. If something visits the mouse and the mouse eats the dog then the dog eats the mouse. If something is young then it likes the dog. If something likes the dog and it is cold then the dog is kind. If the dog is blue then the dog eats the mouse. If something likes the dog then the dog eats the mouse.
The dog is kind.
("dog" "is" "kind" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something eats the mouse then it likes the mouse.
((("something" "eats" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the mouse and the mouse eats the dog then the dog eats the mouse.
((("something" "visits" "mouse" "+") ("mouse" "eats" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something is young then it likes the dog.
((("something" "is" "young" "+")) -> ("something" "likes" "dog" "+"))
If something likes the dog and it is cold then the dog is kind.
((("something" "likes" "dog" "+") ("something" "is" "cold" "+")) -> ("dog" "is" "kind" "+"))
If the dog is blue then the dog eats the mouse.
((("dog" "is" "blue" "+")) -> ("dog" "eats" "mouse" "+"))
If something likes the dog then the dog eats the mouse.
((("something" "likes" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
The dog is young.
True
1
proof
[(triple2)]
("dog" "is" "young" "+")
triple2
The dog does not visit the mouse.
False
1
inv-proof
[(triple3)]
("dog" "visits" "mouse" "-")
triple3
The dog eats the mouse.
True
2
proof
[(((triple6) -> rule6) OR ((triple3 triple4) -> rule2) OR ((((triple2) -> rule3)) -> rule6))]
("dog" "eats" "mouse" "+")
((triple6) -> (rule6 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple3 triple4) -> (rule2 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not like the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "likes" "dog" "-")
((triple2) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog likes the mouse.
True
3
proof
[(((((triple6) -> rule6)) -> rule1) OR ((((triple3 triple4) -> rule2)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("dog" "likes" "mouse" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((triple3 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog does not like the mouse.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1) OR ((((triple3 triple4) -> rule2)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
("dog" "likes" "mouse" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((triple3 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The dog is kind.[(triple1)] The dog is young.[(triple2)] The dog visits the mouse.[(triple3)] The mouse eats the dog.[(triple4)] The mouse is rough.[(triple5)] The mouse likes the dog.[(triple6)] The mouse visits the dog.[(triple7)] @1: The dog eats the mouse.[(((triple6) -> rule6) OR ((triple3 triple4) -> rule2) OR ((((triple2) -> rule3)) -> rule6))] The dog likes the dog.[(((triple2) -> rule3))] @2: The dog likes the mouse.[(((((triple6) -> rule6)) -> rule1) OR ((((triple3 triple4) -> rule2)) -> rule1) OR ((((((triple2) -> rule3)) -> rule6)) -> rule1))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple6) -> (rule6 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((triple3 triple4) -> (rule2 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple2) -> (rule3 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((triple3 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3