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