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