The cow is big. The rabbit visits the squirrel. The squirrel sees the rabbit. The tiger chases the rabbit. If someone is big and nice then they visit the rabbit. All blue people are big. If someone is big then they are not cold. If someone sees the rabbit then the rabbit is blue. If someone is blue and nice then they do not see the tiger. If the rabbit sees the tiger and the tiger sees the cow then the rabbit chases the tiger. If the cow does not see the tiger then the tiger does not see the cow. If someone is green and they do not chase the tiger then they chase the squirrel.
The cow is big.
("cow" "is" "big" "+")
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If someone is big and nice then they visit the rabbit.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "visits" "rabbit" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are not cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
If someone sees the rabbit then the rabbit is blue.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
If someone is blue and nice then they do not see the tiger.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "sees" "tiger" "-"))
If the rabbit sees the tiger and the tiger sees the cow then the rabbit chases the tiger.
((("rabbit" "sees" "tiger" "+") ("tiger" "sees" "cow" "+")) -> ("rabbit" "chases" "tiger" "+"))
If the cow does not see the tiger then the tiger does not see the cow.
((("cow" "sees" "tiger" "~")) -> ("tiger" "sees" "cow" "-"))
If someone is green and they do not chase the tiger then they chase the squirrel.
((("someone" "is" "green" "+") ("someone" "chases" "tiger" "~")) -> ("someone" "chases" "squirrel" "+"))
The squirrel sees the rabbit.
True
1
proof
[(triple3)]
("squirrel" "sees" "rabbit" "+")
triple3
The cow is not big.
False
1
inv-proof
[(triple1)]
("cow" "is" "big" "-")
triple1
The rabbit is blue.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("rabbit" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("rabbit" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("rabbit" "is" "big" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not cold.
True
4
proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
("rabbit" "is" "cold" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is cold.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
("rabbit" "is" "cold" "+")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cow does not chase the squirrel.
Unknown
inv-rconc
[@1: The cow chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The rabbit does not chase the squirrel.
Unknown
inv-rconc
[@1: The rabbit chases the squirrel.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "chases" "squirrel" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "big" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The cow is big.[(triple1)] The rabbit visits the squirrel.[(triple2)] The squirrel sees the rabbit.[(triple3)] The tiger chases the rabbit.[(triple4)] @1: The cow is not cold.[(((triple1) -> rule3))] The rabbit is blue.[(((triple3) -> rule4))] @2: The rabbit is big.[(((((triple3) -> rule4)) -> rule2))] @3: The rabbit is not cold.[(((((((triple3) -> rule4)) -> rule2)) -> rule3))]
The cow is big.
("cow" "is" "big" "+")
triple1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
triple2
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple4
The cow is not cold.
("cow" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The cow is not cold.
("cow" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not cold.
("rabbit" "is" "cold" "-")
((((((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3