The cat needs the mouse. The mouse needs the cat. If something is young then it sees the mouse. If something needs the mouse and it needs the cat then it eats the mouse. If something sees the mouse then it needs the mouse. If something sees the cat and the cat is blue then it sees the mouse. If something is round then it is big. If something sees the cat then it eats the cat. If something eats the cat and the cat needs the mouse then the cat is round. If something needs the mouse then the mouse sees the cat.
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something is young then it sees the mouse.
((("something" "is" "young" "+")) -> ("something" "sees" "mouse" "+"))
If something needs the mouse and it needs the cat then it eats the mouse.
((("something" "needs" "mouse" "+") ("something" "needs" "cat" "+")) -> ("something" "eats" "mouse" "+"))
If something sees the mouse then it needs the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If something sees the cat and the cat is blue then it sees the mouse.
((("something" "sees" "cat" "+") ("cat" "is" "blue" "+")) -> ("something" "sees" "mouse" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something sees the cat then it eats the cat.
((("something" "sees" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat and the cat needs the mouse then the cat is round.
((("something" "eats" "cat" "+") ("cat" "needs" "mouse" "+")) -> ("cat" "is" "round" "+"))
If something needs the mouse then the mouse sees the cat.
((("something" "needs" "mouse" "+")) -> ("mouse" "sees" "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 mouse sees the cat.
True
2
proof
[(((triple1) -> rule8))]
("mouse" "sees" "cat" "+")
((triple1) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse does not see the cat.
False
2
inv-proof
[(((triple1) -> rule8))]
("mouse" "sees" "cat" "-")
((triple1) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse eats the cat.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("mouse" "eats" "cat" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The mouse does not eat the cat.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("mouse" "eats" "cat" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is round.
True
5
proof
[(((((((triple1) -> rule8)) -> rule6) triple1) -> rule7))]
("cat" "is" "round" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat is not round.
False
5
inv-proof
[(((((((triple1) -> rule8)) -> rule6) triple1) -> rule7))]
("cat" "is" "round" "-")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-rconc
[@3: The mouse eats the mouse.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The cat needs the mouse.[(triple1)] The mouse needs the cat.[(triple2)] @1: The mouse sees the cat.[(((triple1) -> rule8))] @2: The mouse eats the cat.[(((((triple1) -> rule8)) -> rule6))] @3: The cat is round.[(((((((triple1) -> rule8)) -> rule6) triple1) -> rule7))] @4: The cat is big.[(((((((((triple1) -> rule8)) -> rule6) triple1) -> rule7)) -> rule5))]
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
((triple1) -> (rule8 % int1))
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2)) triple1) -> (rule7 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int3
The cat is big.
("cat" "is" "big" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule6 % int3)) triple1) -> (rule7 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
int4