Bob is furry. Bob is not round. Bob is white. Dave is not quiet. Dave is white. Fiona is green. Fiona is not smart. Fiona is white. Fiona is young. Gary is quiet. Young, furry people are round. Quiet, green people are not white. Green, young people are white. All green people are furry. If Dave is white then Dave is young. If someone is young then they are green. If someone is furry and round then they are not smart. If someone is quiet and not furry then they are not smart. If Bob is not white then Bob is round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Young, furry people are round.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Quiet, green people are not white.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "-"))
Green, young people are white.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
If Dave is white then Dave is young.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "young" "+"))
If someone is young then they are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is furry and round then they are not smart.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "-"))
If someone is quiet and not furry then they are not smart.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "-"))
If Bob is not white then Bob is round.
((("Bob" "is" "white" "~")) -> ("Bob" "is" "round" "+"))
Gary is quiet.
True
1
proof
[(triple10)]
("Gary" "is" "quiet" "+")
triple10
Bob is not white.
False
1
inv-proof
[(triple3)]
("Bob" "is" "white" "-")
triple3
Fiona is furry.
True
2
proof
[(((triple6) -> rule4) OR ((((triple9) -> rule6)) -> rule4))]
("Fiona" "is" "furry" "+")
((triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is not young.
False
2
inv-proof
[(((triple5) -> rule5))]
("Dave" "is" "young" "-")
((triple5) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is round.
True
4
proof
[(((triple9 ((triple6) -> rule4)) -> rule1) OR ((triple9 ((((triple9) -> rule6)) -> rule4)) -> rule1))]
("Fiona" "is" "round" "+")
((triple9 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is not round.
False
4
inv-proof
[(((triple9 ((triple6) -> rule4)) -> rule1) OR ((triple9 ((((triple9) -> rule6)) -> rule4)) -> rule1))]
("Fiona" "is" "round" "-")
((triple9 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Dave is furry.
True
4
proof
[(((((((triple5) -> rule5)) -> rule6)) -> rule4))]
("Dave" "is" "furry" "+")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule6)) -> rule4))]
("Dave" "is" "furry" "-")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
True
7
proof
[(((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "round" "+")
((((triple5) -> (rule5 % int4)) ((((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not round.
False
7
inv-proof
[(((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1))]
("Dave" "is" "round" "-")
((((triple5) -> (rule5 % int4)) ((((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not smart.
True
12
proof
[(((((((((triple5) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1)) -> rule7))]
("Dave" "is" "smart" "-")
((((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule5 % int5)) ((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Dave is smart.
False
12
inv-proof
[(((((((((triple5) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1)) -> rule7))]
("Dave" "is" "smart" "+")
((((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule5 % int5)) ((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is green.
Unknown
rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "green" "+")
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "green" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is furry.[(triple1)] Bob is not round.[(triple2)] Bob is white.[(triple3)] Dave is not quiet.[(triple4)] Dave is white.[(triple5)] Fiona is green.[(triple6 OR ((triple9) -> rule6))] Fiona is not smart.[(triple7 OR ((((triple6) -> rule4) ((triple9 ((triple6) -> rule4)) -> rule1)) -> rule7) OR ((((((triple9) -> rule6)) -> rule4) ((triple9 ((triple6) -> rule4)) -> rule1)) -> rule7) OR ((((triple6) -> rule4) ((triple9 ((((triple9) -> rule6)) -> rule4)) -> rule1)) -> rule7) OR ((((((triple9) -> rule6)) -> rule4) ((triple9 ((((triple9) -> rule6)) -> rule4)) -> rule1)) -> rule7))] Fiona is white.[(triple8 OR ((triple6 triple9) -> rule3) OR ((((triple9) -> rule6) triple9) -> rule3))] Fiona is young.[(triple9)] Gary is quiet.[(triple10)] @1: Dave is young.[(((triple5) -> rule5))] Fiona is furry.[(((triple6) -> rule4) OR ((((triple9) -> rule6)) -> rule4))] @2: Dave is green.[(((((triple5) -> rule5)) -> rule6))] Fiona is round.[(((triple9 ((triple6) -> rule4)) -> rule1) OR ((triple9 ((((triple9) -> rule6)) -> rule4)) -> rule1))] @3: Dave is furry.[(((((((triple5) -> rule5)) -> rule6)) -> rule4))] @4: Dave is round.[(((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1))] @5: Dave is not smart.[(((((((((triple5) -> rule5)) -> rule6)) -> rule4) ((((triple5) -> rule5) ((((((triple5) -> rule5)) -> rule6)) -> rule4)) -> rule1)) -> rule7))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is not round.
("Bob" "is" "round" "-")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
((triple9) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple7
((((triple6) -> (rule4 % int3)) ((triple9 ((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple9) -> (rule6 % int4))) -> (rule4 % int3)) ((triple9 ((triple6) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((triple6) -> (rule4 % int4)) ((triple9 ((((triple9) -> (rule6 % int3))) -> (rule4 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
int4
((((((triple9) -> (rule6 % int4))) -> (rule4 % int3)) ((triple9 ((((triple9) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Fiona is not smart.
("Fiona" "is" "smart" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
Fiona is white.
("Fiona" "is" "white" "+")
triple8
((triple6 triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple9) -> (rule6 % int2)) triple9) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
((triple5) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((triple9 ((triple6) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((triple9 ((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple5) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((((triple5) -> (rule5 % int4)) ((((((triple5) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not smart.
("Dave" "is" "smart" "-")
((((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule5 % int5)) ((((((triple5) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
int4
Dave is young.
("Dave" "is" "young" "+")
int5