The cow likes the tiger. The lion is big. The squirrel is big. The tiger eats the lion. If someone eats the cow then the cow eats the tiger. If the squirrel likes the cow and the squirrel likes the tiger then the squirrel likes the lion. If the squirrel eats the cow then the cow is nice. If someone eats the cow then the cow eats the lion. If the tiger eats the squirrel then the squirrel sees the lion. If someone eats the lion then they eat the squirrel. If someone likes the cow then the cow is big. If someone likes the tiger then they eat the cow.
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If someone eats the cow then the cow eats the tiger.
((("someone" "eats" "cow" "+")) -> ("cow" "eats" "tiger" "+"))
If the squirrel likes the cow and the squirrel likes the tiger then the squirrel likes the lion.
((("squirrel" "likes" "cow" "+") ("squirrel" "likes" "tiger" "+")) -> ("squirrel" "likes" "lion" "+"))
If the squirrel eats the cow then the cow is nice.
((("squirrel" "eats" "cow" "+")) -> ("cow" "is" "nice" "+"))
If someone eats the cow then the cow eats the lion.
((("someone" "eats" "cow" "+")) -> ("cow" "eats" "lion" "+"))
If the tiger eats the squirrel then the squirrel sees the lion.
((("tiger" "eats" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If someone eats the lion then they eat the squirrel.
((("someone" "eats" "lion" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone likes the cow then the cow is big.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "big" "+"))
If someone likes the tiger then they eat the cow.
((("someone" "likes" "tiger" "+")) -> ("someone" "eats" "cow" "+"))
The cow likes the tiger.
True
1
proof
[(triple1)]
("cow" "likes" "tiger" "+")
triple1
The lion is not big.
False
1
inv-proof
[(triple2)]
("lion" "is" "big" "-")
triple2
The cow eats the cow.
True
2
proof
[(((triple1) -> rule8))]
("cow" "eats" "cow" "+")
((triple1) -> (rule8 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The tiger does not eat the squirrel.
False
2
inv-proof
[(((triple4) -> rule6))]
("tiger" "eats" "squirrel" "-")
((triple4) -> (rule6 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The cow eats the tiger.
True
3
proof
[(((((triple1) -> rule8)) -> rule1))]
("cow" "eats" "tiger" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not eat the lion.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("cow" "eats" "lion" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the squirrel.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
("cow" "eats" "squirrel" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow does not eat the squirrel.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
("cow" "eats" "squirrel" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The lion does not eat the squirrel.
Unknown
inv-rconc
[@1: The lion eats the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "squirrel" "-")
The cow is big.
Unknown
rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "big" "+")
The tiger does not eat the cow.
Unknown
inv-rconc
[@1: The tiger eats the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "cow" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The squirrel eats the tiger.
Unknown
random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
@0: The cow likes the tiger.[(triple1)] The lion is big.[(triple2)] The squirrel is big.[(triple3)] The tiger eats the lion.[(triple4)] @1: The cow eats the cow.[(((triple1) -> rule8))] The tiger eats the squirrel.[(((triple4) -> rule6))] @2: The cow eats the lion.[(((((triple1) -> rule8)) -> rule4))] The cow eats the tiger.[(((((triple1) -> rule8)) -> rule1))] The squirrel sees the lion.[(((((triple4) -> rule6)) -> rule5))] @3: The cow eats the squirrel.[(((((((triple1) -> rule8)) -> rule4)) -> rule6))]
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple4
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule8 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple4) -> (rule6 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((((triple1) -> (rule8 % int2))) -> (rule1 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3