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