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