The bear is rough. The bear is young. The bear likes the mouse. The cat likes the tiger. The mouse chases the bear. The tiger eats the bear. The tiger likes the cat. If something is rough then it likes the tiger. If something is kind then it is round. If the bear likes the tiger then the tiger is rough. If something eats the bear then the bear eats the mouse. If something likes the cat then the cat chases the mouse. If the tiger is rough then the tiger likes the bear. If something is kind then it is rough. If something likes the tiger and the tiger chases the mouse then the mouse chases the tiger.
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something is rough then it likes the tiger.
((("something" "is" "rough" "+")) -> ("something" "likes" "tiger" "+"))
If something is kind then it is round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If the bear likes the tiger then the tiger is rough.
((("bear" "likes" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If something eats the bear then the bear eats the mouse.
((("something" "eats" "bear" "+")) -> ("bear" "eats" "mouse" "+"))
If something likes the cat then the cat chases the mouse.
((("something" "likes" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If the tiger is rough then the tiger likes the bear.
((("tiger" "is" "rough" "+")) -> ("tiger" "likes" "bear" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something likes the tiger and the tiger chases the mouse then the mouse chases the tiger.
((("something" "likes" "tiger" "+") ("tiger" "chases" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
The tiger likes the cat.
True
1
proof
[(triple7)]
("tiger" "likes" "cat" "+")
triple7
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear likes the tiger.
True
2
proof
[(((triple1) -> rule1))]
("bear" "likes" "tiger" "+")
((triple1) -> (rule1 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear does not eat the mouse.
False
2
inv-proof
[(((triple6) -> rule4))]
("bear" "eats" "mouse" "-")
((triple6) -> (rule4 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The tiger is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("tiger" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("tiger" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger likes the bear.
True
4
proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6))]
("tiger" "likes" "bear" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The tiger does not like the bear.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule3)) -> rule6))]
("tiger" "likes" "bear" "-")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "round" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "round" "+")
The mouse does not chase the tiger.
Unknown
inv-rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "chases" "tiger" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "round" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The tiger eats the cat.
Unknown
random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear chases the tiger.
Unknown
random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "+")
@0: The bear is rough.[(triple1)] The bear is young.[(triple2)] The bear likes the mouse.[(triple3)] The cat likes the tiger.[(triple4)] The mouse chases the bear.[(triple5)] The tiger eats the bear.[(triple6)] The tiger likes the cat.[(triple7)] @1: The bear eats the mouse.[(((triple6) -> rule4))] The bear likes the tiger.[(((triple1) -> rule1))] The cat chases the mouse.[(((triple7) -> rule5))] @2: The tiger is rough.[(((((triple1) -> rule1)) -> rule3))] @3: The tiger likes the bear.[(((((((triple1) -> rule1)) -> rule3)) -> rule6))] The tiger likes the tiger.[(((((((triple1) -> rule1)) -> rule3)) -> rule1))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple7
The bear eats the mouse.
("bear" "eats" "mouse" "+")
((triple6) -> (rule4 % int1))
The bear eats the mouse.
("bear" "eats" "mouse" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple1) -> (rule1 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple7) -> (rule5 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int3