The cow visits the lion. The lion needs the tiger. The tiger is not blue. If something is nice and it chases the tiger then it needs the cow. If something needs the tiger then it chases the cow. If something chases the cow then the cow needs the tiger.
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
If something is nice and it chases the tiger then it needs the cow.
((("something" "is" "nice" "+") ("something" "chases" "tiger" "+")) -> ("something" "needs" "cow" "+"))
If something needs the tiger then it chases the cow.
((("something" "needs" "tiger" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow then the cow needs the tiger.
((("something" "chases" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
The cow visits the lion.
True
1
proof
[(triple1)]
("cow" "visits" "lion" "+")
triple1
The lion does not need the tiger.
False
1
inv-proof
[(triple2)]
("lion" "needs" "tiger" "-")
triple2
The lion chases the cow.
True
2
proof
[(((triple2) -> rule2))]
("lion" "chases" "cow" "+")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "chases" "cow" "-")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The cow needs the tiger.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("cow" "needs" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The cow does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("cow" "needs" "tiger" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion does not need the cow.
Unknown
inv-rconc
[@1: The lion needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "cow" "-")
The tiger needs the cow.
Unknown
rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "cow" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "needs" "cow" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The tiger does not need the lion.
Unknown
inv-random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
@0: The cow visits the lion.[(triple1)] The lion needs the tiger.[(triple2)] The tiger is not blue.[(triple3)] @1: The lion chases the cow.[(((triple2) -> rule2))] @2: The cow needs the tiger.[(((((triple2) -> rule2)) -> rule3))] @3: The cow chases the cow.[(((((((triple2) -> rule2)) -> rule3)) -> rule2))]
The cow visits the lion.
("cow" "visits" "lion" "+")
triple1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple2
The tiger is not blue.
("tiger" "is" "blue" "-")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
((triple2) -> (rule2 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
int3