Anne is green. Anne is kind. Anne is round. Anne is white. Bob is furry. Bob is green. Bob is kind. Bob is round. Bob is white. Erin is furry. Erin is green. Erin is rough. Erin is round. Harry is furry. Harry is rough. Rough, white things are smart. If Erin is furry then Erin is green. If something is round then it is furry. If something is furry and smart then it is white. Furry things are smart. If something is smart then it is rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Rough, white things are smart.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Erin is furry then Erin is green.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "green" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is furry and smart then it is white.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Erin is round.
True
1
proof
[(triple13)]
("Erin" "is" "round" "+")
triple13
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
Erin is smart.
True
2
proof
[(((triple10) -> rule5) OR ((((triple13) -> rule3)) -> rule5))]
("Erin" "is" "smart" "+")
((triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not smart.
False
2
inv-proof
[(((triple10) -> rule5) OR ((((triple13) -> rule3)) -> rule5))]
("Erin" "is" "smart" "-")
((triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Anne is smart.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Anne" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Harry is not white.
False
4
inv-proof
[(((triple14 ((triple14) -> rule5)) -> rule4))]
("Harry" "is" "white" "-")
((triple14 ((triple14) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2)] Anne is round.[(triple3)] Anne is white.[(triple4 OR ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule4))] Bob is furry.[(triple5 OR ((triple8) -> rule3))] Bob is green.[(triple6)] Bob is kind.[(triple7)] Bob is round.[(triple8)] Bob is white.[(triple9 OR ((triple5 ((triple5) -> rule5)) -> rule4) OR ((((triple8) -> rule3) ((triple5) -> rule5)) -> rule4) OR ((triple5 ((((triple8) -> rule3)) -> rule5)) -> rule4) OR ((((triple8) -> rule3) ((((triple8) -> rule3)) -> rule5)) -> rule4))] Erin is furry.[(triple10 OR ((triple13) -> rule3))] Erin is green.[(triple11 OR ((triple10) -> rule2) OR ((((triple13) -> rule3)) -> rule2))] Erin is rough.[(triple12 OR ((((triple10) -> rule5)) -> rule6) OR ((((((triple13) -> rule3)) -> rule5)) -> rule6))] Erin is round.[(triple13)] Harry is furry.[(triple14)] Harry is rough.[(triple15 OR ((((triple14) -> rule5)) -> rule6))] @1: Anne is furry.[(((triple3) -> rule3))] Bob is smart.[(((triple5) -> rule5) OR ((((triple8) -> rule3)) -> rule5))] Erin is smart.[(((triple10) -> rule5) OR ((((triple13) -> rule3)) -> rule5))] Harry is smart.[(((triple14) -> rule5))] @2: Anne is smart.[(((((triple3) -> rule3)) -> rule5))] Bob is rough.[(((((triple5) -> rule5)) -> rule6) OR ((((((triple8) -> rule3)) -> rule5)) -> rule6))] Erin is white.[(((triple10 ((triple10) -> rule5)) -> rule4) OR ((((triple13) -> rule3) ((triple10) -> rule5)) -> rule4) OR ((triple10 ((((triple13) -> rule3)) -> rule5)) -> rule4) OR ((((triple13) -> rule3) ((((triple13) -> rule3)) -> rule5)) -> rule4))] Harry is white.[(((triple14 ((triple14) -> rule5)) -> rule4))] @3: Anne is rough.[(((((((triple3) -> rule3)) -> rule5)) -> rule6))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple5
((triple8) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is round.
("Bob" "is" "round" "+")
triple8
Bob is white.
("Bob" "is" "white" "+")
triple9
((triple5 ((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((triple5 ((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple8) -> (rule3 % int3)) ((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple10
((triple13) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple11
((triple10) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple12
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
((((triple14) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple3) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple5) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple8) -> (rule3 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple10) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((((triple13) -> (rule3 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple14) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((((triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple10 ((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple13) -> (rule3 % int3)) ((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((triple10 ((((triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((triple13) -> (rule3 % int3)) ((((triple13) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((triple14 ((triple14) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3