The bear visits the mouse. The cat is round. The mouse likes the cat. The tiger is rough. If someone visits the tiger and they visit the cat then the tiger likes the bear. If someone is blue then they visit the mouse. If someone is big then they visit the mouse. If someone visits the mouse then they like the bear. If someone needs the bear then the bear is round. If someone likes the mouse then they are big. If someone visits the mouse then the mouse is blue. If someone likes the tiger and the tiger likes the cat then they need the bear.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The cat is round.
("cat" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If someone visits the tiger and they visit the cat then the tiger likes the bear.
((("someone" "visits" "tiger" "+") ("someone" "visits" "cat" "+")) -> ("tiger" "likes" "bear" "+"))
If someone is blue then they visit the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is big then they visit the mouse.
((("someone" "is" "big" "+")) -> ("someone" "visits" "mouse" "+"))
If someone visits the mouse then they like the bear.
((("someone" "visits" "mouse" "+")) -> ("someone" "likes" "bear" "+"))
If someone needs the bear then the bear is round.
((("someone" "needs" "bear" "+")) -> ("bear" "is" "round" "+"))
If someone likes the mouse then they are big.
((("someone" "likes" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone visits the mouse then the mouse is blue.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If someone likes the tiger and the tiger likes the cat then they need the bear.
((("someone" "likes" "tiger" "+") ("tiger" "likes" "cat" "+")) -> ("someone" "needs" "bear" "+"))
The tiger is rough.
True
1
proof
[(triple4)]
("tiger" "is" "rough" "+")
triple4
The tiger is not rough.
False
1
inv-proof
[(triple4)]
("tiger" "is" "rough" "-")
triple4
The mouse is blue.
True
2
proof
[(((triple1) -> rule7))]
("mouse" "is" "blue" "+")
((triple1) -> (rule7 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The bear does not like the bear.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "likes" "bear" "-")
((triple1) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The mouse visits the mouse.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("mouse" "visits" "mouse" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not visit the mouse.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("mouse" "visits" "mouse" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse likes the bear.
True
4
proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule4))]
("mouse" "likes" "bear" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse does not like the bear.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule4))]
("mouse" "likes" "bear" "-")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse does not need the bear.
Unknown
inv-rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "needs" "bear" "-")
The tiger visits the mouse.
Unknown
rconc
[@2: The tiger visits the mouse.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("tiger" "visits" "mouse" "+")
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "needs" "bear" "-")
The cat is big.
Unknown
rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "big" "+")
The tiger does not need the mouse.
Unknown
inv-random
[@0: The tiger needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "mouse" "-")
The mouse needs the tiger.
Unknown
random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The bear visits the mouse.[(triple1)] The cat is round.[(triple2)] The mouse likes the cat.[(triple3)] The tiger is rough.[(triple4)] @1: The bear likes the bear.[(((triple1) -> rule4))] The mouse is blue.[(((triple1) -> rule7))] @2: The mouse visits the mouse.[(((((triple1) -> rule7)) -> rule2))] @3: The mouse likes the bear.[(((((((triple1) -> rule7)) -> rule2)) -> rule4))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
The bear likes the bear.
("bear" "likes" "bear" "+")
((triple1) -> (rule4 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple1) -> (rule7 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3