Charlie is big. Charlie is cold. Charlie is red. Charlie is round. Dave is big. Dave is not cold. Dave is not furry. Dave is red. Dave is round. Dave is not white. Dave is young. Erin is big. Erin is cold. Erin is furry. Erin is red. Erin is not young. Young, cold people are not furry. All round, cold people are furry. If someone is cold and white then they are furry. If someone is big then they are round. If someone is cold then they are not young. If Erin is not white then Erin is big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is 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 red.
("Erin" "is" "red" "+")
Erin is not young.
("Erin" "is" "young" "-")
Young, cold people are not furry.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "-"))
All round, cold people are furry.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and white then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is cold then they are not young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "-"))
If Erin is not white then Erin is big.
((("Erin" "is" "white" "~")) -> ("Erin" "is" "big" "+"))
Dave is not white.
True
1
proof
[(triple10)]
("Dave" "is" "white" "-")
triple10
Dave is white.
False
1
inv-proof
[(triple10)]
("Dave" "is" "white" "+")
triple10
Erin is round.
True
2
proof
[(((triple12) -> rule4))]
("Erin" "is" "round" "+")
((triple12) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is young.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "young" "+")
((triple2) -> (rule5 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is red.[(triple3)] Charlie is round.[(triple4 OR ((triple1) -> rule4))] Dave is big.[(triple5)] Dave is not cold.[(triple6)] Dave is not furry.[(triple7)] Dave is not white.[(triple10)] Dave is red.[(triple8)] Dave is round.[(triple9 OR ((triple5) -> rule4))] Dave is young.[(triple11)] Erin is big.[(triple12)] Erin is cold.[(triple13)] Erin is furry.[(triple14 OR ((((triple12) -> rule4) triple13) -> rule2))] Erin is not young.[(triple16 OR ((triple13) -> rule5))] Erin is red.[(triple15)] @1: Charlie is furry.[(((triple4 triple2) -> rule2) OR ((((triple1) -> rule4) triple2) -> rule2))] Charlie is not young.[(((triple2) -> rule5))] Erin is round.[(((triple12) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
((triple1) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is not cold.
("Dave" "is" "cold" "-")
triple6
Dave is not furry.
("Dave" "is" "furry" "-")
triple7
Dave is not white.
("Dave" "is" "white" "-")
triple10
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
((triple5) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is cold.
("Erin" "is" "cold" "+")
triple13
Erin is furry.
("Erin" "is" "furry" "+")
triple14
((((triple12) -> (rule4 % int2)) triple13) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not young.
("Erin" "is" "young" "-")
triple16
((triple13) -> (rule5 % int1))
Erin is not young.
("Erin" "is" "young" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
triple15
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4 triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple1) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((triple2) -> (rule5 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple12) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1