The cat is green. The dog chases the mouse. The mouse visits the cat. The squirrel is nice. If something is nice then it visits the cat. If something is green and not nice then it is kind. If the cat is green then the cat chases the dog. If something sees the cat then the cat does not see the squirrel. If something chases the dog then it sees the cat. If something visits the dog and it does not see the squirrel then it is not rough.
The cat is green.
("cat" "is" "green" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something is nice then it visits the cat.
((("something" "is" "nice" "+")) -> ("something" "visits" "cat" "+"))
If something is green and not nice then it is kind.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "+"))
If the cat is green then the cat chases the dog.
((("cat" "is" "green" "+")) -> ("cat" "chases" "dog" "+"))
If something sees the cat then the cat does not see the squirrel.
((("something" "sees" "cat" "+")) -> ("cat" "sees" "squirrel" "-"))
If something chases the dog then it sees the cat.
((("something" "chases" "dog" "+")) -> ("something" "sees" "cat" "+"))
If something visits the dog and it does not see the squirrel then it is not rough.
((("something" "visits" "dog" "+") ("something" "sees" "squirrel" "~")) -> ("something" "is" "rough" "-"))
The cat is green.
True
1
proof
[(triple1)]
("cat" "is" "green" "+")
triple1
The cat is not green.
False
1
inv-proof
[(triple1)]
("cat" "is" "green" "-")
triple1
The squirrel visits the cat.
True
2
proof
[(((triple4) -> rule1))]
("squirrel" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel does not visit the cat.
False
2
inv-proof
[(((triple4) -> rule1))]
("squirrel" "visits" "cat" "-")
((triple4) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat sees the cat.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("cat" "sees" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat does not see the cat.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("cat" "sees" "cat" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The squirrel does not see the cat.
Unknown
inv-rconc
[@1: The squirrel sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "cat" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "sees" "cat" "+")
The dog does not visit the cat.
Unknown
inv-rconc
[@1: The dog visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "cat" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cat is green.[(triple1)] The dog chases the mouse.[(triple2)] The mouse visits the cat.[(triple3)] The squirrel is nice.[(triple4)] @1: The cat chases the dog.[(((triple1) -> rule3))] The squirrel visits the cat.[(((triple4) -> rule1))] @2: The cat sees the cat.[(((((triple1) -> rule3)) -> rule5))] @3: The cat does not see the squirrel.[(((((((triple1) -> rule3)) -> rule5)) -> rule4))]
The cat is green.
("cat" "is" "green" "+")
triple1
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The cat chases the dog.
("cat" "chases" "dog" "+")
((triple1) -> (rule3 % int1))
The cat chases the dog.
("cat" "chases" "dog" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple4) -> (rule1 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat chases the dog.
("cat" "chases" "dog" "+")
int2
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat does not see the squirrel.
("cat" "sees" "squirrel" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat chases the dog.
("cat" "chases" "dog" "+")
int3