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