Anne is young. Charlie is round. Erin is young. Fiona is smart. Round people are kind. All smart people are kind. All kind, white people are smart. If someone is smart and big then they are white. If Fiona is white and Fiona is green then Fiona is smart. If someone is young then they are smart. Young, kind people are big. If someone is big then they are young.
Anne is young.
("Anne" "is" "young" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
All kind, white people are smart.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and big then they are white.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Fiona is white and Fiona is green then Fiona is smart.
((("Fiona" "is" "white" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "smart" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Young, kind people are big.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Fiona is smart.
True
1
proof
[(triple4)]
("Fiona" "is" "smart" "+")
triple4
Fiona is not smart.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "smart" "-")
triple4
Fiona is kind.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is white.
Unknown
rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule8 <- FAIL)]]
("Fiona" "is" "white" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is young.[(triple1)] Charlie is round.[(triple2)] Erin is young.[(triple3)] Fiona is smart.[(triple4)] @1: Anne is smart.[(((triple1) -> rule6))] Charlie is kind.[(((triple2) -> rule1))] Erin is smart.[(((triple3) -> rule6))] Fiona is kind.[(((triple4) -> rule2))] @2: Anne is kind.[(((((triple1) -> rule6)) -> rule2))] Erin is kind.[(((((triple3) -> rule6)) -> rule2))] @3: Anne is big.[(((triple1 ((((triple1) -> rule6)) -> rule2)) -> rule7))] Erin is big.[(((triple3 ((((triple3) -> rule6)) -> rule2)) -> rule7))] @4: Anne is white.[(((((triple1) -> rule6) ((triple1 ((((triple1) -> rule6)) -> rule2)) -> rule7)) -> rule4))] Erin is white.[(((((triple3) -> rule6) ((triple3 ((((triple3) -> rule6)) -> rule2)) -> rule7)) -> rule4))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int4)) ((triple1 ((((triple1) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((((triple3) -> (rule6 % int4)) ((triple3 ((((triple3) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4