Anne is blue. Anne is kind. Anne is smart. Anne is young. Harry is green. Harry is not kind. Harry is quiet. If someone is quiet and not green then they are kind. Nice people are kind. Smart people are quiet. If someone is young then they are smart. All quiet, green people are young. If someone is smart then they are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is quiet and not green then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All quiet, green people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple3) -> rule6) OR ((((triple4) -> rule4)) -> rule6))]
("Anne" "is" "blue" "+")
triple1
((triple3) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule6) OR ((((triple4) -> rule4)) -> rule6))]
("Anne" "is" "blue" "-")
triple1
((triple3) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is young.
True
3
proof
[(((triple7 triple5) -> rule5))]
("Harry" "is" "young" "+")
((triple7 triple5) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple4) -> rule4)) -> rule3))]
("Anne" "is" "quiet" "-")
((triple3) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is smart.
True
4
proof
[(((((triple7 triple5) -> rule5)) -> rule4))]
("Harry" "is" "smart" "+")
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple7 triple5) -> rule5)) -> rule4))]
("Harry" "is" "smart" "-")
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
True
5
proof
[(((((((triple7 triple5) -> rule5)) -> rule4)) -> rule6))]
("Harry" "is" "blue" "+")
((((((triple7 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not blue.
False
5
inv-proof
[(((((((triple7 triple5) -> rule5)) -> rule4)) -> rule6))]
("Harry" "is" "blue" "-")
((((((triple7 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1 OR ((triple3) -> rule6) OR ((((triple4) -> rule4)) -> rule6))] Anne is kind.[(triple2)] Anne is smart.[(triple3 OR ((triple4) -> rule4))] Anne is young.[(triple4)] Harry is green.[(triple5)] Harry is not kind.[(triple6)] Harry is quiet.[(triple7)] @1: Anne is quiet.[(((triple3) -> rule3) OR ((((triple4) -> rule4)) -> rule3))] Harry is young.[(((triple7 triple5) -> rule5))] @2: Harry is smart.[(((((triple7 triple5) -> rule5)) -> rule4))] @3: Harry is blue.[(((((((triple7 triple5) -> rule5)) -> rule4)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple3) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple4) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is not kind.
("Harry" "is" "kind" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple7 triple5) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple7 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3