The bear is nice. The cow is green. The cow needs the bear. The lion sees the bear. The tiger is red. The tiger needs the lion. The tiger visits the lion. If someone visits the lion then the lion is red. If someone sees the tiger then they visit the bear. If someone is red and they see the bear then the bear needs the cow. If someone sees the tiger then the tiger needs the cow. If the tiger sees the lion and the lion needs the tiger then the lion is cold. If someone needs the cow and the cow needs the tiger then the tiger sees the bear. If someone is cold then they see the lion. If someone visits the bear and the bear needs the cow then the bear visits the lion. If someone needs the cow then they see the tiger.
The bear is nice.
("bear" "is" "nice" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone visits the lion then the lion is red.
((("someone" "visits" "lion" "+")) -> ("lion" "is" "red" "+"))
If someone sees the tiger then they visit the bear.
((("someone" "sees" "tiger" "+")) -> ("someone" "visits" "bear" "+"))
If someone is red and they see the bear then the bear needs the cow.
((("someone" "is" "red" "+") ("someone" "sees" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If someone sees the tiger then the tiger needs the cow.
((("someone" "sees" "tiger" "+")) -> ("tiger" "needs" "cow" "+"))
If the tiger sees the lion and the lion needs the tiger then the lion is cold.
((("tiger" "sees" "lion" "+") ("lion" "needs" "tiger" "+")) -> ("lion" "is" "cold" "+"))
If someone needs the cow and the cow needs the tiger then the tiger sees the bear.
((("someone" "needs" "cow" "+") ("cow" "needs" "tiger" "+")) -> ("tiger" "sees" "bear" "+"))
If someone is cold then they see the lion.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "lion" "+"))
If someone visits the bear and the bear needs the cow then the bear visits the lion.
((("someone" "visits" "bear" "+") ("bear" "needs" "cow" "+")) -> ("bear" "visits" "lion" "+"))
If someone needs the cow then they see the tiger.
((("someone" "needs" "cow" "+")) -> ("someone" "sees" "tiger" "+"))
The tiger is red.
True
1
proof
[(triple5)]
("tiger" "is" "red" "+")
triple5
The bear is not nice.
False
1
inv-proof
[(triple1)]
("bear" "is" "nice" "-")
triple1
The lion is red.
True
2
proof
[(((triple7) -> rule1))]
("lion" "is" "red" "+")
((triple7) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "red" "-")
((triple7) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The bear needs the cow.
True
4
proof
[(((((triple7) -> rule1) triple4) -> rule3))]
("bear" "needs" "cow" "+")
((((triple7) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The bear does not need the cow.
False
4
inv-proof
[(((((triple7) -> rule1) triple4) -> rule3))]
("bear" "needs" "cow" "-")
((((triple7) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The bear sees the tiger.
True
5
proof
[(((((((triple7) -> rule1) triple4) -> rule3)) -> rule9))]
("bear" "sees" "tiger" "+")
((((((triple7) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule9 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The bear does not see the tiger.
False
5
inv-proof
[(((((((triple7) -> rule1) triple4) -> rule3)) -> rule9))]
("bear" "sees" "tiger" "-")
((((((triple7) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule9 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger needs the cow.
True
6
proof
[(((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4))]
("tiger" "needs" "cow" "+")
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger does not need the cow.
False
6
inv-proof
[(((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4))]
("tiger" "needs" "cow" "-")
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger sees the tiger.
True
7
proof
[(((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4)) -> rule9))]
("tiger" "sees" "tiger" "+")
((((((((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The bear needs the cow.
("bear" "needs" "cow" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The bear does not visit the lion.
False
11
inv-proof
[(((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule2) ((((triple7) -> rule1) triple4) -> rule3)) -> rule8) OR ((((((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4)) -> rule9)) -> rule2) ((((triple7) -> rule1) triple4) -> rule3)) -> rule8))]
("bear" "visits" "lion" "-")
((((((((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) ((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule8 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The bear needs the cow.
("bear" "needs" "cow" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((((((triple7) -> (rule1 % int7)) triple4) -> (rule3 % int6))) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) ((((triple7) -> (rule1 % int7)) triple4) -> (rule3 % int6))) -> (rule8 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int5
The bear needs the cow.
("bear" "needs" "cow" "+")
int6
The lion is red.
("lion" "is" "red" "+")
int7
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "sees" "lion" "-")
The lion sees the lion.
Unknown
rconc
[@2: The lion sees the lion.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("lion" "sees" "lion" "+")
The lion does not visit the bear.
Unknown
inv-rconc
[@2: The lion visits the bear.[CWA. Example of deepest failure = (rule2 <- rule9 <- FAIL)]]
("lion" "visits" "bear" "-")
The cow sees the lion.
Unknown
rconc
[@1: The cow sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "sees" "lion" "+")
The bear does not see the lion.
Unknown
inv-rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "sees" "lion" "-")
The cow sees the tiger.
Unknown
rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "sees" "tiger" "+")
The lion does not need the cow.
Unknown
inv-random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger visits the cow.
Unknown
random
[@0: The tiger visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cow" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The lion visits the cow.
Unknown
random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "+")
@0: The bear is nice.[(triple1)] The cow is green.[(triple2)] The cow needs the bear.[(triple3)] The lion sees the bear.[(triple4)] The tiger is red.[(triple5)] The tiger needs the lion.[(triple6)] The tiger visits the lion.[(triple7)] @1: The lion is red.[(((triple7) -> rule1))] @2: The bear needs the cow.[(((((triple7) -> rule1) triple4) -> rule3))] @3: The bear sees the tiger.[(((((((triple7) -> rule1) triple4) -> rule3)) -> rule9))] @4: The bear visits the bear.[(((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule2))] The tiger needs the cow.[(((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4))] @5: The bear visits the lion.[(((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule2) ((((triple7) -> rule1) triple4) -> rule3)) -> rule8) OR ((((((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4)) -> rule9)) -> rule2) ((((triple7) -> rule1) triple4) -> rule3)) -> rule8))] The tiger sees the tiger.[(((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4)) -> rule9))] @6: The tiger visits the bear.[(((((((((((((triple7) -> rule1) triple4) -> rule3)) -> rule9)) -> rule4)) -> rule9)) -> rule2))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow needs the bear.
("cow" "needs" "bear" "+")
triple3
The lion sees the bear.
("lion" "sees" "bear" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple6
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
((triple7) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
((((triple7) -> (rule1 % int2)) triple4) -> (rule3 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((((triple7) -> (rule1 % int3)) triple4) -> (rule3 % int2))) -> (rule9 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((((((((triple7) -> (rule1 % int4)) triple4) -> (rule3 % int3))) -> (rule9 % int2))) -> (rule4 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The bear visits the lion.
("bear" "visits" "lion" "+")
((((((((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) ((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule8 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The bear needs the cow.
("bear" "needs" "cow" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
((((((((((((((triple7) -> (rule1 % int7)) triple4) -> (rule3 % int6))) -> (rule9 % int5))) -> (rule4 % int4))) -> (rule9 % int3))) -> (rule2 % int2)) ((((triple7) -> (rule1 % int7)) triple4) -> (rule3 % int6))) -> (rule8 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int5
The bear needs the cow.
("bear" "needs" "cow" "+")
int6
The lion is red.
("lion" "is" "red" "+")
int7
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((((((triple7) -> (rule1 % int5)) triple4) -> (rule3 % int4))) -> (rule9 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The bear needs the cow.
("bear" "needs" "cow" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((((((((((((triple7) -> (rule1 % int6)) triple4) -> (rule3 % int5))) -> (rule9 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule2 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int4
The bear needs the cow.
("bear" "needs" "cow" "+")
int5
The lion is red.
("lion" "is" "red" "+")
int6