The bear eats the cow. The bear is cold. The bear is kind. The bear is rough. The bear likes the cow. The bear visits the cow. The cow eats the bear. The cow is cold. The cow is green. The cow is kind. The cow likes the bear. The cow visits the bear. If something likes the cow then the cow likes the bear. If something visits the bear then it eats the cow. If the cow is green then the cow visits the bear. If something likes the bear and the bear visits the cow then it is green. If the cow eats the bear then the cow likes the bear. If something eats the cow then it visits the bear.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the cow.
("bear" "likes" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
If something likes the cow then the cow likes the bear.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "bear" "+"))
If something visits the bear then it eats the cow.
((("something" "visits" "bear" "+")) -> ("something" "eats" "cow" "+"))
If the cow is green then the cow visits the bear.
((("cow" "is" "green" "+")) -> ("cow" "visits" "bear" "+"))
If something likes the bear and the bear visits the cow then it is green.
((("something" "likes" "bear" "+") ("bear" "visits" "cow" "+")) -> ("something" "is" "green" "+"))
If the cow eats the bear then the cow likes the bear.
((("cow" "eats" "bear" "+")) -> ("cow" "likes" "bear" "+"))
If something eats the cow then it visits the bear.
((("something" "eats" "cow" "+")) -> ("something" "visits" "bear" "+"))
The cow is green.
True
1
proof
[(triple9 OR ((triple11 triple6) -> rule4) OR ((((triple5) -> rule1) triple6) -> rule4) OR ((((triple7) -> rule5) triple6) -> rule4))]
("cow" "is" "green" "+")
triple9
((triple11 triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple5) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The bear does not like the cow.
False
1
inv-proof
[(triple5)]
("bear" "likes" "cow" "-")
triple5
The cow eats the cow.
True
2
proof
[(((triple12) -> rule2) OR ((((triple9) -> rule3)) -> rule2) OR ((((((triple11 triple6) -> rule4)) -> rule3)) -> rule2) OR ((((((((triple5) -> rule1) triple6) -> rule4)) -> rule3)) -> rule2) OR ((((((((triple7) -> rule5) triple6) -> rule4)) -> rule3)) -> rule2))]
("cow" "eats" "cow" "+")
((triple12) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
((((((triple11 triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((((triple5) -> (rule1 % int4)) triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
int4
((((((((triple7) -> (rule5 % int4)) triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
int4
The bear does not visit the bear.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "visits" "bear" "-")
((triple1) -> (rule6 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is not green.
Unknown
inv-rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "green" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The bear eats the cow.[(triple1)] The bear is cold.[(triple2)] The bear is kind.[(triple3)] The bear is rough.[(triple4)] The bear likes the cow.[(triple5)] The bear visits the cow.[(triple6)] The cow eats the bear.[(triple7)] The cow is cold.[(triple8)] The cow is green.[(triple9 OR ((triple11 triple6) -> rule4) OR ((((triple5) -> rule1) triple6) -> rule4) OR ((((triple7) -> rule5) triple6) -> rule4))] The cow is kind.[(triple10)] The cow likes the bear.[(triple11 OR ((triple5) -> rule1) OR ((triple7) -> rule5))] The cow visits the bear.[(triple12 OR ((triple9) -> rule3) OR ((((triple11 triple6) -> rule4)) -> rule3) OR ((((((triple5) -> rule1) triple6) -> rule4)) -> rule3) OR ((((((triple7) -> rule5) triple6) -> rule4)) -> rule3))] @1: The bear visits the bear.[(((triple1) -> rule6))] The cow eats the cow.[(((triple12) -> rule2) OR ((((triple9) -> rule3)) -> rule2) OR ((((((triple11 triple6) -> rule4)) -> rule3)) -> rule2) OR ((((((((triple5) -> rule1) triple6) -> rule4)) -> rule3)) -> rule2) OR ((((((((triple7) -> rule5) triple6) -> rule4)) -> rule3)) -> rule2))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear likes the cow.
("bear" "likes" "cow" "+")
triple5
The bear visits the cow.
("bear" "visits" "cow" "+")
triple6
The cow eats the bear.
("cow" "eats" "bear" "+")
triple7
The cow is cold.
("cow" "is" "cold" "+")
triple8
The cow is green.
("cow" "is" "green" "+")
triple9
((triple11 triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((((triple5) -> (rule1 % int2)) triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
((((triple7) -> (rule5 % int2)) triple6) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
triple10
The cow likes the bear.
("cow" "likes" "bear" "+")
triple11
((triple5) -> (rule1 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
((triple7) -> (rule5 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
triple12
((triple9) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
((((triple11 triple6) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
((((((triple5) -> (rule1 % int3)) triple6) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
((((((triple7) -> (rule5 % int3)) triple6) -> (rule4 % int2))) -> (rule3 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the bear.
("cow" "likes" "bear" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule6 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple12) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
((((((triple11 triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((((((((triple5) -> (rule1 % int4)) triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
int4
((((((((triple7) -> (rule5 % int4)) triple6) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
int4