Charlie is kind. Erin is blue. Gary is kind. Harry is young. All blue things are young. Kind, white things are young. All round things are kind. All blue things are round. All young, kind things are round. Young things are blue.
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Kind, white things are young.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All young, kind things are round.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Erin is young.
True
2
proof
[(((triple2) -> rule1))]
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "round" "-")
((triple2) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Erin" "is" "kind" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Harry is kind.
True
4
proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule3))]
("Harry" "is" "kind" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not kind.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule3))]
("Harry" "is" "kind" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@3: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule2 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is blue.
Unknown
rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not round.
Unknown
inv-rconc
[@4: Gary is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- rule2 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is round.
Unknown
rconc
[@4: Charlie is round.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
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 kind.[(triple1)] Erin is blue.[(triple2)] Gary is kind.[(triple3)] Harry is young.[(triple4)] @1: Erin is round.[(((triple2) -> rule4))] Erin is young.[(((triple2) -> rule1))] Harry is blue.[(((triple4) -> rule6))] @2: Erin is kind.[(((((triple2) -> rule4)) -> rule3))] Harry is round.[(((((triple4) -> rule6)) -> rule4))] @3: Harry is kind.[(((((((triple4) -> rule6)) -> rule4)) -> rule3))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3