The dog is kind. The mouse likes the dog. The tiger is green. If something chases the mouse and it does not like the mouse then the mouse does not need the dog. If something is green then it likes the dog. If something likes the tiger and it needs the tiger then it is cold. If something needs the mouse and it chases the mouse then it needs the dog. If something is green and it likes the dog then it is kind. If something chases the dog then the dog is cold.
The dog is kind.
("dog" "is" "kind" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The tiger is green.
("tiger" "is" "green" "+")
If something chases the mouse and it does not like the mouse then the mouse does not need the dog.
((("something" "chases" "mouse" "+") ("something" "likes" "mouse" "~")) -> ("mouse" "needs" "dog" "-"))
If something is green then it likes the dog.
((("something" "is" "green" "+")) -> ("something" "likes" "dog" "+"))
If something likes the tiger and it needs the tiger then it is cold.
((("something" "likes" "tiger" "+") ("something" "needs" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something needs the mouse and it chases the mouse then it needs the dog.
((("something" "needs" "mouse" "+") ("something" "chases" "mouse" "+")) -> ("something" "needs" "dog" "+"))
If something is green and it likes the dog then it is kind.
((("something" "is" "green" "+") ("something" "likes" "dog" "+")) -> ("something" "is" "kind" "+"))
If something chases the dog then the dog is cold.
((("something" "chases" "dog" "+")) -> ("dog" "is" "cold" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The tiger likes the dog.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "likes" "dog" "+")
((triple3) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not like the dog.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "likes" "dog" "-")
((triple3) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is kind.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule5))]
("tiger" "is" "kind" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule5))]
("tiger" "is" "kind" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "cold" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "dog" "+")
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "cold" "-")
The tiger chases the mouse.
Unknown
random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The dog is kind.[(triple1)] The mouse likes the dog.[(triple2)] The tiger is green.[(triple3)] @1: The tiger likes the dog.[(((triple3) -> rule2))] @2: The tiger is kind.[(((triple3 ((triple3) -> rule2)) -> rule5))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The tiger is green.
("tiger" "is" "green" "+")
triple3
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple3) -> (rule2 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2