Bob is smart. Dave is round. All big people are not furry. If Dave is furry and Dave is not smart then Dave is not quiet. Blue, furry people are round. Quiet people are not big. Green people are big. All round people are quiet. If someone is smart then they are green. If someone is blue and not smart then they are green.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
All big people are not furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "-"))
If Dave is furry and Dave is not smart then Dave is not quiet.
((("Dave" "is" "furry" "+") ("Dave" "is" "smart" "~")) -> ("Dave" "is" "quiet" "-"))
Blue, furry people are round.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Quiet people are not big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and not smart then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "green" "+"))
Bob is smart.
True
1
proof
[(triple1)]
("Bob" "is" "smart" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple2)]
("Dave" "is" "round" "-")
triple2
Bob is green.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "green" "+")
((triple1) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule7)) -> rule5))]
("Bob" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule4))]
("Dave" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not furry.
True
4
proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule1))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is furry.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule5)) -> rule1))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "green" "+")
Bob is not quiet.
Unknown
inv-rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is smart.[(triple1)] Dave is round.[(triple2)] @1: Bob is green.[(((triple1) -> rule7))] Dave is quiet.[(((triple2) -> rule6))] @2: Bob is big.[(((((triple1) -> rule7)) -> rule5))] Dave is not big.[(((((triple2) -> rule6)) -> rule4))] @3: Bob is not furry.[(((((((triple1) -> rule7)) -> rule5)) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
((((((triple1) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3