Anne is blue. Bob is quiet. Dave is blue. Fiona is nice. Quiet things are rough. All blue things are quiet. Cold, blue things are big.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
All blue things are quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Cold, blue things are big.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "rough" "-")
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is rough.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("Dave" "is" "rough" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "+")
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Bob is quiet.[(triple2)] Dave is blue.[(triple3)] Fiona is nice.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule2))] Bob is rough.[(((triple2) -> rule1))] Dave is quiet.[(((triple3) -> rule2))] @2: Anne is rough.[(((((triple1) -> rule2)) -> rule1))] Dave is rough.[(((((triple3) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2