The bear needs the dog. The cat sees the bear. The dog likes the tiger. The tiger sees the bear. If something needs the dog and it is kind then it sees the bear. If something needs the dog then it likes the cat. If the dog is red and the dog sees the tiger then the tiger likes the bear. If something sees the tiger and it is blue then the tiger is kind. If something is young then it is blue. If something likes the tiger and the tiger sees the cat then the cat needs the dog. If something likes the cat then the cat needs the bear. If something likes the tiger then it is kind.
The bear needs the dog.
("bear" "needs" "dog" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something needs the dog and it is kind then it sees the bear.
((("something" "needs" "dog" "+") ("something" "is" "kind" "+")) -> ("something" "sees" "bear" "+"))
If something needs the dog then it likes the cat.
((("something" "needs" "dog" "+")) -> ("something" "likes" "cat" "+"))
If the dog is red and the dog sees the tiger then the tiger likes the bear.
((("dog" "is" "red" "+") ("dog" "sees" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If something sees the tiger and it is blue then the tiger is kind.
((("something" "sees" "tiger" "+") ("something" "is" "blue" "+")) -> ("tiger" "is" "kind" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something likes the tiger and the tiger sees the cat then the cat needs the dog.
((("something" "likes" "tiger" "+") ("tiger" "sees" "cat" "+")) -> ("cat" "needs" "dog" "+"))
If something likes the cat then the cat needs the bear.
((("something" "likes" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If something likes the tiger then it is kind.
((("something" "likes" "tiger" "+")) -> ("something" "is" "kind" "+"))
The dog likes the tiger.
True
1
proof
[(triple3)]
("dog" "likes" "tiger" "+")
triple3
The dog does not like the tiger.
False
1
inv-proof
[(triple3)]
("dog" "likes" "tiger" "-")
triple3
The dog is kind.
True
2
proof
[(((triple3) -> rule8))]
("dog" "is" "kind" "+")
((triple3) -> (rule8 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The bear does not like the cat.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "likes" "cat" "-")
((triple1) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The cat needs the bear.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("cat" "needs" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat does not need the bear.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("cat" "needs" "bear" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "kind" "-")
The cat needs the dog.
Unknown
rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "dog" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@2: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("cat" "likes" "cat" "-")
The dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
The dog does not see the cat.
Unknown
inv-random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The bear needs the dog.[(triple1)] The cat sees the bear.[(triple2)] The dog likes the tiger.[(triple3)] The tiger sees the bear.[(triple4)] @1: The bear likes the cat.[(((triple1) -> rule2))] The dog is kind.[(((triple3) -> rule8))] @2: The cat needs the bear.[(((((triple1) -> rule2)) -> rule7))]
The bear needs the dog.
("bear" "needs" "dog" "+")
triple1
The cat sees the bear.
("cat" "sees" "bear" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple4
The bear likes the cat.
("bear" "likes" "cat" "+")
((triple1) -> (rule2 % int1))
The bear likes the cat.
("bear" "likes" "cat" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple3) -> (rule8 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The bear likes the cat.
("bear" "likes" "cat" "+")
int2