Charlie is kind. Charlie is red. Dave is furry. Dave is kind. Gary is red. Gary is round. Harry is furry. Furry, round people are young. All young, round people are rough. Kind people are round. If Harry is kind then Harry is red. If someone is rough and red then they are young. If someone is rough and young then they are quiet. Round, quiet people are red.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Furry, round people are young.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
All young, round people are rough.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Harry is kind then Harry is red.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "red" "+"))
If someone is rough and red then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and young then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
Round, quiet people are red.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "round" "-")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is young.
True
4
proof
[(((triple3 ((triple4) -> rule3)) -> rule1))]
("Dave" "is" "young" "+")
((triple3 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not young.
False
4
inv-proof
[(((triple3 ((triple4) -> rule3)) -> rule1))]
("Dave" "is" "young" "-")
((triple3 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
True
7
proof
[(((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "+")
((((triple3 ((triple4) -> (rule3 % int3))) -> (rule1 % int2)) ((triple4) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not rough.
False
7
inv-proof
[(((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2))]
("Dave" "is" "rough" "-")
((((triple3 ((triple4) -> (rule3 % int3))) -> (rule1 % int2)) ((triple4) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
True
12
proof
[(((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6))]
("Dave" "is" "quiet" "+")
((((((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int4))) -> (rule2 % int2)) ((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is not quiet.
False
12
inv-proof
[(((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6))]
("Dave" "is" "quiet" "-")
((((((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int4))) -> (rule2 % int2)) ((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is red.
True
15
proof
[(((((triple4) -> rule3) ((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6)) -> rule7))]
("Dave" "is" "red" "+")
((((triple4) -> (rule3 % int5)) ((((((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int5))) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Dave is not red.
False
15
inv-proof
[(((((triple4) -> rule3) ((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6)) -> rule7))]
("Dave" "is" "red" "-")
((((triple4) -> (rule3 % int5)) ((((((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int5))) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not young.
Unknown
inv-rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is quiet.
Unknown
rconc
[@3: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Charlie is young.
Unknown
rconc
[@3: Charlie is young.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is kind.[(triple1)] Charlie is red.[(triple2)] Dave is furry.[(triple3)] Dave is kind.[(triple4)] Gary is red.[(triple5)] Gary is round.[(triple6)] Harry is furry.[(triple7)] @1: Charlie is round.[(((triple1) -> rule3))] Dave is round.[(((triple4) -> rule3))] @2: Dave is young.[(((triple3 ((triple4) -> rule3)) -> rule1))] @3: Dave is rough.[(((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2))] @4: Dave is quiet.[(((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6))] @5: Dave is red.[(((((triple4) -> rule3) ((((((triple3 ((triple4) -> rule3)) -> rule1) ((triple4) -> rule3)) -> rule2) ((triple3 ((triple4) -> rule3)) -> rule1)) -> rule6)) -> rule7))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3 ((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3 ((triple4) -> (rule3 % int3))) -> (rule1 % int2)) ((triple4) -> (rule3 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int4))) -> (rule2 % int2)) ((triple3 ((triple4) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((triple4) -> (rule3 % int5)) ((((((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int5))) -> (rule2 % int3)) ((triple3 ((triple4) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
int5