The bear chases the squirrel. The rabbit chases the tiger. The squirrel eats the rabbit. The tiger is rough. If something eats the rabbit then the rabbit is rough.
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something eats the rabbit then the rabbit is rough.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
The rabbit chases the tiger.
True
1
proof
[(triple2)]
("rabbit" "chases" "tiger" "+")
triple2
The squirrel does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "rabbit" "-")
triple3
The rabbit is rough.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "is" "rough" "+")
((triple3) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not rough.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "is" "rough" "-")
((triple3) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not eat the tiger.
Unknown
inv-random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "-")
The bear visits the rabbit.
Unknown
random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The bear chases the squirrel.[(triple1)] The rabbit chases the tiger.[(triple2)] The squirrel eats the rabbit.[(triple3)] The tiger is rough.[(triple4)] @1: The rabbit is rough.[(((triple3) -> rule1))]
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple3) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1