The bear chases the tiger. The rabbit likes the squirrel. The squirrel is big. The squirrel is young. The squirrel likes the tiger. The tiger chases the bear. The tiger likes the rabbit. If someone chases the tiger then the tiger eats the rabbit.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If someone chases the tiger then the tiger eats the rabbit.
((("someone" "chases" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
The bear chases the tiger.
True
1
proof
[(triple1)]
("bear" "chases" "tiger" "+")
triple1
The squirrel does not like the tiger.
False
1
inv-proof
[(triple5)]
("squirrel" "likes" "tiger" "-")
triple5
The tiger eats the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger does not eat the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "eats" "rabbit" "-")
((triple1) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The bear does not like the rabbit.
Unknown
inv-random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
@0: The bear chases the tiger.[(triple1)] The rabbit likes the squirrel.[(triple2)] The squirrel is big.[(triple3)] The squirrel is young.[(triple4)] The squirrel likes the tiger.[(triple5)] The tiger chases the bear.[(triple6)] The tiger likes the rabbit.[(triple7)] @1: The tiger eats the rabbit.[(((triple1) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple5
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple6
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple1) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1