The dog is red. Big people are red. All young people are big. If someone is red then they are young. Round, kind people are red. All big people are young. If someone is round then they are big.
The dog is red.
("dog" "is" "red" "+")
Big people are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Round, kind people are red.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
The dog is red.
True
1
proof
[(triple1)]
("dog" "is" "red" "+")
triple1
The dog is not red.
False
1
inv-proof
[(triple1)]
("dog" "is" "red" "-")
triple1
The dog is young.
True
2
proof
[(((triple1) -> rule3))]
("dog" "is" "young" "+")
((triple1) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("dog" "is" "young" "-")
((triple1) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("dog" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
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 red.[(triple1)] @1: The dog is young.[(((triple1) -> rule3))] @2: The dog is big.[(((((triple1) -> rule3)) -> rule2))]
The dog is red.
("dog" "is" "red" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
((triple1) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2