The dog chases the mouse. The mouse is young. The mouse likes the dog. If something is round and rough then it is young. If something visits the dog then the dog is rough. If the dog chases the mouse then the dog likes the mouse. If something likes the mouse and the mouse likes the dog then it chases the mouse. If something chases the mouse then the mouse is round. If the dog likes the mouse then the mouse visits the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If something is round and rough then it is young.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something visits the dog then the dog is rough.
((("something" "visits" "dog" "+")) -> ("dog" "is" "rough" "+"))
If the dog chases the mouse then the dog likes the mouse.
((("dog" "chases" "mouse" "+")) -> ("dog" "likes" "mouse" "+"))
If something likes the mouse and the mouse likes the dog then it chases the mouse.
((("something" "likes" "mouse" "+") ("mouse" "likes" "dog" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the mouse then the mouse is round.
((("something" "chases" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If the dog likes the mouse then the mouse visits the dog.
((("dog" "likes" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
The dog chases the mouse.
True
1
proof
[(triple1)]
("dog" "chases" "mouse" "+")
triple1
The dog does not chase the mouse.
False
1
inv-proof
[(triple1)]
("dog" "chases" "mouse" "-")
triple1
The mouse is round.
True
2
proof
[(((triple1) -> rule5))]
("mouse" "is" "round" "+")
((triple1) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("mouse" "is" "round" "-")
((triple1) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the dog.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("mouse" "visits" "dog" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The mouse does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("mouse" "visits" "dog" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("dog" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The dog is not rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("dog" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The mouse chases the dog.
Unknown
random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "+")
The dog does not visit the mouse.
Unknown
inv-random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog chases the mouse.[(triple1)] The mouse is young.[(triple2)] The mouse likes the dog.[(triple3)] @1: The dog likes the mouse.[(((triple1) -> rule3))] The mouse is round.[(((triple1) -> rule5))] @2: The mouse visits the dog.[(((((triple1) -> rule3)) -> rule6))] @3: The dog is rough.[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((triple1) -> (rule3 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple1) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int3