The bear chases the mouse. The bear is kind. The bear is rough. The bear is round. The bear sees the tiger. The mouse chases the bear. The mouse is kind. The mouse likes the bear. The mouse sees the rabbit. The mouse sees the tiger. The rabbit sees the tiger. The tiger chases the bear. If something sees the mouse and it chases the bear then the mouse is rough. If something likes the bear then it sees the mouse. If something chases the mouse and the mouse chases the rabbit then the rabbit sees the tiger. If something chases the tiger and the tiger is rough then the tiger likes the mouse. If something chases the bear and the bear likes the rabbit then the rabbit chases the mouse. If something sees the mouse then it likes the rabbit. If the rabbit is cold then the rabbit chases the tiger. If something likes the rabbit then the rabbit likes the bear.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
If something sees the mouse and it chases the bear then the mouse is rough.
((("something" "sees" "mouse" "+") ("something" "chases" "bear" "+")) -> ("mouse" "is" "rough" "+"))
If something likes the bear then it sees the mouse.
((("something" "likes" "bear" "+")) -> ("something" "sees" "mouse" "+"))
If something chases the mouse and the mouse chases the rabbit then the rabbit sees the tiger.
((("something" "chases" "mouse" "+") ("mouse" "chases" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If something chases the tiger and the tiger is rough then the tiger likes the mouse.
((("something" "chases" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "likes" "mouse" "+"))
If something chases the bear and the bear likes the rabbit then the rabbit chases the mouse.
((("something" "chases" "bear" "+") ("bear" "likes" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something sees the mouse then it likes the rabbit.
((("something" "sees" "mouse" "+")) -> ("something" "likes" "rabbit" "+"))
If the rabbit is cold then the rabbit chases the tiger.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something likes the rabbit then the rabbit likes the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
The bear is rough.
True
1
proof
[(triple3)]
("bear" "is" "rough" "+")
triple3
The bear does not see the tiger.
False
1
inv-proof
[(triple5)]
("bear" "sees" "tiger" "-")
triple5
The mouse sees the mouse.
True
2
proof
[(((triple8) -> rule2))]
("mouse" "sees" "mouse" "+")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse does not see the mouse.
False
2
inv-proof
[(((triple8) -> rule2))]
("mouse" "sees" "mouse" "-")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse likes the rabbit.
True
3
proof
[(((((triple8) -> rule2)) -> rule6))]
("mouse" "likes" "rabbit" "+")
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is not rough.
False
4
inv-proof
[(((((triple8) -> rule2) triple6) -> rule1))]
("mouse" "is" "rough" "-")
((((triple8) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The rabbit likes the bear.
True
4
proof
[(((((((triple8) -> rule2)) -> rule6)) -> rule8))]
("rabbit" "likes" "bear" "+")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The rabbit does not like the bear.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule6)) -> rule8))]
("rabbit" "likes" "bear" "-")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The rabbit sees the mouse.
True
5
proof
[(((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2))]
("rabbit" "sees" "mouse" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The rabbit does not see the mouse.
False
5
inv-proof
[(((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2))]
("rabbit" "sees" "mouse" "-")
((((((((triple8) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The rabbit likes the rabbit.
True
6
proof
[(((((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2)) -> rule6))]
("rabbit" "likes" "rabbit" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5
The rabbit does not like the rabbit.
False
6
inv-proof
[(((((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2)) -> rule6))]
("rabbit" "likes" "rabbit" "-")
((((((((((triple8) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5
The rabbit does not chase the mouse.
Unknown
inv-rconc
[@3: The rabbit chases the mouse.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule2 <- FAIL)]]
("rabbit" "chases" "mouse" "-")
The tiger likes the rabbit.
Unknown
rconc
[@2: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("tiger" "likes" "rabbit" "+")
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The bear likes the rabbit.
Unknown
rconc
[@2: The bear likes the rabbit.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("bear" "likes" "rabbit" "+")
The tiger does not see the mouse.
Unknown
inv-rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The rabbit chases the tiger.
Unknown
rconc
[@1: The rabbit chases the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "chases" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear chases the mouse.[(triple1)] The bear is kind.[(triple2)] The bear is rough.[(triple3)] The bear is round.[(triple4)] The bear sees the tiger.[(triple5)] The mouse chases the bear.[(triple6)] The mouse is kind.[(triple7)] The mouse likes the bear.[(triple8)] The mouse sees the rabbit.[(triple9)] The mouse sees the tiger.[(triple10)] The rabbit sees the tiger.[(triple11)] The tiger chases the bear.[(triple12)] @1: The mouse sees the mouse.[(((triple8) -> rule2))] @2: The mouse is rough.[(((((triple8) -> rule2) triple6) -> rule1))] The mouse likes the rabbit.[(((((triple8) -> rule2)) -> rule6))] @3: The rabbit likes the bear.[(((((((triple8) -> rule2)) -> rule6)) -> rule8))] @4: The rabbit sees the mouse.[(((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2))] @5: The rabbit likes the rabbit.[(((((((((((triple8) -> rule2)) -> rule6)) -> rule8)) -> rule2)) -> rule6))]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear is round.
("bear" "is" "round" "+")
triple4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple5
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple10
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple11
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple12
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple8) -> (rule2 % int2)) triple6) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((((((triple8) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int4
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int4
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int5