The bear eats the cow. The bear is big. The bear is round. The bear sees the cow. The bear visits the cow. The cow is big. The cow is green. If someone is round then they visit the cow. If someone sees the bear and the bear is round then they visit the cow. If the bear visits the cow and the cow eats the bear then the bear is red. If the bear visits the cow then the cow eats the bear. If someone sees the cow then the cow is green. If someone is green and they eat the cow then the cow eats the bear. If someone is kind then they are green. If someone visits the bear then the bear sees the cow.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
If someone is round then they visit the cow.
((("someone" "is" "round" "+")) -> ("someone" "visits" "cow" "+"))
If someone sees the bear and the bear is round then they visit the cow.
((("someone" "sees" "bear" "+") ("bear" "is" "round" "+")) -> ("someone" "visits" "cow" "+"))
If the bear visits the cow and the cow eats the bear then the bear is red.
((("bear" "visits" "cow" "+") ("cow" "eats" "bear" "+")) -> ("bear" "is" "red" "+"))
If the bear visits the cow then the cow eats the bear.
((("bear" "visits" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If someone sees the cow then the cow is green.
((("someone" "sees" "cow" "+")) -> ("cow" "is" "green" "+"))
If someone is green and they eat the cow then the cow eats the bear.
((("someone" "is" "green" "+") ("someone" "eats" "cow" "+")) -> ("cow" "eats" "bear" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone visits the bear then the bear sees the cow.
((("someone" "visits" "bear" "+")) -> ("bear" "sees" "cow" "+"))
The bear sees the cow.
True
1
proof
[(triple4)]
("bear" "sees" "cow" "+")
triple4
The bear does not eat the cow.
False
1
inv-proof
[(triple1)]
("bear" "eats" "cow" "-")
triple1
The cow eats the bear.
True
2
proof
[(((triple5) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("cow" "eats" "bear" "+")
((triple5) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The cow does not eat the bear.
False
2
inv-proof
[(((triple5) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("cow" "eats" "bear" "-")
((triple5) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The bear is red.
True
4
proof
[(((triple5 ((triple5) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((triple5) -> rule4)) -> rule3) OR ((triple5 ((((triple3) -> rule1)) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule3))]
("bear" "is" "red" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The bear is not red.
False
4
inv-proof
[(((triple5 ((triple5) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((triple5) -> rule4)) -> rule3) OR ((triple5 ((((triple3) -> rule1)) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule3))]
("bear" "is" "red" "-")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "cow" "-")
The bear is green.
Unknown
rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "green" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
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 eats the cow.[(triple1)] The bear is big.[(triple2)] The bear is round.[(triple3)] The bear sees the cow.[(triple4)] The bear visits the cow.[(triple5 OR ((triple3) -> rule1))] The cow is big.[(triple6)] The cow is green.[(triple7 OR ((triple4) -> rule5))] @1: The cow eats the bear.[(((triple5) -> rule4) OR ((((triple3) -> rule1)) -> rule4))] @2: The bear is red.[(((triple5 ((triple5) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((triple5) -> rule4)) -> rule3) OR ((triple5 ((((triple3) -> rule1)) -> rule4)) -> rule3) OR ((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule3))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the cow.
("bear" "sees" "cow" "+")
triple4
The bear visits the cow.
("bear" "visits" "cow" "+")
triple5
((triple3) -> (rule1 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple6
The cow is green.
("cow" "is" "green" "+")
triple7
((triple4) -> (rule5 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple5) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear visits the cow.
("bear" "visits" "cow" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((triple5 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((triple5 ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
The bear visits the cow.
("bear" "visits" "cow" "+")
int3