The cow needs the squirrel. The cow sees the squirrel. The cow visits the rabbit. The rabbit is green. The rabbit is rough. The rabbit needs the cow. The rabbit needs the squirrel. The rabbit sees the cow. The squirrel needs the rabbit. The squirrel sees the cow. The squirrel sees the rabbit. The squirrel visits the rabbit. If someone needs the cow and the cow is kind then they need the squirrel. If someone sees the squirrel and the squirrel visits the cow then they need the cow. If someone needs the squirrel and the squirrel needs the rabbit then the rabbit visits the squirrel. If someone visits the squirrel then the squirrel visits the cow. If the rabbit sees the squirrel and the rabbit visits the squirrel then the rabbit visits the cow. If someone is kind and they visit the rabbit then the rabbit visits the cow. If someone visits the rabbit and the rabbit needs the squirrel then the squirrel needs the cow. If someone needs the squirrel then they are cold.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
If someone needs the cow and the cow is kind then they need the squirrel.
((("someone" "needs" "cow" "+") ("cow" "is" "kind" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone sees the squirrel and the squirrel visits the cow then they need the cow.
((("someone" "sees" "squirrel" "+") ("squirrel" "visits" "cow" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the squirrel and the squirrel needs the rabbit then the rabbit visits the squirrel.
((("someone" "needs" "squirrel" "+") ("squirrel" "needs" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone visits the squirrel then the squirrel visits the cow.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "cow" "+"))
If the rabbit sees the squirrel and the rabbit visits the squirrel then the rabbit visits the cow.
((("rabbit" "sees" "squirrel" "+") ("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "visits" "cow" "+"))
If someone is kind and they visit the rabbit then the rabbit visits the cow.
((("someone" "is" "kind" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cow" "+"))
If someone visits the rabbit and the rabbit needs the squirrel then the squirrel needs the cow.
((("someone" "visits" "rabbit" "+") ("rabbit" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If someone needs the squirrel then they are cold.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "cold" "+"))
The rabbit is rough.
True
1
proof
[(triple5)]
("rabbit" "is" "rough" "+")
triple5
The rabbit is not rough.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "rough" "-")
triple5
The rabbit visits the squirrel.
True
3
proof
[(((triple1 triple9) -> rule3) OR ((triple7 triple9) -> rule3))]
("rabbit" "visits" "squirrel" "+")
((triple1 triple9) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
((triple7 triple9) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("cow" "is" "cold" "-")
((triple1) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The squirrel visits the cow.
True
4
proof
[(((((triple1 triple9) -> rule3)) -> rule4) OR ((((triple7 triple9) -> rule3)) -> rule4))]
("squirrel" "visits" "cow" "+")
((((triple1 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
((((triple7 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The squirrel does not visit the cow.
False
4
inv-proof
[(((((triple1 triple9) -> rule3)) -> rule4) OR ((((triple7 triple9) -> rule3)) -> rule4))]
("squirrel" "visits" "cow" "-")
((((triple1 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
((((triple7 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The cow needs the cow.
True
6
proof
[(((triple2 ((((triple1 triple9) -> rule3)) -> rule4)) -> rule2) OR ((triple2 ((((triple7 triple9) -> rule3)) -> rule4)) -> rule2))]
("cow" "needs" "cow" "+")
((triple2 ((((triple1 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
((triple2 ((((triple7 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The cow does not need the cow.
False
6
inv-proof
[(((triple2 ((((triple1 triple9) -> rule3)) -> rule4)) -> rule2) OR ((triple2 ((((triple7 triple9) -> rule3)) -> rule4)) -> rule2))]
("cow" "needs" "cow" "-")
((triple2 ((((triple1 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
((triple2 ((((triple7 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The rabbit visits the cow.
Unknown
rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The squirrel is not cold.
Unknown
inv-rconc
[@2: The squirrel is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The cow needs the squirrel.[(triple1)] The cow sees the squirrel.[(triple2)] The cow visits the rabbit.[(triple3)] The rabbit is green.[(triple4)] The rabbit is rough.[(triple5)] The rabbit needs the cow.[(triple6)] The rabbit needs the squirrel.[(triple7)] The rabbit sees the cow.[(triple8)] The squirrel needs the rabbit.[(triple9)] The squirrel sees the cow.[(triple10)] The squirrel sees the rabbit.[(triple11)] The squirrel visits the rabbit.[(triple12)] @1: The cow is cold.[(((triple1) -> rule8))] The rabbit is cold.[(((triple7) -> rule8))] The rabbit visits the squirrel.[(((triple1 triple9) -> rule3) OR ((triple7 triple9) -> rule3))] The squirrel needs the cow.[(((triple12 triple7) -> rule7) OR ((triple3 triple7) -> rule7))] @2: The squirrel visits the cow.[(((((triple1 triple9) -> rule3)) -> rule4) OR ((((triple7 triple9) -> rule3)) -> rule4))] @3: The cow needs the cow.[(((triple2 ((((triple1 triple9) -> rule3)) -> rule4)) -> rule2) OR ((triple2 ((((triple7 triple9) -> rule3)) -> rule4)) -> rule2))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple2
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple3
The rabbit is green.
("rabbit" "is" "green" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple6
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple7
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple8
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple9
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
triple10
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple11
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
triple12
The cow is cold.
("cow" "is" "cold" "+")
((triple1) -> (rule8 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple7) -> (rule8 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple1 triple9) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
((triple7 triple9) -> (rule3 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple12 triple7) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
((triple3 triple7) -> (rule7 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
((((triple1 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
((((triple7 triple9) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple2 ((((triple1 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3
((triple2 ((((triple7 triple9) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
int2
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int3