Charlie is big. Charlie is not cold. Charlie is round. Charlie is young. Dave is not big. Dave is furry. Dave is rough. Dave is not round. Dave is not white. Dave is young. Erin is big. Erin is cold. Erin is furry. Erin is rough. Erin is round. Erin is young. If something is cold and not rough then it is not white. All big things are furry. If something is cold and big then it is round. If Dave is not white and Dave is not round then Dave is furry. If Erin is rough and Erin is not round then Erin is white. If Charlie is not furry then Charlie is round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is not white.
("Dave" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is cold and not rough then it is not white.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "-"))
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is cold and big then it is round.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If Dave is not white and Dave is not round then Dave is furry.
((("Dave" "is" "white" "~") ("Dave" "is" "round" "~")) -> ("Dave" "is" "furry" "+"))
If Erin is rough and Erin is not round then Erin is white.
((("Erin" "is" "rough" "+") ("Erin" "is" "round" "~")) -> ("Erin" "is" "white" "+"))
If Charlie is not furry then Charlie is round.
((("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "round" "+"))
Erin is furry.
True
1
proof
[(triple13 OR ((triple11) -> rule2))]
("Erin" "is" "furry" "+")
triple13
((triple11) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is not young.
False
1
inv-proof
[(triple10)]
("Dave" "is" "young" "-")
triple10
Charlie is furry.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Charlie is not cold.[(triple2)] Charlie is round.[(triple3)] Charlie is young.[(triple4)] Dave is furry.[(triple6 OR ((triple9 triple8) -> rule4))] Dave is not big.[(triple5)] Dave is not round.[(triple8)] Dave is not white.[(triple9)] Dave is rough.[(triple7)] Dave is young.[(triple10)] Erin is big.[(triple11)] Erin is cold.[(triple12)] Erin is furry.[(triple13 OR ((triple11) -> rule2))] Erin is rough.[(triple14)] Erin is round.[(triple15 OR ((triple12 triple11) -> rule3))] Erin is young.[(triple16)] @1: Charlie is furry.[(((triple1) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((triple9 triple8) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
triple5
Dave is not round.
("Dave" "is" "round" "-")
triple8
Dave is not white.
("Dave" "is" "white" "-")
triple9
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple10
Erin is big.
("Erin" "is" "big" "+")
triple11
Erin is cold.
("Erin" "is" "cold" "+")
triple12
Erin is furry.
("Erin" "is" "furry" "+")
triple13
((triple11) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple14
Erin is round.
("Erin" "is" "round" "+")
triple15
((triple12 triple11) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple16
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1