Charlie is furry. Charlie is nice. Charlie is rough. Charlie is round. Gary is furry. Gary is quiet. Gary is red. Rough, round people are furry. If someone is blue then they are quiet. Round people are furry. Furry people are red. If Charlie is red and Charlie is quiet then Charlie is nice. If Charlie is red and Charlie is blue then Charlie is nice. All round, nice people are red. Nice people are quiet.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Rough, round people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red and Charlie is quiet then Charlie is nice.
((("Charlie" "is" "red" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "nice" "+"))
If Charlie is red and Charlie is blue then Charlie is nice.
((("Charlie" "is" "red" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "nice" "+"))
All round, nice people are red.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "rough" "-")
triple3
Charlie is red.
True
2
proof
[(((triple1) -> rule4) OR ((triple4 triple2) -> rule7) OR ((((triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule1)) -> rule4))]
("Charlie" "is" "red" "+")
((triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple3 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not red.
False
2
inv-proof
[(((triple1) -> rule4) OR ((triple4 triple2) -> rule7) OR ((((triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule1)) -> rule4))]
("Charlie" "is" "red" "-")
((triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple3 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Charlie is furry.[(triple1 OR ((triple4) -> rule3) OR ((triple3 triple4) -> rule1))] Charlie is nice.[(triple2)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Gary is furry.[(triple5)] Gary is quiet.[(triple6)] Gary is red.[(triple7 OR ((triple5) -> rule4))] @1: Charlie is quiet.[(((triple2) -> rule8))] Charlie is red.[(((triple1) -> rule4) OR ((triple4 triple2) -> rule7) OR ((((triple4) -> rule3)) -> rule4) OR ((((triple3 triple4) -> rule1)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((triple4) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple3 triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
((triple5) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple3 triple4) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2