Anne is red. Gary is nice. Harry is smart. All big people are young. White people are young. All nice, big people are furry. All red people are white. White, red people are nice. If someone is white and young then they are nice.
Anne is red.
("Anne" "is" "red" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All nice, big people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
White, red people are nice.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and young then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Harry is not smart.
False
1
inv-proof
[(triple3)]
("Harry" "is" "smart" "-")
triple3
Anne is white.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "white" "+")
((triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "white" "-")
((triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "+")
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is red.[(triple1)] Gary is nice.[(triple2)] Harry is smart.[(triple3)] @1: Anne is white.[(((triple1) -> rule4))] @2: Anne is nice.[(((((triple1) -> rule4) triple1) -> rule5) OR ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule6))] Anne is young.[(((((triple1) -> rule4)) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2