Bob is rough. Fiona is round. Gary is kind. Harry is blue. Harry is red. Harry is rough. Harry is round. Cold things are kind. If something is cold then it is rough. Kind, nice things are rough. All kind things are nice. If something is round and rough then it is nice. If something is red and rough then it is blue. Rough things are kind. Kind, round things are cold.
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Kind, nice things are rough.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
All kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is round and rough then it is nice.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is red and rough then it is blue.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Kind, round things are cold.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
Bob is kind.
True
2
proof
[(((triple1) -> rule7))]
("Bob" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Harry is not nice.
False
3
inv-proof
[(((triple7 triple6) -> rule5) OR ((((triple6) -> rule7)) -> rule4))]
("Harry" "is" "nice" "-")
((triple7 triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
True
4
proof
[(((((triple6) -> rule7) triple7) -> rule8))]
("Harry" "is" "cold" "+")
((((triple6) -> (rule7 % int2)) triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple6) -> rule7) triple7) -> rule8))]
("Harry" "is" "cold" "-")
((((triple6) -> (rule7 % int2)) triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "blue" "-")
Fiona is kind.
Unknown
rconc
[@4: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is rough.[(triple1)] Fiona is round.[(triple2)] Gary is kind.[(triple3)] Harry is blue.[(triple4 OR ((triple5 triple6) -> rule6))] Harry is red.[(triple5)] Harry is rough.[(triple6)] Harry is round.[(triple7)] @1: Bob is kind.[(((triple1) -> rule7))] Gary is nice.[(((triple3) -> rule4))] Harry is kind.[(((triple6) -> rule7))] Harry is nice.[(((triple7 triple6) -> rule5) OR ((((triple6) -> rule7)) -> rule4))] @2: Bob is nice.[(((((triple1) -> rule7)) -> rule4))] Gary is rough.[(((triple3 ((triple3) -> rule4)) -> rule3))] Harry is cold.[(((((triple6) -> rule7) triple7) -> rule8))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
((triple5 triple6) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 triple6) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple6) -> (rule7 % int2)) triple7) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2