Bob is kind. Bob is not red. Erin is red. Erin is smart. Fiona is not kind. Harry is kind. Harry is round. If someone is kind then they are nice. All young people are nice. If someone is smart then they are young. If Bob is nice and Bob is young then Bob is round. If someone is nice and young then they are not round. Kind, smart people are red.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not red.
("Bob" "is" "red" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If Bob is nice and Bob is young then Bob is round.
((("Bob" "is" "nice" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "round" "+"))
If someone is nice and young then they are not round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "-"))
Kind, smart people are red.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Harry is kind.
True
1
proof
[(triple6)]
("Harry" "is" "kind" "+")
triple6
Fiona is kind.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "kind" "+")
triple5
Bob is nice.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple6) -> rule1))]
("Harry" "is" "nice" "-")
((triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Erin is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Erin" "is" "nice" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not round.
True
6
proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))]
("Erin" "is" "round" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
False
6
inv-proof
[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))]
("Erin" "is" "round" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "red" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is kind.[(triple1)] Bob is not red.[(triple2)] Erin is red.[(triple3)] Erin is smart.[(triple4)] Fiona is not kind.[(triple5)] Harry is kind.[(triple6)] Harry is round.[(triple7)] @1: Bob is nice.[(((triple1) -> rule1))] Erin is young.[(((triple4) -> rule3))] Harry is nice.[(((triple6) -> rule1))] @2: Erin is nice.[(((((triple4) -> rule3)) -> rule2))] @3: Erin is not round.[(((((((triple4) -> rule3)) -> rule2) ((triple4) -> rule3)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is not red.
("Bob" "is" "red" "-")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
triple4
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not round.
("Erin" "is" "round" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule5 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3