Bob is green. Fiona is nice. If someone is round and rough then they are blue. If someone is round then they are smart. All green people are round.
Bob is green.
("Bob" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If someone is round and rough then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Fiona is nice.
True
1
proof
[(triple2)]
("Fiona" "is" "nice" "+")
triple2
Fiona is not nice.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "nice" "-")
triple2
Bob is round.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "round" "-")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Bob is green.[(triple1)] Fiona is nice.[(triple2)] @1: Bob is round.[(((triple1) -> rule3))] @2: Bob is smart.[(((((triple1) -> rule3)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2