The bear is red. The bear sees the rabbit. The bear sees the tiger. The bear does not visit the tiger. The cat eats the rabbit. The cat sees the rabbit. The cat sees the tiger. The rabbit eats the bear. The rabbit sees the cat. The tiger eats the bear. The tiger eats the cat. The tiger eats the rabbit. The tiger is young. The tiger does not see the bear. The tiger sees the cat. The tiger does not visit the bear. Red things are young. If something eats the tiger then the tiger eats the cat. If something is young then it eats the tiger.
The bear is red.
("bear" "is" "red" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something eats the tiger then the tiger eats the cat.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If something is young then it eats the tiger.
((("something" "is" "young" "+")) -> ("something" "eats" "tiger" "+"))
The tiger eats the cat.
True
1
proof
[(triple11 OR ((((triple13) -> rule3)) -> rule2) OR ((((((triple1) -> rule1)) -> rule3)) -> rule2))]
("tiger" "eats" "cat" "+")
triple11
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The tiger does not eat the bear.
False
1
inv-proof
[(triple10)]
("tiger" "eats" "bear" "-")
triple10
The bear is young.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple13) -> rule3))]
("tiger" "eats" "tiger" "-")
((triple13) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The bear eats the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("bear" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear does not eat the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("bear" "eats" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "young" "-")
The rabbit eats the tiger.
Unknown
rconc
[@2: The rabbit eats the tiger.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("rabbit" "eats" "tiger" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "young" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The cat eats the bear.
Unknown
random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "+")
@0: The bear does not visit the tiger.[(triple4)] The bear is red.[(triple1)] The bear sees the rabbit.[(triple2)] The bear sees the tiger.[(triple3)] The cat eats the rabbit.[(triple5)] The cat sees the rabbit.[(triple6)] The cat sees the tiger.[(triple7)] The rabbit eats the bear.[(triple8)] The rabbit sees the cat.[(triple9)] The tiger does not see the bear.[(triple14)] The tiger does not visit the bear.[(triple16)] The tiger eats the bear.[(triple10)] The tiger eats the cat.[(triple11 OR ((((triple13) -> rule3)) -> rule2) OR ((((((triple1) -> rule1)) -> rule3)) -> rule2))] The tiger eats the rabbit.[(triple12)] The tiger is young.[(triple13)] The tiger sees the cat.[(triple15)] @1: The bear is young.[(((triple1) -> rule1))] The tiger eats the tiger.[(((triple13) -> rule3))] @2: The bear eats the tiger.[(((((triple1) -> rule1)) -> rule3))]
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
triple4
The bear is red.
("bear" "is" "red" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple5
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple6
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple7
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple8
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple9
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
triple14
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
triple16
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple10
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple11
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule1 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple13) -> (rule3 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2