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