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