The dog chases the mouse. The dog chases the rabbit. The mouse is round. The mouse likes the rabbit. The rabbit chases the dog. The rabbit is green. The rabbit is nice. The rabbit is red. The rabbit is round. The rabbit needs the mouse. If something likes the mouse and the mouse chases the rabbit then the mouse chases the dog. If the dog needs the rabbit then the rabbit chases the dog. If something is round then it is rough. If something chases the dog then it chases the rabbit. If something is rough then it chases the dog. If something needs the rabbit and it likes the mouse then the rabbit needs the mouse.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If something likes the mouse and the mouse chases the rabbit then the mouse chases the dog.
((("something" "likes" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("mouse" "chases" "dog" "+"))
If the dog needs the rabbit then the rabbit chases the dog.
((("dog" "needs" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something chases the dog then it chases the rabbit.
((("something" "chases" "dog" "+")) -> ("something" "chases" "rabbit" "+"))
If something is rough then it chases the dog.
((("something" "is" "rough" "+")) -> ("something" "chases" "dog" "+"))
If something needs the rabbit and it likes the mouse then the rabbit needs the mouse.
((("something" "needs" "rabbit" "+") ("something" "likes" "mouse" "+")) -> ("rabbit" "needs" "mouse" "+"))
The rabbit is round.
True
1
proof
[(triple9)]
("rabbit" "is" "round" "+")
triple9
The rabbit does not need the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "needs" "mouse" "-")
triple10
The rabbit is rough.
True
2
proof
[(((triple9) -> rule3))]
("rabbit" "is" "rough" "+")
((triple9) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple5) -> rule4) OR ((((((triple9) -> rule3)) -> rule5)) -> rule4))]
("rabbit" "chases" "rabbit" "-")
((triple5) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The mouse chases the dog.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("mouse" "chases" "dog" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not chase the dog.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("mouse" "chases" "dog" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse chases the rabbit.
True
4
proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("mouse" "chases" "rabbit" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse does not chase the rabbit.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
("mouse" "chases" "rabbit" "-")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The dog does not chase the dog.
Unknown
inv-rconc
[@2: The dog chases the dog.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("dog" "chases" "dog" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "rough" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The rabbit chases the mouse.
Unknown
random
[@0: The rabbit chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "mouse" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog needs the mouse.
Unknown
random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The dog chases the mouse.[(triple1)] The dog chases the rabbit.[(triple2)] The mouse is round.[(triple3)] The mouse likes the rabbit.[(triple4)] The rabbit chases the dog.[(triple5 OR ((((triple9) -> rule3)) -> rule5))] The rabbit is green.[(triple6)] The rabbit is nice.[(triple7)] The rabbit is red.[(triple8)] The rabbit is round.[(triple9)] The rabbit needs the mouse.[(triple10)] @1: The mouse is rough.[(((triple3) -> rule3))] The rabbit chases the rabbit.[(((triple5) -> rule4) OR ((((((triple9) -> rule3)) -> rule5)) -> rule4))] The rabbit is rough.[(((triple9) -> rule3))] @2: The mouse chases the dog.[(((((triple3) -> rule3)) -> rule5))] @3: The mouse chases the rabbit.[(((((((triple3) -> rule3)) -> rule5)) -> rule4))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple5
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The rabbit is red.
("rabbit" "is" "red" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple5) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((((((triple9) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple9) -> (rule3 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3