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