Bob is not green. Charlie is furry. Fiona is furry. Harry is nice. If Fiona is smart and Fiona is green then Fiona is big. Green, nice things are furry. All furry things are smart. Big things are smart. If something is green then it is smart. If something is blue then it is not cold. If Harry is nice then Harry is furry. If Fiona is nice then Fiona is green.
Bob is not green.
("Bob" "is" "green" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Fiona is smart and Fiona is green then Fiona is big.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "big" "+"))
Green, nice things are furry.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If something is blue then it is not cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If Harry is nice then Harry is furry.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "+"))
If Fiona is nice then Fiona is green.
((("Fiona" "is" "nice" "+")) -> ("Fiona" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Bob is green.
False
1
inv-proof
[(triple1)]
("Bob" "is" "green" "+")
triple1
Fiona is smart.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "furry" "-")
((triple4) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
True
3
proof
[(((((triple4) -> rule7)) -> rule3))]
("Harry" "is" "smart" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule3))]
("Harry" "is" "smart" "-")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "green" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is not green.[(triple1)] Charlie is furry.[(triple2)] Fiona is furry.[(triple3)] Harry is nice.[(triple4)] @1: Charlie is smart.[(((triple2) -> rule3))] Fiona is smart.[(((triple3) -> rule3))] Harry is furry.[(((triple4) -> rule7))] @2: Harry is smart.[(((((triple4) -> rule7)) -> rule3))]
Bob is not green.
("Bob" "is" "green" "-")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2