Bob is big. Charlie is big. Charlie is green. Gary is cold. Gary is furry. Gary is green. Gary is quiet. All quiet, furry things are big. If something is big and green then it is kind. If something is big then it is kind.
Bob is big.
("Bob" "is" "big" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All quiet, furry things are big.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is big and green then it is kind.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Gary is green.
True
1
proof
[(triple6)]
("Gary" "is" "green" "+")
triple6
Gary is not quiet.
False
1
inv-proof
[(triple7)]
("Gary" "is" "quiet" "-")
triple7
Charlie is kind.
True
2
proof
[(((triple2) -> rule3) OR ((triple2 triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2 triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is not big.
False
3
inv-proof
[(((triple7 triple5) -> rule1))]
("Gary" "is" "big" "-")
((triple7 triple5) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Charlie is big.[(triple2)] Charlie is green.[(triple3)] Gary is cold.[(triple4)] Gary is furry.[(triple5)] Gary is green.[(triple6)] Gary is quiet.[(triple7)] @1: Bob is kind.[(((triple1) -> rule3))] Charlie is kind.[(((triple2) -> rule3) OR ((triple2 triple3) -> rule2))] Gary is big.[(((triple7 triple5) -> rule1))] @2: Gary is kind.[(((((triple7 triple5) -> rule1)) -> rule3) OR ((((triple7 triple5) -> rule1) triple6) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple2 triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7 triple5) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple7 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple7 triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2