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