Bob is big. Dave is big. Dave is blue. Dave is cold. Dave is furry. Fiona is blue. Fiona is furry. Furry people are cold. If Fiona is cold then Fiona is young.
Bob is big.
("Bob" "is" "big" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Fiona is cold then Fiona is young.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "young" "+"))
Dave is cold.
True
1
proof
[(triple4 OR ((triple5) -> rule1))]
("Dave" "is" "cold" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not furry.
False
1
inv-proof
[(triple5)]
("Dave" "is" "furry" "-")
triple5
Fiona is cold.
True
2
proof
[(((triple7) -> rule1))]
("Fiona" "is" "cold" "+")
((triple7) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple7) -> rule1))]
("Fiona" "is" "cold" "-")
((triple7) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("Fiona" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not young.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Fiona" "is" "young" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is big.[(triple1)] Dave is big.[(triple2)] Dave is blue.[(triple3)] Dave is cold.[(triple4 OR ((triple5) -> rule1))] Dave is furry.[(triple5)] Fiona is blue.[(triple6)] Fiona is furry.[(triple7)] @1: Fiona is cold.[(((triple7) -> rule1))] @2: Fiona is young.[(((((triple7) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
((triple5) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7) -> (rule1 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2