The bear eats the tiger. The bear is rough. The cat eats the bear. The cat is red. The cat is young. The cat sees the bear. The tiger eats the bear. If someone eats the bear then they eat the cat. If the cat is not rough then the cat eats the bear. If the cat sees the bear and the cat does not eat the bear then the cat does not need the bear.
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is rough.
("bear" "is" "rough" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
If someone eats the bear then they eat the cat.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "cat" "+"))
If the cat is not rough then the cat eats the bear.
((("cat" "is" "rough" "~")) -> ("cat" "eats" "bear" "+"))
If the cat sees the bear and the cat does not eat the bear then the cat does not need the bear.
((("cat" "sees" "bear" "+") ("cat" "eats" "bear" "~")) -> ("cat" "needs" "bear" "-"))
The cat is red.
True
1
proof
[(triple4)]
("cat" "is" "red" "+")
triple4
The bear does not eat the tiger.
False
1
inv-proof
[(triple1)]
("bear" "eats" "tiger" "-")
triple1
The cat eats the cat.
True
2
proof
[(((triple3) -> rule1))]
("cat" "eats" "cat" "+")
((triple3) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "eats" "cat" "-")
((triple3) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The bear does not eat the cat.
Unknown
inv-rconc
[@1: The bear eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "cat" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat does not see the tiger.
Unknown
inv-random
[@0: The cat sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "tiger" "-")
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 tiger.[(triple1)] The bear is rough.[(triple2)] The cat eats the bear.[(triple3)] The cat is red.[(triple4)] The cat is young.[(triple5)] The cat sees the bear.[(triple6)] The tiger eats the bear.[(triple7)] @1: The cat eats the cat.[(((triple3) -> rule1))] The tiger eats the cat.[(((triple7) -> rule1))]
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple6
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple3) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple7) -> (rule1 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1