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