Anne is blue. Anne is nice. Anne is round. Dave is blue. Dave is nice. Dave is quiet. Fiona is kind. Fiona is smart. Harry is blue. Harry is kind. Harry is quiet. Harry is round. Nice, smart people are white. If someone is kind and nice then they are smart. Quiet people are nice. All round people are kind. If Harry is smart then Harry is white. If Harry is blue and Harry is quiet then Harry is smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Nice, smart people are white.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and nice then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Harry is smart then Harry is white.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "white" "+"))
If Harry is blue and Harry is quiet then Harry is smart.
((("Harry" "is" "blue" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "smart" "+"))
Dave is blue.
True
1
proof
[(triple4)]
("Dave" "is" "blue" "+")
triple4
Fiona is not kind.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "kind" "-")
triple7
Anne is kind.
True
2
proof
[(((triple3) -> rule4))]
("Anne" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple3) -> rule4))]
("Anne" "is" "kind" "-")
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is white.
True
4
proof
[(((((triple9 triple11) -> rule6)) -> rule5) OR ((((triple11) -> rule3) ((triple9 triple11) -> rule6)) -> rule1) OR ((((triple10 ((triple11) -> rule3)) -> rule2)) -> rule5) OR ((((((triple12) -> rule4) ((triple11) -> rule3)) -> rule2)) -> rule5) OR ((((triple11) -> rule3) ((triple10 ((triple11) -> rule3)) -> rule2)) -> rule1) OR ((((triple11) -> rule3) ((((triple12) -> rule4) ((triple11) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "white" "+")
((((triple9 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple9 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple10 ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple12) -> (rule4 % int4)) ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple11) -> (rule3 % int3)) ((triple10 ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple11) -> (rule3 % int4)) ((((triple12) -> (rule4 % int3)) ((triple11) -> (rule3 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Anne is not smart.
False
4
inv-proof
[(((((triple3) -> rule4) triple2) -> rule2))]
("Anne" "is" "smart" "-")
((((triple3) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
True
6
proof
[(((triple2 ((((triple3) -> rule4) triple2) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((triple2 ((((triple3) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not white.
False
6
inv-proof
[(((triple2 ((((triple3) -> rule4) triple2) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((triple2 ((((triple3) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@3: Dave is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule4 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is nice.[(triple2)] Anne is round.[(triple3)] Dave is blue.[(triple4)] Dave is nice.[(triple5 OR ((triple6) -> rule3))] Dave is quiet.[(triple6)] Fiona is kind.[(triple7)] Fiona is smart.[(triple8)] Harry is blue.[(triple9)] Harry is kind.[(triple10 OR ((triple12) -> rule4))] Harry is quiet.[(triple11)] Harry is round.[(triple12)] @1: Anne is kind.[(((triple3) -> rule4))] Harry is nice.[(((triple11) -> rule3))] Harry is smart.[(((triple9 triple11) -> rule6) OR ((triple10 ((triple11) -> rule3)) -> rule2) OR ((((triple12) -> rule4) ((triple11) -> rule3)) -> rule2))] @2: Anne is smart.[(((((triple3) -> rule4) triple2) -> rule2))] Harry is white.[(((((triple9 triple11) -> rule6)) -> rule5) OR ((((triple11) -> rule3) ((triple9 triple11) -> rule6)) -> rule1) OR ((((triple10 ((triple11) -> rule3)) -> rule2)) -> rule5) OR ((((((triple12) -> rule4) ((triple11) -> rule3)) -> rule2)) -> rule5) OR ((((triple11) -> rule3) ((triple10 ((triple11) -> rule3)) -> rule2)) -> rule1) OR ((((triple11) -> rule3) ((((triple12) -> rule4) ((triple11) -> rule3)) -> rule2)) -> rule1))] @3: Anne is white.[(((triple2 ((((triple3) -> rule4) triple2) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple12) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Anne is kind.
("Anne" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple11) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple9 triple11) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple10 ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple12) -> (rule4 % int3)) ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple9 triple11) -> (rule6 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple9 triple11) -> (rule6 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple10 ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple12) -> (rule4 % int4)) ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((triple11) -> (rule3 % int3)) ((triple10 ((triple11) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple11) -> (rule3 % int4)) ((((triple12) -> (rule4 % int3)) ((triple11) -> (rule3 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((triple2 ((((triple3) -> (rule4 % int3)) triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3