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