The cat does not need the squirrel. The cat sees the rabbit. The cat sees the squirrel. The rabbit is cold. The rabbit is not rough. The squirrel chases the cat. The squirrel does not see the tiger. The tiger is not green. The tiger does not need the squirrel. The tiger sees the cat. If something chases the cat then it sees the cat. Nice, green things are cold.
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something chases the cat then it sees the cat.
((("something" "chases" "cat" "+")) -> ("something" "sees" "cat" "+"))
Nice, green things are cold.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
The rabbit is not rough.
True
1
proof
[(triple5)]
("rabbit" "is" "rough" "-")
triple5
The tiger needs the squirrel.
False
1
inv-proof
[(triple9)]
("tiger" "needs" "squirrel" "+")
triple9
The squirrel sees the cat.
True
2
proof
[(((triple6) -> rule1))]
("squirrel" "sees" "cat" "+")
((triple6) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The squirrel does not see the cat.
False
2
inv-proof
[(((triple6) -> rule1))]
("squirrel" "sees" "cat" "-")
((triple6) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "cold" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The cat does not need the squirrel.[(triple1)] The cat sees the rabbit.[(triple2)] The cat sees the squirrel.[(triple3)] The rabbit is cold.[(triple4)] The rabbit is not rough.[(triple5)] The squirrel chases the cat.[(triple6)] The squirrel does not see the tiger.[(triple7)] The tiger does not need the squirrel.[(triple9)] The tiger is not green.[(triple8)] The tiger sees the cat.[(triple10)] @1: The squirrel sees the cat.[(((triple6) -> rule1))]
The cat does not need the squirrel.
("cat" "needs" "squirrel" "-")
triple1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple5
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple6
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
triple7
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple9
The tiger is not green.
("tiger" "is" "green" "-")
triple8
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
((triple6) -> (rule1 % int1))
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
int1