Charlie is cold. Charlie is green. Charlie is kind. Harry is blue. Harry is furry. Harry is green. Harry is nice. All smart things are furry. If Charlie is furry and Charlie is smart then Charlie is green. Cold things are smart. Furry things are blue. Kind things are smart. All nice things are blue. Blue, furry things are nice. If Charlie is blue then Charlie is nice.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Charlie is furry and Charlie is smart then Charlie is green.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "green" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Blue, furry things are nice.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If Charlie is blue then Charlie is nice.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "nice" "+"))
Harry is blue.
True
1
proof
[(triple4 OR ((triple5) -> rule4) OR ((triple7) -> rule6))]
("Harry" "is" "blue" "+")
triple4
((triple5) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple7 OR ((triple4 triple5) -> rule7) OR ((((triple5) -> rule4) triple5) -> rule7))]
("Harry" "is" "nice" "-")
triple7
((triple4 triple5) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Charlie is smart.
True
2
proof
[(((triple1) -> rule3) OR ((triple3) -> rule5))]
("Charlie" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple3) -> rule5))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2 OR ((((((triple1) -> rule3)) -> rule1) ((triple1) -> rule3)) -> rule2) OR ((((((triple1) -> rule3)) -> rule1) ((triple3) -> rule5)) -> rule2) OR ((((((triple3) -> rule5)) -> rule1) ((triple1) -> rule3)) -> rule2) OR ((((((triple3) -> rule5)) -> rule1) ((triple3) -> rule5)) -> rule2))] Charlie is kind.[(triple3)] Harry is blue.[(triple4 OR ((triple5) -> rule4) OR ((triple7) -> rule6))] Harry is furry.[(triple5)] Harry is green.[(triple6)] Harry is nice.[(triple7 OR ((triple4 triple5) -> rule7) OR ((((triple5) -> rule4) triple5) -> rule7))] @1: Charlie is smart.[(((triple1) -> rule3) OR ((triple3) -> rule5))] @2: Charlie is furry.[(((((triple1) -> rule3)) -> rule1) OR ((((triple3) -> rule5)) -> rule1))] @3: Charlie is blue.[(((((((triple1) -> rule3)) -> rule1)) -> rule4) OR ((((((triple3) -> rule5)) -> rule1)) -> rule4))] @4: Charlie is nice.[(((((((((triple1) -> rule3)) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple3) -> rule5)) -> rule1)) -> rule4)) -> rule8) OR ((((((((triple1) -> rule3)) -> rule1)) -> rule4) ((((triple1) -> rule3)) -> rule1)) -> rule7) OR ((((((((triple1) -> rule3)) -> rule1)) -> rule4) ((((triple3) -> rule5)) -> rule1)) -> rule7) OR ((((((((triple3) -> rule5)) -> rule1)) -> rule4) ((((triple1) -> rule3)) -> rule1)) -> rule7) OR ((((((((triple3) -> rule5)) -> rule1)) -> rule4) ((((triple3) -> rule5)) -> rule1)) -> rule7))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2)) ((triple3) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2)) ((triple3) -> (rule5 % int3))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
((triple5) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple4 triple5) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple3) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
int4