The bear eats the cat. The bear is kind. The cat eats the bear. The cat eats the tiger. The cat needs the tiger. The cat sees the bear. The cat does not see the tiger. The rabbit eats the cat. The rabbit is red. The rabbit needs the tiger. The tiger eats the bear. The tiger eats the rabbit. The tiger is kind. The tiger is not young. The tiger sees the bear. If something is red then it sees the tiger. If something sees the tiger then it does not see the bear. If something is round and it does not see the bear then the bear is cold.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is kind.
("bear" "is" "kind" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something is red then it sees the tiger.
((("something" "is" "red" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger then it does not see the bear.
((("something" "sees" "tiger" "+")) -> ("something" "sees" "bear" "-"))
If something is round and it does not see the bear then the bear is cold.
((("something" "is" "round" "+") ("something" "sees" "bear" "~")) -> ("bear" "is" "cold" "+"))
The rabbit is red.
True
1
proof
[(triple9)]
("rabbit" "is" "red" "+")
triple9
The tiger is not kind.
False
1
inv-proof
[(triple13)]
("tiger" "is" "kind" "-")
triple13
The rabbit sees the tiger.
True
2
proof
[(((triple9) -> rule1))]
("rabbit" "sees" "tiger" "+")
((triple9) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit does not see the tiger.
False
2
inv-proof
[(((triple9) -> rule1))]
("rabbit" "sees" "tiger" "-")
((triple9) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit does not see the bear.
True
3
proof
[(((((triple9) -> rule1)) -> rule2))]
("rabbit" "sees" "bear" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The rabbit sees the bear.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule2))]
("rabbit" "sees" "bear" "+")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "cold" "+")
The bear does not see the tiger.
Unknown
inv-rconc
[@1: The bear sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "tiger" "-")
The bear needs the rabbit.
Unknown
random
[@0: The bear needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "rabbit" "+")
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 bear.
Unknown
random
[@0: The tiger needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bear" "+")
@0: The bear eats the cat.[(triple1)] The bear is kind.[(triple2)] The cat does not see the tiger.[(triple7)] The cat eats the bear.[(triple3)] The cat eats the tiger.[(triple4)] The cat needs the tiger.[(triple5)] The cat sees the bear.[(triple6)] The rabbit eats the cat.[(triple8)] The rabbit is red.[(triple9)] The rabbit needs the tiger.[(triple10)] The tiger eats the bear.[(triple11)] The tiger eats the rabbit.[(triple12)] The tiger is kind.[(triple13)] The tiger is not young.[(triple14)] The tiger sees the bear.[(triple15)] @1: The rabbit sees the tiger.[(((triple9) -> rule1))] @2: The rabbit does not see the bear.[(((((triple9) -> rule1)) -> rule2))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The cat does not see the tiger.
("cat" "sees" "tiger" "-")
triple7
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple4
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple6
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple10
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger is not young.
("tiger" "is" "young" "-")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple9) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
((((triple9) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2