The cow needs the mouse. The dog needs the rabbit. The mouse needs the rabbit. The rabbit needs the cow. Red people are round. If someone is round then they need the cow. If someone needs the rabbit and they see the rabbit then the rabbit sees the cow. If someone needs the mouse and they are red then they are cold. If someone visits the rabbit and the rabbit visits the cow then they are round. If someone needs the cow and they need the mouse then the mouse sees the cow. If someone needs the rabbit then they are red. If someone needs the dog and they are red then the dog is cold.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they need the cow.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the rabbit and they see the rabbit then the rabbit sees the cow.
((("someone" "needs" "rabbit" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone needs the mouse and they are red then they are cold.
((("someone" "needs" "mouse" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone visits the rabbit and the rabbit visits the cow then they are round.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "cow" "+")) -> ("someone" "is" "round" "+"))
If someone needs the cow and they need the mouse then the mouse sees the cow.
((("someone" "needs" "cow" "+") ("someone" "needs" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If someone needs the rabbit then they are red.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone needs the dog and they are red then the dog is cold.
((("someone" "needs" "dog" "+") ("someone" "is" "red" "+")) -> ("dog" "is" "cold" "+"))
The cow needs the mouse.
True
1
proof
[(triple1)]
("cow" "needs" "mouse" "+")
triple1
The mouse does not need the rabbit.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "rabbit" "-")
triple3
The mouse is red.
True
2
proof
[(((triple3) -> rule7))]
("mouse" "is" "red" "+")
((triple3) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The dog is not red.
False
2
inv-proof
[(((triple2) -> rule7))]
("dog" "is" "red" "-")
((triple2) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse is round.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("mouse" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The dog is not round.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1))]
("dog" "is" "round" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse needs the cow.
True
4
proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule2))]
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse does not need the cow.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule1)) -> rule2))]
("mouse" "needs" "cow" "-")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "red" "-")
The mouse sees the cow.
Unknown
rconc
[@4: The mouse sees the cow.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- rule7 <- FAIL)]]
("mouse" "sees" "cow" "+")
The rabbit does not see the cow.
Unknown
inv-rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "cow" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "cold" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog sees the rabbit.
Unknown
random
[@0: The dog sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "rabbit" "+")
The mouse does not visit the rabbit.
Unknown
inv-random
[@0: The mouse visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "rabbit" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow needs the mouse.[(triple1)] The dog needs the rabbit.[(triple2)] The mouse needs the rabbit.[(triple3)] The rabbit needs the cow.[(triple4)] @1: The dog is red.[(((triple2) -> rule7))] The mouse is red.[(((triple3) -> rule7))] @2: The dog is round.[(((((triple2) -> rule7)) -> rule1))] The mouse is round.[(((((triple3) -> rule7)) -> rule1))] @3: The dog needs the cow.[(((((((triple2) -> rule7)) -> rule1)) -> rule2))] The mouse needs the cow.[(((((((triple3) -> rule7)) -> rule1)) -> rule2))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple4
The dog is red.
("dog" "is" "red" "+")
((triple2) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple3) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The dog is round.
("dog" "is" "round" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3