The bear is young. The bear sees the tiger. The cat chases the bear. The cat does not chase the tiger. The cat is green. The tiger is kind. The tiger needs the bear. If something is green then it is kind. If something is kind then it chases the cat.
The bear is young.
("bear" "is" "young" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
The cat is green.
("cat" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If something is green then it is kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it chases the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
The bear is young.
True
1
proof
[(triple1)]
("bear" "is" "young" "+")
triple1
The tiger does not need the bear.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "bear" "-")
triple7
The tiger chases the cat.
True
2
proof
[(((triple6) -> rule2))]
("tiger" "chases" "cat" "+")
((triple6) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger does not chase the cat.
False
2
inv-proof
[(((triple6) -> rule2))]
("tiger" "chases" "cat" "-")
((triple6) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat chases the cat.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("cat" "chases" "cat" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not chase the cat.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("cat" "chases" "cat" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The bear does not chase the cat.
Unknown
inv-rconc
[@2: The bear chases the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("bear" "chases" "cat" "-")
The bear is kind.
Unknown
rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "+")
The cat does not see the bear.
Unknown
inv-random
[@0: The cat sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "bear" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear is young.[(triple1)] The bear sees the tiger.[(triple2)] The cat chases the bear.[(triple3)] The cat does not chase the tiger.[(triple4)] The cat is green.[(triple5)] The tiger is kind.[(triple6)] The tiger needs the bear.[(triple7)] @1: The cat is kind.[(((triple5) -> rule1))] The tiger chases the cat.[(((triple6) -> rule2))] @2: The cat chases the cat.[(((((triple5) -> rule1)) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
triple4
The cat is green.
("cat" "is" "green" "+")
triple5
The tiger is kind.
("tiger" "is" "kind" "+")
triple6
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple7
The cat is kind.
("cat" "is" "kind" "+")
((triple5) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple6) -> (rule2 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2