The cow is red. The cow is not round. The cow needs the tiger. The cow does not see the tiger. The tiger does not eat the cow. The tiger is cold. The tiger is kind. The tiger is nice. The tiger is red. The tiger is round. The tiger needs the cow. The tiger sees the cow. If the tiger is round and the tiger sees the cow then the tiger needs the cow. If something needs the tiger then it is not nice. If something is nice then it needs the cow.
The cow is red.
("cow" "is" "red" "+")
The cow is not round.
("cow" "is" "round" "-")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If the tiger is round and the tiger sees the cow then the tiger needs the cow.
((("tiger" "is" "round" "+") ("tiger" "sees" "cow" "+")) -> ("tiger" "needs" "cow" "+"))
If something needs the tiger then it is not nice.
((("something" "needs" "tiger" "+")) -> ("something" "is" "nice" "-"))
If something is nice then it needs the cow.
((("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
The tiger sees the cow.
True
1
proof
[(triple12)]
("tiger" "sees" "cow" "+")
triple12
The tiger does not need the cow.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule3) OR ((triple10 triple12) -> rule1))]
("tiger" "needs" "cow" "-")
triple11
((triple8) -> (rule3 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
((triple10 triple12) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow does not see the tiger.[(triple4)] The cow is not round.[(triple2)] The cow is red.[(triple1)] The cow needs the tiger.[(triple3)] The tiger does not eat the cow.[(triple5)] The tiger is cold.[(triple6)] The tiger is kind.[(triple7)] The tiger is nice.[(triple8)] The tiger is red.[(triple9)] The tiger is round.[(triple10)] The tiger needs the cow.[(triple11 OR ((triple8) -> rule3) OR ((triple10 triple12) -> rule1))] The tiger sees the cow.[(triple12)] @1: The cow is not nice.[(((triple3) -> rule2))]
The cow does not see the tiger.
("cow" "sees" "tiger" "-")
triple4
The cow is not round.
("cow" "is" "round" "-")
triple2
The cow is red.
("cow" "is" "red" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The tiger does not eat the cow.
("tiger" "eats" "cow" "-")
triple5
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple11
((triple8) -> (rule3 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
((triple10 triple12) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple12
The cow is not nice.
("cow" "is" "nice" "-")
((triple3) -> (rule2 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1