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