The bear needs the cow. The cow is nice. The mouse eats the cow. The tiger chases the mouse. If something eats the bear and it eats the cow then the bear chases the tiger. Nice things are big. If something is red and it chases the bear then the bear is rough. If something eats the bear then it eats the tiger. If something eats the bear and the bear needs the tiger then the tiger chases the mouse. If the tiger is rough and the tiger is cold then the tiger chases the bear. If something eats the bear then it eats the tiger. If something chases the mouse and it needs the tiger then it is red.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow is nice.
("cow" "is" "nice" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
If something eats the bear and it eats the cow then the bear chases the tiger.
((("something" "eats" "bear" "+") ("something" "eats" "cow" "+")) -> ("bear" "chases" "tiger" "+"))
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is red and it chases the bear then the bear is rough.
((("something" "is" "red" "+") ("something" "chases" "bear" "+")) -> ("bear" "is" "rough" "+"))
If something eats the bear then it eats the tiger.
((("something" "eats" "bear" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the bear and the bear needs the tiger then the tiger chases the mouse.
((("something" "eats" "bear" "+") ("bear" "needs" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If the tiger is rough and the tiger is cold then the tiger chases the bear.
((("tiger" "is" "rough" "+") ("tiger" "is" "cold" "+")) -> ("tiger" "chases" "bear" "+"))
If something eats the bear then it eats the tiger.
((("something" "eats" "bear" "+")) -> ("something" "eats" "tiger" "+"))
If something chases the mouse and it needs the tiger then it is red.
((("something" "chases" "mouse" "+") ("something" "needs" "tiger" "+")) -> ("something" "is" "red" "+"))
The tiger chases the mouse.
True
1
proof
[(triple4)]
("tiger" "chases" "mouse" "+")
triple4
The tiger does not chase the mouse.
False
1
inv-proof
[(triple4)]
("tiger" "chases" "mouse" "-")
triple4
The cow is big.
True
2
proof
[(((triple2) -> rule2))]
("cow" "is" "big" "+")
((triple2) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "is" "big" "-")
((triple2) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "tiger" "-")
The cow eats the tiger.
Unknown
rconc
[@1: The cow eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "tiger" "+")
The tiger does not need the bear.
Unknown
inv-random
[@0: The tiger needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bear" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
@0: The bear needs the cow.[(triple1)] The cow is nice.[(triple2)] The mouse eats the cow.[(triple3)] The tiger chases the mouse.[(triple4)] @1: The cow is big.[(((triple2) -> rule2))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple4
The cow is big.
("cow" "is" "big" "+")
((triple2) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1