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