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