Anne is cold. Anne is red. Anne is rough. Charlie is big. Charlie is not blue. Charlie is nice. Charlie is red. Gary is not blue. Gary is rough. Harry is big. Harry is blue. Harry is smart. If Gary is cold and Gary is not smart then Gary is blue. If someone is smart and not big then they are nice. If someone is big and not cold then they are nice. If someone is big and rough then they are not red. If someone is nice then they are red. Smart people are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Gary is cold and Gary is not smart then Gary is blue.
((("Gary" "is" "cold" "+") ("Gary" "is" "smart" "~")) -> ("Gary" "is" "blue" "+"))
If someone is smart and not big then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "nice" "+"))
If someone is big and not cold then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
If someone is big and rough then they are not red.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Charlie is not blue.
True
1
proof
[(triple5)]
("Charlie" "is" "blue" "-")
triple5
Harry is not blue.
False
1
inv-proof
[(triple11)]
("Harry" "is" "blue" "-")
triple11
Harry is rough.
True
2
proof
[(((triple12) -> rule6))]
("Harry" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple12) -> rule6))]
("Harry" "is" "rough" "-")
((triple12) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not red.
True
4
proof
[(((triple10 ((triple12) -> rule6)) -> rule4))]
("Harry" "is" "red" "-")
((triple10 ((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is red.
False
4
inv-proof
[(((triple10 ((triple12) -> rule6)) -> rule4))]
("Harry" "is" "red" "+")
((triple10 ((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "nice" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "nice" "+")
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Charlie is big.[(triple4)] Charlie is nice.[(triple6)] Charlie is not blue.[(triple5)] Charlie is red.[(triple7 OR ((triple6) -> rule5))] Gary is not blue.[(triple8)] Gary is rough.[(triple9)] Harry is big.[(triple10)] Harry is blue.[(triple11)] Harry is smart.[(triple12)] @1: Harry is rough.[(((triple12) -> rule6))] @2: Harry is not red.[(((triple10 ((triple12) -> rule6)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple7
((triple6) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((triple10 ((triple12) -> (rule6 % int2))) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2