The bear does not eat the cat. The bear is not red. The bear sees the cat. The cat eats the cow. The cat is not big. The cat is not blue. The cat is kind. The cat does not need the bear. The cat needs the cow. The cat sees the cow. The cow eats the cat. The cow is blue. The cow is not kind. The cow needs the cat. The cow sees the bear. The cow sees the cat. If the cow eats the cat then the cow eats the bear. If something eats the bear then the bear is not rough.
The bear does not eat the cat.
("bear" "eats" "cat" "-")
The bear is not red.
("bear" "is" "red" "-")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is not big.
("cat" "is" "big" "-")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is kind.
("cat" "is" "kind" "+")
The cat does not need the bear.
("cat" "needs" "bear" "-")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is not kind.
("cow" "is" "kind" "-")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If the cow eats the cat then the cow eats the bear.
((("cow" "eats" "cat" "+")) -> ("cow" "eats" "bear" "+"))
If something eats the bear then the bear is not rough.
((("something" "eats" "bear" "+")) -> ("bear" "is" "rough" "-"))
The cow eats the cat.
True
1
proof
[(triple11)]
("cow" "eats" "cat" "+")
triple11
The bear is red.
False
1
inv-proof
[(triple2)]
("bear" "is" "red" "+")
triple2
The cow eats the bear.
True
2
proof
[(((triple11) -> rule1))]
("cow" "eats" "bear" "+")
((triple11) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The cow does not eat the bear.
False
2
inv-proof
[(((triple11) -> rule1))]
("cow" "eats" "bear" "-")
((triple11) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear is not rough.
True
3
proof
[(((((triple11) -> rule1)) -> rule2))]
("bear" "is" "rough" "-")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear is rough.
False
3
inv-proof
[(((((triple11) -> rule1)) -> rule2))]
("bear" "is" "rough" "+")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
The cat does not see the bear.
Unknown
inv-random
[@0: The cat sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bear" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear does not eat the cat.[(triple1)] The bear is not red.[(triple2)] The bear sees the cat.[(triple3)] The cat does not need the bear.[(triple8)] The cat eats the cow.[(triple4)] The cat is kind.[(triple7)] The cat is not big.[(triple5)] The cat is not blue.[(triple6)] The cat needs the cow.[(triple9)] The cat sees the cow.[(triple10)] The cow eats the cat.[(triple11)] The cow is blue.[(triple12)] The cow is not kind.[(triple13)] The cow needs the cat.[(triple14)] The cow sees the bear.[(triple15)] The cow sees the cat.[(triple16)] @1: The cow eats the bear.[(((triple11) -> rule1))] @2: The bear is not rough.[(((((triple11) -> rule1)) -> rule2))]
The bear does not eat the cat.
("bear" "eats" "cat" "-")
triple1
The bear is not red.
("bear" "is" "red" "-")
triple2
The bear sees the cat.
("bear" "sees" "cat" "+")
triple3
The cat does not need the bear.
("cat" "needs" "bear" "-")
triple8
The cat eats the cow.
("cat" "eats" "cow" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple7
The cat is not big.
("cat" "is" "big" "-")
triple5
The cat is not blue.
("cat" "is" "blue" "-")
triple6
The cat needs the cow.
("cat" "needs" "cow" "+")
triple9
The cat sees the cow.
("cat" "sees" "cow" "+")
triple10
The cow eats the cat.
("cow" "eats" "cat" "+")
triple11
The cow is blue.
("cow" "is" "blue" "+")
triple12
The cow is not kind.
("cow" "is" "kind" "-")
triple13
The cow needs the cat.
("cow" "needs" "cat" "+")
triple14
The cow sees the bear.
("cow" "sees" "bear" "+")
triple15
The cow sees the cat.
("cow" "sees" "cat" "+")
triple16
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple11) -> (rule1 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear is not rough.
("bear" "is" "rough" "-")
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2