The dog chases the mouse. The dog sees the mouse. The mouse chases the dog. The mouse is big. The mouse is red. The mouse likes the dog. The mouse sees the dog. If the dog sees the mouse then the mouse sees the dog. If something is round then it likes the dog. If something sees the dog and the dog likes the mouse then the mouse chases the dog. If something likes the mouse then the mouse is nice. All red things are round. If the mouse is red then the mouse sees the dog. If something chases the dog then it likes the mouse. If something sees the mouse and it is red then the mouse sees the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If the dog sees the mouse then the mouse sees the dog.
((("dog" "sees" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If something is round then it likes the dog.
((("something" "is" "round" "+")) -> ("something" "likes" "dog" "+"))
If something sees the dog and the dog likes the mouse then the mouse chases the dog.
((("something" "sees" "dog" "+") ("dog" "likes" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If something likes the mouse then the mouse is nice.
((("something" "likes" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If the mouse is red then the mouse sees the dog.
((("mouse" "is" "red" "+")) -> ("mouse" "sees" "dog" "+"))
If something chases the dog then it likes the mouse.
((("something" "chases" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something sees the mouse and it is red then the mouse sees the dog.
((("something" "sees" "mouse" "+") ("something" "is" "red" "+")) -> ("mouse" "sees" "dog" "+"))
The mouse is big.
True
1
proof
[(triple4)]
("mouse" "is" "big" "+")
triple4
The mouse is not red.
False
1
inv-proof
[(triple5)]
("mouse" "is" "red" "-")
triple5
The mouse is round.
True
2
proof
[(((triple5) -> rule5))]
("mouse" "is" "round" "+")
((triple5) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule7))]
("mouse" "likes" "mouse" "-")
((triple3) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
True
3
proof
[(((((triple3) -> rule7)) -> rule4))]
("mouse" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The mouse is not nice.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4))]
("mouse" "is" "nice" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The dog does not like the mouse.
Unknown
inv-rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "likes" "mouse" "-")
The dog likes the dog.
Unknown
rconc
[@2: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("dog" "likes" "dog" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "round" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog sees the mouse.[(triple2)] The mouse chases the dog.[(triple3)] The mouse is big.[(triple4)] The mouse is red.[(triple5)] The mouse likes the dog.[(triple6 OR ((((triple5) -> rule5)) -> rule2))] The mouse sees the dog.[(triple7 OR ((triple2) -> rule1) OR ((triple5) -> rule6))] @1: The mouse is round.[(((triple5) -> rule5))] The mouse likes the mouse.[(((triple3) -> rule7))] @2: The mouse is nice.[(((((triple3) -> rule7)) -> rule4))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple6
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
The mouse likes the dog.
("mouse" "likes" "dog" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple7
((triple2) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
((triple5) -> (rule6 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple5) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple3) -> (rule7 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2