Bob is nice. Fiona is cold. Fiona is furry. Fiona is green. Fiona is nice. Fiona is smart. Harry is green. All cold things are smart. If something is green then it is smart. All smart things are furry. All round things are cold. If something is green and not cold then it is young. All nice things are young. If something is young and furry then it is nice. If something is furry and not round then it is nice.
Bob is nice.
("Bob" "is" "nice" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is green.
("Harry" "is" "green" "+")
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is green and not cold then it is young.
((("something" "is" "green" "+") ("something" "is" "cold" "~")) -> ("something" "is" "young" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is young and furry then it is nice.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is furry and not round then it is nice.
((("something" "is" "furry" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "+"))
Fiona is furry.
True
1
proof
[(triple3 OR ((triple6) -> rule3) OR ((((triple2) -> rule1)) -> rule3) OR ((((triple4) -> rule2)) -> rule3))]
("Fiona" "is" "furry" "+")
triple3
((triple6) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is not cold.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "cold" "-")
triple2
Bob is young.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "young" "+")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "young" "-")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is furry.
True
3
proof
[(((((triple7) -> rule2)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple7) -> rule2)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Bob is cold.
Unknown
rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not furry.
Unknown
inv-rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule4 <- FAIL)]]
("Bob" "is" "furry" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is nice.[(triple1)] Fiona is cold.[(triple2)] Fiona is furry.[(triple3 OR ((triple6) -> rule3) OR ((((triple2) -> rule1)) -> rule3) OR ((((triple4) -> rule2)) -> rule3))] Fiona is green.[(triple4)] Fiona is nice.[(triple5)] Fiona is smart.[(triple6 OR ((triple2) -> rule1) OR ((triple4) -> rule2))] Harry is green.[(triple7)] @1: Bob is young.[(((triple1) -> rule6))] Fiona is young.[(((triple5) -> rule6))] Harry is smart.[(((triple7) -> rule2))] @2: Harry is furry.[(((((triple7) -> rule2)) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
((triple6) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
((triple2) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple5) -> (rule6 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2