The bear eats the cat. The bear eats the mouse. The bear is green. The bear needs the mouse. The cat eats the bear. The cat is green. The mouse needs the bear. All green things are nice. If something is nice and it chases the mouse then the mouse chases the cat. If something is nice then it chases the cat.
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat is green.
("cat" "is" "green" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is nice and it chases the mouse then the mouse chases the cat.
((("something" "is" "nice" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "chases" "cat" "+"))
If something is nice then it chases the cat.
((("something" "is" "nice" "+")) -> ("something" "chases" "cat" "+"))
The cat eats the bear.
True
1
proof
[(triple5)]
("cat" "eats" "bear" "+")
triple5
The bear does not need the mouse.
False
1
inv-proof
[(triple4)]
("bear" "needs" "mouse" "-")
triple4
The bear is nice.
True
2
proof
[(((triple3) -> rule1))]
("bear" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "is" "nice" "-")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear chases the cat.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("bear" "chases" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not chase the cat.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("bear" "chases" "cat" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "-")
The mouse chases the cat.
Unknown
rconc
[@2: The mouse chases the cat.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "chases" "cat" "+")
The mouse does not need the cat.
Unknown
inv-random
[@0: The mouse needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "cat" "-")
The bear chases the mouse.
Unknown
random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The cat chases the bear.
Unknown
random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "+")
@0: The bear eats the cat.[(triple1)] The bear eats the mouse.[(triple2)] The bear is green.[(triple3)] The bear needs the mouse.[(triple4)] The cat eats the bear.[(triple5)] The cat is green.[(triple6)] The mouse needs the bear.[(triple7)] @1: The bear is nice.[(((triple3) -> rule1))] The cat is nice.[(((triple6) -> rule1))] @2: The bear chases the cat.[(((((triple3) -> rule1)) -> rule3))] The cat chases the cat.[(((((triple6) -> rule1)) -> rule3))]
The bear eats the cat.
("bear" "eats" "cat" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The cat eats the bear.
("cat" "eats" "bear" "+")
triple5
The cat is green.
("cat" "is" "green" "+")
triple6
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple7
The bear is nice.
("bear" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((triple6) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2