The cow eats the lion. The cow is round. The cow sees the lion. The lion chases the cow. The lion eats the cow. The lion eats the squirrel. The lion is blue. The lion is round. The squirrel chases the cow. The squirrel chases the lion. The squirrel eats the cow. The squirrel sees the lion. If someone eats the cow then the cow sees the lion. If someone eats the squirrel then they chase the squirrel. If someone is green then they chase the cow. If someone sees the lion and the lion sees the squirrel then the lion chases the cow. If someone is round and they eat the cow then they chase the squirrel. If someone chases the squirrel and the squirrel eats the cow then the cow is green.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone eats the cow then the cow sees the lion.
((("someone" "eats" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone eats the squirrel then they chase the squirrel.
((("someone" "eats" "squirrel" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is green then they chase the cow.
((("someone" "is" "green" "+")) -> ("someone" "chases" "cow" "+"))
If someone sees the lion and the lion sees the squirrel then the lion chases the cow.
((("someone" "sees" "lion" "+") ("lion" "sees" "squirrel" "+")) -> ("lion" "chases" "cow" "+"))
If someone is round and they eat the cow then they chase the squirrel.
((("someone" "is" "round" "+") ("someone" "eats" "cow" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the squirrel and the squirrel eats the cow then the cow is green.
((("someone" "chases" "squirrel" "+") ("squirrel" "eats" "cow" "+")) -> ("cow" "is" "green" "+"))
The lion eats the cow.
True
1
proof
[(triple5)]
("lion" "eats" "cow" "+")
triple5
The lion is not blue.
False
1
inv-proof
[(triple7)]
("lion" "is" "blue" "-")
triple7
The lion chases the squirrel.
True
2
proof
[(((triple6) -> rule2) OR ((triple8 triple5) -> rule5))]
("lion" "chases" "squirrel" "+")
((triple6) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
((triple8 triple5) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The lion does not chase the squirrel.
False
2
inv-proof
[(((triple6) -> rule2) OR ((triple8 triple5) -> rule5))]
("lion" "chases" "squirrel" "-")
((triple6) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
((triple8 triple5) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The cow is green.
True
4
proof
[(((((triple6) -> rule2) triple11) -> rule6) OR ((((triple8 triple5) -> rule5) triple11) -> rule6))]
("cow" "is" "green" "+")
((((triple6) -> (rule2 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((((triple8 triple5) -> (rule5 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The cow is not green.
False
4
inv-proof
[(((((triple6) -> rule2) triple11) -> rule6) OR ((((triple8 triple5) -> rule5) triple11) -> rule6))]
("cow" "is" "green" "-")
((((triple6) -> (rule2 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((((triple8 triple5) -> (rule5 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The cow chases the cow.
True
5
proof
[(((((((triple6) -> rule2) triple11) -> rule6)) -> rule3) OR ((((((triple8 triple5) -> rule5) triple11) -> rule6)) -> rule3))]
("cow" "chases" "cow" "+")
((((((triple6) -> (rule2 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((((triple8 triple5) -> (rule5 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The cow does not chase the cow.
False
5
inv-proof
[(((((((triple6) -> rule2) triple11) -> rule6)) -> rule3) OR ((((((triple8 triple5) -> rule5) triple11) -> rule6)) -> rule3))]
("cow" "chases" "cow" "-")
((((((triple6) -> (rule2 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((((triple8 triple5) -> (rule5 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The cow chases the squirrel.
Unknown
rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "squirrel" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The cow does not see the squirrel.
Unknown
inv-random
[@0: The cow sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "squirrel" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow eats the lion.[(triple1)] The cow is round.[(triple2)] The cow sees the lion.[(triple3 OR ((triple11) -> rule1) OR ((triple5) -> rule1))] The lion chases the cow.[(triple4)] The lion eats the cow.[(triple5)] The lion eats the squirrel.[(triple6)] The lion is blue.[(triple7)] The lion is round.[(triple8)] The squirrel chases the cow.[(triple9)] The squirrel chases the lion.[(triple10)] The squirrel eats the cow.[(triple11)] The squirrel sees the lion.[(triple12)] @1: The lion chases the squirrel.[(((triple6) -> rule2) OR ((triple8 triple5) -> rule5))] @2: The cow is green.[(((((triple6) -> rule2) triple11) -> rule6) OR ((((triple8 triple5) -> rule5) triple11) -> rule6))] @3: The cow chases the cow.[(((((((triple6) -> rule2) triple11) -> rule6)) -> rule3) OR ((((((triple8 triple5) -> rule5) triple11) -> rule6)) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
((triple11) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
((triple5) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple6
The lion is blue.
("lion" "is" "blue" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple9
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple10
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple6) -> (rule2 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
((triple8 triple5) -> (rule5 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The cow is green.
("cow" "is" "green" "+")
((((triple6) -> (rule2 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
((((triple8 triple5) -> (rule5 % int2)) triple11) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple6) -> (rule2 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3
((((((triple8 triple5) -> (rule5 % int3)) triple11) -> (rule6 % int2))) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int3