The bear is green. The bear is kind. The cat chases the tiger. The cat likes the squirrel. The cat visits the squirrel. The squirrel chases the cat. The squirrel is young. The squirrel likes the bear. The tiger chases the cat. The tiger likes the bear. The tiger visits the cat. The tiger visits the squirrel. If something chases the cat then it is kind. If something is kind then it likes the tiger.
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something chases the cat then it is kind.
((("something" "chases" "cat" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it likes the tiger.
((("something" "is" "kind" "+")) -> ("something" "likes" "tiger" "+"))
The tiger visits the cat.
True
1
proof
[(triple11)]
("tiger" "visits" "cat" "+")
triple11
The tiger does not chase the cat.
False
1
inv-proof
[(triple9)]
("tiger" "chases" "cat" "-")
triple9
The squirrel is kind.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "is" "kind" "+")
((triple6) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The bear does not like the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "likes" "tiger" "-")
((triple2) -> (rule2 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The squirrel likes the tiger.
True
3
proof
[(((((triple6) -> rule1)) -> rule2))]
("squirrel" "likes" "tiger" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel does not like the tiger.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule2))]
("squirrel" "likes" "tiger" "-")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "-")
The cat likes the tiger.
Unknown
rconc
[@2: The cat likes the tiger.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "likes" "tiger" "+")
The bear does not like the cat.
Unknown
inv-random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "-")
The squirrel visits the bear.
Unknown
random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger likes the squirrel.
Unknown
random
[@0: The tiger likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "squirrel" "+")
@0: The bear is green.[(triple1)] The bear is kind.[(triple2)] The cat chases the tiger.[(triple3)] The cat likes the squirrel.[(triple4)] The cat visits the squirrel.[(triple5)] The squirrel chases the cat.[(triple6)] The squirrel is young.[(triple7)] The squirrel likes the bear.[(triple8)] The tiger chases the cat.[(triple9)] The tiger likes the bear.[(triple10)] The tiger visits the cat.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The bear likes the tiger.[(((triple2) -> rule2))] The squirrel is kind.[(((triple6) -> rule1))] The tiger is kind.[(((triple9) -> rule1))] @2: The squirrel likes the tiger.[(((((triple6) -> rule1)) -> rule2))] The tiger likes the tiger.[(((((triple9) -> rule1)) -> rule2))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple5
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple6
The squirrel is young.
("squirrel" "is" "young" "+")
triple7
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple8
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple9
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple10
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple2) -> (rule2 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple6) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple9) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2