The bear is not green. The cat chases the squirrel. The squirrel chases the tiger. The tiger chases the bear. The tiger chases the squirrel. The tiger eats the bear. The tiger eats the squirrel. If something visits the bear then it is kind. If something eats the bear then it is big. If something visits the bear and it does not chase the tiger then the bear does not eat the cat. If something chases the squirrel then the squirrel eats the cat. If something is red and it visits the cat then it eats the squirrel. If something eats the bear then it is not green. If something eats the cat then the cat eats the tiger. If the bear chases the cat and the bear is not big then the bear does not eat the tiger.
The bear is not green.
("bear" "is" "green" "-")
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
If something visits the bear then it is kind.
((("something" "visits" "bear" "+")) -> ("something" "is" "kind" "+"))
If something eats the bear then it is big.
((("something" "eats" "bear" "+")) -> ("something" "is" "big" "+"))
If something visits the bear and it does not chase the tiger then the bear does not eat the cat.
((("something" "visits" "bear" "+") ("something" "chases" "tiger" "~")) -> ("bear" "eats" "cat" "-"))
If something chases the squirrel then the squirrel eats the cat.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "eats" "cat" "+"))
If something is red and it visits the cat then it eats the squirrel.
((("something" "is" "red" "+") ("something" "visits" "cat" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the bear then it is not green.
((("something" "eats" "bear" "+")) -> ("something" "is" "green" "-"))
If something eats the cat then the cat eats the tiger.
((("something" "eats" "cat" "+")) -> ("cat" "eats" "tiger" "+"))
If the bear chases the cat and the bear is not big then the bear does not eat the tiger.
((("bear" "chases" "cat" "+") ("bear" "is" "big" "~")) -> ("bear" "eats" "tiger" "-"))
The bear is not green.
True
1
proof
[(triple1)]
("bear" "is" "green" "-")
triple1
The squirrel does not chase the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "tiger" "-")
triple3
The tiger is not green.
True
2
proof
[(((triple6) -> rule6))]
("tiger" "is" "green" "-")
((triple6) -> (rule6 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The tiger is green.
False
2
inv-proof
[(((triple6) -> rule6))]
("tiger" "is" "green" "+")
((triple6) -> (rule6 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The cat eats the tiger.
True
3
proof
[(((((triple2) -> rule4)) -> rule7) OR ((((triple5) -> rule4)) -> rule7))]
("cat" "eats" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The cat does not eat the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7) OR ((((triple5) -> rule4)) -> rule7))]
("cat" "eats" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "kind" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "big" "-")
The cat visits the bear.
Unknown
random
[@0: The cat visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bear" "+")
The squirrel does not visit the bear.
Unknown
inv-random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is not green.[(triple1)] The cat chases the squirrel.[(triple2)] The squirrel chases the tiger.[(triple3)] The tiger chases the bear.[(triple4)] The tiger chases the squirrel.[(triple5)] The tiger eats the bear.[(triple6)] The tiger eats the squirrel.[(triple7)] @1: The squirrel eats the cat.[(((triple2) -> rule4) OR ((triple5) -> rule4))] The tiger is big.[(((triple6) -> rule2))] The tiger is not green.[(((triple6) -> rule6))] @2: The cat eats the tiger.[(((((triple2) -> rule4)) -> rule7) OR ((((triple5) -> rule4)) -> rule7))]
The bear is not green.
("bear" "is" "green" "-")
triple1
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple3
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple4
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple7
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((triple2) -> (rule4 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
((triple5) -> (rule4 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple6) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not green.
("tiger" "is" "green" "-")
((triple6) -> (rule6 % int1))
The tiger is not green.
("tiger" "is" "green" "-")
int1
The cat eats the tiger.
("cat" "eats" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule7 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int2