Charlie is blue. Charlie is red. Charlie is round. Dave is cold. Dave is kind. Dave is quiet. Dave is not red. Dave is not round. Fiona is blue. Fiona is not cold. Fiona is kind. Fiona is nice. Fiona is quiet. Fiona is not red. Fiona is round. Harry is round. All nice, round things are kind. Cold, kind things are not blue. If Harry is round then Harry is cold. All cold, round things are nice. If Harry is round and Harry is not blue then Harry is quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not round.
("Dave" "is" "round" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is round.
("Harry" "is" "round" "+")
All nice, round things are kind.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Cold, kind things are not blue.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "-"))
If Harry is round then Harry is cold.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "cold" "+"))
All cold, round things are nice.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Harry is round and Harry is not blue then Harry is quiet.
((("Harry" "is" "round" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple6)]
("Dave" "is" "quiet" "+")
triple6
Dave is not kind.
False
1
inv-proof
[(triple5)]
("Dave" "is" "kind" "-")
triple5
Dave is not blue.
True
3
proof
[(((triple4 triple5) -> rule2))]
("Dave" "is" "blue" "-")
((triple4 triple5) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Harry is not cold.
False
2
inv-proof
[(((triple16) -> rule3))]
("Harry" "is" "cold" "-")
((triple16) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
True
4
proof
[(((((triple16) -> rule3) triple16) -> rule4))]
("Harry" "is" "nice" "+")
((((triple16) -> (rule3 % int2)) triple16) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not nice.
False
4
inv-proof
[(((((triple16) -> rule3) triple16) -> rule4))]
("Harry" "is" "nice" "-")
((((triple16) -> (rule3 % int2)) triple16) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
True
6
proof
[(((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1))]
("Harry" "is" "kind" "+")
((((((triple16) -> (rule3 % int3)) triple16) -> (rule4 % int2)) triple16) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not kind.
False
6
inv-proof
[(((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1))]
("Harry" "is" "kind" "-")
((((((triple16) -> (rule3 % int3)) triple16) -> (rule4 % int2)) triple16) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not blue.
True
9
proof
[(((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2))]
("Harry" "is" "blue" "-")
((((triple16) -> (rule3 % int4)) ((((((triple16) -> (rule3 % int4)) triple16) -> (rule4 % int3)) triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is blue.
False
9
inv-proof
[(((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2))]
("Harry" "is" "blue" "+")
((((triple16) -> (rule3 % int4)) ((((((triple16) -> (rule3 % int4)) triple16) -> (rule4 % int3)) triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is quiet.
True
11
proof
[(((triple16 ((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "quiet" "+")
((triple16 ((((triple16) -> (rule3 % int5)) ((((((triple16) -> (rule3 % int5)) triple16) -> (rule4 % int4)) triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Harry is not quiet.
False
11
inv-proof
[(((triple16 ((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2)) -> rule5))]
("Harry" "is" "quiet" "-")
((triple16 ((((triple16) -> (rule3 % int5)) ((((((triple16) -> (rule3 % int5)) triple16) -> (rule4 % int4)) triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Charlie is blue.[(triple1)] Charlie is red.[(triple2)] Charlie is round.[(triple3)] Dave is cold.[(triple4)] Dave is kind.[(triple5)] Dave is not red.[(triple7)] Dave is not round.[(triple8)] Dave is quiet.[(triple6)] Fiona is blue.[(triple9)] Fiona is kind.[(triple11 OR ((triple12 triple15) -> rule1))] Fiona is nice.[(triple12)] Fiona is not cold.[(triple10)] Fiona is not red.[(triple14)] Fiona is quiet.[(triple13)] Fiona is round.[(triple15)] Harry is round.[(triple16)] @1: Dave is not blue.[(((triple4 triple5) -> rule2))] Harry is cold.[(((triple16) -> rule3))] @2: Harry is nice.[(((((triple16) -> rule3) triple16) -> rule4))] @3: Harry is kind.[(((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1))] @4: Harry is not blue.[(((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2))] @5: Harry is quiet.[(((triple16 ((((triple16) -> rule3) ((((((triple16) -> rule3) triple16) -> rule4) triple16) -> rule1)) -> rule2)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is not red.
("Dave" "is" "red" "-")
triple7
Dave is not round.
("Dave" "is" "round" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple11
((triple12 triple15) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple10
Fiona is not red.
("Fiona" "is" "red" "-")
triple14
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple13
Fiona is round.
("Fiona" "is" "round" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Dave is not blue.
("Dave" "is" "blue" "-")
((triple4 triple5) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple16) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple16) -> (rule3 % int2)) triple16) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple16) -> (rule3 % int3)) triple16) -> (rule4 % int2)) triple16) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not blue.
("Harry" "is" "blue" "-")
((((triple16) -> (rule3 % int4)) ((((((triple16) -> (rule3 % int4)) triple16) -> (rule4 % int3)) triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple16 ((((triple16) -> (rule3 % int5)) ((((((triple16) -> (rule3 % int5)) triple16) -> (rule4 % int4)) triple16) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5