Charlie is furry. Charlie is quiet. Erin is quiet. If someone is quiet and not blue then they are big. All furry people are big. If someone is young and quiet then they are big. If someone is big and furry then they are young. All big, furry people are young. If someone is big and young then they are green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is quiet and not blue then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "big" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is young and quiet then they are big.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is big and furry then they are young.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
All big, furry people are young.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If someone is big and young then they are green.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Erin is not quiet.
False
1
inv-proof
[(triple3)]
("Erin" "is" "quiet" "-")
triple3
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule4) OR ((((triple1) -> rule2) triple1) -> rule5))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule4) OR ((((triple1) -> rule2) triple1) -> rule5))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "green" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is furry.[(triple1)] Charlie is quiet.[(triple2)] Erin is quiet.[(triple3)] @1: Charlie is big.[(((triple1) -> rule2))] @2: Charlie is young.[(((((triple1) -> rule2) triple1) -> rule4) OR ((((triple1) -> rule2) triple1) -> rule5))] @3: Charlie is green.[(((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule4)) -> rule6) OR ((((triple1) -> rule2) ((((triple1) -> rule2) triple1) -> rule5)) -> rule6))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((((triple1) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3