The bear is green. The squirrel needs the tiger. The tiger likes the squirrel. If someone needs the squirrel then the squirrel is cold. If the squirrel needs the tiger then the squirrel is blue. If someone is blue then they need the squirrel.
The bear is green.
("bear" "is" "green" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If someone needs the squirrel then the squirrel is cold.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
If the squirrel needs the tiger then the squirrel is blue.
((("squirrel" "needs" "tiger" "+")) -> ("squirrel" "is" "blue" "+"))
If someone is blue then they need the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
The tiger likes the squirrel.
True
1
proof
[(triple3)]
("tiger" "likes" "squirrel" "+")
triple3
The tiger does not like the squirrel.
False
1
inv-proof
[(triple3)]
("tiger" "likes" "squirrel" "-")
triple3
The squirrel is blue.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "is" "blue" "-")
((triple2) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the squirrel.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("squirrel" "needs" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel does not need the squirrel.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("squirrel" "needs" "squirrel" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The tiger does not need the squirrel.
Unknown
inv-rconc
[@1: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "squirrel" "-")
The bear needs the squirrel.
Unknown
rconc
[@1: The bear needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "squirrel" "+")
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
The tiger does not chase the bear.
Unknown
inv-random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The bear is green.[(triple1)] The squirrel needs the tiger.[(triple2)] The tiger likes the squirrel.[(triple3)] @1: The squirrel is blue.[(((triple2) -> rule2))] @2: The squirrel needs the squirrel.[(((((triple2) -> rule2)) -> rule3))] @3: The squirrel is cold.[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
The bear is green.
("bear" "is" "green" "+")
triple1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple2
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3