Anne is quiet. Bob is young. Charlie is kind. Fiona is young. If something is quiet then it is big. Kind things are white. If something is young then it is kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is quiet then it is big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is young then it is kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Fiona is young.
True
1
proof
[(triple4)]
("Fiona" "is" "young" "+")
triple4
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Anne is big.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "big" "-")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Bob" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "big" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Bob is young.[(triple2)] Charlie is kind.[(triple3)] Fiona is young.[(triple4)] @1: Anne is big.[(((triple1) -> rule1))] Bob is kind.[(((triple2) -> rule3))] Charlie is white.[(((triple3) -> rule2))] Fiona is kind.[(((triple4) -> rule3))] @2: Bob is white.[(((((triple2) -> rule3)) -> rule2))] Fiona is white.[(((((triple4) -> rule3)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2