The bear chases the cat. The bear is cold. The bear is red. The bear sees the cat. The cat chases the rabbit. The cat chases the tiger. The cat is cold. The cat is not green. The cat sees the tiger. The rabbit is blue. The rabbit is green. The rabbit sees the cat. The rabbit sees the tiger. The tiger chases the rabbit. The tiger is red. The tiger needs the cat. If someone is red then they chase the cat. If someone chases the rabbit and they do not need the tiger then the tiger does not chase the cat. If someone sees the rabbit then they need the cat. If someone is green then they chase the bear. If someone sees the bear then the bear chases the cat. If someone chases the tiger then they are kind. If the cat does not chase the rabbit then the rabbit chases the cat. If the rabbit chases the bear then the bear is green.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the rabbit and they do not need the tiger then the tiger does not chase the cat.
((("someone" "chases" "rabbit" "+") ("someone" "needs" "tiger" "~")) -> ("tiger" "chases" "cat" "-"))
If someone sees the rabbit then they need the cat.
((("someone" "sees" "rabbit" "+")) -> ("someone" "needs" "cat" "+"))
If someone is green then they chase the bear.
((("someone" "is" "green" "+")) -> ("someone" "chases" "bear" "+"))
If someone sees the bear then the bear chases the cat.
((("someone" "sees" "bear" "+")) -> ("bear" "chases" "cat" "+"))
If someone chases the tiger then they are kind.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If the cat does not chase the rabbit then the rabbit chases the cat.
((("cat" "chases" "rabbit" "~")) -> ("rabbit" "chases" "cat" "+"))
If the rabbit chases the bear then the bear is green.
((("rabbit" "chases" "bear" "+")) -> ("bear" "is" "green" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The cat is not cold.
False
1
inv-proof
[(triple7)]
("cat" "is" "cold" "-")
triple7
The cat is kind.
True
2
proof
[(((triple6) -> rule6))]
("cat" "is" "kind" "+")
((triple6) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit does not chase the bear.
False
2
inv-proof
[(((triple11) -> rule4))]
("rabbit" "chases" "bear" "-")
((triple11) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The bear is green.
True
3
proof
[(((((triple11) -> rule4)) -> rule8))]
("bear" "is" "green" "+")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The bear is not green.
False
3
inv-proof
[(((((triple11) -> rule4)) -> rule8))]
("bear" "is" "green" "-")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The bear chases the bear.
True
4
proof
[(((((((triple11) -> rule4)) -> rule8)) -> rule4))]
("bear" "chases" "bear" "+")
((((((triple11) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The bear does not chase the bear.
False
4
inv-proof
[(((((((triple11) -> rule4)) -> rule8)) -> rule4))]
("bear" "chases" "bear" "-")
((((((triple11) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit does not need the cat.
Unknown
inv-rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "cat" "-")
The bear needs the cat.
Unknown
rconc
[@1: The bear needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "needs" "cat" "+")
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "kind" "-")
The cat chases the cat.
Unknown
rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "+")
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The tiger does not see the cat.
Unknown
inv-random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The bear chases the cat.[(triple1 OR ((triple3) -> rule1))] The bear is cold.[(triple2)] The bear is red.[(triple3)] The bear sees the cat.[(triple4)] The cat chases the rabbit.[(triple5)] The cat chases the tiger.[(triple6)] The cat is cold.[(triple7)] The cat is not green.[(triple8)] The cat sees the tiger.[(triple9)] The rabbit is blue.[(triple10)] The rabbit is green.[(triple11)] The rabbit sees the cat.[(triple12)] The rabbit sees the tiger.[(triple13)] The tiger chases the rabbit.[(triple14)] The tiger is red.[(triple15)] The tiger needs the cat.[(triple16)] @1: The cat is kind.[(((triple6) -> rule6))] The rabbit chases the bear.[(((triple11) -> rule4))] The tiger chases the cat.[(((triple15) -> rule1))] @2: The bear is green.[(((((triple11) -> rule4)) -> rule8))] @3: The bear chases the bear.[(((((((triple11) -> rule4)) -> rule8)) -> rule4))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
((triple3) -> (rule1 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple5
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple6
The cat is cold.
("cat" "is" "cold" "+")
triple7
The cat is not green.
("cat" "is" "green" "-")
triple8
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple9
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple10
The rabbit is green.
("rabbit" "is" "green" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple13
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple14
The tiger is red.
("tiger" "is" "red" "+")
triple15
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple16
The cat is kind.
("cat" "is" "kind" "+")
((triple6) -> (rule6 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple11) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple15) -> (rule1 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple11) -> (rule4 % int2))) -> (rule8 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
((((((triple11) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3