Charlie is not green. Gary is kind. Harry is young. If Harry is green and Harry is young then Harry is blue. If someone is green then they are blue. Furry people are blue. Kind people are furry. All blue, smart people are kind. Furry, blue people are smart.
Charlie is not green.
("Charlie" "is" "green" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is green and Harry is young then Harry is blue.
((("Harry" "is" "green" "+") ("Harry" "is" "young" "+")) -> ("Harry" "is" "blue" "+"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All blue, smart people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Furry, blue people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Gary is kind.
True
1
proof
[(triple2)]
("Gary" "is" "kind" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Gary is furry.
True
2
proof
[(((triple2) -> rule4))]
("Gary" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple2) -> rule4))]
("Gary" "is" "furry" "-")
((triple2) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "smart" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not smart.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule6))]
("Gary" "is" "smart" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@4: Charlie is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is furry.
Unknown
rconc
[@3: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule2 <- FAIL)]]
("Charlie" "is" "furry" "+")
Harry is not furry.
Unknown
inv-rconc
[@3: Harry is furry.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is blue.
Unknown
rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is not green.[(triple1)] Gary is kind.[(triple2)] Harry is young.[(triple3)] @1: Gary is furry.[(((triple2) -> rule4))] @2: Gary is blue.[(((((triple2) -> rule4)) -> rule3))] @3: Gary is smart.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule3)) -> rule6))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3