The cat chases the cow. The cat chases the lion. The cat does not need the cow. The cat needs the tiger. The cat sees the tiger. The cow is nice. The cow needs the tiger. The cow sees the lion. The lion needs the cat. The lion sees the cat. The lion sees the cow. The tiger is red. The tiger needs the cat. The tiger sees the cat. The tiger sees the cow. If something is round then it chases the tiger. If something chases the lion and the lion is not cold then it does not need the tiger. If something sees the lion then it does not see the cat. If something sees the lion and it is round then it does not see the tiger. If something is nice and it does not see the cat then it needs the cow. If the tiger does not see the cat then the cat chases the tiger. If something needs the cow then the cow needs the lion. If something needs the cat and it chases the tiger then the cat does not need the tiger.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat does not need the cow.
("cat" "needs" "cow" "-")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something is round then it chases the tiger.
((("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the lion and the lion is not cold then it does not need the tiger.
((("something" "chases" "lion" "+") ("lion" "is" "cold" "~")) -> ("something" "needs" "tiger" "-"))
If something sees the lion then it does not see the cat.
((("something" "sees" "lion" "+")) -> ("something" "sees" "cat" "-"))
If something sees the lion and it is round then it does not see the tiger.
((("something" "sees" "lion" "+") ("something" "is" "round" "+")) -> ("something" "sees" "tiger" "-"))
If something is nice and it does not see the cat then it needs the cow.
((("something" "is" "nice" "+") ("something" "sees" "cat" "~")) -> ("something" "needs" "cow" "+"))
If the tiger does not see the cat then the cat chases the tiger.
((("tiger" "sees" "cat" "~")) -> ("cat" "chases" "tiger" "+"))
If something needs the cow then the cow needs the lion.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "lion" "+"))
If something needs the cat and it chases the tiger then the cat does not need the tiger.
((("something" "needs" "cat" "+") ("something" "chases" "tiger" "+")) -> ("cat" "needs" "tiger" "-"))
The cat chases the cow.
True
1
proof
[(triple1)]
("cat" "chases" "cow" "+")
triple1
The tiger is not red.
False
1
inv-proof
[(triple12)]
("tiger" "is" "red" "-")
triple12
The cow does not see the cat.
True
2
proof
[(((triple8) -> rule3))]
("cow" "sees" "cat" "-")
((triple8) -> (rule3 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow sees the cat.
False
2
inv-proof
[(((triple8) -> rule3))]
("cow" "sees" "cat" "+")
((triple8) -> (rule3 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow needs the cow.
True
4
proof
[(((triple6 ((triple8) -> rule3)) -> rule5))]
("cow" "needs" "cow" "+")
((triple6 ((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
The cow does not need the cow.
False
4
inv-proof
[(((triple6 ((triple8) -> rule3)) -> rule5))]
("cow" "needs" "cow" "-")
((triple6 ((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
The cow needs the lion.
True
5
proof
[(((((triple6 ((triple8) -> rule3)) -> rule5)) -> rule7))]
("cow" "needs" "lion" "+")
((((triple6 ((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not see the cat.
("cow" "sees" "cat" "-")
int3
The cow does not need the lion.
False
5
inv-proof
[(((((triple6 ((triple8) -> rule3)) -> rule5)) -> rule7))]
("cow" "needs" "lion" "-")
((((triple6 ((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not see the cat.
("cow" "sees" "cat" "-")
int3
The tiger does not need the cow.
Unknown
inv-rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "cow" "-")
The cow chases the tiger.
Unknown
rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The lion chases the tiger.
Unknown
rconc
[@1: The lion chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "tiger" "+")
The cow does not chase the cat.
Unknown
inv-random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
@0: The cat chases the cow.[(triple1)] The cat chases the lion.[(triple2)] The cat does not need the cow.[(triple3)] The cat needs the tiger.[(triple4)] The cat sees the tiger.[(triple5)] The cow is nice.[(triple6)] The cow needs the tiger.[(triple7)] The cow sees the lion.[(triple8)] The lion needs the cat.[(triple9)] The lion sees the cat.[(triple10)] The lion sees the cow.[(triple11)] The tiger is red.[(triple12)] The tiger needs the cat.[(triple13)] The tiger sees the cat.[(triple14)] The tiger sees the cow.[(triple15)] @1: The cow does not see the cat.[(((triple8) -> rule3))] @2: The cow needs the cow.[(((triple6 ((triple8) -> rule3)) -> rule5))] @3: The cow needs the lion.[(((((triple6 ((triple8) -> rule3)) -> rule5)) -> rule7))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple2
The cat does not need the cow.
("cat" "needs" "cow" "-")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple5
The cow is nice.
("cow" "is" "nice" "+")
triple6
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
The cow sees the lion.
("cow" "sees" "lion" "+")
triple8
The lion needs the cat.
("lion" "needs" "cat" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The lion sees the cow.
("lion" "sees" "cow" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple13
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple14
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple15
The cow does not see the cat.
("cow" "sees" "cat" "-")
((triple8) -> (rule3 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple6 ((triple8) -> (rule3 % int2))) -> (rule5 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
((((triple6 ((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not see the cat.
("cow" "sees" "cat" "-")
int3