The bear chases the cat. The bear does not chase the lion. The bear chases the tiger. The bear visits the lion. The cat chases the tiger. The cat visits the lion. The lion visits the bear. The lion visits the cat. The tiger chases the lion. The tiger is not kind. The tiger needs the lion. If someone chases the lion then they do not visit the tiger. If someone chases the cat and the cat needs the lion then the lion visits the cat. If someone chases the cat then they are young. If someone needs the bear then the bear visits the cat. If someone chases the cat then the cat chases the tiger. If someone visits the cat then they are nice. If someone visits the cat and they are nice then they need the bear. If someone chases the cat and they do not visit the cat then the cat does not visit the tiger.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone chases the lion then they do not visit the tiger.
((("someone" "chases" "lion" "+")) -> ("someone" "visits" "tiger" "-"))
If someone chases the cat and the cat needs the lion then the lion visits the cat.
((("someone" "chases" "cat" "+") ("cat" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone chases the cat then they are young.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "young" "+"))
If someone needs the bear then the bear visits the cat.
((("someone" "needs" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone chases the cat then the cat chases the tiger.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "tiger" "+"))
If someone visits the cat then they are nice.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the cat and they are nice then they need the bear.
((("someone" "visits" "cat" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "bear" "+"))
If someone chases the cat and they do not visit the cat then the cat does not visit the tiger.
((("someone" "chases" "cat" "+") ("someone" "visits" "cat" "~")) -> ("cat" "visits" "tiger" "-"))
The bear chases the tiger.
True
1
proof
[(triple3)]
("bear" "chases" "tiger" "+")
triple3
The bear chases the lion.
False
1
inv-proof
[(triple2)]
("bear" "chases" "lion" "+")
triple2
The lion is nice.
True
2
proof
[(((triple8) -> rule6))]
("lion" "is" "nice" "+")
((triple8) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger visits the tiger.
False
2
inv-proof
[(((triple9) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The lion needs the bear.
True
4
proof
[(((triple8 ((triple8) -> rule6)) -> rule7))]
("lion" "needs" "bear" "+")
((triple8 ((triple8) -> (rule6 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion does not need the bear.
False
4
inv-proof
[(((triple8 ((triple8) -> rule6)) -> rule7))]
("lion" "needs" "bear" "-")
((triple8 ((triple8) -> (rule6 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear visits the cat.
True
5
proof
[(((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4))]
("bear" "visits" "cat" "+")
((((triple8 ((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The bear does not visit the cat.
False
5
inv-proof
[(((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4))]
("bear" "visits" "cat" "-")
((((triple8 ((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The bear is nice.
True
6
proof
[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6))]
("bear" "is" "nice" "+")
((((((triple8 ((triple8) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The bear is not nice.
False
6
inv-proof
[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6))]
("bear" "is" "nice" "-")
((((((triple8 ((triple8) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The bear needs the bear.
True
12
proof
[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4) ((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6)) -> rule7))]
("bear" "needs" "bear" "+")
((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
The lion is nice.
("lion" "is" "nice" "+")
int5
The bear does not need the bear.
False
12
inv-proof
[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4) ((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6)) -> rule7))]
("bear" "needs" "bear" "-")
((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
The lion is nice.
("lion" "is" "nice" "+")
int5
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "nice" "-")
The tiger needs the bear.
Unknown
rconc
[@1: The tiger needs the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "needs" "bear" "+")
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "needs" "bear" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "young" "+")
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "nice" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "young" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the tiger.[(triple3)] The bear does not chase the lion.[(triple2)] The bear visits the lion.[(triple4)] The cat chases the tiger.[(triple5 OR ((triple1) -> rule5))] The cat visits the lion.[(triple6)] The lion visits the bear.[(triple7)] The lion visits the cat.[(triple8)] The tiger chases the lion.[(triple9)] The tiger is not kind.[(triple10)] The tiger needs the lion.[(triple11)] @1: The bear is young.[(((triple1) -> rule3))] The lion is nice.[(((triple8) -> rule6))] The tiger does not visit the tiger.[(((triple9) -> rule1))] @2: The lion needs the bear.[(((triple8 ((triple8) -> rule6)) -> rule7))] @3: The bear visits the cat.[(((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4))] @4: The bear is nice.[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6))] @5: The bear needs the bear.[(((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4) ((((((triple8 ((triple8) -> rule6)) -> rule7)) -> rule4)) -> rule6)) -> rule7))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple3
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple4
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple5
((triple1) -> (rule5 % int1))
The cat chases the tiger.
("cat" "chases" "tiger" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The lion visits the cat.
("lion" "visits" "cat" "+")
triple8
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple9
The tiger is not kind.
("tiger" "is" "kind" "-")
triple10
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple11
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple8) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
((triple9) -> (rule1 % int1))
The tiger does not visit the tiger.
("tiger" "visits" "tiger" "-")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
((triple8 ((triple8) -> (rule6 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
((((triple8 ((triple8) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
((((((triple8 ((triple8) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
int4
The bear needs the bear.
("bear" "needs" "bear" "+")
((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3)) ((((((triple8 ((triple8) -> (rule6 % int5))) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear visits the cat.
("bear" "visits" "cat" "+")
int3
The lion needs the bear.
("lion" "needs" "bear" "+")
int4
The lion is nice.
("lion" "is" "nice" "+")
int5