Anne is blue. Anne is kind. Anne is quiet. Anne is smart. Charlie is blue. Charlie is rough. Charlie is round. Charlie is smart. Dave is blue. Dave is furry. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Erin is kind. Smart people are rough. If someone is kind then they are furry. Rough people are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Anne is quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "round" "-")
triple7
Anne is rough.
True
2
proof
[(((triple4) -> rule1))]
("Anne" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((((triple4) -> rule1)) -> rule3)) -> rule2))]
("Anne" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Charlie is furry.
True
3
proof
[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not furry.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "furry" "-")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2 OR ((((triple4) -> rule1)) -> rule3))] Anne is quiet.[(triple3)] Anne is smart.[(triple4)] Charlie is blue.[(triple5)] Charlie is rough.[(triple6 OR ((triple8) -> rule1))] Charlie is round.[(triple7)] Charlie is smart.[(triple8)] Dave is blue.[(triple9)] Dave is furry.[(triple10 OR ((triple11) -> rule2) OR ((((triple13) -> rule3)) -> rule2) OR ((((((triple15) -> rule1)) -> rule3)) -> rule2))] Dave is kind.[(triple11 OR ((triple13) -> rule3) OR ((((triple15) -> rule1)) -> rule3))] Dave is quiet.[(triple12)] Dave is rough.[(triple13 OR ((triple15) -> rule1))] Dave is round.[(triple14)] Dave is smart.[(triple15)] Erin is kind.[(triple16)] @1: Anne is furry.[(((triple2) -> rule2) OR ((((((triple4) -> rule1)) -> rule3)) -> rule2))] Anne is rough.[(((triple4) -> rule1))] Charlie is kind.[(((triple6) -> rule3) OR ((((triple8) -> rule1)) -> rule3))] Erin is furry.[(((triple16) -> rule2))] @2: Charlie is furry.[(((((triple6) -> rule3)) -> rule2) OR ((((((triple8) -> rule1)) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple8) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is furry.
("Dave" "is" "furry" "+")
triple10
((triple11) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple15) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple11
((triple13) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple12
Dave is rough.
("Dave" "is" "rough" "+")
triple13
((triple15) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple14
Dave is smart.
("Dave" "is" "smart" "+")
triple15
Erin is kind.
("Erin" "is" "kind" "+")
triple16
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple6) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((triple16) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3