The bear eats the cat. The bear eats the tiger. The bear is nice. The cat eats the rabbit. The cat eats the tiger. The cat needs the bear. The cat needs the rabbit. The cat needs the tiger. The cat visits the bear. The cat visits the tiger. The rabbit does not visit the bear. The rabbit visits the cat. The tiger needs the rabbit. The tiger does not visit the cat. The tiger does not visit the rabbit. If something visits the tiger then the tiger does not eat the cat. If something is round and not nice then it is young. If something visits the cat then it is young. If something needs the rabbit then it visits the bear. If something is young then it eats the bear. If something eats the rabbit then it does not need the cat. If something is round and it eats the cat then the cat does not eat the rabbit. If something eats the bear then the bear does not visit the rabbit.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is nice.
("bear" "is" "nice" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
If something visits the tiger then the tiger does not eat the cat.
((("something" "visits" "tiger" "+")) -> ("tiger" "eats" "cat" "-"))
If something is round and not nice then it is young.
((("something" "is" "round" "+") ("something" "is" "nice" "~")) -> ("something" "is" "young" "+"))
If something visits the cat then it is young.
((("something" "visits" "cat" "+")) -> ("something" "is" "young" "+"))
If something needs the rabbit then it visits the bear.
((("something" "needs" "rabbit" "+")) -> ("something" "visits" "bear" "+"))
If something is young then it eats the bear.
((("something" "is" "young" "+")) -> ("something" "eats" "bear" "+"))
If something eats the rabbit then it does not need the cat.
((("something" "eats" "rabbit" "+")) -> ("something" "needs" "cat" "-"))
If something is round and it eats the cat then the cat does not eat the rabbit.
((("something" "is" "round" "+") ("something" "eats" "cat" "+")) -> ("cat" "eats" "rabbit" "-"))
If something eats the bear then the bear does not visit the rabbit.
((("something" "eats" "bear" "+")) -> ("bear" "visits" "rabbit" "-"))
The bear eats the cat.
True
1
proof
[(triple1)]
("bear" "eats" "cat" "+")
triple1
The cat does not visit the tiger.
False
1
inv-proof
[(triple10)]
("cat" "visits" "tiger" "-")
triple10
The rabbit is young.
True
2
proof
[(((triple12) -> rule3))]
("rabbit" "is" "young" "+")
((triple12) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat needs the cat.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "needs" "cat" "+")
((triple4) -> (rule6 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The rabbit eats the bear.
True
3
proof
[(((((triple12) -> rule3)) -> rule5))]
("rabbit" "eats" "bear" "+")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not eat the bear.
False
3
inv-proof
[(((((triple12) -> rule3)) -> rule5))]
("rabbit" "eats" "bear" "-")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The bear does not visit the rabbit.
True
4
proof
[(((((((triple12) -> rule3)) -> rule5)) -> rule8))]
("bear" "visits" "rabbit" "-")
((((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The bear visits the rabbit.
False
4
inv-proof
[(((((((triple12) -> rule3)) -> rule5)) -> rule8))]
("bear" "visits" "rabbit" "+")
((((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "young" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "young" "+")
The bear does not eat the bear.
Unknown
inv-rconc
[@2: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "bear" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The bear eats the cat.[(triple1)] The bear eats the tiger.[(triple2)] The bear is nice.[(triple3)] The cat eats the rabbit.[(triple4)] The cat eats the tiger.[(triple5)] The cat needs the bear.[(triple6)] The cat needs the rabbit.[(triple7)] The cat needs the tiger.[(triple8)] The cat visits the bear.[(triple9 OR ((triple7) -> rule4))] The cat visits the tiger.[(triple10)] The rabbit does not visit the bear.[(triple11)] The rabbit visits the cat.[(triple12)] The tiger does not visit the cat.[(triple14)] The tiger does not visit the rabbit.[(triple15)] The tiger needs the rabbit.[(triple13)] @1: The cat does not need the cat.[(((triple4) -> rule6))] The rabbit is young.[(((triple12) -> rule3))] The tiger does not eat the cat.[(((triple10) -> rule1))] The tiger visits the bear.[(((triple13) -> rule4))] @2: The rabbit eats the bear.[(((((triple12) -> rule3)) -> rule5))] @3: The bear does not visit the rabbit.[(((((((triple12) -> rule3)) -> rule5)) -> rule8))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple4
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple5
The cat needs the bear.
("cat" "needs" "bear" "+")
triple6
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple7
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple8
The cat visits the bear.
("cat" "visits" "bear" "+")
triple9
((triple7) -> (rule4 % int1))
The cat visits the bear.
("cat" "visits" "bear" "+")
int1
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple10
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
triple11
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple12
The tiger does not visit the cat.
("tiger" "visits" "cat" "-")
triple14
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
triple15
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple13
The cat does not need the cat.
("cat" "needs" "cat" "-")
((triple4) -> (rule6 % int1))
The cat does not need the cat.
("cat" "needs" "cat" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple12) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
((triple10) -> (rule1 % int1))
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple13) -> (rule4 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((((triple12) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
((((((triple12) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The bear does not visit the rabbit.
("bear" "visits" "rabbit" "-")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3