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