Charlie is not blue. Charlie is not furry. Charlie is white. Charlie is young. Dave is furry. Dave is quiet. Fiona is quiet. Fiona is smart. Harry is kind. Harry is not smart. Harry is white. If something is young and kind then it is blue. Kind things are young. If something is white and kind then it is not smart. If something is furry and quiet then it is kind. Blue, kind things are white.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
If something is young and kind then it is blue.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is white and kind then it is not smart.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "-"))
If something is furry and quiet then it is kind.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Blue, kind things are white.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Charlie is white.
True
1
proof
[(triple3)]
("Charlie" "is" "white" "+")
triple3
Fiona is not quiet.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "quiet" "-")
triple7
Harry is young.
True
2
proof
[(((triple9) -> rule2))]
("Harry" "is" "young" "+")
((triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is not kind.
False
3
inv-proof
[(((triple5 triple6) -> rule4))]
("Dave" "is" "kind" "-")
((triple5 triple6) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
True
4
proof
[(((((triple5 triple6) -> rule4)) -> rule2))]
("Dave" "is" "young" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple9) -> rule2) triple9) -> rule1))]
("Harry" "is" "blue" "-")
((((triple9) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Dave is blue.
True
8
proof
[(((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1))]
("Dave" "is" "blue" "+")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5 triple6) -> (rule4 % int3))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not blue.
False
8
inv-proof
[(((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1))]
("Dave" "is" "blue" "-")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5 triple6) -> (rule4 % int3))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is white.
True
12
proof
[(((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5))]
("Dave" "is" "white" "+")
((((((((triple5 triple6) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5 triple6) -> (rule4 % int4))) -> (rule1 % int2)) ((triple5 triple6) -> (rule4 % int4))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not white.
False
12
inv-proof
[(((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5))]
("Dave" "is" "white" "-")
((((((((triple5 triple6) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5 triple6) -> (rule4 % int4))) -> (rule1 % int2)) ((triple5 triple6) -> (rule4 % int4))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not smart.
True
16
proof
[(((((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5) ((triple5 triple6) -> rule4)) -> rule3))]
("Dave" "is" "smart" "-")
((((((((((triple5 triple6) -> (rule4 % int5))) -> (rule2 % int4)) ((triple5 triple6) -> (rule4 % int5))) -> (rule1 % int3)) ((triple5 triple6) -> (rule4 % int5))) -> (rule5 % int2)) ((triple5 triple6) -> (rule4 % int5))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Dave is smart.
False
16
inv-proof
[(((((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5) ((triple5 triple6) -> rule4)) -> rule3))]
("Dave" "is" "smart" "+")
((((((((((triple5 triple6) -> (rule4 % int5))) -> (rule2 % int4)) ((triple5 triple6) -> (rule4 % int5))) -> (rule1 % int3)) ((triple5 triple6) -> (rule4 % int5))) -> (rule5 % int2)) ((triple5 triple6) -> (rule4 % int5))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "young" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Charlie is not blue.[(triple1)] Charlie is not furry.[(triple2)] Charlie is white.[(triple3)] Charlie is young.[(triple4)] Dave is furry.[(triple5)] Dave is quiet.[(triple6)] Fiona is quiet.[(triple7)] Fiona is smart.[(triple8)] Harry is kind.[(triple9)] Harry is not smart.[(triple10 OR ((triple11 triple9) -> rule3) OR ((((((((triple9) -> rule2) triple9) -> rule1) triple9) -> rule5) triple9) -> rule3))] Harry is white.[(triple11 OR ((((((triple9) -> rule2) triple9) -> rule1) triple9) -> rule5))] @1: Dave is kind.[(((triple5 triple6) -> rule4))] Harry is young.[(((triple9) -> rule2))] @2: Dave is young.[(((((triple5 triple6) -> rule4)) -> rule2))] Harry is blue.[(((((triple9) -> rule2) triple9) -> rule1))] @3: Dave is blue.[(((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1))] @4: Dave is white.[(((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5))] @5: Dave is not smart.[(((((((((((triple5 triple6) -> rule4)) -> rule2) ((triple5 triple6) -> rule4)) -> rule1) ((triple5 triple6) -> rule4)) -> rule5) ((triple5 triple6) -> rule4)) -> rule3))]
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is not smart.
("Harry" "is" "smart" "-")
triple10
((triple11 triple9) -> (rule3 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
((((((((triple9) -> (rule2 % int4)) triple9) -> (rule1 % int3)) triple9) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
triple11
((((((triple9) -> (rule2 % int3)) triple9) -> (rule1 % int2)) triple9) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((triple5 triple6) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple9) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple9) -> (rule2 % int2)) triple9) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) ((triple5 triple6) -> (rule4 % int3))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple5 triple6) -> (rule4 % int4))) -> (rule2 % int3)) ((triple5 triple6) -> (rule4 % int4))) -> (rule1 % int2)) ((triple5 triple6) -> (rule4 % int4))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is not smart.
("Dave" "is" "smart" "-")
((((((((((triple5 triple6) -> (rule4 % int5))) -> (rule2 % int4)) ((triple5 triple6) -> (rule4 % int5))) -> (rule1 % int3)) ((triple5 triple6) -> (rule4 % int5))) -> (rule5 % int2)) ((triple5 triple6) -> (rule4 % int5))) -> (rule3 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5