Charlie is not blue. Charlie is cold. Charlie is furry. Charlie is smart. Charlie is not white. Charlie is young. Gary is blue. Gary is cold. Gary is furry. Gary is red. Gary is not smart. Gary is white. Gary is young. Harry is furry. Harry is not smart. Harry is white. If someone is smart then they are furry. If someone is smart then they are not white. If Harry is cold then Harry is not young. All white people are cold. If Harry is smart and Harry is not furry then Harry is red. If someone is cold and red then they are young.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
Harry is white.
("Harry" "is" "white" "+")
If someone is smart then they are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart then they are not white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
If Harry is cold then Harry is not young.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "young" "-"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Harry is smart and Harry is not furry then Harry is red.
((("Harry" "is" "smart" "+") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "red" "+"))
If someone is cold and red then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Gary is white.
True
1
proof
[(triple12)]
("Gary" "is" "white" "+")
triple12
Gary is not cold.
False
1
inv-proof
[(triple8 OR ((triple12) -> rule4))]
("Gary" "is" "cold" "-")
triple8
((triple12) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Harry is cold.
True
2
proof
[(((triple16) -> rule4))]
("Harry" "is" "cold" "+")
((triple16) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple16) -> rule4))]
("Harry" "is" "cold" "-")
((triple16) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not young.
True
3
proof
[(((((triple16) -> rule4)) -> rule3))]
("Harry" "is" "young" "-")
((((triple16) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is young.
False
3
inv-proof
[(((((triple16) -> rule4)) -> rule3))]
("Harry" "is" "young" "+")
((((triple16) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple4) -> rule1))] Charlie is not blue.[(triple1)] Charlie is not white.[(triple5 OR ((triple4) -> rule2))] Charlie is smart.[(triple4)] Charlie is young.[(triple6)] Gary is blue.[(triple7)] Gary is cold.[(triple8 OR ((triple12) -> rule4))] Gary is furry.[(triple9)] Gary is not smart.[(triple11)] Gary is red.[(triple10)] Gary is white.[(triple12)] Gary is young.[(triple13 OR ((triple8 triple10) -> rule6) OR ((((triple12) -> rule4) triple10) -> rule6))] Harry is furry.[(triple14)] Harry is not smart.[(triple15)] Harry is white.[(triple16)] @1: Harry is cold.[(((triple16) -> rule4))] @2: Harry is not young.[(((((triple16) -> rule4)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is not white.
("Charlie" "is" "white" "-")
triple5
((triple4) -> (rule2 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple12) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple9
Gary is not smart.
("Gary" "is" "smart" "-")
triple11
Gary is red.
("Gary" "is" "red" "+")
triple10
Gary is white.
("Gary" "is" "white" "+")
triple12
Gary is young.
("Gary" "is" "young" "+")
triple13
((triple8 triple10) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple12) -> (rule4 % int2)) triple10) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple14
Harry is not smart.
("Harry" "is" "smart" "-")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Harry is cold.
("Harry" "is" "cold" "+")
((triple16) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not young.
("Harry" "is" "young" "-")
((((triple16) -> (rule4 % int2))) -> (rule3 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2