The bear chases the mouse. The bear eats the cat. The bear is young. The cat chases the mouse. The cat chases the tiger. The cat is big. The cat is round. The cat is young. The cat sees the bear. The cat sees the tiger. The mouse chases the cat. The tiger is round. If someone sees the cat then they eat the tiger. If someone eats the cat then the cat is round. If someone is kind then they chase the mouse.
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear is young.
("bear" "is" "young" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone sees the cat then they eat the tiger.
((("someone" "sees" "cat" "+")) -> ("someone" "eats" "tiger" "+"))
If someone eats the cat then the cat is round.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "round" "+"))
If someone is kind then they chase the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "chases" "mouse" "+"))
The cat chases the mouse.
True
1
proof
[(triple4)]
("cat" "chases" "mouse" "+")
triple4
The cat is not round.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule2))]
("cat" "is" "round" "-")
triple7
((triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "tiger" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear chases the mouse.[(triple1)] The bear eats the cat.[(triple2)] The bear is young.[(triple3)] The cat chases the mouse.[(triple4)] The cat chases the tiger.[(triple5)] The cat is big.[(triple6)] The cat is round.[(triple7 OR ((triple2) -> rule2))] The cat is young.[(triple8)] The cat sees the bear.[(triple9)] The cat sees the tiger.[(triple10)] The mouse chases the cat.[(triple11)] The tiger is round.[(triple12)]
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple1
The bear eats the cat.
("bear" "eats" "cat" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple4
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple5
The cat is big.
("cat" "is" "big" "+")
triple6
The cat is round.
("cat" "is" "round" "+")
triple7
((triple2) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple8
The cat sees the bear.
("cat" "sees" "bear" "+")
triple9
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple10
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12