Anne is rough. Dave is young. Erin is rough. All smart, kind things are rough. Nice, rough things are not kind. All rough things are nice. Rough things are nice. If something is rough then it is smart. Kind, smart things are young. If something is nice and not rough then it is quiet. Quiet things are green.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All smart, kind things are rough.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Nice, rough things are not kind.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "-"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Kind, smart things are young.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is nice and not rough then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "rough" "~")) -> ("something" "is" "quiet" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Erin is rough.
True
1
proof
[(triple3)]
("Erin" "is" "rough" "+")
triple3
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is rough.[(triple1)] Dave is young.[(triple2)] Erin is rough.[(triple3)] @1: Anne is nice.[(((triple1) -> rule3) OR ((triple1) -> rule4))] Anne is smart.[(((triple1) -> rule5))] Erin is nice.[(((triple3) -> rule3) OR ((triple3) -> rule4))] Erin is smart.[(((triple3) -> rule5))] @2: Anne is not kind.[(((((triple1) -> rule3) triple1) -> rule2) OR ((((triple1) -> rule4) triple1) -> rule2))] Erin is not kind.[(((((triple3) -> rule3) triple3) -> rule2) OR ((((triple3) -> rule4) triple3) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple1) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Erin is not kind.
("Erin" "is" "kind" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple3) -> (rule4 % int2)) triple3) -> (rule2 % int1))
Erin is not kind.
("Erin" "is" "kind" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2