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