Bob is kind. Charlie is blue. Charlie is quiet. Charlie is not smart. Erin is blue. Erin is young. Fiona is not quiet. If Fiona is kind then Fiona is smart. If someone is young and blue then they are smart. If someone is blue and smart then they are red. All kind, smart people are red. If someone is young and not quiet then they are not big. All young, kind people are big. Blue, red people are kind. If Fiona is quiet and Fiona is not young then Fiona is not big.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
If Fiona is kind then Fiona is smart.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "smart" "+"))
If someone is young and blue then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue and smart then they are red.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All kind, smart people are red.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is young and not quiet then they are not big.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "big" "-"))
All young, kind people are big.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Blue, red people are kind.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is quiet and Fiona is not young then Fiona is not big.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "young" "~")) -> ("Fiona" "is" "big" "-"))
Erin is blue.
True
1
proof
[(triple5)]
("Erin" "is" "blue" "+")
triple5
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Erin is smart.
True
3
proof
[(((triple6 triple5) -> rule2))]
("Erin" "is" "smart" "+")
((triple6 triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple6 triple5) -> rule2))]
("Erin" "is" "smart" "-")
((triple6 triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
True
5
proof
[(((triple5 ((triple6 triple5) -> rule2)) -> rule3))]
("Erin" "is" "red" "+")
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not red.
False
5
inv-proof
[(((triple5 ((triple6 triple5) -> rule2)) -> rule3))]
("Erin" "is" "red" "-")
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
True
7
proof
[(((triple5 ((triple5 ((triple6 triple5) -> rule2)) -> rule3)) -> rule7))]
("Erin" "is" "kind" "+")
((triple5 ((triple5 ((triple6 triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not kind.
False
7
inv-proof
[(((triple5 ((triple5 ((triple6 triple5) -> rule2)) -> rule3)) -> rule7))]
("Erin" "is" "kind" "-")
((triple5 ((triple5 ((triple6 triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Bob" "is" "red" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "big" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is kind.[(triple1)] Charlie is blue.[(triple2)] Charlie is not smart.[(triple4)] Charlie is quiet.[(triple3)] Erin is blue.[(triple5)] Erin is young.[(triple6)] Fiona is not quiet.[(triple7)] @1: Erin is smart.[(((triple6 triple5) -> rule2))] @2: Erin is red.[(((triple5 ((triple6 triple5) -> rule2)) -> rule3))] @3: Erin is kind.[(((triple5 ((triple5 ((triple6 triple5) -> rule2)) -> rule3)) -> rule7))] @4: Erin is big.[(((triple6 ((triple5 ((triple5 ((triple6 triple5) -> rule2)) -> rule3)) -> rule7)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple6 triple5) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple5 ((triple6 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple5 ((triple5 ((triple6 triple5) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple6 ((triple5 ((triple5 ((triple6 triple5) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4