Bob is cold. Bob is not furry. Bob is green. Bob is kind. Bob is round. Bob is young. Charlie is big. Charlie is not cold. Charlie is furry. Dave is big. Dave is cold. Dave is furry. Dave is not green. Dave is kind. Dave is round. Dave is young. All furry things are big. If something is big and not cold then it is young. If Charlie is green and Charlie is big then Charlie is not furry. If Bob is big then Bob is not green. If Bob is cold then Bob is green. All young, furry things are kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
All furry things are big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big and not cold then it is young.
((("something" "is" "big" "+") ("something" "is" "cold" "~")) -> ("something" "is" "young" "+"))
If Charlie is green and Charlie is big then Charlie is not furry.
((("Charlie" "is" "green" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "furry" "-"))
If Bob is big then Bob is not green.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "green" "-"))
If Bob is cold then Bob is green.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "green" "+"))
All young, furry things are kind.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Bob is young.
True
1
proof
[(triple6)]
("Bob" "is" "young" "+")
triple6
Dave is not kind.
False
1
inv-proof
[(triple14 OR ((triple16 triple12) -> rule6))]
("Dave" "is" "kind" "-")
triple14
((triple16 triple12) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is young.
True
3
proof
[(((triple7 triple8) -> rule2) OR ((((triple9) -> rule1) triple8) -> rule2))]
("Charlie" "is" "young" "+")
((triple7 triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((triple7 triple8) -> rule2) OR ((((triple9) -> rule1) triple8) -> rule2))]
("Charlie" "is" "young" "-")
((triple7 triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
True
5
proof
[(((((triple7 triple8) -> rule2) triple9) -> rule6) OR ((((((triple9) -> rule1) triple8) -> rule2) triple9) -> rule6))]
("Charlie" "is" "kind" "+")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple9) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((((triple7 triple8) -> rule2) triple9) -> rule6) OR ((((((triple9) -> rule1) triple8) -> rule2) triple9) -> rule6))]
("Charlie" "is" "kind" "-")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple9) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple3 OR ((triple1) -> rule5))] Bob is kind.[(triple4)] Bob is not furry.[(triple2)] Bob is round.[(triple5)] Bob is young.[(triple6)] Charlie is big.[(triple7 OR ((triple9) -> rule1))] Charlie is furry.[(triple9)] Charlie is not cold.[(triple8)] Dave is big.[(triple10 OR ((triple12) -> rule1))] Dave is cold.[(triple11)] Dave is furry.[(triple12)] Dave is kind.[(triple14 OR ((triple16 triple12) -> rule6))] Dave is not green.[(triple13)] Dave is round.[(triple15)] Dave is young.[(triple16)] @1: Charlie is young.[(((triple7 triple8) -> rule2) OR ((((triple9) -> rule1) triple8) -> rule2))] @2: Charlie is kind.[(((((triple7 triple8) -> rule2) triple9) -> rule6) OR ((((((triple9) -> rule1) triple8) -> rule2) triple9) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple1) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Charlie is big.
("Charlie" "is" "big" "+")
triple7
((triple9) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple8
Dave is big.
("Dave" "is" "big" "+")
triple10
((triple12) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple11
Dave is furry.
("Dave" "is" "furry" "+")
triple12
Dave is kind.
("Dave" "is" "kind" "+")
triple14
((triple16 triple12) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple15
Dave is young.
("Dave" "is" "young" "+")
triple16
Charlie is young.
("Charlie" "is" "young" "+")
((triple7 triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple9) -> (rule1 % int2)) triple8) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple7 triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple9) -> (rule1 % int3)) triple8) -> (rule2 % int2)) triple9) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3