Bob is not blue. Bob is round. Dave is furry. Dave is quiet. Dave is smart. Gary is blue. Gary is green. Harry is blue. Harry is furry. Harry is not quiet. If Gary is green then Gary is rough. If Bob is rough then Bob is not green. All rough people are smart. Round people are smart. All rough, smart people are round. If Dave is smart then Dave is rough. All round, quiet people are not blue. If Harry is smart and Harry is not blue then Harry is furry.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is round.
("Bob" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If Gary is green then Gary is rough.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "rough" "+"))
If Bob is rough then Bob is not green.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "green" "-"))
All rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All rough, smart people are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Dave is smart then Dave is rough.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "rough" "+"))
All round, quiet people are not blue.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "-"))
If Harry is smart and Harry is not blue then Harry is furry.
((("Harry" "is" "smart" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "furry" "+"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Dave is rough.
True
2
proof
[(((triple5) -> rule6))]
("Dave" "is" "rough" "+")
((triple5) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple5) -> rule6))]
("Dave" "is" "rough" "-")
((triple5) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is smart.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Dave is not round.
False
4
inv-proof
[(((((triple5) -> rule6) triple5) -> rule5))]
("Dave" "is" "round" "-")
((((triple5) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not blue.
True
6
proof
[(((((((triple5) -> rule6) triple5) -> rule5) triple4) -> rule7))]
("Dave" "is" "blue" "-")
((((((triple5) -> (rule6 % int3)) triple5) -> (rule5 % int2)) triple4) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is blue.
False
6
inv-proof
[(((((((triple5) -> rule6) triple5) -> rule5) triple4) -> rule7))]
("Dave" "is" "blue" "+")
((((((triple5) -> (rule6 % int3)) triple5) -> (rule5 % int2)) triple4) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is smart.
Unknown
rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Harry" "is" "smart" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is not blue.[(triple1)] Bob is round.[(triple2)] Dave is furry.[(triple3)] Dave is quiet.[(triple4)] Dave is smart.[(triple5)] Gary is blue.[(triple6)] Gary is green.[(triple7)] Harry is blue.[(triple8)] Harry is furry.[(triple9)] Harry is not quiet.[(triple10)] @1: Bob is smart.[(((triple2) -> rule4))] Dave is rough.[(((triple5) -> rule6))] Gary is rough.[(((triple7) -> rule1))] @2: Dave is round.[(((((triple5) -> rule6) triple5) -> rule5))] Gary is smart.[(((((triple7) -> rule1)) -> rule3))] @3: Dave is not blue.[(((((((triple5) -> rule6) triple5) -> rule5) triple4) -> rule7))] Gary is round.[(((((triple7) -> rule1) ((((triple7) -> rule1)) -> rule3)) -> rule5))]
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple10
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple5) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple7) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple5) -> (rule6 % int2)) triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
((((((triple5) -> (rule6 % int3)) triple5) -> (rule5 % int2)) triple4) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((triple7) -> (rule1 % int3)) ((((triple7) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3