The bald eagle is cold. The cat does not see the squirrel. The cat sees the tiger. The squirrel needs the bald eagle. The tiger is cold. The tiger is kind. The tiger sees the squirrel. If something sees the tiger then the tiger likes the cat. If something needs the squirrel and it is cold then it needs the tiger. If something likes the squirrel and it is rough then the squirrel needs the bald eagle.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If something sees the tiger then the tiger likes the cat.
((("something" "sees" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
If something needs the squirrel and it is cold then it needs the tiger.
((("something" "needs" "squirrel" "+") ("something" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If something likes the squirrel and it is rough then the squirrel needs the bald eagle.
((("something" "likes" "squirrel" "+") ("something" "is" "rough" "+")) -> ("squirrel" "needs" "bald eagle" "+"))
The cat sees the tiger.
True
1
proof
[(triple3)]
("cat" "sees" "tiger" "+")
triple3
The cat sees the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "sees" "squirrel" "+")
triple2
The tiger likes the cat.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger does not like the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "likes" "cat" "-")
((triple3) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The cat needs the tiger.
Unknown
rconc
[@1: The cat needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "tiger" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The bald eagle is cold.[(triple1)] The cat does not see the squirrel.[(triple2)] The cat sees the tiger.[(triple3)] The squirrel needs the bald eagle.[(triple4)] The tiger is cold.[(triple5)] The tiger is kind.[(triple6)] The tiger sees the squirrel.[(triple7)] @1: The tiger likes the cat.[(((triple3) -> rule1))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
triple2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple3
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
triple4
The tiger is cold.
("tiger" "is" "cold" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple7
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((triple3) -> (rule1 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1