Anne is quiet. Charlie is nice. All smart things are quiet. If Anne is quiet then Anne is round. Young things are quiet. Round, big things are rough. Nice, rough things are round. If something is young and rough then it is nice. Quiet, nice things are young. If Anne is round and Anne is big then Anne is rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
All smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If Anne is quiet then Anne is round.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Round, big things are rough.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Nice, rough things are round.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is young and rough then it is nice.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Quiet, nice things are young.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If Anne is round and Anne is big then Anne is rough.
((("Anne" "is" "round" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "rough" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Anne is round.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "round" "-")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Charlie is nice.[(triple2)] @1: Anne is round.[(((triple1) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1