The cat is nice. The mouse is round. The squirrel chases the tiger. The tiger eats the mouse. If someone chases the squirrel then they eat the squirrel. If someone is green then they eat the squirrel. If someone visits the mouse and the mouse visits the cat then they chase the tiger. If someone is rough and they visit the cat then the cat is rough. If the tiger visits the squirrel and the squirrel eats the tiger then the squirrel visits the cat. If someone visits the mouse and they chase the cat then the cat is green. If someone is blue then they eat the mouse. If someone chases the tiger then they chase the cat.
The cat is nice.
("cat" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
If someone chases the squirrel then they eat the squirrel.
((("someone" "chases" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is green then they eat the squirrel.
((("someone" "is" "green" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone visits the mouse and the mouse visits the cat then they chase the tiger.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "cat" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is rough and they visit the cat then the cat is rough.
((("someone" "is" "rough" "+") ("someone" "visits" "cat" "+")) -> ("cat" "is" "rough" "+"))
If the tiger visits the squirrel and the squirrel eats the tiger then the squirrel visits the cat.
((("tiger" "visits" "squirrel" "+") ("squirrel" "eats" "tiger" "+")) -> ("squirrel" "visits" "cat" "+"))
If someone visits the mouse and they chase the cat then the cat is green.
((("someone" "visits" "mouse" "+") ("someone" "chases" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone is blue then they eat the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "mouse" "+"))
If someone chases the tiger then they chase the cat.
((("someone" "chases" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple3)]
("squirrel" "chases" "tiger" "+")
triple3
The tiger does not eat the mouse.
False
1
inv-proof
[(triple4)]
("tiger" "eats" "mouse" "-")
triple4
The squirrel chases the cat.
True
2
proof
[(((triple3) -> rule8))]
("squirrel" "chases" "cat" "+")
((triple3) -> (rule8 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel does not chase the cat.
False
2
inv-proof
[(((triple3) -> rule8))]
("squirrel" "chases" "cat" "-")
((triple3) -> (rule8 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "eats" "mouse" "-")
The cat eats the squirrel.
Unknown
rconc
[@2: The cat eats the squirrel.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("cat" "eats" "squirrel" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The cat is nice.[(triple1)] The mouse is round.[(triple2)] The squirrel chases the tiger.[(triple3)] The tiger eats the mouse.[(triple4)] @1: The squirrel chases the cat.[(((triple3) -> rule8))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The mouse is round.
("mouse" "is" "round" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((triple3) -> (rule8 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1