The cow does not chase the tiger. The lion eats the tiger. The mouse chases the tiger. The tiger does not eat the mouse. If something chases the tiger then the tiger needs the cow. If something chases the cow and it is not red then the cow needs the lion. If the lion needs the cow then the cow chases the lion. If the mouse chases the lion then the lion is round. If something needs the cow then it does not need the tiger. If something needs the lion then the lion is rough.
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
If something chases the tiger then the tiger needs the cow.
((("something" "chases" "tiger" "+")) -> ("tiger" "needs" "cow" "+"))
If something chases the cow and it is not red then the cow needs the lion.
((("something" "chases" "cow" "+") ("something" "is" "red" "~")) -> ("cow" "needs" "lion" "+"))
If the lion needs the cow then the cow chases the lion.
((("lion" "needs" "cow" "+")) -> ("cow" "chases" "lion" "+"))
If the mouse chases the lion then the lion is round.
((("mouse" "chases" "lion" "+")) -> ("lion" "is" "round" "+"))
If something needs the cow then it does not need the tiger.
((("something" "needs" "cow" "+")) -> ("something" "needs" "tiger" "-"))
If something needs the lion then the lion is rough.
((("something" "needs" "lion" "+")) -> ("lion" "is" "rough" "+"))
The lion eats the tiger.
True
1
proof
[(triple2)]
("lion" "eats" "tiger" "+")
triple2
The lion does not eat the tiger.
False
1
inv-proof
[(triple2)]
("lion" "eats" "tiger" "-")
triple2
The tiger needs the cow.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "needs" "cow" "+")
((triple3) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the cow.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "needs" "cow" "-")
((triple3) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("tiger" "needs" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger needs the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("tiger" "needs" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow does not need the lion.
Unknown
inv-rconc
[@1: The cow needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "lion" "-")
The lion is rough.
Unknown
rconc
[@2: The lion is rough.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "is" "rough" "+")
The lion is not round.
Unknown
inv-rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "round" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
The cow does not eat the mouse.
Unknown
inv-random
[@0: The cow eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "mouse" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow does not chase the tiger.[(triple1)] The lion eats the tiger.[(triple2)] The mouse chases the tiger.[(triple3)] The tiger does not eat the mouse.[(triple4)] @1: The tiger needs the cow.[(((triple3) -> rule1))] @2: The tiger does not need the tiger.[(((((triple3) -> rule1)) -> rule5))]
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
triple1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple3
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple3) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The tiger does not need the tiger.
("tiger" "needs" "tiger" "-")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2