Bob is smart. Fiona is quiet. Fiona is not smart. All smart things are young. If Fiona is round then Fiona is not kind. All rough things are blue. All quiet things are not kind. If Bob is smart and Bob is not blue then Bob is not young. If something is rough then it is not quiet. Blue, rough things are quiet. All young things are quiet.
Bob is smart.
("Bob" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not smart.
("Fiona" "is" "smart" "-")
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If Fiona is round then Fiona is not kind.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "kind" "-"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All quiet things are not kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "-"))
If Bob is smart and Bob is not blue then Bob is not young.
((("Bob" "is" "smart" "+") ("Bob" "is" "blue" "~")) -> ("Bob" "is" "young" "-"))
If something is rough then it is not quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
Blue, rough things are quiet.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Fiona is not smart.
True
1
proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Bob is not smart.
False
1
inv-proof
[(triple1)]
("Bob" "is" "smart" "-")
triple1
Fiona is not kind.
True
2
proof
[(((triple2) -> rule4))]
("Fiona" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Fiona is kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Fiona" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not kind.
True
4
proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "kind" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is kind.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule4))]
("Bob" "is" "kind" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Bob is smart.[(triple1)] Fiona is not smart.[(triple3)] Fiona is quiet.[(triple2)] @1: Bob is young.[(((triple1) -> rule1))] Fiona is not kind.[(((triple2) -> rule4))] @2: Bob is quiet.[(((((triple1) -> rule1)) -> rule8))] @3: Bob is not kind.[(((((((triple1) -> rule1)) -> rule8)) -> rule4))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Fiona is not smart.
("Fiona" "is" "smart" "-")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is not kind.
("Fiona" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Fiona is not kind.
("Fiona" "is" "kind" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3