Bob is blue. Bob is furry. Bob is green. Bob is kind. Bob is quiet. Bob is round. Bob is young. Dave is kind. Dave is quiet. Dave is round. Fiona is young. Gary is green. Gary is kind. Gary is round. Gary is young. If Dave is green then Dave is furry. All green, quiet people are round. Furry, young people are kind. Round, furry people are quiet. All kind, round people are furry. All round, furry people are young. If Fiona is kind then Fiona is green. If someone is quiet and round then they are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is green then Dave is furry.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "furry" "+"))
All green, quiet people are round.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Furry, young people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Round, furry people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
All kind, round people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All round, furry people are young.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Fiona is kind then Fiona is green.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "green" "+"))
If someone is quiet and round then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Bob is green.
True
1
proof
[(triple3)]
("Bob" "is" "green" "+")
triple3
Dave is not quiet.
False
1
inv-proof
[(triple9 OR ((triple10 ((triple8 triple10) -> rule5)) -> rule4))]
("Dave" "is" "quiet" "-")
triple9
((triple10 ((triple8 triple10) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is blue.
True
3
proof
[(((triple9 triple10) -> rule8) OR ((((triple10 ((triple8 triple10) -> rule5)) -> rule4) triple10) -> rule8))]
("Dave" "is" "blue" "+")
((triple9 triple10) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10 ((triple8 triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is not furry.
False
3
inv-proof
[(((triple8 triple10) -> rule5))]
("Dave" "is" "furry" "-")
((triple8 triple10) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is green.
Unknown
rconc
[@3: Fiona is green.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is blue.[(triple1 OR ((triple5 triple6) -> rule8) OR ((triple5 ((triple3 triple5) -> rule2)) -> rule8) OR ((((triple6 triple2) -> rule4) triple6) -> rule8) OR ((((triple6 triple2) -> rule4) ((triple3 triple5) -> rule2)) -> rule8) OR ((((triple6 ((triple4 triple6) -> rule5)) -> rule4) triple6) -> rule8) OR ((((triple6 ((triple4 triple6) -> rule5)) -> rule4) ((triple3 triple5) -> rule2)) -> rule8))] Bob is furry.[(triple2 OR ((triple4 triple6) -> rule5) OR ((triple4 ((triple3 triple5) -> rule2)) -> rule5))] Bob is green.[(triple3)] Bob is kind.[(triple4 OR ((triple2 triple7) -> rule3) OR ((triple2 ((triple6 triple2) -> rule6)) -> rule3) OR ((triple2 ((((triple3 triple5) -> rule2) triple2) -> rule6)) -> rule3))] Bob is quiet.[(triple5 OR ((triple6 triple2) -> rule4) OR ((triple6 ((triple4 triple6) -> rule5)) -> rule4))] Bob is round.[(triple6 OR ((triple3 triple5) -> rule2))] Bob is young.[(triple7 OR ((triple6 triple2) -> rule6) OR ((triple6 ((triple4 triple6) -> rule5)) -> rule6) OR ((((triple3 triple5) -> rule2) triple2) -> rule6) OR ((((triple3 triple5) -> rule2) ((triple4 triple6) -> rule5)) -> rule6) OR ((triple6 ((triple4 ((triple3 triple5) -> rule2)) -> rule5)) -> rule6) OR ((((triple3 triple5) -> rule2) ((triple4 ((triple3 triple5) -> rule2)) -> rule5)) -> rule6))] Dave is kind.[(triple8)] Dave is quiet.[(triple9 OR ((triple10 ((triple8 triple10) -> rule5)) -> rule4))] Dave is round.[(triple10)] Fiona is young.[(triple11)] Gary is green.[(triple12)] Gary is kind.[(triple13)] Gary is round.[(triple14)] Gary is young.[(triple15 OR ((triple14 ((triple13 triple14) -> rule5)) -> rule6))] @1: Dave is blue.[(((triple9 triple10) -> rule8) OR ((((triple10 ((triple8 triple10) -> rule5)) -> rule4) triple10) -> rule8))] Dave is furry.[(((triple8 triple10) -> rule5))] Gary is furry.[(((triple13 triple14) -> rule5))] @2: Dave is young.[(((triple10 ((triple8 triple10) -> rule5)) -> rule6))] Gary is quiet.[(((triple14 ((triple13 triple14) -> rule5)) -> rule4))] @3: Gary is blue.[(((((triple14 ((triple13 triple14) -> rule5)) -> rule4) triple14) -> rule8))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple5 triple6) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple5 ((triple3 triple5) -> (rule2 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple6 triple2) -> (rule4 % int2)) triple6) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple6 triple2) -> (rule4 % int3)) ((triple3 triple5) -> (rule2 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple6 ((triple4 triple6) -> (rule5 % int3))) -> (rule4 % int2)) triple6) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((triple6 ((triple4 triple6) -> (rule5 % int4))) -> (rule4 % int3)) ((triple3 triple5) -> (rule2 % int2))) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple4 triple6) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple4 ((triple3 triple5) -> (rule2 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple2 triple7) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple6 triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple2 ((((triple3 triple5) -> (rule2 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
((triple6 triple2) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple6 ((triple4 triple6) -> (rule5 % int2))) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple3 triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple6 triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple6 ((triple4 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 triple5) -> (rule2 % int2)) triple2) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((triple4 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((triple6 ((triple4 ((triple3 triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((triple3 triple5) -> (rule2 % int3)) ((triple4 ((triple3 triple5) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
((triple10 ((triple8 triple10) -> (rule5 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
Gary is green.
("Gary" "is" "green" "+")
triple12
Gary is kind.
("Gary" "is" "kind" "+")
triple13
Gary is round.
("Gary" "is" "round" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
((triple14 ((triple13 triple14) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple9 triple10) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10 ((triple8 triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple10) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple8 triple10) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple13 triple14) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple10 ((triple8 triple10) -> (rule5 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple14 ((triple13 triple14) -> (rule5 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple14 ((triple13 triple14) -> (rule5 % int3))) -> (rule4 % int2)) triple14) -> (rule8 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3