Charlie is quiet. Fiona is big. Gary is young. Harry is cold. If something is quiet and blue then it is young. All quiet things are big. If something is blue and young then it is quiet. Blue, furry things are cold. If something is white then it is young. Quiet things are furry. If something is quiet then it is white. If Charlie is furry and Charlie is big then Charlie is young.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If something is quiet and blue then it is young.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is blue and young then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Blue, furry things are cold.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If something is quiet then it is white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If Charlie is furry and Charlie is big then Charlie is young.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "young" "+"))
Harry is cold.
True
1
proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Charlie is white.
True
2
proof
[(((triple1) -> rule7))]
("Charlie" "is" "white" "+")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule7))]
("Charlie" "is" "white" "-")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
True
3
proof
[(((((triple1) -> rule7)) -> rule5) OR ((((triple1) -> rule6) ((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not young.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5) OR ((((triple1) -> rule6) ((triple1) -> rule2)) -> rule8))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Fiona is young.
Unknown
rconc
[@3: Fiona is young.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
Harry is not young.
Unknown
inv-rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is quiet.[(triple1)] Fiona is big.[(triple2)] Gary is young.[(triple3)] Harry is cold.[(triple4)] @1: Charlie is big.[(((triple1) -> rule2))] Charlie is furry.[(((triple1) -> rule6))] Charlie is white.[(((triple1) -> rule7))] @2: Charlie is young.[(((((triple1) -> rule7)) -> rule5) OR ((((triple1) -> rule6) ((triple1) -> rule2)) -> rule8))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is big.
("Fiona" "is" "big" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple1) -> (rule6 % int3)) ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3