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