The mouse eats the rabbit. The mouse is big. The mouse is cold. The mouse is red. The mouse does not need the rabbit. The mouse does not visit the rabbit. The rabbit eats the mouse. The rabbit is cold. The rabbit is red. The rabbit is young. The rabbit needs the mouse. The rabbit visits the mouse. All cold things are blue. If something visits the mouse then it needs the mouse. If the rabbit eats the mouse then the rabbit needs the mouse. If the rabbit eats the mouse and the rabbit visits the mouse then the rabbit is cold. If something needs the rabbit and it visits the rabbit then the rabbit is not big. If something visits the mouse and the mouse needs the rabbit then it is cold. If something needs the mouse and it does not visit the rabbit then the mouse eats the rabbit. If something is blue then it eats the rabbit.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse does not need the rabbit.
("mouse" "needs" "rabbit" "-")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If something visits the mouse then it needs the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If the rabbit eats the mouse then the rabbit needs the mouse.
((("rabbit" "eats" "mouse" "+")) -> ("rabbit" "needs" "mouse" "+"))
If the rabbit eats the mouse and the rabbit visits the mouse then the rabbit is cold.
((("rabbit" "eats" "mouse" "+") ("rabbit" "visits" "mouse" "+")) -> ("rabbit" "is" "cold" "+"))
If something needs the rabbit and it visits the rabbit then the rabbit is not big.
((("something" "needs" "rabbit" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "big" "-"))
If something visits the mouse and the mouse needs the rabbit then it is cold.
((("something" "visits" "mouse" "+") ("mouse" "needs" "rabbit" "+")) -> ("something" "is" "cold" "+"))
If something needs the mouse and it does not visit the rabbit then the mouse eats the rabbit.
((("something" "needs" "mouse" "+") ("something" "visits" "rabbit" "~")) -> ("mouse" "eats" "rabbit" "+"))
If something is blue then it eats the rabbit.
((("something" "is" "blue" "+")) -> ("something" "eats" "rabbit" "+"))
The mouse is red.
True
1
proof
[(triple4)]
("mouse" "is" "red" "+")
triple4
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule1)) -> rule8))]
("mouse" "eats" "rabbit" "-")
triple1
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit is blue.
True
2
proof
[(((triple8) -> rule1) OR ((((triple7 triple12) -> rule4)) -> rule1))]
("rabbit" "is" "blue" "+")
((triple8) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple7 triple12) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is not blue.
False
2
inv-proof
[(((triple8) -> rule1) OR ((((triple7 triple12) -> rule4)) -> rule1))]
("rabbit" "is" "blue" "-")
((triple8) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple7 triple12) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit eats the rabbit.
True
3
proof
[(((((triple8) -> rule1)) -> rule8) OR ((((((triple7 triple12) -> rule4)) -> rule1)) -> rule8))]
("rabbit" "eats" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((((triple7 triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule8) OR ((((((triple7 triple12) -> rule4)) -> rule1)) -> rule8))]
("rabbit" "eats" "rabbit" "-")
((((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((((triple7 triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
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 young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse does not need the rabbit.[(triple5)] The mouse does not visit the rabbit.[(triple6)] The mouse eats the rabbit.[(triple1 OR ((((triple3) -> rule1)) -> rule8))] The mouse is big.[(triple2)] The mouse is cold.[(triple3)] The mouse is red.[(triple4)] The rabbit eats the mouse.[(triple7)] The rabbit is cold.[(triple8 OR ((triple7 triple12) -> rule4))] The rabbit is red.[(triple9)] The rabbit is young.[(triple10)] The rabbit needs the mouse.[(triple11 OR ((triple12) -> rule2) OR ((triple7) -> rule3))] The rabbit visits the mouse.[(triple12)] @1: The mouse is blue.[(((triple3) -> rule1))] The rabbit is blue.[(((triple8) -> rule1) OR ((((triple7 triple12) -> rule4)) -> rule1))] @2: The rabbit eats the rabbit.[(((((triple8) -> rule1)) -> rule8) OR ((((((triple7 triple12) -> rule4)) -> rule1)) -> rule8))]
The mouse does not need the rabbit.
("mouse" "needs" "rabbit" "-")
triple5
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple6
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
((((triple3) -> (rule1 % int2))) -> (rule8 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
((triple7 triple12) -> (rule4 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple11
((triple12) -> (rule2 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple12
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple8) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple7 triple12) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple8) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((((triple7 triple12) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3