The cow is nice. The cow sees the lion. The lion chases the cow. The lion likes the tiger. The lion sees the tiger. The tiger chases the cow. The tiger sees the cow. If something is nice and it chases the tiger then it likes the lion. If something likes the cow then it is round. If something sees the tiger then it likes the cow. If something likes the cow and the cow is blue then the cow likes the tiger. If something chases the cow and the cow sees the lion then the lion sees the cow. If something chases the cow then the cow is cold.
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something is nice and it chases the tiger then it likes the lion.
((("something" "is" "nice" "+") ("something" "chases" "tiger" "+")) -> ("something" "likes" "lion" "+"))
If something likes the cow then it is round.
((("something" "likes" "cow" "+")) -> ("something" "is" "round" "+"))
If something sees the tiger then it likes the cow.
((("something" "sees" "tiger" "+")) -> ("something" "likes" "cow" "+"))
If something likes the cow and the cow is blue then the cow likes the tiger.
((("something" "likes" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "likes" "tiger" "+"))
If something chases the cow and the cow sees the lion then the lion sees the cow.
((("something" "chases" "cow" "+") ("cow" "sees" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If something chases the cow then the cow is cold.
((("something" "chases" "cow" "+")) -> ("cow" "is" "cold" "+"))
The lion chases the cow.
True
1
proof
[(triple3)]
("lion" "chases" "cow" "+")
triple3
The cow does not see the lion.
False
1
inv-proof
[(triple2)]
("cow" "sees" "lion" "-")
triple2
The cow is cold.
True
2
proof
[(((triple3) -> rule6) OR ((triple6) -> rule6))]
("cow" "is" "cold" "+")
((triple3) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple6) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The lion does not see the cow.
False
3
inv-proof
[(((triple3 triple2) -> rule5) OR ((triple6 triple2) -> rule5))]
("lion" "sees" "cow" "-")
((triple3 triple2) -> (rule5 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((triple6 triple2) -> (rule5 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is round.
True
3
proof
[(((((triple5) -> rule3)) -> rule2))]
("lion" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The lion is not round.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule2))]
("lion" "is" "round" "-")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2
The tiger is not round.
Unknown
inv-rconc
[@2: The tiger is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("tiger" "is" "round" "-")
The cow likes the lion.
Unknown
rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "lion" "+")
The cow is not round.
Unknown
inv-rconc
[@2: The cow is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("cow" "is" "round" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cow is nice.[(triple1)] The cow sees the lion.[(triple2)] The lion chases the cow.[(triple3)] The lion likes the tiger.[(triple4)] The lion sees the tiger.[(triple5)] The tiger chases the cow.[(triple6)] The tiger sees the cow.[(triple7)] @1: The cow is cold.[(((triple3) -> rule6) OR ((triple6) -> rule6))] The lion likes the cow.[(((triple5) -> rule3))] The lion sees the cow.[(((triple3 triple2) -> rule5) OR ((triple6 triple2) -> rule5))] @2: The lion is round.[(((((triple5) -> rule3)) -> rule2))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple6
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple7
The cow is cold.
("cow" "is" "cold" "+")
((triple3) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((triple6) -> (rule6 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple5) -> (rule3 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple3 triple2) -> (rule5 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
((triple6 triple2) -> (rule5 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion likes the cow.
("lion" "likes" "cow" "+")
int2