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