Charlie is blue. Charlie is furry. Charlie is young. Erin is white. Erin is young. Gary is blue. Gary is quiet. Gary is white. Gary is not young. Harry is nice. Harry is quiet. Harry is smart. Blue people are furry. If Harry is young and Harry is nice then Harry is blue. All nice people are young. Quiet people are smart. If Harry is young then Harry is nice. If someone is blue and not furry then they are not white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Harry is young and Harry is nice then Harry is blue.
((("Harry" "is" "young" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "blue" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Harry is young then Harry is nice.
((("Harry" "is" "young" "+")) -> ("Harry" "is" "nice" "+"))
If someone is blue and not furry then they are not white.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "-"))
Gary is not young.
True
1
proof
[(triple9)]
("Gary" "is" "young" "-")
triple9
Gary is young.
False
1
inv-proof
[(triple9)]
("Gary" "is" "young" "+")
triple9
Gary is smart.
True
2
proof
[(((triple7) -> rule4))]
("Gary" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple6) -> rule1))]
("Gary" "is" "furry" "-")
((triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is blue.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "blue" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule2))]
("Harry" "is" "blue" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
True
5
proof
[(((((((triple10) -> rule3) triple10) -> rule2)) -> rule1))]
("Harry" "is" "furry" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not furry.
False
5
inv-proof
[(((((((triple10) -> rule3) triple10) -> rule2)) -> rule1))]
("Harry" "is" "furry" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2 OR ((triple1) -> rule1))] Charlie is young.[(triple3)] Erin is white.[(triple4)] Erin is young.[(triple5)] Gary is blue.[(triple6)] Gary is not young.[(triple9)] Gary is quiet.[(triple7)] Gary is white.[(triple8)] Harry is nice.[(triple10)] Harry is quiet.[(triple11)] Harry is smart.[(triple12 OR ((triple11) -> rule4))] @1: Gary is furry.[(((triple6) -> rule1))] Gary is smart.[(((triple7) -> rule4))] Harry is young.[(((triple10) -> rule3))] @2: Harry is blue.[(((((triple10) -> rule3) triple10) -> rule2))] @3: Harry is furry.[(((((((triple10) -> rule3) triple10) -> rule2)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is not young.
("Gary" "is" "young" "-")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple11) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple10) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3