Anne is big. Anne is smart. Bob is cold. Bob is green. Bob is nice. Charlie is big. Charlie is cold. Charlie is furry. Charlie is green. Charlie is nice. Charlie is young. Harry is big. Harry is green. Harry is nice. Harry is young. If Charlie is big then Charlie is green. If someone is big then they are cold.
Anne is big.
("Anne" "is" "big" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If Charlie is big then Charlie is green.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
If someone is big then they are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Harry is big.
True
1
proof
[(triple12)]
("Harry" "is" "big" "+")
triple12
Charlie is not big.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "big" "-")
triple6
Anne is cold.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple12) -> rule2))]
("Harry" "is" "cold" "-")
((triple12) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is big.[(triple1)] Anne is smart.[(triple2)] Bob is cold.[(triple3)] Bob is green.[(triple4)] Bob is nice.[(triple5)] Charlie is big.[(triple6)] Charlie is cold.[(triple7 OR ((triple6) -> rule2))] Charlie is furry.[(triple8)] Charlie is green.[(triple9 OR ((triple6) -> rule1))] Charlie is nice.[(triple10)] Charlie is young.[(triple11)] Harry is big.[(triple12)] Harry is green.[(triple13)] Harry is nice.[(triple14)] Harry is young.[(triple15)] @1: Anne is cold.[(((triple1) -> rule2))] Harry is cold.[(((triple12) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is green.
("Harry" "is" "green" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple12) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1