The cow likes the tiger. The dog likes the squirrel. The squirrel is young. The tiger sees the squirrel. All green people are kind. If someone likes the squirrel then they are green.
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the squirrel then they are green.
((("someone" "likes" "squirrel" "+")) -> ("someone" "is" "green" "+"))
The squirrel is young.
True
1
proof
[(triple3)]
("squirrel" "is" "young" "+")
triple3
The cow does not like the tiger.
False
1
inv-proof
[(triple1)]
("cow" "likes" "tiger" "-")
triple1
The dog is green.
True
2
proof
[(((triple2) -> rule2))]
("dog" "is" "green" "+")
((triple2) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("dog" "is" "green" "-")
((triple2) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is kind.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("dog" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("dog" "is" "kind" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The tiger is not kind.
Unknown
inv-rconc
[@2: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("tiger" "is" "kind" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "green" "+")
The squirrel is not kind.
Unknown
inv-rconc
[@2: The squirrel is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "is" "kind" "-")
The tiger likes the cow.
Unknown
random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
@0: The cow likes the tiger.[(triple1)] The dog likes the squirrel.[(triple2)] The squirrel is young.[(triple3)] The tiger sees the squirrel.[(triple4)] @1: The dog is green.[(((triple2) -> rule2))] @2: The dog is kind.[(((((triple2) -> rule2)) -> rule1))]
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
((triple2) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2