Bob is smart. Charlie is big. Fiona is kind. Smart things are quiet. Big, kind things are smart. If something is kind then it is big.
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Big, kind things are smart.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Fiona is kind.
True
1
proof
[(triple3)]
("Fiona" "is" "kind" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "big" "-")
((triple3) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Fiona" "is" "smart" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not smart.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Fiona" "is" "smart" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
True
5
proof
[(((((((triple3) -> rule3) triple3) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not quiet.
False
5
inv-proof
[(((((((triple3) -> rule3) triple3) -> rule2)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "big" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is smart.[(triple1)] Charlie is big.[(triple2)] Fiona is kind.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule1))] Fiona is big.[(((triple3) -> rule3))] @2: Fiona is smart.[(((((triple3) -> rule3) triple3) -> rule2))] @3: Fiona is quiet.[(((((((triple3) -> rule3) triple3) -> rule2)) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule3 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3