Charlie is cold. Charlie is red. Charlie is smart. Erin is blue. Gary is cold. Gary is young. Harry is cold. Harry is kind. Harry is smart. Harry is young. If something is blue then it is young. Red, young things are blue. If Charlie is blue and Charlie is young then Charlie is kind.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Red, young things are blue.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Charlie is blue and Charlie is young then Charlie is kind.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "kind" "+"))
Gary is cold.
True
1
proof
[(triple5)]
("Gary" "is" "cold" "+")
triple5
Charlie is not red.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "red" "-")
triple2
Erin is young.
True
2
proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "young" "-")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "young" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Charlie is cold.[(triple1)] Charlie is red.[(triple2)] Charlie is smart.[(triple3)] Erin is blue.[(triple4)] Gary is cold.[(triple5)] Gary is young.[(triple6)] Harry is cold.[(triple7)] Harry is kind.[(triple8)] Harry is smart.[(triple9)] Harry is young.[(triple10)] @1: Erin is young.[(((triple4) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1