Bob is nice. Fiona is kind. Gary is cold. All nice, smart things are green. If something is nice then it is smart. If Fiona is smart and Fiona is not young then Fiona is cold.
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All nice, smart things are green.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Fiona is smart and Fiona is not young then Fiona is cold.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "young" "~")) -> ("Fiona" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Fiona is not kind.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "kind" "-")
triple2
Bob is smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "green" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Fiona is kind.[(triple2)] Gary is cold.[(triple3)] @1: Bob is smart.[(((triple1) -> rule2))] @2: Bob is green.[(((triple1 ((triple1) -> rule2)) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2