The cow is big. The lion is rough. The lion likes the cow. The tiger eats the cow. The tiger is cold. The tiger is rough. The tiger likes the lion. If someone eats the cow then they are blue. If someone is big then they eat the cow.
The cow is big.
("cow" "is" "big" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If someone eats the cow then they are blue.
((("someone" "eats" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone is big then they eat the cow.
((("someone" "is" "big" "+")) -> ("someone" "eats" "cow" "+"))
The tiger is rough.
True
1
proof
[(triple6)]
("tiger" "is" "rough" "+")
triple6
The cow is not big.
False
1
inv-proof
[(triple1)]
("cow" "is" "big" "-")
triple1
The tiger is blue.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "is" "blue" "+")
((triple4) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "eats" "cow" "-")
((triple1) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("cow" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("cow" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The lion is not blue.
Unknown
inv-rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "is" "blue" "-")
The lion eats the cow.
Unknown
rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "eats" "cow" "+")
The cow does not chase the lion.
Unknown
inv-random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The cow does not eat the tiger.
Unknown
inv-random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
@0: The cow is big.[(triple1)] The lion is rough.[(triple2)] The lion likes the cow.[(triple3)] The tiger eats the cow.[(triple4)] The tiger is cold.[(triple5)] The tiger is rough.[(triple6)] The tiger likes the lion.[(triple7)] @1: The cow eats the cow.[(((triple1) -> rule2))] The tiger is blue.[(((triple4) -> rule1))] @2: The cow is blue.[(((((triple1) -> rule2)) -> rule1))]
The cow is big.
("cow" "is" "big" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The lion likes the cow.
("lion" "likes" "cow" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger is rough.
("tiger" "is" "rough" "+")
triple6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple7
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple1) -> (rule2 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple4) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2