Bob is blue. Bob is rough. Bob is round. Fiona is green. Harry is cold. Harry is not round. Harry is young. If Bob is cold and Bob is green then Bob is red. All cold, round people are blue. If someone is cold then they are blue. If someone is rough and not green then they are young. If someone is cold and not rough then they are young. If someone is round and red then they are cold.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is young.
("Harry" "is" "young" "+")
If Bob is cold and Bob is green then Bob is red.
((("Bob" "is" "cold" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "red" "+"))
All cold, round people are blue.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and not green then they are young.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "young" "+"))
If someone is cold and not rough then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "+"))
If someone is round and red then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
Fiona is green.
True
1
proof
[(triple4)]
("Fiona" "is" "green" "+")
triple4
Fiona is not green.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "green" "-")
triple4
Harry is blue.
True
2
proof
[(((triple5) -> rule3))]
("Harry" "is" "blue" "+")
((triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple5) -> rule3))]
("Harry" "is" "blue" "-")
((triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "red" "-")
Fiona is blue.
Unknown
rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is rough.[(triple2)] Bob is round.[(triple3)] Fiona is green.[(triple4)] Harry is cold.[(triple5)] Harry is not round.[(triple6)] Harry is young.[(triple7)] @1: Harry is blue.[(((triple5) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is not round.
("Harry" "is" "round" "-")
triple6
Harry is young.
("Harry" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
((triple5) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1