Anne is big. Anne is not blue. Bob is big. Bob is kind. Dave is cold. Dave is kind. Dave is young. Fiona is blue. Fiona is quiet. Fiona is not young. All rough things are big. If something is big then it is kind. If something is quiet then it is rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is not blue.
("Anne" "is" "blue" "-")
Bob is big.
("Bob" "is" "big" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple5)]
("Dave" "is" "cold" "-")
triple5
Anne is kind.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Fiona is big.
True
3
proof
[(((((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not big.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule1))]
("Fiona" "is" "big" "-")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is kind.
True
4
proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "kind" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not kind.
False
4
inv-proof
[(((((((triple9) -> rule3)) -> rule1)) -> rule2))]
("Fiona" "is" "kind" "-")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is not blue.[(triple2)] Bob is big.[(triple3)] Bob is kind.[(triple4 OR ((triple3) -> rule2))] Dave is cold.[(triple5)] Dave is kind.[(triple6)] Dave is young.[(triple7)] Fiona is blue.[(triple8)] Fiona is not young.[(triple10)] Fiona is quiet.[(triple9)] @1: Anne is kind.[(((triple1) -> rule2))] Fiona is rough.[(((triple9) -> rule3))] @2: Fiona is big.[(((((triple9) -> rule3)) -> rule1))] @3: Fiona is kind.[(((((((triple9) -> rule3)) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not blue.
("Anne" "is" "blue" "-")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple3) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is not young.
("Fiona" "is" "young" "-")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple9) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((((triple9) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple9) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3