The bear likes the squirrel. The cat likes the squirrel. The squirrel chases the bear. The tiger is blue. If someone likes the squirrel and the squirrel chases the tiger then the squirrel visits the bear. If someone likes the bear then they chase the squirrel. If someone chases the bear then they chase the squirrel. If someone is rough then they chase the squirrel. If someone chases the squirrel then the squirrel is round. If the bear is kind and the bear likes the cat then the bear does not visit the squirrel.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If someone likes the squirrel and the squirrel chases the tiger then the squirrel visits the bear.
((("someone" "likes" "squirrel" "+") ("squirrel" "chases" "tiger" "+")) -> ("squirrel" "visits" "bear" "+"))
If someone likes the bear then they chase the squirrel.
((("someone" "likes" "bear" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the bear then they chase the squirrel.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is rough then they chase the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the squirrel then the squirrel is round.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If the bear is kind and the bear likes the cat then the bear does not visit the squirrel.
((("bear" "is" "kind" "+") ("bear" "likes" "cat" "+")) -> ("bear" "visits" "squirrel" "-"))
The squirrel chases the bear.
True
1
proof
[(triple3)]
("squirrel" "chases" "bear" "+")
triple3
The tiger is not blue.
False
1
inv-proof
[(triple4)]
("tiger" "is" "blue" "-")
triple4
The squirrel chases the squirrel.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "chases" "squirrel" "+")
((triple3) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "chases" "squirrel" "-")
((triple3) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is round.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("squirrel" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is not round.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("squirrel" "is" "round" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The bear does not chase the squirrel.
Unknown
inv-rconc
[@1: The bear chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "squirrel" "-")
The tiger chases the squirrel.
Unknown
rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "squirrel" "+")
The cat does not chase the squirrel.
Unknown
inv-rconc
[@1: The cat chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "squirrel" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
The cat does not visit the bear.
Unknown
inv-random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The bear likes the squirrel.[(triple1)] The cat likes the squirrel.[(triple2)] The squirrel chases the bear.[(triple3)] The tiger is blue.[(triple4)] @1: The squirrel chases the squirrel.[(((triple3) -> rule3))] @2: The squirrel is round.[(((((triple3) -> rule3)) -> rule5))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple3
The tiger is blue.
("tiger" "is" "blue" "+")
triple4
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple3) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2