Anne is quiet. Charlie is round. Dave is quiet. Harry is young. All kind, nice things are young. If something is rough and kind then it is round. If something is quiet and blue then it is rough. Nice, quiet things are rough. Round things are nice. Nice things are kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
All kind, nice things are young.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is rough and kind then it is round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is quiet and blue then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Nice, quiet things are rough.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Dave is quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "+")
triple3
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Charlie is nice.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
True
6
proof
[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule1))]
("Charlie" "is" "young" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not young.
False
6
inv-proof
[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule1))]
("Charlie" "is" "young" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Anne is round.
Unknown
rconc
[@3: Anne is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule5 <- FAIL)]]
("Anne" "is" "round" "+")
Dave is not kind.
Unknown
inv-rconc
[@3: Dave is kind.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is young.
Unknown
rconc
[@4: Dave is young.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is quiet.[(triple1)] Charlie is round.[(triple2)] Dave is quiet.[(triple3)] Harry is young.[(triple4)] @1: Charlie is nice.[(((triple2) -> rule5))] @2: Charlie is kind.[(((((triple2) -> rule5)) -> rule6))] @3: Charlie is young.[(((((((triple2) -> rule5)) -> rule6) ((triple2) -> rule5)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple2) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2)) ((triple2) -> (rule5 % int3))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3