Dave is kind. Erin is quiet. Harry is red. If something is kind then it is cold. If Erin is cold and Erin is rough then Erin is kind. Kind things are smart. If Dave is rough and Dave is kind then Dave is nice. If something is cold then it is smart. If something is cold then it is smart.
Dave is kind.
("Dave" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Erin is cold and Erin is rough then Erin is kind.
((("Erin" "is" "cold" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "kind" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Dave is rough and Dave is kind then Dave is nice.
((("Dave" "is" "rough" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "nice" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Dave is cold.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Erin is cold.
Unknown
rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Erin" "is" "cold" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Dave is kind.[(triple1)] Erin is quiet.[(triple2)] Harry is red.[(triple3)] @1: Dave is cold.[(((triple1) -> rule1))] Dave is smart.[(((triple1) -> rule3) OR ((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule1)) -> rule6))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2