Anne is kind. Anne is round. Bob is blue. Bob is furry. Bob is green. Bob is round. Bob is smart. Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Charlie is round. Charlie is smart. Charlie is young. Harry is blue. Harry is round. All round, blue people are kind. If someone is blue then they are young. All smart people are round. All furry people are kind. Green people are kind. Young, round people are smart.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
All round, blue people are kind.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Young, round people are smart.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Charlie is furry.
True
1
proof
[(triple9)]
("Charlie" "is" "furry" "+")
triple9
Bob is not round.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule3))]
("Bob" "is" "round" "-")
triple6
((triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
True
2
proof
[(((triple4) -> rule4) OR ((triple5) -> rule5) OR ((triple6 triple3) -> rule1) OR ((((triple7) -> rule3) triple3) -> rule1))]
("Bob" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple6 triple3) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple7) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is not young.
False
2
inv-proof
[(((triple15) -> rule2))]
("Harry" "is" "young" "-")
((triple15) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
True
4
proof
[(((((triple15) -> rule2) triple16) -> rule6))]
("Harry" "is" "smart" "+")
((((triple15) -> (rule2 % int2)) triple16) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple15) -> rule2) triple16) -> rule6))]
("Harry" "is" "smart" "-")
((((triple15) -> (rule2 % int2)) triple16) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is smart.
Unknown
rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is kind.[(triple1)] Anne is round.[(triple2)] Bob is blue.[(triple3)] Bob is furry.[(triple4)] Bob is green.[(triple5)] Bob is round.[(triple6 OR ((triple7) -> rule3))] Bob is smart.[(triple7 OR ((((triple3) -> rule2) triple6) -> rule6))] Charlie is blue.[(triple8)] Charlie is furry.[(triple9)] Charlie is green.[(triple10)] Charlie is kind.[(triple11 OR ((triple10) -> rule5) OR ((triple9) -> rule4) OR ((triple12 triple8) -> rule1) OR ((((triple13) -> rule3) triple8) -> rule1))] Charlie is round.[(triple12 OR ((triple13) -> rule3))] Charlie is smart.[(triple13 OR ((triple14 triple12) -> rule6) OR ((((triple8) -> rule2) triple12) -> rule6))] Charlie is young.[(triple14 OR ((triple8) -> rule2))] Harry is blue.[(triple15)] Harry is round.[(triple16)] @1: Bob is kind.[(((triple4) -> rule4) OR ((triple5) -> rule5) OR ((triple6 triple3) -> rule1) OR ((((triple7) -> rule3) triple3) -> rule1))] Bob is young.[(((triple3) -> rule2))] Harry is kind.[(((triple16 triple15) -> rule1))] Harry is young.[(((triple15) -> rule2))] @2: Harry is smart.[(((((triple15) -> rule2) triple16) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
((triple7) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple7
((((triple3) -> (rule2 % int2)) triple6) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is green.
("Charlie" "is" "green" "+")
triple10
Charlie is kind.
("Charlie" "is" "kind" "+")
triple11
((triple10) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple9) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple12 triple8) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple13) -> (rule3 % int2)) triple8) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
triple12
((triple13) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple13
((triple14 triple12) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple8) -> (rule2 % int2)) triple12) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple14
((triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Bob is kind.
("Bob" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple5) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple6 triple3) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple7) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple16 triple15) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple15) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple15) -> (rule2 % int2)) triple16) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2