Charlie is big. Charlie is not blue. Charlie is cold. Charlie is green. Charlie is quiet. Charlie is round. Charlie is not smart. Harry is big. Harry is not round. Harry is smart. If someone is smart then they are blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple10)]
("Harry" "is" "smart" "-")
triple10
Harry is blue.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "blue" "+")
((triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple10) -> rule1))]
("Harry" "is" "blue" "-")
((triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple3)] Charlie is green.[(triple4)] Charlie is not blue.[(triple2)] Charlie is not smart.[(triple7)] Charlie is quiet.[(triple5)] Charlie is round.[(triple6)] Harry is big.[(triple8)] Harry is not round.[(triple9)] Harry is smart.[(triple10)] @1: Harry is blue.[(((triple10) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is not round.
("Harry" "is" "round" "-")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
((triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1