Anne is blue. Anne is green. Anne is nice. Anne is smart. Anne is not white. Anne is young. Bob is blue. Bob is smart. Harry is blue. Harry is smart. Harry is white. Harry is young. If someone is nice and white then they are blue. If someone is nice and white then they are not blue. All green people are rough. If someone is young and not nice then they are not green. White people are green. If someone is blue then they are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not white.
("Anne" "is" "white" "-")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is nice and white then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and white then they are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "-"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and not nice then they are not green.
((("someone" "is" "young" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "green" "-"))
White people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is blue then they are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Bob is smart.
True
1
proof
[(triple8)]
("Bob" "is" "smart" "+")
triple8
Anne is not green.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Anne" "is" "green" "-")
triple2
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Bob is green.
True
2
proof
[(((triple7) -> rule6))]
("Bob" "is" "green" "+")
((triple7) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple11) -> rule5) OR ((triple9) -> rule6))]
("Harry" "is" "green" "-")
((triple11) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is rough.
True
3
proof
[(((((triple7) -> rule6)) -> rule3))]
("Bob" "is" "rough" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule3))]
("Bob" "is" "rough" "-")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule6))] Anne is nice.[(triple3)] Anne is not white.[(triple5)] Anne is smart.[(triple4)] Anne is young.[(triple6)] Bob is blue.[(triple7)] Bob is smart.[(triple8)] Harry is blue.[(triple9)] Harry is smart.[(triple10)] Harry is white.[(triple11)] Harry is young.[(triple12)] @1: Anne is rough.[(((triple2) -> rule3) OR ((((triple1) -> rule6)) -> rule3))] Bob is green.[(((triple7) -> rule6))] Harry is green.[(((triple11) -> rule5) OR ((triple9) -> rule6))] @2: Bob is rough.[(((((triple7) -> rule6)) -> rule3))] Harry is rough.[(((((triple11) -> rule5)) -> rule3) OR ((((triple9) -> rule6)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not white.
("Anne" "is" "white" "-")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple6
Bob is blue.
("Bob" "is" "blue" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Anne is rough.
("Anne" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple7) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple11) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple7) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple9) -> (rule6 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2