The bear sees the cat. The cat is rough. The dog is red. The tiger sees the cat. If something is rough and it needs the tiger then it sees the bear. If something needs the cat and the cat is red then the cat needs the dog. If something eats the bear and the bear is big then it is big. If something eats the bear and it is kind then the bear is red. All rough things are young. If something is rough then it is big.
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat is rough.
("cat" "is" "rough" "+")
The dog is red.
("dog" "is" "red" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is rough and it needs the tiger then it sees the bear.
((("something" "is" "rough" "+") ("something" "needs" "tiger" "+")) -> ("something" "sees" "bear" "+"))
If something needs the cat and the cat is red then the cat needs the dog.
((("something" "needs" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "needs" "dog" "+"))
If something eats the bear and the bear is big then it is big.
((("something" "eats" "bear" "+") ("bear" "is" "big" "+")) -> ("something" "is" "big" "+"))
If something eats the bear and it is kind then the bear is red.
((("something" "eats" "bear" "+") ("something" "is" "kind" "+")) -> ("bear" "is" "red" "+"))
All rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The tiger does not see the cat.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "cat" "-")
triple4
The cat is big.
True
2
proof
[(((triple2) -> rule6))]
("cat" "is" "big" "+")
((triple2) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple2) -> rule6))]
("cat" "is" "big" "-")
((triple2) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "young" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "big" "+")
The bear does not see the dog.
Unknown
inv-random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "-")
The tiger eats the dog.
Unknown
random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "+")
@0: The bear sees the cat.[(triple1)] The cat is rough.[(triple2)] The dog is red.[(triple3)] The tiger sees the cat.[(triple4)] @1: The cat is big.[(((triple2) -> rule6))] The cat is young.[(((triple2) -> rule5))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
((triple2) -> (rule6 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is young.
("cat" "is" "young" "+")
((triple2) -> (rule5 % int1))
The cat is young.
("cat" "is" "young" "+")
int1