Anne is cold. Anne is round. Charlie is cold. Dave is cold. Dave is rough. Harry is cold. Harry is quiet. Quiet, white things are rough. Cold things are rough. If Dave is young and Dave is rough then Dave is round. All rough, quiet things are white. All quiet things are young. All white things are round. If something is white and not cold then it is round. All young, white things are not smart.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Quiet, white things are rough.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If Dave is young and Dave is rough then Dave is round.
((("Dave" "is" "young" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "round" "+"))
All rough, quiet things are white.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is white and not cold then it is round.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "round" "+"))
All young, white things are not smart.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "-"))
Dave is rough.
True
1
proof
[(triple5 OR ((triple4) -> rule2))]
("Dave" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Harry is young.
True
2
proof
[(((triple7) -> rule5))]
("Harry" "is" "young" "+")
((triple7) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "rough" "-")
((triple6) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
True
4
proof
[(((((triple6) -> rule2) triple7) -> rule4))]
("Harry" "is" "white" "+")
((((triple6) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple6) -> rule2) triple7) -> rule4))]
("Harry" "is" "white" "-")
((((triple6) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
True
5
proof
[(((((((triple6) -> rule2) triple7) -> rule4)) -> rule6))]
("Harry" "is" "round" "+")
((((((triple6) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is smart.
False
7
inv-proof
[(((((triple7) -> rule5) ((((triple6) -> rule2) triple7) -> rule4)) -> rule8))]
("Harry" "is" "smart" "+")
((((triple7) -> (rule5 % int4)) ((((triple6) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "young" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Dave" "is" "round" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Anne is round.[(triple2)] Charlie is cold.[(triple3)] Dave is cold.[(triple4)] Dave is rough.[(triple5 OR ((triple4) -> rule2))] Harry is cold.[(triple6)] Harry is quiet.[(triple7)] @1: Anne is rough.[(((triple1) -> rule2))] Charlie is rough.[(((triple3) -> rule2))] Harry is rough.[(((triple6) -> rule2))] Harry is young.[(((triple7) -> rule5))] @2: Harry is white.[(((((triple6) -> rule2) triple7) -> rule4))] @3: Harry is not smart.[(((((triple7) -> rule5) ((((triple6) -> rule2) triple7) -> rule4)) -> rule8))] Harry is round.[(((((((triple6) -> rule2) triple7) -> rule4)) -> rule6))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple6) -> (rule2 % int2)) triple7) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
((((triple7) -> (rule5 % int4)) ((((triple6) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((((triple6) -> (rule2 % int3)) triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3