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