Bob is red. Fiona is nice. Gary is furry. Harry is furry. All furry things are nice. If something is kind and red then it is white. All nice, white things are cold. If Gary is nice then Gary is green. If something is green then it is nice. If Bob is green then Bob is furry. All nice things are cold. Red, white things are green.
Bob is red.
("Bob" "is" "red" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is kind and red then it is white.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All nice, white things are cold.
((("something" "is" "nice" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Gary is nice then Gary is green.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "green" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Bob is green then Bob is furry.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "furry" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Red, white things are green.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Gary is furry.
True
1
proof
[(triple3)]
("Gary" "is" "furry" "+")
triple3
Fiona is not nice.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "nice" "-")
triple2
Gary is nice.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "nice" "-")
((triple4) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
True
3
proof
[(((((triple4) -> rule1)) -> rule7))]
("Harry" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("Gary" "is" "green" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Bob is furry.
Unknown
rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule2 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not nice.
Unknown
inv-rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule8 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Bob is red.[(triple1)] Fiona is nice.[(triple2)] Gary is furry.[(triple3)] Harry is furry.[(triple4)] @1: Fiona is cold.[(((triple2) -> rule7))] Gary is nice.[(((triple3) -> rule1))] Harry is nice.[(((triple4) -> rule1))] @2: Gary is cold.[(((((triple3) -> rule1)) -> rule7))] Gary is green.[(((((triple3) -> rule1)) -> rule4))] Harry is cold.[(((((triple4) -> rule1)) -> rule7))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple2) -> (rule7 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple4) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule1 % int2))) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2