The mouse is nice. The squirrel does not need the mouse. The tiger is not nice. If someone is big then they chase the mouse. All nice people are big.
The mouse is nice.
("mouse" "is" "nice" "+")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
If someone is big then they chase the mouse.
((("someone" "is" "big" "+")) -> ("someone" "chases" "mouse" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
The mouse is nice.
True
1
proof
[(triple1)]
("mouse" "is" "nice" "+")
triple1
The mouse is not nice.
False
1
inv-proof
[(triple1)]
("mouse" "is" "nice" "-")
triple1
The mouse is big.
True
2
proof
[(((triple1) -> rule2))]
("mouse" "is" "big" "+")
((triple1) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("mouse" "is" "big" "-")
((triple1) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse chases the mouse.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("mouse" "chases" "mouse" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse does not chase the mouse.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("mouse" "chases" "mouse" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The squirrel does not chase the mouse.
Unknown
inv-rconc
[@2: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("squirrel" "chases" "mouse" "-")
The tiger is big.
Unknown
rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "big" "+")
The tiger does not chase the mouse.
Unknown
inv-rconc
[@2: The tiger chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
The tiger does not eat the mouse.
Unknown
inv-random
[@0: The tiger eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "mouse" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The mouse is nice.[(triple1)] The squirrel does not need the mouse.[(triple2)] The tiger is not nice.[(triple3)] @1: The mouse is big.[(((triple1) -> rule2))] @2: The mouse chases the mouse.[(((((triple1) -> rule2)) -> rule1))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple2
The tiger is not nice.
("tiger" "is" "nice" "-")
triple3
The mouse is big.
("mouse" "is" "big" "+")
((triple1) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2