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