The dog is kind. If the dog is kind and the dog is big then the dog is red. All kind people are big. If the dog is not big then the dog is young. All big, red people are young. If someone is kind and not red then they are young. Kind, rough people are not young.
The dog is kind.
("dog" "is" "kind" "+")
If the dog is kind and the dog is big then the dog is red.
((("dog" "is" "kind" "+") ("dog" "is" "big" "+")) -> ("dog" "is" "red" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the dog is not big then the dog is young.
((("dog" "is" "big" "~")) -> ("dog" "is" "young" "+"))
All big, red people are young.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not red then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "young" "+"))
Kind, rough people are not young.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
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 big.
True
2
proof
[(((triple1) -> rule2))]
("dog" "is" "big" "+")
((triple1) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "is" "big" "-")
((triple1) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is red.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("dog" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("dog" "is" "red" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
True
7
proof
[(((((triple1) -> rule2) ((triple1 ((triple1) -> rule2)) -> rule1)) -> rule4))]
("dog" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
The dog is not young.
False
7
inv-proof
[(((((triple1) -> rule2) ((triple1 ((triple1) -> rule2)) -> rule1)) -> rule4))]
("dog" "is" "young" "-")
((((triple1) -> (rule2 % int3)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3
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 chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is kind.[(triple1)] @1: The dog is big.[(((triple1) -> rule2))] @2: The dog is red.[(((triple1 ((triple1) -> rule2)) -> rule1))] @3: The dog is young.[(((((triple1) -> rule2) ((triple1 ((triple1) -> rule2)) -> rule1)) -> rule4))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
((triple1) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple1) -> (rule2 % int3)) ((triple1 ((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is big.
("dog" "is" "big" "+")
int3