Bob is white. Fiona is cold. Fiona is furry. Fiona is round. Gary is smart. Gary is white. Harry is red. If something is round and smart then it is red. If something is round and cold then it is smart.
Bob is white.
("Bob" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is red.
("Harry" "is" "red" "+")
If something is round and smart then it is red.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is round and cold then it is smart.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple5)]
("Gary" "is" "smart" "+")
triple5
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Fiona is smart.
True
3
proof
[(((triple4 triple2) -> rule2))]
("Fiona" "is" "smart" "+")
((triple4 triple2) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
3
inv-proof
[(((triple4 triple2) -> rule2))]
("Fiona" "is" "smart" "-")
((triple4 triple2) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
True
5
proof
[(((triple4 ((triple4 triple2) -> rule2)) -> rule1))]
("Fiona" "is" "red" "+")
((triple4 ((triple4 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not red.
False
5
inv-proof
[(((triple4 ((triple4 triple2) -> rule2)) -> rule1))]
("Fiona" "is" "red" "-")
((triple4 ((triple4 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is white.[(triple1)] Fiona is cold.[(triple2)] Fiona is furry.[(triple3)] Fiona is round.[(triple4)] Gary is smart.[(triple5)] Gary is white.[(triple6)] Harry is red.[(triple7)] @1: Fiona is smart.[(((triple4 triple2) -> rule2))] @2: Fiona is red.[(((triple4 ((triple4 triple2) -> rule2)) -> rule1))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple4 triple2) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple4 ((triple4 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2