The dog is nice. Rough, nice people are young. All kind people are young. If someone is kind and not rough then they are not young. If someone is kind and big then they are nice. If the dog is big then the dog is kind. If the dog is young and the dog is not rough then the dog is kind. Young, rough people are big. All nice people are big.
The dog is nice.
("dog" "is" "nice" "+")
Rough, nice people are young.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not rough then they are not young.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "-"))
If someone is kind and big then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If the dog is big then the dog is kind.
((("dog" "is" "big" "+")) -> ("dog" "is" "kind" "+"))
If the dog is young and the dog is not rough then the dog is kind.
((("dog" "is" "young" "+") ("dog" "is" "rough" "~")) -> ("dog" "is" "kind" "+"))
Young, rough people are big.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
The dog is nice.
True
1
proof
[(triple1)]
("dog" "is" "nice" "+")
triple1
The dog is not nice.
False
1
inv-proof
[(triple1)]
("dog" "is" "nice" "-")
triple1
The dog is big.
True
2
proof
[(((triple1) -> rule8))]
("dog" "is" "big" "+")
((triple1) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple1) -> rule8))]
("dog" "is" "big" "-")
((triple1) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
True
3
proof
[(((((triple1) -> rule8)) -> rule5))]
("dog" "is" "kind" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule5))]
("dog" "is" "kind" "-")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog is nice.[(triple1)] @1: The dog is big.[(((triple1) -> rule8))] @2: The dog is kind.[(((((triple1) -> rule8)) -> rule5))] @3: The dog is young.[(((((((triple1) -> rule8)) -> rule5)) -> rule2))]
The dog is nice.
("dog" "is" "nice" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
((triple1) -> (rule8 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3