The cat chases the mouse. The cat chases the tiger. The cat is big. The cat is rough. The cat sees the tiger. The cat visits the mouse. The cat visits the tiger. The mouse visits the cat. The mouse visits the tiger. The tiger is big. The tiger is round. The tiger sees the cat. The tiger sees the mouse. The tiger visits the cat. The tiger visits the mouse. If someone is rough and round then they are big. If someone visits the cat then they see the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is rough and round then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone visits the cat then they see the mouse.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "mouse" "+"))
The cat is big.
True
1
proof
[(triple3)]
("cat" "is" "big" "+")
triple3
The mouse does not visit the tiger.
False
1
inv-proof
[(triple9)]
("mouse" "visits" "tiger" "-")
triple9
The mouse sees the mouse.
True
2
proof
[(((triple8) -> rule2))]
("mouse" "sees" "mouse" "+")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple8) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The cat does not see the mouse.
Unknown
inv-rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "mouse" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat chases the tiger.[(triple2)] The cat is big.[(triple3)] The cat is rough.[(triple4)] The cat sees the tiger.[(triple5)] The cat visits the mouse.[(triple6)] The cat visits the tiger.[(triple7)] The mouse visits the cat.[(triple8)] The mouse visits the tiger.[(triple9)] The tiger is big.[(triple10)] The tiger is round.[(triple11)] The tiger sees the cat.[(triple12)] The tiger sees the mouse.[(triple13 OR ((triple14) -> rule2))] The tiger visits the cat.[(triple14)] The tiger visits the mouse.[(triple15)] @1: The mouse sees the mouse.[(((triple8) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple7
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple8
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple13
((triple14) -> (rule2 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1