The mouse chases the rabbit. The mouse eats the rabbit. The mouse is big. The mouse is not blue. The rabbit chases the mouse. The rabbit is big. The rabbit is red. If the mouse visits the rabbit then the rabbit does not eat the mouse. If the mouse eats the rabbit then the mouse is not cold. If someone chases the mouse then the mouse visits the rabbit. If someone chases the rabbit then they chase the mouse. If someone chases the rabbit then they eat the rabbit. If the rabbit eats the mouse and the mouse visits the rabbit then the rabbit is cold. If the mouse is red then the mouse chases the rabbit. If the mouse does not visit the rabbit and the rabbit does not visit the mouse then the mouse is big.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
If the mouse visits the rabbit then the rabbit does not eat the mouse.
((("mouse" "visits" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "-"))
If the mouse eats the rabbit then the mouse is not cold.
((("mouse" "eats" "rabbit" "+")) -> ("mouse" "is" "cold" "-"))
If someone chases the mouse then the mouse visits the rabbit.
((("someone" "chases" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If someone chases the rabbit then they chase the mouse.
((("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the rabbit then they eat the rabbit.
((("someone" "chases" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If the rabbit eats the mouse and the mouse visits the rabbit then the rabbit is cold.
((("rabbit" "eats" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If the mouse is red then the mouse chases the rabbit.
((("mouse" "is" "red" "+")) -> ("mouse" "chases" "rabbit" "+"))
If the mouse does not visit the rabbit and the rabbit does not visit the mouse then the mouse is big.
((("mouse" "visits" "rabbit" "~") ("rabbit" "visits" "mouse" "~")) -> ("mouse" "is" "big" "+"))
The mouse is big.
True
1
proof
[(triple3)]
("mouse" "is" "big" "+")
triple3
The mouse is blue.
False
1
inv-proof
[(triple4)]
("mouse" "is" "blue" "+")
triple4
The mouse chases the mouse.
True
2
proof
[(((triple1) -> rule4))]
("mouse" "chases" "mouse" "+")
((triple1) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule4))]
("mouse" "chases" "mouse" "-")
((triple1) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The rabbit is not cold.
Unknown
inv-rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse eats the rabbit.[(triple2 OR ((triple1) -> rule5))] The mouse is big.[(triple3)] The mouse is not blue.[(triple4)] The rabbit chases the mouse.[(triple5)] The rabbit is big.[(triple6)] The rabbit is red.[(triple7)] @1: The mouse chases the mouse.[(((triple1) -> rule4))] The mouse is not cold.[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] The mouse visits the rabbit.[(((triple5) -> rule3) OR ((((triple1) -> rule4)) -> rule3))] @2: The rabbit does not eat the mouse.[(((((triple5) -> rule3)) -> rule1) OR ((((((triple1) -> rule4)) -> rule3)) -> rule1))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple2
((triple1) -> (rule5 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse is not blue.
("mouse" "is" "blue" "-")
triple4
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple5
The rabbit is big.
("rabbit" "is" "big" "+")
triple6
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple1) -> (rule4 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple2) -> (rule2 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((triple5) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int2
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit does not eat the mouse.
("rabbit" "eats" "mouse" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int3