The cow needs the squirrel. The rabbit is cold. The squirrel chases the rabbit. If someone eats the cow then the cow does not chase the squirrel. If someone chases the rabbit then they are rough. If someone is rough then they chase the squirrel. If someone is round and they do not need the cow then they are kind. If someone chases the cow and they are not cold then they do not need the squirrel. If someone chases the squirrel then the squirrel does not eat the cow.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
If someone eats the cow then the cow does not chase the squirrel.
((("someone" "eats" "cow" "+")) -> ("cow" "chases" "squirrel" "-"))
If someone chases the rabbit then they are rough.
((("someone" "chases" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they chase the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone is round and they do not need the cow then they are kind.
((("someone" "is" "round" "+") ("someone" "needs" "cow" "~")) -> ("someone" "is" "kind" "+"))
If someone chases the cow and they are not cold then they do not need the squirrel.
((("someone" "chases" "cow" "+") ("someone" "is" "cold" "~")) -> ("someone" "needs" "squirrel" "-"))
If someone chases the squirrel then the squirrel does not eat the cow.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "eats" "cow" "-"))
The cow needs the squirrel.
True
1
proof
[(triple1)]
("cow" "needs" "squirrel" "+")
triple1
The squirrel does not chase the rabbit.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "rabbit" "-")
triple3
The squirrel is rough.
True
2
proof
[(((triple3) -> rule2))]
("squirrel" "is" "rough" "+")
((triple3) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple3) -> rule2))]
("squirrel" "is" "rough" "-")
((triple3) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not chase the squirrel.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("squirrel" "chases" "squirrel" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not eat the cow.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("squirrel" "eats" "cow" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel eats the cow.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("squirrel" "eats" "cow" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "kind" "-")
The rabbit chases the squirrel.
Unknown
rconc
[@2: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("rabbit" "chases" "squirrel" "+")
The cow does not chase the squirrel.
Unknown
inv-rconc
[@2: The cow chases the squirrel.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "chases" "squirrel" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The rabbit does not eat the cow.
Unknown
inv-random
[@0: The rabbit eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow needs the squirrel.[(triple1)] The rabbit is cold.[(triple2)] The squirrel chases the rabbit.[(triple3)] @1: The squirrel is rough.[(((triple3) -> rule2))] @2: The squirrel chases the squirrel.[(((((triple3) -> rule2)) -> rule3))] @3: The squirrel does not eat the cow.[(((((((triple3) -> rule2)) -> rule3)) -> rule6))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple3) -> (rule2 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel does not eat the cow.
("squirrel" "eats" "cow" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3