Bob is big. Bob is blue. Bob is red. Charlie is blue. Charlie is furry. Charlie is red. Charlie is not round. All red, furry people are not round. Smart people are round. Big people are smart. Round, blue people are not furry. If someone is round and smart then they are not furry. If someone is blue and not round then they are young. All furry, blue people are young. If someone is smart then they are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
All red, furry people are not round.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "-"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Round, blue people are not furry.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "-"))
If someone is round and smart then they are not furry.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "-"))
If someone is blue and not round then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
All furry, blue people are young.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Charlie is furry.
True
1
proof
[(triple5)]
("Charlie" "is" "furry" "+")
triple5
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Bob is smart.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple4 triple7) -> rule6) OR ((triple5 triple4) -> rule7) OR ((triple4 ((triple6 triple5) -> rule1)) -> rule6))]
("Charlie" "is" "young" "-")
((triple4 triple7) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 ((triple6 triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
int2
Bob is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Bob" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not furry.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple2) -> rule4) OR ((((((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is furry.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple2) -> rule4) OR ((((((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2)] Bob is red.[(triple3)] Charlie is blue.[(triple4)] Charlie is furry.[(triple5)] Charlie is not round.[(triple7 OR ((triple6 triple5) -> rule1))] Charlie is red.[(triple6)] @1: Bob is smart.[(((triple1) -> rule3))] Charlie is young.[(((triple4 triple7) -> rule6) OR ((triple5 triple4) -> rule7) OR ((triple4 ((triple6 triple5) -> rule1)) -> rule6))] @2: Bob is round.[(((((triple1) -> rule3)) -> rule2))] Bob is young.[(((((triple1) -> rule3)) -> rule8))] @3: Bob is not furry.[(((((((triple1) -> rule3)) -> rule2) triple2) -> rule4) OR ((((((triple1) -> rule3)) -> rule2) ((triple1) -> rule3)) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
Charlie is not round.
("Charlie" "is" "round" "-")
triple7
((triple6 triple5) -> (rule1 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple4 triple7) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple5 triple4) -> (rule7 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((triple4 ((triple6 triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not furry.
("Bob" "is" "furry" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) ((triple1) -> (rule3 % int3))) -> (rule5 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3