The bear is not round. The cat does not eat the bear. The cat is not cold. The cat is not green. The cat is red. The cow is green. The cow sees the bear. If the bear visits the cow then the bear sees the cow. If someone sees the bear then the bear visits the cow.
The bear is not round.
("bear" "is" "round" "-")
The cat does not eat the bear.
("cat" "eats" "bear" "-")
The cat is not cold.
("cat" "is" "cold" "-")
The cat is not green.
("cat" "is" "green" "-")
The cat is red.
("cat" "is" "red" "+")
The cow is green.
("cow" "is" "green" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
If the bear visits the cow then the bear sees the cow.
((("bear" "visits" "cow" "+")) -> ("bear" "sees" "cow" "+"))
If someone sees the bear then the bear visits the cow.
((("someone" "sees" "bear" "+")) -> ("bear" "visits" "cow" "+"))
The cat does not eat the bear.
True
1
proof
[(triple2)]
("cat" "eats" "bear" "-")
triple2
The cow does not see the bear.
False
1
inv-proof
[(triple7)]
("cow" "sees" "bear" "-")
triple7
The bear visits the cow.
True
2
proof
[(((triple7) -> rule2))]
("bear" "visits" "cow" "+")
((triple7) -> (rule2 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The bear does not visit the cow.
False
2
inv-proof
[(((triple7) -> rule2))]
("bear" "visits" "cow" "-")
((triple7) -> (rule2 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The bear sees the cow.
True
3
proof
[(((((triple7) -> rule2)) -> rule1))]
("bear" "sees" "cow" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The bear does not see the cow.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule1))]
("bear" "sees" "cow" "-")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The bear does not see the cat.
Unknown
inv-random
[@0: The bear sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cat" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cat does not visit the cow.
Unknown
inv-random
[@0: The cat visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cow" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear is not round.[(triple1)] The cat does not eat the bear.[(triple2)] The cat is not cold.[(triple3)] The cat is not green.[(triple4)] The cat is red.[(triple5)] The cow is green.[(triple6)] The cow sees the bear.[(triple7)] @1: The bear visits the cow.[(((triple7) -> rule2))] @2: The bear sees the cow.[(((((triple7) -> rule2)) -> rule1))]
The bear is not round.
("bear" "is" "round" "-")
triple1
The cat does not eat the bear.
("cat" "eats" "bear" "-")
triple2
The cat is not cold.
("cat" "is" "cold" "-")
triple3
The cat is not green.
("cat" "is" "green" "-")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The cow sees the bear.
("cow" "sees" "bear" "+")
triple7
The bear visits the cow.
("bear" "visits" "cow" "+")
((triple7) -> (rule2 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2