The cow is green. The lion eats the cow. The tiger eats the lion. If something likes the cow then it is green. All green things are nice. If something likes the cow then the cow likes the tiger. If something eats the lion then the lion likes the tiger. If something likes the tiger and it eats the cow then the tiger does not like the cow. If something likes the tiger then it chases the lion. If something is green then it likes the lion. If something is green then it likes the cow.
The cow is green.
("cow" "is" "green" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If something likes the cow then it is green.
((("something" "likes" "cow" "+")) -> ("something" "is" "green" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something likes the cow then the cow likes the tiger.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "tiger" "+"))
If something eats the lion then the lion likes the tiger.
((("something" "eats" "lion" "+")) -> ("lion" "likes" "tiger" "+"))
If something likes the tiger and it eats the cow then the tiger does not like the cow.
((("something" "likes" "tiger" "+") ("something" "eats" "cow" "+")) -> ("tiger" "likes" "cow" "-"))
If something likes the tiger then it chases the lion.
((("something" "likes" "tiger" "+")) -> ("something" "chases" "lion" "+"))
If something is green then it likes the lion.
((("something" "is" "green" "+")) -> ("something" "likes" "lion" "+"))
If something is green then it likes the cow.
((("something" "is" "green" "+")) -> ("something" "likes" "cow" "+"))
The tiger eats the lion.
True
1
proof
[(triple3)]
("tiger" "eats" "lion" "+")
triple3
The tiger does not eat the lion.
False
1
inv-proof
[(triple3)]
("tiger" "eats" "lion" "-")
triple3
The lion likes the tiger.
True
2
proof
[(((triple3) -> rule4))]
("lion" "likes" "tiger" "+")
((triple3) -> (rule4 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "is" "nice" "-")
((triple1) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow likes the tiger.
True
3
proof
[(((((triple1) -> rule8)) -> rule3))]
("cow" "likes" "tiger" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The tiger likes the cow.
False
4
inv-proof
[(((((triple3) -> rule4) triple2) -> rule5))]
("tiger" "likes" "cow" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The cow chases the lion.
True
4
proof
[(((((((triple1) -> rule8)) -> rule3)) -> rule6))]
("cow" "chases" "lion" "+")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow does not chase the lion.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule3)) -> rule6))]
("cow" "chases" "lion" "-")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The lion does not like the lion.
Unknown
inv-rconc
[@3: The lion likes the lion.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule8 <- FAIL)]]
("lion" "likes" "lion" "-")
The tiger likes the lion.
Unknown
rconc
[@2: The tiger likes the lion.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("tiger" "likes" "lion" "+")
The lion is not green.
Unknown
inv-rconc
[@2: The lion is green.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("lion" "is" "green" "-")
The lion likes the cow.
Unknown
rconc
[@2: The lion likes the cow.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("lion" "likes" "cow" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
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 tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The cow is green.[(triple1)] The lion eats the cow.[(triple2)] The tiger eats the lion.[(triple3)] @1: The cow is nice.[(((triple1) -> rule2))] The cow likes the cow.[(((triple1) -> rule8))] The cow likes the lion.[(((triple1) -> rule7))] The lion likes the tiger.[(((triple3) -> rule4))] @2: The cow likes the tiger.[(((((triple1) -> rule8)) -> rule3))] The lion chases the lion.[(((((triple3) -> rule4)) -> rule6))] The tiger does not like the cow.[(((((triple3) -> rule4) triple2) -> rule5))] @3: The cow chases the lion.[(((((((triple1) -> rule8)) -> rule3)) -> rule6))]
The cow is green.
("cow" "is" "green" "+")
triple1
The lion eats the cow.
("lion" "eats" "cow" "+")
triple2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
((triple1) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
((triple1) -> (rule7 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
((triple3) -> (rule4 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
((((triple3) -> (rule4 % int2)) triple2) -> (rule5 % int1))
The tiger does not like the cow.
("tiger" "likes" "cow" "-")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The cow chases the lion.
("cow" "chases" "lion" "+")
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3