Anne is cold. Charlie is cold. Erin is big. Harry is young. All young things are kind. All round things are kind. If Harry is kind then Harry is round.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is big.
("Erin" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Harry is kind.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Harry" "is" "round" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Harry" "is" "round" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is cold.[(triple1)] Charlie is cold.[(triple2)] Erin is big.[(triple3)] Harry is young.[(triple4)] @1: Harry is kind.[(((triple4) -> rule1))] @2: Harry is round.[(((((triple4) -> rule1)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2