The bear does not like the tiger. The mouse is kind. The tiger chases the bear. If the tiger is round and the tiger is not green then the tiger chases the mouse. Kind things are red. If something is cold and it visits the bear then the bear chases the tiger. If something is round and it does not like the mouse then the mouse visits the bear. If the mouse visits the tiger and the tiger chases the bear then the mouse likes the tiger. If something is cold then it does not chase the tiger. Red things are cold. If something visits the tiger and it is not cold then the tiger likes the bear.
The bear does not like the tiger.
("bear" "likes" "tiger" "-")
The mouse is kind.
("mouse" "is" "kind" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If the tiger is round and the tiger is not green then the tiger chases the mouse.
((("tiger" "is" "round" "+") ("tiger" "is" "green" "~")) -> ("tiger" "chases" "mouse" "+"))
Kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is cold and it visits the bear then the bear chases the tiger.
((("something" "is" "cold" "+") ("something" "visits" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
If something is round and it does not like the mouse then the mouse visits the bear.
((("something" "is" "round" "+") ("something" "likes" "mouse" "~")) -> ("mouse" "visits" "bear" "+"))
If the mouse visits the tiger and the tiger chases the bear then the mouse likes the tiger.
((("mouse" "visits" "tiger" "+") ("tiger" "chases" "bear" "+")) -> ("mouse" "likes" "tiger" "+"))
If something is cold then it does not chase the tiger.
((("something" "is" "cold" "+")) -> ("something" "chases" "tiger" "-"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something visits the tiger and it is not cold then the tiger likes the bear.
((("something" "visits" "tiger" "+") ("something" "is" "cold" "~")) -> ("tiger" "likes" "bear" "+"))
The bear does not like the tiger.
True
1
proof
[(triple1)]
("bear" "likes" "tiger" "-")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple2)]
("mouse" "is" "kind" "-")
triple2
The mouse is red.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is not red.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "is" "red" "-")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
True
3
proof
[(((((triple2) -> rule2)) -> rule7))]
("mouse" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is not cold.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule7))]
("mouse" "is" "cold" "-")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not chase the tiger.
True
4
proof
[(((((((triple2) -> rule2)) -> rule7)) -> rule6))]
("mouse" "chases" "tiger" "-")
((((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse chases the tiger.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule7)) -> rule6))]
("mouse" "chases" "tiger" "+")
((((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The tiger is not cold.
Unknown
inv-rconc
[@2: The tiger is cold.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The bear is red.
Unknown
rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "red" "+")
The bear does not chase the tiger.
Unknown
inv-rconc
[@2: The bear chases the tiger.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("bear" "chases" "tiger" "-")
The tiger likes the bear.
Unknown
rconc
[@1: The tiger likes the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "likes" "bear" "+")
The mouse does not chase the bear.
Unknown
inv-random
[@0: The mouse chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear does not like the tiger.[(triple1)] The mouse is kind.[(triple2)] The tiger chases the bear.[(triple3)] @1: The mouse is red.[(((triple2) -> rule2))] @2: The mouse is cold.[(((((triple2) -> rule2)) -> rule7))] @3: The mouse does not chase the tiger.[(((((((triple2) -> rule2)) -> rule7)) -> rule6))]
The bear does not like the tiger.
("bear" "likes" "tiger" "-")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
((((((triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3