The bear chases the cat. The bear chases the squirrel. The bear eats the cat. The bear is green. The bear is red. The bear sees the squirrel. The cat is cold. The cat sees the tiger. The squirrel chases the bear. The squirrel chases the cat. The squirrel eats the bear. The squirrel eats the cat. The squirrel is big. The squirrel sees the cat. The tiger eats the cat. The tiger is round. If something sees the tiger and it is round then it is green. If something sees the squirrel then the squirrel is big. If the bear sees the squirrel then the bear is red. If something eats the bear and the bear eats the squirrel then the squirrel chases the cat. If something eats the cat then it is cold. Cold things are green.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something sees the tiger and it is round then it is green.
((("something" "sees" "tiger" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something sees the squirrel then the squirrel is big.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If the bear sees the squirrel then the bear is red.
((("bear" "sees" "squirrel" "+")) -> ("bear" "is" "red" "+"))
If something eats the bear and the bear eats the squirrel then the squirrel chases the cat.
((("something" "eats" "bear" "+") ("bear" "eats" "squirrel" "+")) -> ("squirrel" "chases" "cat" "+"))
If something eats the cat then it is cold.
((("something" "eats" "cat" "+")) -> ("something" "is" "cold" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
The squirrel is big.
True
1
proof
[(triple13 OR ((triple6) -> rule2))]
("squirrel" "is" "big" "+")
triple13
((triple6) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The bear does not chase the squirrel.
False
1
inv-proof
[(triple2)]
("bear" "chases" "squirrel" "-")
triple2
The tiger is cold.
True
2
proof
[(((triple15) -> rule5))]
("tiger" "is" "cold" "+")
((triple15) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple12) -> rule5))]
("squirrel" "is" "cold" "-")
((triple12) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is green.
True
3
proof
[(((((triple15) -> rule5)) -> rule6))]
("tiger" "is" "green" "+")
((((triple15) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The squirrel is not green.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule6))]
("squirrel" "is" "green" "-")
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel does not chase the tiger.
Unknown
inv-random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
The bear does not eat the tiger.
Unknown
inv-random
[@0: The bear eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "tiger" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The squirrel does not see the bear.
Unknown
inv-random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "-")
The bear chases the tiger.
Unknown
random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the squirrel.[(triple2)] The bear eats the cat.[(triple3)] The bear is green.[(triple4 OR ((((triple3) -> rule5)) -> rule6))] The bear is red.[(triple5 OR ((triple6) -> rule3))] The bear sees the squirrel.[(triple6)] The cat is cold.[(triple7)] The cat sees the tiger.[(triple8)] The squirrel chases the bear.[(triple9)] The squirrel chases the cat.[(triple10)] The squirrel eats the bear.[(triple11)] The squirrel eats the cat.[(triple12)] The squirrel is big.[(triple13 OR ((triple6) -> rule2))] The squirrel sees the cat.[(triple14)] The tiger eats the cat.[(triple15)] The tiger is round.[(triple16)] @1: The bear is cold.[(((triple3) -> rule5))] The cat is green.[(((triple7) -> rule6))] The squirrel is cold.[(((triple12) -> rule5))] The tiger is cold.[(((triple15) -> rule5))] @2: The squirrel is green.[(((((triple12) -> rule5)) -> rule6))] The tiger is green.[(((((triple15) -> rule5)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear eats the cat.
("bear" "eats" "cat" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is red.
("bear" "is" "red" "+")
triple5
((triple6) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple6
The cat is cold.
("cat" "is" "cold" "+")
triple7
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple8
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple9
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple10
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple11
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple12
The squirrel is big.
("squirrel" "is" "big" "+")
triple13
((triple6) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple14
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple15
The tiger is round.
("tiger" "is" "round" "+")
triple16
The bear is cold.
("bear" "is" "cold" "+")
((triple3) -> (rule5 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The cat is green.
("cat" "is" "green" "+")
((triple7) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple12) -> (rule5 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((triple15) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((((triple15) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2