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