Bob is big. Bob is cold. Bob is not red. Bob is smart. Bob is white. Fiona is rough. Fiona is not white. All round, big things are cold. All round, big things are rough. Smart things are round. If Fiona is white then Fiona is big. If Fiona is white then Fiona is smart. If Fiona is not smart and Fiona is not white then Fiona is not cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
All round, big things are cold.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All round, big things are rough.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If Fiona is white then Fiona is big.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "big" "+"))
If Fiona is white then Fiona is smart.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "smart" "+"))
If Fiona is not smart and Fiona is not white then Fiona is not cold.
((("Fiona" "is" "smart" "~") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "cold" "-"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Bob is red.
False
1
inv-proof
[(triple3)]
("Bob" "is" "red" "+")
triple3
Bob is round.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "round" "+")
((triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple4) -> rule3))]
("Bob" "is" "round" "-")
((triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
True
4
proof
[(((((triple4) -> rule3) triple1) -> rule2))]
("Bob" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((((triple4) -> rule3) triple1) -> rule2))]
("Bob" "is" "rough" "-")
((((triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is not round.
Unknown
inv-rconc
[@2: Fiona is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((((triple4) -> rule3) triple1) -> rule1))] Bob is not red.[(triple3)] Bob is smart.[(triple4)] Bob is white.[(triple5)] Fiona is not white.[(triple7)] Fiona is rough.[(triple6)] @1: Bob is round.[(((triple4) -> rule3))] @2: Bob is rough.[(((((triple4) -> rule3) triple1) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((((triple4) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not red.
("Bob" "is" "red" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Fiona is not white.
("Fiona" "is" "white" "-")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
Bob is round.
("Bob" "is" "round" "+")
((triple4) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2