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