Dave is cold. Gary is big. Gary is green. Green, furry things are quiet. If something is kind and furry then it is quiet. If Gary is big then Gary is kind. All big things are green. All cold things are quiet. All big things are green. If something is big and kind then it is quiet. If Gary is quiet and Gary is big then Gary is nice.
Dave is cold.
("Dave" "is" "cold" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Green, furry things are quiet.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is kind and furry then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If Gary is big then Gary is kind.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "kind" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something is big and kind then it is quiet.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
If Gary is quiet and Gary is big then Gary is nice.
((("Gary" "is" "quiet" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "nice" "+"))
Gary is green.
True
1
proof
[(triple3 OR ((triple2) -> rule4) OR ((triple2) -> rule6))]
("Gary" "is" "green" "+")
triple3
((triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple2) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Gary is kind.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule7))]
("Gary" "is" "quiet" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not quiet.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule7))]
("Gary" "is" "quiet" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is cold.[(triple1)] Gary is big.[(triple2)] Gary is green.[(triple3 OR ((triple2) -> rule4) OR ((triple2) -> rule6))] @1: Dave is quiet.[(((triple1) -> rule5))] Gary is kind.[(((triple2) -> rule3))] @2: Gary is quiet.[(((triple2 ((triple2) -> rule3)) -> rule7))] @3: Gary is nice.[(((((triple2 ((triple2) -> rule3)) -> rule7) triple2) -> rule8))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((triple2) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple2) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule7 % int2)) triple2) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3