Erin is big. Harry is big. Harry is young. If someone is young then they are quiet. Rough people are not young. All rough people are white.
Erin is big.
("Erin" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Rough people are not young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "-"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "quiet" "-")
((triple3) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Erin is big.[(triple1)] Harry is big.[(triple2)] Harry is young.[(triple3)] @1: Harry is quiet.[(((triple3) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1