Anne is big. Anne is round. Charlie is kind. Charlie is nice. Erin is big. Erin is kind. Erin is smart. All smart, blue people are round. All furry people are smart. All nice people are round. Furry people are smart. If someone is smart then they are nice. All furry people are kind. Nice people are kind. Round, big people are smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All smart, blue people are round.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Round, big people are smart.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((triple4) -> rule7))]
("Charlie" "is" "kind" "+")
triple3
((triple4) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Erin is nice.
True
2
proof
[(((triple7) -> rule5))]
("Erin" "is" "nice" "+")
((triple7) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple7) -> rule5))]
("Erin" "is" "nice" "-")
((triple7) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
True
3
proof
[(((((triple7) -> rule5)) -> rule3))]
("Erin" "is" "round" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple2 triple1) -> rule8)) -> rule5))]
("Anne" "is" "nice" "-")
((((triple2 triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
True
5
proof
[(((((((triple2 triple1) -> rule8)) -> rule5)) -> rule7))]
("Anne" "is" "kind" "+")
((((((triple2 triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not kind.
False
5
inv-proof
[(((((((triple2 triple1) -> rule8)) -> rule5)) -> rule7))]
("Anne" "is" "kind" "-")
((((((triple2 triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is big.[(triple1)] Anne is round.[(triple2)] Charlie is kind.[(triple3 OR ((triple4) -> rule7))] Charlie is nice.[(triple4)] Erin is big.[(triple5)] Erin is kind.[(triple6 OR ((((triple7) -> rule5)) -> rule7))] Erin is smart.[(triple7)] @1: Anne is smart.[(((triple2 triple1) -> rule8))] Charlie is round.[(((triple4) -> rule3))] Erin is nice.[(((triple7) -> rule5))] @2: Anne is nice.[(((((triple2 triple1) -> rule8)) -> rule5))] Erin is round.[(((((triple7) -> rule5)) -> rule3))] @3: Anne is kind.[(((((((triple2 triple1) -> rule8)) -> rule5)) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple4) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
((((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple7) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2 triple1) -> (rule8 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple2 triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3