The cat chases the mouse. The cat likes the squirrel. The mouse chases the tiger. The mouse likes the cat. The mouse visits the cat. The mouse visits the tiger. The squirrel is green. The squirrel likes the tiger. The squirrel visits the cat. The tiger does not like the cat. The tiger likes the squirrel. The tiger visits the cat. If the tiger is green then the tiger chases the mouse. If something likes the tiger then it visits the tiger.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the tiger is green then the tiger chases the mouse.
((("tiger" "is" "green" "+")) -> ("tiger" "chases" "mouse" "+"))
If something likes the tiger then it visits the tiger.
((("something" "likes" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
The squirrel likes the tiger.
True
1
proof
[(triple8)]
("squirrel" "likes" "tiger" "+")
triple8
The cat does not chase the mouse.
False
1
inv-proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The squirrel visits the tiger.
True
2
proof
[(((triple8) -> rule2))]
("squirrel" "visits" "tiger" "+")
((triple8) -> (rule2 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The squirrel does not visit the tiger.
False
2
inv-proof
[(((triple8) -> rule2))]
("squirrel" "visits" "tiger" "-")
((triple8) -> (rule2 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The cat chases the mouse.[(triple1)] The cat likes the squirrel.[(triple2)] The mouse chases the tiger.[(triple3)] The mouse likes the cat.[(triple4)] The mouse visits the cat.[(triple5)] The mouse visits the tiger.[(triple6)] The squirrel is green.[(triple7)] The squirrel likes the tiger.[(triple8)] The squirrel visits the cat.[(triple9)] The tiger does not like the cat.[(triple10)] The tiger likes the squirrel.[(triple11)] The tiger visits the cat.[(triple12)] @1: The squirrel visits the tiger.[(((triple8) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple3
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple4
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple5
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple8
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple9
The tiger does not like the cat.
("tiger" "likes" "cat" "-")
triple10
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
((triple8) -> (rule2 % int1))
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
int1