The dog is kind. Green people are young. If the dog is kind then the dog is green. All kind people are nice. If someone is young then they are nice. Green, red people are kind. Nice, green people are kind.
The dog is kind.
("dog" "is" "kind" "+")
Green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If the dog is kind then the dog is green.
((("dog" "is" "kind" "+")) -> ("dog" "is" "green" "+"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Green, red people are kind.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Nice, green people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
The dog is kind.
True
1
proof
[(triple1)]
("dog" "is" "kind" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple1)]
("dog" "is" "kind" "-")
triple1
The dog is green.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "green" "+")
((triple1) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "green" "-")
((triple1) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The dog is kind.[(triple1)] @1: The dog is green.[(((triple1) -> rule2))] The dog is nice.[(((triple1) -> rule3) OR ((((((triple1) -> rule2)) -> rule1)) -> rule4))] @2: The dog is young.[(((((triple1) -> rule2)) -> rule1))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
((triple1) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple1) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2