Bob is cold. Fiona is red. Harry is red. Red people are smart. If someone is smart then they are not nice. If Harry is nice and Harry is not red then Harry is white.
Bob is cold.
("Bob" "is" "cold" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are not nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "-"))
If Harry is nice and Harry is not red then Harry is white.
((("Harry" "is" "nice" "+") ("Harry" "is" "red" "~")) -> ("Harry" "is" "white" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Fiona is smart.
True
2
proof
[(((triple2) -> rule1))]
("Fiona" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is not nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Fiona is red.[(triple2)] Harry is red.[(triple3)] @1: Fiona is smart.[(((triple2) -> rule1))] Harry is smart.[(((triple3) -> rule1))] @2: Fiona is not nice.[(((((triple2) -> rule1)) -> rule2))] Harry is not nice.[(((((triple3) -> rule1)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Fiona is not nice.
("Fiona" "is" "nice" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is not nice.
("Fiona" "is" "nice" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Harry is not nice.
("Harry" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2