The bear likes the mouse. The bear likes the tiger. The bear sees the lion. The lion likes the bear. The lion likes the tiger. The lion needs the bear. The lion does not see the mouse. The mouse is nice. The mouse likes the bear. The mouse likes the tiger. The mouse sees the bear. The tiger likes the lion. If someone is red then they are cold. All big people are nice. If someone needs the bear then they are red. If someone is cold then they do not see the bear. If the lion likes the tiger and the lion is cold then the tiger needs the bear. If someone sees the bear then the bear likes the tiger. If someone needs the bear then they like the lion. If someone needs the tiger and the tiger does not see the bear then they like the bear. If the bear is not red then the bear does not see the lion.
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the bear then they are red.
((("someone" "needs" "bear" "+")) -> ("someone" "is" "red" "+"))
If someone is cold then they do not see the bear.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "bear" "-"))
If the lion likes the tiger and the lion is cold then the tiger needs the bear.
((("lion" "likes" "tiger" "+") ("lion" "is" "cold" "+")) -> ("tiger" "needs" "bear" "+"))
If someone sees the bear then the bear likes the tiger.
((("someone" "sees" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
If someone needs the bear then they like the lion.
((("someone" "needs" "bear" "+")) -> ("someone" "likes" "lion" "+"))
If someone needs the tiger and the tiger does not see the bear then they like the bear.
((("someone" "needs" "tiger" "+") ("tiger" "sees" "bear" "~")) -> ("someone" "likes" "bear" "+"))
If the bear is not red then the bear does not see the lion.
((("bear" "is" "red" "~")) -> ("bear" "sees" "lion" "-"))
The mouse likes the tiger.
True
1
proof
[(triple10)]
("mouse" "likes" "tiger" "+")
triple10
The lion sees the mouse.
False
1
inv-proof
[(triple7)]
("lion" "sees" "mouse" "+")
triple7
The lion is red.
True
2
proof
[(((triple6) -> rule3))]
("lion" "is" "red" "+")
((triple6) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple6) -> rule3))]
("lion" "is" "red" "-")
((triple6) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is cold.
True
3
proof
[(((((triple6) -> rule3)) -> rule1))]
("lion" "is" "cold" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is not cold.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule1))]
("lion" "is" "cold" "-")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not see the bear.
True
4
proof
[(((((((triple6) -> rule3)) -> rule1)) -> rule4))]
("lion" "sees" "bear" "-")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not see the bear.
("lion" "sees" "bear" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger does not need the bear.
False
5
inv-proof
[(((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5))]
("tiger" "needs" "bear" "-")
((triple5 ((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger is red.
True
6
proof
[(((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3))]
("tiger" "is" "red" "+")
((((triple5 ((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is not red.
False
6
inv-proof
[(((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3))]
("tiger" "is" "red" "-")
((((triple5 ((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is cold.
True
7
proof
[(((((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3)) -> rule1))]
("tiger" "is" "cold" "+")
((((((triple5 ((((triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The tiger is not cold.
False
7
inv-proof
[(((((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3)) -> rule1))]
("tiger" "is" "cold" "-")
((((((triple5 ((((triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The mouse is not cold.
Unknown
inv-rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "is" "cold" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "nice" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "nice" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "nice" "+")
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "red" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "likes" "lion" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The tiger does not like the mouse.
Unknown
inv-random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "-")
The bear needs the lion.
Unknown
random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "+")
The bear does not see the tiger.
Unknown
inv-random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear likes the mouse.[(triple1)] The bear likes the tiger.[(triple2 OR ((triple11) -> rule6))] The bear sees the lion.[(triple3)] The lion does not see the mouse.[(triple7)] The lion likes the bear.[(triple4)] The lion likes the tiger.[(triple5)] The lion needs the bear.[(triple6)] The mouse is nice.[(triple8)] The mouse likes the bear.[(triple9)] The mouse likes the tiger.[(triple10)] The mouse sees the bear.[(triple11)] The tiger likes the lion.[(triple12 OR ((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule7))] @1: The lion is red.[(((triple6) -> rule3))] The lion likes the lion.[(((triple6) -> rule7))] @2: The lion is cold.[(((((triple6) -> rule3)) -> rule1))] @3: The lion does not see the bear.[(((((((triple6) -> rule3)) -> rule1)) -> rule4))] The tiger needs the bear.[(((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5))] @4: The tiger is red.[(((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3))] @5: The tiger is cold.[(((((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3)) -> rule1))] @6: The tiger does not see the bear.[(((((((((triple5 ((((triple6) -> rule3)) -> rule1)) -> rule5)) -> rule3)) -> rule1)) -> rule4))]
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple2
((triple11) -> (rule6 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple3
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple7
The lion likes the bear.
("lion" "likes" "bear" "+")
triple4
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple5
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple9
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple10
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple11
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple12
((((triple5 ((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is red.
("lion" "is" "red" "+")
((triple6) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple6) -> (rule7 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not see the bear.
("lion" "sees" "bear" "-")
((((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not see the bear.
("lion" "sees" "bear" "-")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
((triple5 ((((triple6) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
((((triple5 ((((triple6) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
((((((triple5 ((((triple6) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int3
The lion is cold.
("lion" "is" "cold" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
((((((((triple5 ((((triple6) -> (rule3 % int6))) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger needs the bear.
("tiger" "needs" "bear" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
int5
The lion is red.
("lion" "is" "red" "+")
int6