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