Charlie is blue. Charlie is not cold. Charlie is kind. Charlie is red. Charlie is not young. Dave is blue. Dave is not kind. Dave is young. Fiona is big. Fiona is kind. Harry is red. Harry is young. If Harry is red then Harry is not smart. If Fiona is cold and Fiona is not blue then Fiona is young. If something is red and not smart then it is kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is young.
("Dave" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is red then Harry is not smart.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "smart" "-"))
If Fiona is cold and Fiona is not blue then Fiona is young.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "blue" "~")) -> ("Fiona" "is" "young" "+"))
If something is red and not smart then it is kind.
((("something" "is" "red" "+") ("something" "is" "smart" "~")) -> ("something" "is" "kind" "+"))
Charlie is not cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Dave is not blue.
False
1
inv-proof
[(triple6)]
("Dave" "is" "blue" "-")
triple6
Harry is not smart.
True
2
proof
[(((triple11) -> rule1))]
("Harry" "is" "smart" "-")
((triple11) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is smart.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "smart" "+")
((triple11) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is kind.
True
4
proof
[(((triple11 ((triple11) -> rule1)) -> rule3))]
("Harry" "is" "kind" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Harry is not kind.
False
4
inv-proof
[(((triple11 ((triple11) -> rule1)) -> rule3))]
("Harry" "is" "kind" "-")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple3)] Charlie is not cold.[(triple2)] Charlie is not young.[(triple5)] Charlie is red.[(triple4)] Dave is blue.[(triple6)] Dave is not kind.[(triple7)] Dave is young.[(triple8)] Fiona is big.[(triple9)] Fiona is kind.[(triple10)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Harry is not smart.[(((triple11) -> rule1))] @2: Harry is kind.[(((triple11 ((triple11) -> rule1)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is not young.
("Charlie" "is" "young" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Dave is not kind.
("Dave" "is" "kind" "-")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is not smart.
("Harry" "is" "smart" "-")
((triple11) -> (rule1 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not smart.
("Harry" "is" "smart" "-")
int2