Charlie is quiet. Dave is kind. Erin is cold. Harry is not blue. Kind, blue things are cold. Young things are not cold. All quiet things are kind. Furry, blue things are big. If something is quiet and kind then it is young. Big things are young.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Kind, blue things are cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Young things are not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
All quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Furry, blue things are big.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is quiet and kind then it is young.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Harry is not blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Erin is not cold.
False
1
inv-proof
[(triple3)]
("Erin" "is" "cold" "-")
triple3
Charlie is kind.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule5))]
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule5))]
("Charlie" "is" "young" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "big" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Charlie is quiet.[(triple1)] Dave is kind.[(triple2)] Erin is cold.[(triple3)] Harry is not blue.[(triple4)] @1: Charlie is kind.[(((triple1) -> rule3))] @2: Charlie is young.[(((triple1 ((triple1) -> rule3)) -> rule5))] @3: Charlie is not cold.[(((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule2))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is not blue.
("Harry" "is" "blue" "-")
triple4
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3