The cow does not need the squirrel. The mouse is young. The mouse needs the cow. The mouse sees the squirrel. The mouse visits the squirrel. The rabbit needs the cow. The squirrel is kind. If someone needs the cow and they need the rabbit then the rabbit is cold. If someone sees the cow and the cow needs the rabbit then they see the squirrel. If someone needs the cow and they are green then they see the squirrel. Kind people are green. If someone is cold then they see the rabbit. If someone sees the mouse and the mouse needs the squirrel then the squirrel is green. If someone is young then they need the rabbit. If someone sees the rabbit then they are young.
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
If someone needs the cow and they need the rabbit then the rabbit is cold.
((("someone" "needs" "cow" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone sees the cow and the cow needs the rabbit then they see the squirrel.
((("someone" "sees" "cow" "+") ("cow" "needs" "rabbit" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone needs the cow and they are green then they see the squirrel.
((("someone" "needs" "cow" "+") ("someone" "is" "green" "+")) -> ("someone" "sees" "squirrel" "+"))
Kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is cold then they see the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone sees the mouse and the mouse needs the squirrel then the squirrel is green.
((("someone" "sees" "mouse" "+") ("mouse" "needs" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If someone is young then they need the rabbit.
((("someone" "is" "young" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the rabbit then they are young.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "young" "+"))
The squirrel is kind.
True
1
proof
[(triple7)]
("squirrel" "is" "kind" "+")
triple7
The mouse does not visit the squirrel.
False
1
inv-proof
[(triple5)]
("mouse" "visits" "squirrel" "-")
triple5
The squirrel is green.
True
2
proof
[(((triple7) -> rule4))]
("squirrel" "is" "green" "+")
((triple7) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse does not need the rabbit.
False
2
inv-proof
[(((triple2) -> rule7))]
("mouse" "needs" "rabbit" "-")
((triple2) -> (rule7 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The rabbit is cold.
True
4
proof
[(((triple3 ((triple2) -> rule7)) -> rule1))]
("rabbit" "is" "cold" "+")
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit is not cold.
False
4
inv-proof
[(((triple3 ((triple2) -> rule7)) -> rule1))]
("rabbit" "is" "cold" "-")
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit sees the rabbit.
True
5
proof
[(((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5))]
("rabbit" "sees" "rabbit" "+")
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The rabbit does not see the rabbit.
False
5
inv-proof
[(((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5))]
("rabbit" "sees" "rabbit" "-")
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The rabbit is young.
True
6
proof
[(((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8))]
("rabbit" "is" "young" "+")
((((((triple3 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The rabbit is not young.
False
6
inv-proof
[(((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8))]
("rabbit" "is" "young" "-")
((((((triple3 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The rabbit needs the rabbit.
True
7
proof
[(((((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8)) -> rule7))]
("rabbit" "needs" "rabbit" "+")
((((((((triple3 ((triple2) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int5
The rabbit does not need the rabbit.
False
7
inv-proof
[(((((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8)) -> rule7))]
("rabbit" "needs" "rabbit" "-")
((((((((triple3 ((triple2) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int5
The squirrel does not see the rabbit.
Unknown
inv-rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "rabbit" "-")
The squirrel is young.
Unknown
rconc
[@2: The squirrel is young.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("squirrel" "is" "young" "+")
The cow does not see the rabbit.
Unknown
inv-rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "sees" "rabbit" "-")
The rabbit sees the squirrel.
Unknown
rconc
[@2: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "sees" "squirrel" "+")
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "green" "-")
The squirrel needs the rabbit.
Unknown
rconc
[@3: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule5 <- FAIL)]]
("squirrel" "needs" "rabbit" "+")
The squirrel does not visit the mouse.
Unknown
inv-random
[@0: The squirrel visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "mouse" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The rabbit does not visit the mouse.
Unknown
inv-random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cow does not need the squirrel.[(triple1)] The mouse is young.[(triple2)] The mouse needs the cow.[(triple3)] The mouse sees the squirrel.[(triple4)] The mouse visits the squirrel.[(triple5)] The rabbit needs the cow.[(triple6)] The squirrel is kind.[(triple7)] @1: The mouse needs the rabbit.[(((triple2) -> rule7))] The squirrel is green.[(((triple7) -> rule4))] @2: The rabbit is cold.[(((triple3 ((triple2) -> rule7)) -> rule1))] @3: The rabbit sees the rabbit.[(((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5))] @4: The rabbit is young.[(((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8))] @5: The rabbit needs the rabbit.[(((((((((triple3 ((triple2) -> rule7)) -> rule1)) -> rule5)) -> rule8)) -> rule7))]
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
triple1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple6
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((triple2) -> (rule7 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple7) -> (rule4 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple3 ((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple3 ((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
((((((triple3 ((triple2) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int4
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((((triple3 ((triple2) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int5