Anne is not green. Anne is round. Bob is green. Bob is nice. Fiona is red. Fiona is round. Harry is not green. All round people are big. All rough people are not big. If someone is rough and nice then they are not green. If someone is red and nice then they are green. If someone is big then they are red. Rough people are not red. Cold people are not nice. All cold, rough people are round.
Anne is not green.
("Anne" "is" "green" "-")
Anne is round.
("Anne" "is" "round" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is not green.
("Harry" "is" "green" "-")
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All rough people are not big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "-"))
If someone is rough and nice then they are not green.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
If someone is red and nice then they are green.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Rough people are not red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
Cold people are not nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "-"))
All cold, rough people are round.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Anne is round.
True
1
proof
[(triple2)]
("Anne" "is" "round" "+")
triple2
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Anne is big.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "big" "+")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Anne" "is" "big" "-")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
True
3
proof
[(((((triple2) -> rule1)) -> rule5))]
("Anne" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not red.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule5))]
("Anne" "is" "red" "-")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is not red.
Unknown
inv-rconc
[@3: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule8 <- FAIL)]]
("Bob" "is" "red" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Harry" "is" "big" "+")
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is not green.[(triple1)] Anne is round.[(triple2)] Bob is green.[(triple3)] Bob is nice.[(triple4)] Fiona is red.[(triple5 OR ((((triple6) -> rule1)) -> rule5))] Fiona is round.[(triple6)] Harry is not green.[(triple7)] @1: Anne is big.[(((triple2) -> rule1))] Fiona is big.[(((triple6) -> rule1))] @2: Anne is red.[(((((triple2) -> rule1)) -> rule5))]
Anne is not green.
("Anne" "is" "green" "-")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Harry is not green.
("Harry" "is" "green" "-")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple6) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2