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