Dave is nice. Dave is rough. Erin is kind. Erin is red. Gary is red. Gary is rough. Harry is rough. All nice, red things are rough. If something is nice then it is smart. Nice, blue things are red. All blue, quiet things are nice. If Erin is kind then Erin is nice. If something is smart and red then it is quiet. If something is kind and red then it is blue. All quiet, nice things are kind.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All nice, red things are rough.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Nice, blue things are red.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
All blue, quiet things are nice.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If Erin is kind then Erin is nice.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "nice" "+"))
If something is smart and red then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and red then it is blue.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
All quiet, nice things are kind.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Erin is kind.
True
1
proof
[(triple3)]
("Erin" "is" "kind" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Dave is smart.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is not blue.
False
3
inv-proof
[(((triple3 triple4) -> rule7))]
("Erin" "is" "blue" "-")
((triple3 triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Harry is nice.
Unknown
rconc
[@3: Harry is nice.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule8 <- FAIL)]]
("Harry" "is" "nice" "+")
@0: Dave is nice.[(triple1)] Dave is rough.[(triple2)] Erin is kind.[(triple3)] Erin is red.[(triple4)] Gary is red.[(triple5)] Gary is rough.[(triple6)] Harry is rough.[(triple7)] @1: Dave is smart.[(((triple1) -> rule2))] Erin is blue.[(((triple3 triple4) -> rule7))] Erin is nice.[(((triple3) -> rule5))] @2: Erin is rough.[(((((triple3) -> rule5) triple4) -> rule1))] Erin is smart.[(((((triple3) -> rule5)) -> rule2))] @3: Erin is quiet.[(((((((triple3) -> rule5)) -> rule2) triple4) -> rule6))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3 triple4) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3