Anne is quiet. Bob is young. Erin is big. Fiona is round. If someone is kind and young then they are smart. All young people are kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is kind and young then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Fiona is not round.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "round" "-")
triple4
Bob is kind.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "kind" "-")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule1))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule1))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Anne is quiet.[(triple1)] Bob is young.[(triple2)] Erin is big.[(triple3)] Fiona is round.[(triple4)] @1: Bob is kind.[(((triple2) -> rule2))] @2: Bob is smart.[(((((triple2) -> rule2) triple2) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2