Bob is big. Erin is young. Fiona is big. Gary is cold. If something is cold then it is furry. All round, rough things are young. If something is furry then it is blue.
Bob is big.
("Bob" "is" "big" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
All round, rough things are young.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Gary is cold.
True
1
proof
[(triple4)]
("Gary" "is" "cold" "+")
triple4
Fiona is not big.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "big" "-")
triple3
Gary is furry.
True
2
proof
[(((triple4) -> rule1))]
("Gary" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "furry" "-")
((triple4) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Gary" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not blue.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Gary" "is" "blue" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is big.[(triple1)] Erin is young.[(triple2)] Fiona is big.[(triple3)] Gary is cold.[(triple4)] @1: Gary is furry.[(((triple4) -> rule1))] @2: Gary is blue.[(((((triple4) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2