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