The bear visits the cat. The cat is cold. The mouse is green. The tiger chases the mouse. If someone sees the cat then the cat is rough. If someone is rough then they do not visit the cat. If someone visits the tiger then the tiger visits the mouse. If someone is green then they are rough. If someone sees the tiger and the tiger is not green then they are nice. If someone is rough then they visit the tiger.
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is cold.
("cat" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If someone sees the cat then the cat is rough.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "rough" "+"))
If someone is rough then they do not visit the cat.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "cat" "-"))
If someone visits the tiger then the tiger visits the mouse.
((("someone" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the tiger and the tiger is not green then they are nice.
((("someone" "sees" "tiger" "+") ("tiger" "is" "green" "~")) -> ("someone" "is" "nice" "+"))
If someone is rough then they visit the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "tiger" "+"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The cat is not cold.
False
1
inv-proof
[(triple2)]
("cat" "is" "cold" "-")
triple2
The mouse is rough.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "is" "rough" "-")
((triple3) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the tiger.
True
3
proof
[(((((triple3) -> rule4)) -> rule6))]
("mouse" "visits" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse visits the cat.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("mouse" "visits" "cat" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The tiger visits the mouse.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
("tiger" "visits" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The tiger does not visit the mouse.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
("tiger" "visits" "mouse" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The bear does not visit the tiger.
Unknown
inv-rconc
[@2: The bear visits the tiger.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("bear" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@2: The tiger visits the tiger.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "nice" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "rough" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The cat sees the tiger.
Unknown
random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "+")
@0: The bear visits the cat.[(triple1)] The cat is cold.[(triple2)] The mouse is green.[(triple3)] The tiger chases the mouse.[(triple4)] @1: The mouse is rough.[(((triple3) -> rule4))] @2: The mouse does not visit the cat.[(((((triple3) -> rule4)) -> rule2))] The mouse visits the tiger.[(((((triple3) -> rule4)) -> rule6))] @3: The tiger visits the mouse.[(((((((triple3) -> rule4)) -> rule6)) -> rule3))]
The bear visits the cat.
("bear" "visits" "cat" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
((triple3) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3