Erin is not big. Erin is quiet. Erin is young. Harry is quiet. Harry is not red. Harry is round. Harry is smart. Big people are rough. All rough, round people are not young. If someone is red and young then they are round. If someone is young and big then they are round. If someone is young then they are round. If someone is rough then they are quiet.
Erin is not big.
("Erin" "is" "big" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All rough, round people are not young.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "-"))
If someone is red and young then they are round.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is young and big then they are round.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Harry is round.
True
1
proof
[(triple6)]
("Harry" "is" "round" "+")
triple6
Erin is big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is round.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "round" "+")
((triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "round" "-")
((triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is not big.[(triple1)] Erin is quiet.[(triple2)] Erin is young.[(triple3)] Harry is not red.[(triple5)] Harry is quiet.[(triple4)] Harry is round.[(triple6)] Harry is smart.[(triple7)] @1: Erin is round.[(((triple3) -> rule5))]
Erin is not big.
("Erin" "is" "big" "-")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is not red.
("Harry" "is" "red" "-")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1