Charlie is red. Charlie is smart. Fiona is green. Fiona is quiet. Gary is green. Gary is red. Gary is smart. Gary is young. Harry is quiet. Harry is young. If Harry is furry then Harry is smart. If someone is red then they are furry. All green people are red. All smart people are kind. Green people are red. If Charlie is furry then Charlie is kind. Green, young people are furry. Green, smart people are furry.
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is furry then Harry is smart.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "smart" "+"))
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
If Charlie is furry then Charlie is kind.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "kind" "+"))
Green, young people are furry.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Green, smart people are furry.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Charlie is smart.
True
1
proof
[(triple2)]
("Charlie" "is" "smart" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple10)]
("Harry" "is" "young" "-")
triple10
Gary is furry.
True
2
proof
[(((triple6) -> rule2) OR ((triple5 triple7) -> rule8) OR ((triple5 triple8) -> rule7) OR ((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule5)) -> rule2))]
("Gary" "is" "furry" "+")
((triple6) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple5 triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple5 triple8) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is furry.
True
3
proof
[(((((triple3) -> rule3)) -> rule2) OR ((((triple3) -> rule5)) -> rule2))]
("Fiona" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is not furry.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2) OR ((((triple3) -> rule5)) -> rule2))]
("Fiona" "is" "furry" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is kind.
Unknown
rconc
[@4: Harry is kind.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Charlie is red.[(triple1)] Charlie is smart.[(triple2)] Fiona is green.[(triple3)] Fiona is quiet.[(triple4)] Gary is green.[(triple5)] Gary is red.[(triple6 OR ((triple5) -> rule3) OR ((triple5) -> rule5))] Gary is smart.[(triple7)] Gary is young.[(triple8)] Harry is quiet.[(triple9)] Harry is young.[(triple10)] @1: Charlie is furry.[(((triple1) -> rule2))] Charlie is kind.[(((triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule6))] Fiona is red.[(((triple3) -> rule3) OR ((triple3) -> rule5))] Gary is furry.[(((triple6) -> rule2) OR ((triple5 triple7) -> rule8) OR ((triple5 triple8) -> rule7) OR ((((triple5) -> rule3)) -> rule2) OR ((((triple5) -> rule5)) -> rule2))] Gary is kind.[(((triple7) -> rule4))] @2: Fiona is furry.[(((((triple3) -> rule3)) -> rule2) OR ((((triple3) -> rule5)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple5) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Gary is young.
("Gary" "is" "young" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((triple3) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple3) -> (rule5 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple5 triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple5 triple8) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple7) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2