The bear chases the cow. The bear chases the lion. The bear is nice. The bear is round. The bear needs the cow. The bear visits the cow. The bear visits the lion. The cow chases the bear. The cow is nice. The cow visits the bear. The lion chases the cow. The lion is rough. The lion is round. The lion needs the bear. The lion needs the cow. The lion visits the cow. If someone is nice then they chase the bear. If someone chases the bear then they chase the lion. If someone chases the cow then they are nice.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone is nice then they chase the bear.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the bear then they chase the lion.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the cow then they are nice.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "nice" "+"))
The cow is nice.
True
1
proof
[(triple9)]
("cow" "is" "nice" "+")
triple9
The lion is not round.
False
1
inv-proof
[(triple13)]
("lion" "is" "round" "-")
triple13
The cow chases the lion.
True
2
proof
[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))]
("cow" "chases" "lion" "+")
((triple8) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The cow does not chase the lion.
False
2
inv-proof
[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))]
("cow" "chases" "lion" "-")
((triple8) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The lion chases the bear.
True
3
proof
[(((((triple11) -> rule3)) -> rule1))]
("lion" "chases" "bear" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not chase the bear.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule1))]
("lion" "chases" "bear" "-")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion chases the lion.
True
4
proof
[(((((((triple11) -> rule3)) -> rule1)) -> rule2))]
("lion" "chases" "lion" "+")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion does not chase the lion.
False
4
inv-proof
[(((((((triple11) -> rule3)) -> rule1)) -> rule2))]
("lion" "chases" "lion" "-")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The cow needs the lion.
Unknown
random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear chases the cow.[(triple1)] The bear chases the lion.[(triple2 OR ((((triple3) -> rule1)) -> rule2) OR ((((((triple1) -> rule3)) -> rule1)) -> rule2))] The bear is nice.[(triple3 OR ((triple1) -> rule3))] The bear is round.[(triple4)] The bear needs the cow.[(triple5)] The bear visits the cow.[(triple6)] The bear visits the lion.[(triple7)] The cow chases the bear.[(triple8 OR ((triple9) -> rule1))] The cow is nice.[(triple9)] The cow visits the bear.[(triple10)] The lion chases the cow.[(triple11)] The lion is rough.[(triple12)] The lion is round.[(triple13)] The lion needs the bear.[(triple14)] The lion needs the cow.[(triple15)] The lion visits the cow.[(triple16)] @1: The bear chases the bear.[(((triple3) -> rule1) OR ((((triple1) -> rule3)) -> rule1))] The cow chases the lion.[(((triple8) -> rule2) OR ((((triple9) -> rule1)) -> rule2))] The lion is nice.[(((triple11) -> rule3))] @2: The lion chases the bear.[(((((triple11) -> rule3)) -> rule1))] @3: The lion chases the lion.[(((((((triple11) -> rule3)) -> rule1)) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear chases the lion.
("bear" "chases" "lion" "+")
triple2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
triple3
((triple1) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is round.
("bear" "is" "round" "+")
triple4
The bear needs the cow.
("bear" "needs" "cow" "+")
triple5
The bear visits the cow.
("bear" "visits" "cow" "+")
triple6
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The cow chases the bear.
("cow" "chases" "bear" "+")
triple8
((triple9) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
triple9
The cow visits the bear.
("cow" "visits" "bear" "+")
triple10
The lion chases the cow.
("lion" "chases" "cow" "+")
triple11
The lion is rough.
("lion" "is" "rough" "+")
triple12
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the bear.
("lion" "needs" "bear" "+")
triple14
The lion needs the cow.
("lion" "needs" "cow" "+")
triple15
The lion visits the cow.
("lion" "visits" "cow" "+")
triple16
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple3) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The cow chases the lion.
("cow" "chases" "lion" "+")
((triple8) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((triple11) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((triple11) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3