Dave is quiet. Fiona is cold. Harry is red. All rough things are kind. All rough, kind things are young. All quiet things are rough.
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
All rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All rough, kind things are young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Fiona is cold.
True
1
proof
[(triple2)]
("Fiona" "is" "cold" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Dave is rough.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "rough" "-")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "young" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not young.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "young" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Dave is quiet.[(triple1)] Fiona is cold.[(triple2)] Harry is red.[(triple3)] @1: Dave is rough.[(((triple1) -> rule3))] @2: Dave is kind.[(((((triple1) -> rule3)) -> rule1))] @3: Dave is young.[(((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule1)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3