The bear eats the rabbit. The mouse eats the bear. The rabbit visits the mouse. The tiger eats the bear. If the bear chases the tiger and the tiger visits the mouse then the tiger does not eat the bear. If something chases the tiger then the tiger chases the mouse. If the mouse eats the bear then the bear is nice. If something is nice then it chases the tiger. If something chases the bear then it is not big. If the tiger is cold then the tiger chases the bear. If the tiger is round then the tiger visits the mouse. If the rabbit chases the tiger and the rabbit chases the mouse then the tiger visits the bear.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
If the bear chases the tiger and the tiger visits the mouse then the tiger does not eat the bear.
((("bear" "chases" "tiger" "+") ("tiger" "visits" "mouse" "+")) -> ("tiger" "eats" "bear" "-"))
If something chases the tiger then the tiger chases the mouse.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If the mouse eats the bear then the bear is nice.
((("mouse" "eats" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something is nice then it chases the tiger.
((("something" "is" "nice" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the bear then it is not big.
((("something" "chases" "bear" "+")) -> ("something" "is" "big" "-"))
If the tiger is cold then the tiger chases the bear.
((("tiger" "is" "cold" "+")) -> ("tiger" "chases" "bear" "+"))
If the tiger is round then the tiger visits the mouse.
((("tiger" "is" "round" "+")) -> ("tiger" "visits" "mouse" "+"))
If the rabbit chases the tiger and the rabbit chases the mouse then the tiger visits the bear.
((("rabbit" "chases" "tiger" "+") ("rabbit" "chases" "mouse" "+")) -> ("tiger" "visits" "bear" "+"))
The mouse eats the bear.
True
1
proof
[(triple2)]
("mouse" "eats" "bear" "+")
triple2
The rabbit does not visit the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "visits" "mouse" "-")
triple3
The bear is nice.
True
2
proof
[(((triple2) -> rule3))]
("bear" "is" "nice" "+")
((triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "is" "nice" "-")
((triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule4))]
("bear" "chases" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not chase the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4))]
("bear" "chases" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The tiger chases the mouse.
True
4
proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule2))]
("tiger" "chases" "mouse" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The tiger does not chase the mouse.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule4)) -> rule2))]
("tiger" "chases" "mouse" "-")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The tiger does not chase the bear.
Unknown
inv-rconc
[@1: The tiger chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "bear" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The rabbit does not chase the tiger.
Unknown
inv-rconc
[@1: The rabbit chases the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "tiger" "-")
The tiger visits the bear.
Unknown
rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "bear" "+")
The mouse does not chase the rabbit.
Unknown
inv-random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "-")
The bear eats the tiger.
Unknown
random
[@0: The bear eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "tiger" "+")
The mouse does not visit the bear.
Unknown
inv-random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
@0: The bear eats the rabbit.[(triple1)] The mouse eats the bear.[(triple2)] The rabbit visits the mouse.[(triple3)] The tiger eats the bear.[(triple4)] @1: The bear is nice.[(((triple2) -> rule3))] @2: The bear chases the tiger.[(((((triple2) -> rule3)) -> rule4))] @3: The tiger chases the mouse.[(((((((triple2) -> rule3)) -> rule4)) -> rule2))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple3
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple4
The bear is nice.
("bear" "is" "nice" "+")
((triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
((((((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3