The cat needs the mouse. The cat visits the mouse. The mouse needs the cat. If something chases the mouse and the mouse needs the cat then it visits the mouse. If something is green then it needs the mouse. If something chases the cat and the cat chases the mouse then it visits the cat. If something visits the mouse then it visits the cat. If something visits the cat then it needs the cat. If something chases the mouse then it visits the cat. If something chases the cat then the cat visits the mouse. If something needs the mouse then the mouse chases the cat.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something chases the mouse and the mouse needs the cat then it visits the mouse.
((("something" "chases" "mouse" "+") ("mouse" "needs" "cat" "+")) -> ("something" "visits" "mouse" "+"))
If something is green then it needs the mouse.
((("something" "is" "green" "+")) -> ("something" "needs" "mouse" "+"))
If something chases the cat and the cat chases the mouse then it visits the cat.
((("something" "chases" "cat" "+") ("cat" "chases" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something visits the mouse then it visits the cat.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something visits the cat then it needs the cat.
((("something" "visits" "cat" "+")) -> ("something" "needs" "cat" "+"))
If something chases the mouse then it visits the cat.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something chases the cat then the cat visits the mouse.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If something needs the mouse then the mouse chases the cat.
((("something" "needs" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
The cat needs the mouse.
True
1
proof
[(triple1)]
("cat" "needs" "mouse" "+")
triple1
The cat does not need the mouse.
False
1
inv-proof
[(triple1)]
("cat" "needs" "mouse" "-")
triple1
The cat visits the cat.
True
2
proof
[(((triple2) -> rule4) OR ((((((triple1) -> rule8)) -> rule7)) -> rule4))]
("cat" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((((triple1) -> rule8)) -> rule7)) -> rule4))]
("cat" "visits" "cat" "-")
((triple2) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The cat needs the cat.
True
3
proof
[(((((triple2) -> rule4)) -> rule5) OR ((((((((triple1) -> rule8)) -> rule7)) -> rule4)) -> rule5))]
("cat" "needs" "cat" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The cat does not need the cat.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5) OR ((((((((triple1) -> rule8)) -> rule7)) -> rule4)) -> rule5))]
("cat" "needs" "cat" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4
The mouse does not visit the cat.
Unknown
inv-rconc
[@2: The mouse visits the cat.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("mouse" "visits" "cat" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The cat does not chase the mouse.
Unknown
inv-random
[@0: The cat chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "mouse" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat needs the mouse.[(triple1)] The cat visits the mouse.[(triple2 OR ((((triple1) -> rule8)) -> rule7))] The mouse needs the cat.[(triple3)] @1: The cat visits the cat.[(((triple2) -> rule4) OR ((((((triple1) -> rule8)) -> rule7)) -> rule4))] The mouse chases the cat.[(((triple1) -> rule8))] @2: The cat needs the cat.[(((((triple2) -> rule4)) -> rule5) OR ((((((((triple1) -> rule8)) -> rule7)) -> rule4)) -> rule5))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int2
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple3
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple2) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple1) -> (rule8 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((((((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int4