Charlie is furry. Harry is red. Harry is young. Young, red things are smart. All nice things are smart. If something is furry then it is green. Green, young things are nice. Red things are furry. If Charlie is red and Charlie is furry then Charlie is young.
Charlie is furry.
("Charlie" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Young, red things are smart.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
Green, young things are nice.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Charlie is red and Charlie is furry then Charlie is young.
((("Charlie" "is" "red" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "young" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "furry" "-")
((triple2) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("Harry" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule3))]
("Harry" "is" "green" "-")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "smart" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is furry.[(triple1)] Harry is red.[(triple2)] Harry is young.[(triple3)] @1: Charlie is green.[(((triple1) -> rule3))] Harry is furry.[(((triple2) -> rule5))] Harry is smart.[(((triple3 triple2) -> rule1) OR ((((((((triple2) -> rule5)) -> rule3) triple3) -> rule4)) -> rule2))] @2: Harry is green.[(((((triple2) -> rule5)) -> rule3))] @3: Harry is nice.[(((((((triple2) -> rule5)) -> rule3) triple3) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Harry is red.
("Harry" "is" "red" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple2) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3 triple2) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) triple3) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3