The bear chases the cat. The bear sees the tiger. The cat eats the bear. The cat eats the tiger. The tiger chases the cat. The tiger eats the bear. The tiger sees the bear. Round things are big. If something sees the tiger and the tiger is nice then the tiger eats the cat. If something chases the bear then the bear sees the cat. If the cat eats the bear and the bear sees the tiger then the cat chases the bear. If something is young and nice then it eats the cat. If the tiger is young then the tiger eats the bear. If something chases the tiger then the tiger chases the bear. If something eats the bear then it eats the tiger.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the tiger.
("cat" "eats" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
Round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something sees the tiger and the tiger is nice then the tiger eats the cat.
((("something" "sees" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "eats" "cat" "+"))
If something chases the bear then the bear sees the cat.
((("something" "chases" "bear" "+")) -> ("bear" "sees" "cat" "+"))
If the cat eats the bear and the bear sees the tiger then the cat chases the bear.
((("cat" "eats" "bear" "+") ("bear" "sees" "tiger" "+")) -> ("cat" "chases" "bear" "+"))
If something is young and nice then it eats the cat.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "eats" "cat" "+"))
If the tiger is young then the tiger eats the bear.
((("tiger" "is" "young" "+")) -> ("tiger" "eats" "bear" "+"))
If something chases the tiger then the tiger chases the bear.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "bear" "+"))
If something eats the bear then it eats the tiger.
((("something" "eats" "bear" "+")) -> ("something" "eats" "tiger" "+"))
The tiger eats the bear.
True
1
proof
[(triple6)]
("tiger" "eats" "bear" "+")
triple6
The tiger does not chase the cat.
False
1
inv-proof
[(triple5)]
("tiger" "chases" "cat" "-")
triple5
The tiger eats the tiger.
True
2
proof
[(((triple6) -> rule8))]
("tiger" "eats" "tiger" "+")
((triple6) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple6) -> rule8))]
("tiger" "eats" "tiger" "-")
((triple6) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The bear does not eat the cat.
Unknown
inv-rconc
[@1: The bear eats the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "cat" "-")
The bear eats the tiger.
Unknown
rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "eats" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear chases the cat.[(triple1)] The bear sees the tiger.[(triple2)] The cat eats the bear.[(triple3)] The cat eats the tiger.[(triple4 OR ((triple3) -> rule8))] The tiger chases the cat.[(triple5)] The tiger eats the bear.[(triple6)] The tiger sees the bear.[(triple7)] @1: The cat chases the bear.[(((triple3 triple2) -> rule4))] The tiger eats the tiger.[(((triple6) -> rule8))] @2: The bear sees the cat.[(((((triple3 triple2) -> rule4)) -> rule3))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The cat eats the tiger.
("cat" "eats" "tiger" "+")
triple4
((triple3) -> (rule8 % int1))
The cat eats the tiger.
("cat" "eats" "tiger" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple7
The cat chases the bear.
("cat" "chases" "bear" "+")
((triple3 triple2) -> (rule4 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple6) -> (rule8 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
((((triple3 triple2) -> (rule4 % int2))) -> (rule3 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2