Charlie is blue. Charlie is not furry. Charlie is not kind. Dave is quiet. Erin is blue. Erin is kind. Erin is not rough. Erin is round. Erin is not young. Fiona is not blue. Fiona is round. Quiet, round people are rough. If Dave is furry and Dave is rough then Dave is blue. If Dave is rough then Dave is kind. All kind people are blue. If someone is furry and not quiet then they are blue. If someone is round and furry then they are blue. If someone is quiet then they are round. All blue, rough people are young. If someone is young and not quiet then they are not kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is not young.
("Erin" "is" "young" "-")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Quiet, round people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If Dave is furry and Dave is rough then Dave is blue.
((("Dave" "is" "furry" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
If Dave is rough then Dave is kind.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "kind" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is furry and not quiet then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
If someone is round and furry then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All blue, rough people are young.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is young and not quiet then they are not kind.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "kind" "-"))
Erin is not rough.
True
1
proof
[(triple7)]
("Erin" "is" "rough" "-")
triple7
Charlie is kind.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "kind" "+")
triple3
Dave is round.
True
2
proof
[(((triple4) -> rule7))]
("Dave" "is" "round" "+")
((triple4) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple4) -> rule7))]
("Dave" "is" "round" "-")
((triple4) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
True
4
proof
[(((triple4 ((triple4) -> rule7)) -> rule1))]
("Dave" "is" "rough" "+")
((triple4 ((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((triple4 ((triple4) -> rule7)) -> rule1))]
("Dave" "is" "rough" "-")
((triple4 ((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
True
5
proof
[(((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "kind" "+")
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not kind.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3))]
("Dave" "is" "kind" "-")
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
True
6
proof
[(((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4))]
("Dave" "is" "blue" "+")
((((((triple4 ((triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not blue.
False
6
inv-proof
[(((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4))]
("Dave" "is" "blue" "-")
((((((triple4 ((triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is young.
True
11
proof
[(((((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4) ((triple4 ((triple4) -> rule7)) -> rule1)) -> rule8))]
("Dave" "is" "young" "+")
((((((((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Dave is not young.
False
11
inv-proof
[(((((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4) ((triple4 ((triple4) -> rule7)) -> rule1)) -> rule8))]
("Dave" "is" "young" "-")
((((((((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "rough" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "young" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Charlie is not furry.[(triple2)] Charlie is not kind.[(triple3)] Dave is quiet.[(triple4)] Erin is blue.[(triple5 OR ((triple6) -> rule4))] Erin is kind.[(triple6)] Erin is not rough.[(triple7)] Erin is not young.[(triple9)] Erin is round.[(triple8)] Fiona is not blue.[(triple10)] Fiona is round.[(triple11)] @1: Dave is round.[(((triple4) -> rule7))] @2: Dave is rough.[(((triple4 ((triple4) -> rule7)) -> rule1))] @3: Dave is kind.[(((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3))] @4: Dave is blue.[(((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4))] @5: Dave is young.[(((((((((triple4 ((triple4) -> rule7)) -> rule1)) -> rule3)) -> rule4) ((triple4 ((triple4) -> rule7)) -> rule1)) -> rule8))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
triple5
((triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is not rough.
("Erin" "is" "rough" "-")
triple7
Erin is not young.
("Erin" "is" "young" "-")
triple9
Erin is round.
("Erin" "is" "round" "+")
triple8
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple10
Fiona is round.
("Fiona" "is" "round" "+")
triple11
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 ((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple4 ((triple4) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
((((((((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) ((triple4 ((triple4) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5