The cow eats the lion. The cow is rough. The cow likes the squirrel. The cow needs the squirrel. The lion eats the cow. The lion likes the cow. The lion needs the squirrel. The squirrel eats the cow. The squirrel is round. The squirrel likes the lion. If someone eats the lion then the lion is green. If someone is round then they eat the lion. Green people are round.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone is round then they eat the lion.
((("someone" "is" "round" "+")) -> ("someone" "eats" "lion" "+"))
Green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
The cow likes the squirrel.
True
1
proof
[(triple3)]
("cow" "likes" "squirrel" "+")
triple3
The squirrel does not eat the cow.
False
1
inv-proof
[(triple8)]
("squirrel" "eats" "cow" "-")
triple8
The lion is green.
True
2
proof
[(((triple1) -> rule1) OR ((((triple9) -> rule2)) -> rule1))]
("lion" "is" "green" "+")
((triple1) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel does not eat the lion.
False
2
inv-proof
[(((triple9) -> rule2))]
("squirrel" "eats" "lion" "-")
((triple9) -> (rule2 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The lion is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule3) OR ((((((triple9) -> rule2)) -> rule1)) -> rule3))]
("lion" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The lion is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3) OR ((((((triple9) -> rule2)) -> rule1)) -> rule3))]
("lion" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The lion eats the lion.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((((((((triple9) -> rule2)) -> rule1)) -> rule3)) -> rule2))]
("lion" "eats" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int4
The lion does not eat the lion.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((((((((triple9) -> rule2)) -> rule1)) -> rule3)) -> rule2))]
("lion" "eats" "lion" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int4
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The cow does not eat the squirrel.
Unknown
inv-random
[@0: The cow eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "squirrel" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The lion does not eat the squirrel.
Unknown
inv-random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The squirrel does not need the lion.
Unknown
inv-random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The cow eats the lion.[(triple1)] The cow is rough.[(triple2)] The cow likes the squirrel.[(triple3)] The cow needs the squirrel.[(triple4)] The lion eats the cow.[(triple5)] The lion likes the cow.[(triple6)] The lion needs the squirrel.[(triple7)] The squirrel eats the cow.[(triple8)] The squirrel is round.[(triple9)] The squirrel likes the lion.[(triple10)] @1: The lion is green.[(((triple1) -> rule1) OR ((((triple9) -> rule2)) -> rule1))] The squirrel eats the lion.[(((triple9) -> rule2))] @2: The lion is round.[(((((triple1) -> rule1)) -> rule3) OR ((((((triple9) -> rule2)) -> rule1)) -> rule3))] @3: The lion eats the lion.[(((((((triple1) -> rule1)) -> rule3)) -> rule2) OR ((((((((triple9) -> rule2)) -> rule1)) -> rule3)) -> rule2))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion likes the cow.
("lion" "likes" "cow" "+")
triple6
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple7
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
((triple1) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
((triple9) -> (rule2 % int1))
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple9) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int3
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((((triple9) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
int4