Bob is nice. Charlie is blue. Dave is smart. Fiona is kind. Smart things are nice. If something is young then it is nice. Kind, smart things are nice. Kind, quiet things are nice. If something is young and kind then it is not blue. If something is quiet and kind then it is young. Rough things are young. If something is kind then it is rough.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
Kind, smart things are nice.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Kind, quiet things are nice.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is young and kind then it is not blue.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "-"))
If something is quiet and kind then it is young.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Fiona is rough.
True
2
proof
[(((triple4) -> rule8))]
("Fiona" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is young.
True
3
proof
[(((((triple4) -> rule8)) -> rule7))]
("Fiona" "is" "young" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not young.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule7))]
("Fiona" "is" "young" "-")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "rough" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Dave" "is" "young" "+")
Charlie is not nice.
Unknown
inv-rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule8 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is nice.[(triple1)] Charlie is blue.[(triple2)] Dave is smart.[(triple3)] Fiona is kind.[(triple4)] @1: Dave is nice.[(((triple3) -> rule1))] Fiona is rough.[(((triple4) -> rule8))] @2: Fiona is young.[(((((triple4) -> rule8)) -> rule7))] @3: Fiona is nice.[(((((((triple4) -> rule8)) -> rule7)) -> rule2))] Fiona is not blue.[(((((((triple4) -> rule8)) -> rule7) triple4) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not blue.
("Fiona" "is" "blue" "-")
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2)) triple4) -> (rule5 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3