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