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