The bear is kind. The dog is kind. The tiger chases the dog. If the bear visits the tiger then the bear is cold. If someone is cold then they like the bear. If someone is young then they chase the bear. If someone is young then they visit the tiger. If someone likes the dog and the dog is red then they are red. If someone is kind then they visit the tiger.
The bear is kind.
("bear" "is" "kind" "+")
The dog is kind.
("dog" "is" "kind" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
If the bear visits the tiger then the bear is cold.
((("bear" "visits" "tiger" "+")) -> ("bear" "is" "cold" "+"))
If someone is cold then they like the bear.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "bear" "+"))
If someone is young then they chase the bear.
((("someone" "is" "young" "+")) -> ("someone" "chases" "bear" "+"))
If someone is young then they visit the tiger.
((("someone" "is" "young" "+")) -> ("someone" "visits" "tiger" "+"))
If someone likes the dog and the dog is red then they are red.
((("someone" "likes" "dog" "+") ("dog" "is" "red" "+")) -> ("someone" "is" "red" "+"))
If someone is kind then they visit the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "tiger" "+"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The tiger does not chase the dog.
False
1
inv-proof
[(triple3)]
("tiger" "chases" "dog" "-")
triple3
The bear visits the tiger.
True
2
proof
[(((triple1) -> rule6))]
("bear" "visits" "tiger" "+")
((triple1) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear does not visit the tiger.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "visits" "tiger" "-")
((triple1) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear is cold.
True
3
proof
[(((((triple1) -> rule6)) -> rule1))]
("bear" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear is not cold.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("bear" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear likes the bear.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("bear" "likes" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The bear does not like the bear.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("bear" "likes" "bear" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "bear" "-")
The tiger likes the bear.
Unknown
rconc
[@1: The tiger likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "likes" "bear" "+")
The tiger does not chase the bear.
Unknown
inv-rconc
[@1: The tiger chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "bear" "-")
The tiger is red.
Unknown
rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "red" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bear is kind.[(triple1)] The dog is kind.[(triple2)] The tiger chases the dog.[(triple3)] @1: The bear visits the tiger.[(((triple1) -> rule6))] The dog visits the tiger.[(((triple2) -> rule6))] @2: The bear is cold.[(((((triple1) -> rule6)) -> rule1))] @3: The bear likes the bear.[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
((triple1) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
((triple2) -> (rule6 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3