The lion sees the rabbit. The rabbit is nice. The rabbit is red. The rabbit needs the lion. The rabbit sees the lion. The rabbit sees the tiger. The squirrel is green. The squirrel needs the lion. The squirrel sees the lion. The squirrel sees the rabbit. The squirrel visits the tiger. The tiger is red. The tiger sees the lion. The tiger sees the rabbit. The tiger visits the lion. If something needs the lion then the lion is rough.
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something needs the lion then the lion is rough.
((("something" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
The tiger sees the lion.
True
1
proof
[(triple13)]
("tiger" "sees" "lion" "+")
triple13
The rabbit does not need the lion.
False
1
inv-proof
[(triple4)]
("rabbit" "needs" "lion" "-")
triple4
The lion is rough.
True
2
proof
[(((triple4) -> rule1) OR ((triple8) -> rule1))]
("lion" "is" "rough" "+")
((triple4) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple8) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple8) -> rule1))]
("lion" "is" "rough" "-")
((triple4) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple8) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion does not see the squirrel.
Unknown
inv-random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "-")
The rabbit visits the tiger.
Unknown
random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger needs the lion.
Unknown
random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "+")
@0: The lion sees the rabbit.[(triple1)] The rabbit is nice.[(triple2)] The rabbit is red.[(triple3)] The rabbit needs the lion.[(triple4)] The rabbit sees the lion.[(triple5)] The rabbit sees the tiger.[(triple6)] The squirrel is green.[(triple7)] The squirrel needs the lion.[(triple8)] The squirrel sees the lion.[(triple9)] The squirrel sees the rabbit.[(triple10)] The squirrel visits the tiger.[(triple11)] The tiger is red.[(triple12)] The tiger sees the lion.[(triple13)] The tiger sees the rabbit.[(triple14)] The tiger visits the lion.[(triple15)] @1: The lion is rough.[(((triple4) -> rule1) OR ((triple8) -> rule1))]
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple4
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple5
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple6
The squirrel is green.
("squirrel" "is" "green" "+")
triple7
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple8
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple10
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple13
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion is rough.
("lion" "is" "rough" "+")
((triple4) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple8) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1