The bear chases the lion. The bear is young. The cow needs the tiger. The lion needs the bear. The tiger needs the bear. The tiger needs the cow. The tiger needs the lion. If something needs the bear and the bear needs the tiger then it needs the lion. If something is young then it needs the tiger. If something chases the lion then it needs the bear. If something is green and it chases the lion then the lion is green. If the lion is cold then the lion chases the cow. If something is young and it needs the lion then the lion is cold. If something is round then it needs the tiger. If something chases the cow then it needs the tiger. If something is red and it sees the bear then it chases the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is young.
("bear" "is" "young" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something needs the bear and the bear needs the tiger then it needs the lion.
((("something" "needs" "bear" "+") ("bear" "needs" "tiger" "+")) -> ("something" "needs" "lion" "+"))
If something is young then it needs the tiger.
((("something" "is" "young" "+")) -> ("something" "needs" "tiger" "+"))
If something chases the lion then it needs the bear.
((("something" "chases" "lion" "+")) -> ("something" "needs" "bear" "+"))
If something is green and it chases the lion then the lion is green.
((("something" "is" "green" "+") ("something" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
If the lion is cold then the lion chases the cow.
((("lion" "is" "cold" "+")) -> ("lion" "chases" "cow" "+"))
If something is young and it needs the lion then the lion is cold.
((("something" "is" "young" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "cold" "+"))
If something is round then it needs the tiger.
((("something" "is" "round" "+")) -> ("something" "needs" "tiger" "+"))
If something chases the cow then it needs the tiger.
((("something" "chases" "cow" "+")) -> ("something" "needs" "tiger" "+"))
If something is red and it sees the bear then it chases the bear.
((("something" "is" "red" "+") ("something" "sees" "bear" "+")) -> ("something" "chases" "bear" "+"))
The cow needs the tiger.
True
1
proof
[(triple3)]
("cow" "needs" "tiger" "+")
triple3
The bear does not chase the lion.
False
1
inv-proof
[(triple1)]
("bear" "chases" "lion" "-")
triple1
The bear needs the tiger.
True
2
proof
[(((triple2) -> rule2))]
("bear" "needs" "tiger" "+")
((triple2) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "needs" "tiger" "-")
((triple2) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the lion.
True
5
proof
[(((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1))]
("bear" "needs" "lion" "+")
((((triple1) -> (rule3 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The lion does not need the lion.
False
4
inv-proof
[(((triple4 ((triple2) -> rule2)) -> rule1))]
("lion" "needs" "lion" "-")
((triple4 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The lion is cold.
True
7
proof
[(((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6))]
("lion" "is" "cold" "+")
((triple2 ((((triple1) -> (rule3 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
The lion is not cold.
False
7
inv-proof
[(((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6))]
("lion" "is" "cold" "-")
((triple2 ((((triple1) -> (rule3 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
The lion chases the cow.
True
8
proof
[(((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5))]
("lion" "chases" "cow" "+")
((((triple2 ((((triple1) -> (rule3 % int5)) ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear needs the lion.
("bear" "needs" "lion" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
The lion does not chase the cow.
False
8
inv-proof
[(((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5))]
("lion" "chases" "cow" "-")
((((triple2 ((((triple1) -> (rule3 % int5)) ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear needs the lion.
("bear" "needs" "lion" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
The lion needs the tiger.
True
9
proof
[(((((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule8))]
("lion" "needs" "tiger" "+")
((((((triple2 ((((triple1) -> (rule3 % int6)) ((triple2) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear needs the lion.
("bear" "needs" "lion" "+")
int4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int5
The bear needs the bear.
("bear" "needs" "bear" "+")
int6
The lion does not need the tiger.
False
9
inv-proof
[(((((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule8))]
("lion" "needs" "tiger" "-")
((((((triple2 ((((triple1) -> (rule3 % int6)) ((triple2) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear needs the lion.
("bear" "needs" "lion" "+")
int4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int5
The bear needs the bear.
("bear" "needs" "bear" "+")
int6
The cow does not chase the bear.
Unknown
inv-rconc
[@1: The cow chases the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "chases" "bear" "-")
The cow needs the lion.
Unknown
rconc
[@2: The cow needs the lion.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cow" "needs" "lion" "+")
The tiger does not chase the bear.
Unknown
inv-rconc
[@1: The tiger chases the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("tiger" "chases" "bear" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "green" "+")
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "chases" "bear" "-")
The cow needs the bear.
Unknown
rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "bear" "+")
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 green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cow chases the lion.
Unknown
random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The bear needs the cow.
Unknown
random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "+")
@0: The bear chases the lion.[(triple1)] The bear is young.[(triple2)] The cow needs the tiger.[(triple3)] The lion needs the bear.[(triple4)] The tiger needs the bear.[(triple5)] The tiger needs the cow.[(triple6)] The tiger needs the lion.[(triple7 OR ((triple5 ((triple2) -> rule2)) -> rule1))] @1: The bear needs the bear.[(((triple1) -> rule3))] The bear needs the tiger.[(((triple2) -> rule2))] @2: The bear needs the lion.[(((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1))] The lion needs the lion.[(((triple4 ((triple2) -> rule2)) -> rule1))] @3: The lion is cold.[(((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6))] @4: The lion chases the cow.[(((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5))] @5: The lion needs the tiger.[(((((((triple2 ((((triple1) -> rule3) ((triple2) -> rule2)) -> rule1)) -> rule6)) -> rule5)) -> rule8))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The lion needs the bear.
("lion" "needs" "bear" "+")
triple4
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple5
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple6
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple7
((triple5 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule3 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((triple2) -> (rule2 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((((triple1) -> (rule3 % int3)) ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The bear needs the bear.
("bear" "needs" "bear" "+")
int3
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple4 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
((triple2 ((((triple1) -> (rule3 % int4)) ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int3
The bear needs the bear.
("bear" "needs" "bear" "+")
int4
The lion chases the cow.
("lion" "chases" "cow" "+")
((((triple2 ((((triple1) -> (rule3 % int5)) ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The bear needs the lion.
("bear" "needs" "lion" "+")
int3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
int5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((((((triple2 ((((triple1) -> (rule3 % int6)) ((triple2) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion chases the cow.
("lion" "chases" "cow" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The bear needs the lion.
("bear" "needs" "lion" "+")
int4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int5
The bear needs the bear.
("bear" "needs" "bear" "+")
int6