Charlie is not furry. Charlie is not green. Charlie is red. Charlie is round. Charlie is young. Dave is not green. Dave is red. Dave is not round. Dave is young. Erin is green. Erin is quiet. Erin is round. Erin is young. Gary is quiet. Gary is round. Gary is young. All green people are young. If someone is young then they are red. If someone is big then they are red. All round people are not big. If Gary is not green then Gary is quiet. Round people are not furry. If Dave is round then Dave is quiet. If someone is furry and not red then they are quiet.
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All round people are not big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "-"))
If Gary is not green then Gary is quiet.
((("Gary" "is" "green" "~")) -> ("Gary" "is" "quiet" "+"))
Round people are not furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "-"))
If Dave is round then Dave is quiet.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "quiet" "+"))
If someone is furry and not red then they are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "quiet" "+"))
Gary is round.
True
1
proof
[(triple15)]
("Gary" "is" "round" "+")
triple15
Dave is green.
False
1
inv-proof
[(triple6)]
("Dave" "is" "green" "+")
triple6
Gary is red.
True
2
proof
[(((triple16) -> rule2))]
("Gary" "is" "red" "+")
((triple16) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is big.
False
2
inv-proof
[(((triple4) -> rule4))]
("Charlie" "is" "big" "+")
((triple4) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Charlie is not furry.[(triple1 OR ((triple4) -> rule6))] Charlie is not green.[(triple2)] Charlie is red.[(triple3 OR ((triple5) -> rule2))] Charlie is round.[(triple4)] Charlie is young.[(triple5)] Dave is not green.[(triple6)] Dave is not round.[(triple8)] Dave is red.[(triple7 OR ((triple9) -> rule2))] Dave is young.[(triple9)] Erin is green.[(triple10)] Erin is quiet.[(triple11)] Erin is round.[(triple12)] Erin is young.[(triple13 OR ((triple10) -> rule1))] Gary is quiet.[(triple14)] Gary is round.[(triple15)] Gary is young.[(triple16)] @1: Charlie is not big.[(((triple4) -> rule4))] Erin is not big.[(((triple12) -> rule4))] Erin is not furry.[(((triple12) -> rule6))] Erin is red.[(((triple13) -> rule2) OR ((((triple10) -> rule1)) -> rule2))] Gary is not big.[(((triple15) -> rule4))] Gary is not furry.[(((triple15) -> rule6))] Gary is red.[(((triple16) -> rule2))]
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple1
((triple4) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is not green.
("Charlie" "is" "green" "-")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
((triple5) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is not green.
("Dave" "is" "green" "-")
triple6
Dave is not round.
("Dave" "is" "round" "-")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple7
((triple9) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple9
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11
Erin is round.
("Erin" "is" "round" "+")
triple12
Erin is young.
("Erin" "is" "young" "+")
triple13
((triple10) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Charlie is not big.
("Charlie" "is" "big" "-")
((triple4) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Erin is not big.
("Erin" "is" "big" "-")
((triple12) -> (rule4 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not furry.
("Erin" "is" "furry" "-")
((triple12) -> (rule6 % int1))
Erin is not furry.
("Erin" "is" "furry" "-")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple13) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Gary is not big.
("Gary" "is" "big" "-")
((triple15) -> (rule4 % int1))
Gary is not big.
("Gary" "is" "big" "-")
int1
Gary is not furry.
("Gary" "is" "furry" "-")
((triple15) -> (rule6 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple16) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1