The cat does not chase the lion. The cow is nice. The lion sees the cow. The tiger likes the cow. If someone chases the cat and the cat likes the cow then the cow sees the tiger. If someone sees the cow then the cow is round. If the cat is young and the cat is kind then the cat is red. If someone sees the cat then the cat chases the cow. If someone is round and nice then they chase the lion. If the tiger likes the lion and the lion likes the cat then the tiger does not see the lion.
The cat does not chase the lion.
("cat" "chases" "lion" "-")
The cow is nice.
("cow" "is" "nice" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone chases the cat and the cat likes the cow then the cow sees the tiger.
((("someone" "chases" "cat" "+") ("cat" "likes" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If someone sees the cow then the cow is round.
((("someone" "sees" "cow" "+")) -> ("cow" "is" "round" "+"))
If the cat is young and the cat is kind then the cat is red.
((("cat" "is" "young" "+") ("cat" "is" "kind" "+")) -> ("cat" "is" "red" "+"))
If someone sees the cat then the cat chases the cow.
((("someone" "sees" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If someone is round and nice then they chase the lion.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "chases" "lion" "+"))
If the tiger likes the lion and the lion likes the cat then the tiger does not see the lion.
((("tiger" "likes" "lion" "+") ("lion" "likes" "cat" "+")) -> ("tiger" "sees" "lion" "-"))
The tiger likes the cow.
True
1
proof
[(triple4)]
("tiger" "likes" "cow" "+")
triple4
The lion does not see the cow.
False
1
inv-proof
[(triple3)]
("lion" "sees" "cow" "-")
triple3
The cow is round.
True
2
proof
[(((triple3) -> rule2))]
("cow" "is" "round" "+")
((triple3) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is not round.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "is" "round" "-")
((triple3) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the lion.
True
4
proof
[(((((triple3) -> rule2) triple2) -> rule5))]
("cow" "chases" "lion" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cow does not chase the lion.
False
4
inv-proof
[(((((triple3) -> rule2) triple2) -> rule5))]
("cow" "chases" "lion" "-")
((((triple3) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "red" "-")
The cow sees the tiger.
Unknown
rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "tiger" "+")
The cat does not chase the cow.
Unknown
inv-rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "cow" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The tiger does not see the lion.
Unknown
inv-random
[@0: The tiger sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "lion" "-")
The cow chases the cat.
Unknown
random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "+")
@0: The cat does not chase the lion.[(triple1)] The cow is nice.[(triple2)] The lion sees the cow.[(triple3)] The tiger likes the cow.[(triple4)] @1: The cow is round.[(((triple3) -> rule2))] @2: The cow chases the lion.[(((((triple3) -> rule2) triple2) -> rule5))]
The cat does not chase the lion.
("cat" "chases" "lion" "-")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The lion sees the cow.
("lion" "sees" "cow" "+")
triple3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
((triple3) -> (rule2 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the lion.
("cow" "chases" "lion" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule5 % int1))
The cow chases the lion.
("cow" "chases" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
int2