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