Bob is blue. Charlie is round. Dave is not green. Fiona is young. If Charlie is young then Charlie is blue. Green, blue things are young. If something is green and not quiet then it is young. If Dave is not blue then Dave is smart. All blue, smart things are cold. Smart, green things are cold. If something is blue then it is not smart. If Charlie is not green then Charlie is not cold.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is not green.
("Dave" "is" "green" "-")
Fiona is young.
("Fiona" "is" "young" "+")
If Charlie is young then Charlie is blue.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "blue" "+"))
Green, blue things are young.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is green and not quiet then it is young.
((("something" "is" "green" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "young" "+"))
If Dave is not blue then Dave is smart.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "smart" "+"))
All blue, smart things are cold.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
Smart, green things are cold.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is not smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "-"))
If Charlie is not green then Charlie is not cold.
((("Charlie" "is" "green" "~")) -> ("Charlie" "is" "cold" "-"))
Fiona is young.
True
1
proof
[(triple4)]
("Fiona" "is" "young" "+")
triple4
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Bob is not smart.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "smart" "-")
((triple1) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is smart.
False
2
inv-proof
[(((triple1) -> rule7))]
("Bob" "is" "smart" "+")
((triple1) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Bob is blue.[(triple1)] Charlie is round.[(triple2)] Dave is not green.[(triple3)] Fiona is young.[(triple4)] @1: Bob is not smart.[(((triple1) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is not green.
("Dave" "is" "green" "-")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule7 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1