The mouse is green. The mouse needs the rabbit. The mouse needs the tiger. The mouse visits the rabbit. The rabbit is round. The rabbit needs the tiger. The tiger chases the mouse. The tiger is big. The tiger needs the mouse. The tiger needs the rabbit. The tiger visits the mouse. The tiger visits the rabbit. If something needs the mouse and the mouse visits the rabbit then it is big. If something is young and it chases the rabbit then the rabbit visits the mouse. If something visits the mouse and the mouse visits the rabbit then the mouse chases the rabbit. If something chases the rabbit then it needs the mouse. If something is big and red then it chases the rabbit. If something needs the rabbit and it chases the rabbit then it is red.
The mouse is green.
("mouse" "is" "green" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something needs the mouse and the mouse visits the rabbit then it is big.
((("something" "needs" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("something" "is" "big" "+"))
If something is young and it chases the rabbit then the rabbit visits the mouse.
((("something" "is" "young" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If something visits the mouse and the mouse visits the rabbit then the mouse chases the rabbit.
((("something" "visits" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("mouse" "chases" "rabbit" "+"))
If something chases the rabbit then it needs the mouse.
((("something" "chases" "rabbit" "+")) -> ("something" "needs" "mouse" "+"))
If something is big and red then it chases the rabbit.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "chases" "rabbit" "+"))
If something needs the rabbit and it chases the rabbit then it is red.
((("something" "needs" "rabbit" "+") ("something" "chases" "rabbit" "+")) -> ("something" "is" "red" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple4)]
("mouse" "visits" "rabbit" "+")
triple4
The mouse does not need the tiger.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "tiger" "-")
triple3
The mouse chases the rabbit.
True
3
proof
[(((triple11 triple4) -> rule3))]
("mouse" "chases" "rabbit" "+")
((triple11 triple4) -> (rule3 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse does not chase the rabbit.
False
3
inv-proof
[(((triple11 triple4) -> rule3))]
("mouse" "chases" "rabbit" "-")
((triple11 triple4) -> (rule3 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse needs the mouse.
True
4
proof
[(((((triple11 triple4) -> rule3)) -> rule4))]
("mouse" "needs" "mouse" "+")
((((triple11 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse does not need the mouse.
False
4
inv-proof
[(((((triple11 triple4) -> rule3)) -> rule4))]
("mouse" "needs" "mouse" "-")
((((triple11 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is big.
True
6
proof
[(((((((triple11 triple4) -> rule3)) -> rule4) triple4) -> rule1))]
("mouse" "is" "big" "+")
((((((triple11 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The mouse is not big.
False
6
inv-proof
[(((((((triple11 triple4) -> rule3)) -> rule4) triple4) -> rule1))]
("mouse" "is" "big" "-")
((((((triple11 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3
The rabbit does not need the mouse.
Unknown
inv-rconc
[@3: The rabbit needs the mouse.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- FAIL)]]
("rabbit" "needs" "mouse" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@2: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "red" "-")
The tiger is red.
Unknown
rconc
[@2: The tiger is red.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("tiger" "is" "red" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The mouse is green.[(triple1)] The mouse needs the rabbit.[(triple2)] The mouse needs the tiger.[(triple3)] The mouse visits the rabbit.[(triple4)] The rabbit is round.[(triple5)] The rabbit needs the tiger.[(triple6)] The tiger chases the mouse.[(triple7)] The tiger is big.[(triple8 OR ((triple9 triple4) -> rule1))] The tiger needs the mouse.[(triple9)] The tiger needs the rabbit.[(triple10)] The tiger visits the mouse.[(triple11)] The tiger visits the rabbit.[(triple12)] @1: The mouse chases the rabbit.[(((triple11 triple4) -> rule3))] @2: The mouse is red.[(((triple2 ((triple11 triple4) -> rule3)) -> rule6))] The mouse needs the mouse.[(((((triple11 triple4) -> rule3)) -> rule4))] @3: The mouse is big.[(((((((triple11 triple4) -> rule3)) -> rule4) triple4) -> rule1))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple7
The tiger is big.
("tiger" "is" "big" "+")
triple8
((triple9 triple4) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple9
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple10
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple11
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple12
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple11 triple4) -> (rule3 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple2 ((triple11 triple4) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple11 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((((triple11 triple4) -> (rule3 % int3))) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int3