Bob is furry. Charlie is furry. Dave is blue. Fiona is furry. All furry people are young. If someone is furry and not nice then they are young. Furry, young people are blue. If someone is cold then they are rough. All rough, furry people are red. All furry, rough people are red. All rough people are not red. If Dave is rough and Dave is not nice then Dave is not furry.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
All furry people are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is furry and not nice then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "young" "+"))
Furry, young people are blue.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
All rough, furry people are red.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All furry, rough people are red.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All rough people are not red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "-"))
If Dave is rough and Dave is not nice then Dave is not furry.
((("Dave" "is" "rough" "+") ("Dave" "is" "nice" "~")) -> ("Dave" "is" "furry" "-"))
Bob is furry.
True
1
proof
[(triple1)]
("Bob" "is" "furry" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Bob is young.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Fiona" "is" "young" "-")
((triple4) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is blue.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "blue" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((triple2 ((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "blue" "-")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Charlie is furry.[(triple2)] Dave is blue.[(triple3)] Fiona is furry.[(triple4)] @1: Bob is young.[(((triple1) -> rule1))] Charlie is young.[(((triple2) -> rule1))] Fiona is young.[(((triple4) -> rule1))] @2: Bob is blue.[(((triple1 ((triple1) -> rule1)) -> rule3))] Charlie is blue.[(((triple2 ((triple2) -> rule1)) -> rule3))] Fiona is blue.[(((triple4 ((triple4) -> rule1)) -> rule3))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple4) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2 ((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2