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