Erin is blue. Gary is blue. Harry is round. Round things are kind. If Harry is blue and Harry is round then Harry is kind. If something is furry and nice then it is smart. If Harry is blue then Harry is nice. All kind things are green. All green things are nice.
Erin is blue.
("Erin" "is" "blue" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Harry is blue and Harry is round then Harry is kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "kind" "+"))
If something is furry and nice then it is smart.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Harry is blue then Harry is nice.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "nice" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Gary is blue.
True
1
proof
[(triple2)]
("Gary" "is" "blue" "+")
triple2
Erin is not blue.
False
1
inv-proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
Harry is kind.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "kind" "-")
((triple3) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("Harry" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("Harry" "is" "green" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
True
4
proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "nice" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not nice.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule6))]
("Harry" "is" "nice" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "-")
Erin is green.
Unknown
rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Erin is blue.[(triple1)] Gary is blue.[(triple2)] Harry is round.[(triple3)] @1: Harry is kind.[(((triple3) -> rule1))] @2: Harry is green.[(((((triple3) -> rule1)) -> rule5))] @3: Harry is nice.[(((((((triple3) -> rule1)) -> rule5)) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3